diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 7206cf890..97d18bcf2 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1880,16 +1880,16 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & expr_ref div_p1(m); div_p1 = m_bv_util.mk_bv_add(div, m_bv_util.mk_numeral(1, sbits)); - expr_ref tie2(m), v51(m); - expr_ref tie_pttrn(m_bv_util.mk_concat(one_1, m_bv_util.mk_numeral(0, sbits - 1)), m); + expr_ref tie_pttrn(m), tie2(m), tie2_c(m), div_last(m), v51(m); + tie_pttrn = m_bv_util.mk_concat(one_1, m_bv_util.mk_numeral(0, sbits-1)); m_simp.mk_eq(rem, tie_pttrn, tie2); - expr_ref div_last(m_bv_util.mk_extract(0, 0, div), m); - - expr_ref div_last_eq_1(m.mk_eq(div_last, one_1), m); - expr_ref rte_and_dl_eq_1(m.mk_and(rm_is_rte, div_last_eq_1), m); - expr_ref rte_and_dl_eq_1_or_rta(m.mk_or(rte_and_dl_eq_1, rm_is_rta), m); - expr_ref tie_pttrn_ule_rem(m_bv_util.mk_ule(tie_pttrn, rem), m); - expr_ref tie2_c(m.mk_ite(tie2, rte_and_dl_eq_1_or_rta, tie_pttrn_ule_rem), m); + div_last = m_bv_util.mk_extract(0, 0, div); + expr_ref div_last_eq_1(m), rte_and_dl_eq_1(m), rte_and_dl_eq_1_or_rta(m), tie_pttrn_ule_rem(m); + div_last_eq_1 = m.mk_eq(div_last, one_1); + rte_and_dl_eq_1 = m.mk_and(rm_is_rte, div_last_eq_1); + rte_and_dl_eq_1_or_rta = m.mk_or(rte_and_dl_eq_1, rm_is_rta); + tie_pttrn_ule_rem = m_bv_util.mk_ule(tie_pttrn, rem); + tie2_c = m.mk_ite(tie2, rte_and_dl_eq_1_or_rta, tie_pttrn_ule_rem); m_simp.mk_ite(tie2_c, div_p1, div, v51); dbg_decouple("fpa2bv_r2i_v51", v51); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7a28b2609..ca939a1e8 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -623,6 +623,7 @@ namespace smt { } m_th_rw(c); + expr_ref xe_eq_ye(m), not_xe_eq_ye(m), c_eq_iff(m); xe_eq_ye = m.mk_eq(xe, ye); not_xe_eq_ye = m.mk_not(xe_eq_ye); @@ -879,6 +880,7 @@ namespace smt { m_fpa_util.is_to_real_unspecified(f); if (include && !m_is_added_to_model.contains(f)) { m_is_added_to_model.insert(f); + get_manager().inc_ref(f); return true; } return false; diff --git a/src/tactic/arith/pb2bv_model_converter.cpp b/src/tactic/arith/pb2bv_model_converter.cpp index 3e17ea675..8dbacc6cd 100644 --- a/src/tactic/arith/pb2bv_model_converter.cpp +++ b/src/tactic/arith/pb2bv_model_converter.cpp @@ -21,6 +21,10 @@ Notes: #include"model_v2_pp.h" #include"pb2bv_model_converter.h" +pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m) : m(_m) { + +} + pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m, obj_map const & c2bit, bound_manager const & bm): m(_m) { obj_map::iterator it = c2bit.begin(); @@ -98,5 +102,16 @@ void pb2bv_model_converter::display(std::ostream & out) { } model_converter * pb2bv_model_converter::translate(ast_translation & translator) { - NOT_IMPLEMENTED_YET(); + ast_manager & to = translator.to(); + pb2bv_model_converter * res = alloc(pb2bv_model_converter, to); + svector::iterator it = m_c2bit.begin(); + svector::iterator end = m_c2bit.end(); + for (; it != end; it++) { + func_decl * f1 = translator(it->first); + func_decl * f2 = translator(it->second); + res->m_c2bit.push_back(func_decl_pair(f1, f2)); + to.inc_ref(f1); + to.inc_ref(f2); + } + return res; } diff --git a/src/tactic/arith/pb2bv_model_converter.h b/src/tactic/arith/pb2bv_model_converter.h index 98cb0b235..8b6256ccc 100644 --- a/src/tactic/arith/pb2bv_model_converter.h +++ b/src/tactic/arith/pb2bv_model_converter.h @@ -28,6 +28,7 @@ class pb2bv_model_converter : public model_converter { ast_manager & m; svector m_c2bit; public: + pb2bv_model_converter(ast_manager & _m); pb2bv_model_converter(ast_manager & _m, obj_map const & c2bit, bound_manager const & bm); virtual ~pb2bv_model_converter(); virtual void operator()(model_ref & md); diff --git a/src/tactic/portfolio/default_tactic.h b/src/tactic/portfolio/default_tactic.h index f684fba85..2f40fa145 100644 --- a/src/tactic/portfolio/default_tactic.h +++ b/src/tactic/portfolio/default_tactic.h @@ -25,4 +25,8 @@ class tactic; tactic * mk_default_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* +ADD_TACTIC("default", "default strategy used when no logic is specified.", "mk_default_tactic(m, p)") +*/ + #endif diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 914d113b2..bd8d4958d 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -239,35 +239,6 @@ void hwf_manager::mul(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & #else o.value = x.value * y.value; #endif - -#if 0 - // On the x86 FPU (x87), we use custom assembly routines because - // the code generated for x*y and x/y suffers from the double - // rounding on underflow problem. The scaling trick is described - // in Roger Golliver: `Efficiently producing default orthogonal IEEE - // double results using extended IEEE hardware', see - // http://www.open-std.org/JTC1/SC22/JSG/docs/m3/docs/jsgn326.pdf - // CMW: Tthis is not really needed if we use only the SSE2 FPU, - // it shouldn't hurt the performance too much though. - - static const int const1 = -DBL_SCALE; - static const int const2 = +DBL_SCALE; - double xv = x.value; - double yv = y.value; - double & ov = o.value; - - __asm { - fild const1; - fld xv; - fscale; - fstp st(1); - fmul yv; - fild const2; - fxch st(1); - fscale; - fstp ov; - } -#endif } void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & o) { @@ -277,28 +248,6 @@ void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & #else o.value = x.value / y.value; #endif - -#if 0 - // see mul(...) - - static const int const1 = -DBL_SCALE; - static const int const2 = +DBL_SCALE; - double xv = x.value; - double yv = y.value; - double & ov = o.value; - - __asm { - fild const1; - fld xv; - fscale; - fstp st(1); - fdiv yv; - fild const2; - fxch st(1); - fscale; - fstp ov; - } -#endif } #ifdef _M_IA64 @@ -390,25 +339,6 @@ void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) { #else o.value = remainder(x.value, y.value); #endif - -#if 0 - // Here is an x87 alternative if the above makes problems; this may also be faster. - double xv = x.value; - double yv = y.value; - double & ov = o.value; - - // This is from: http://webster.cs.ucr.edu/AoA/DOS/ch14/CH14-4.html#HEADING4-173 - __asm { - fld yv - fld xv -L: fprem1 - fstsw ax // Get condition bits in AX. - test ah, 100b // See if C2 is set. - jnz L // Repeat if not done yet. - fstp ov // Store remainder away. - fstp st(0) // Pop old y value. - } -#endif } void hwf_manager::maximum(hwf const & x, hwf const & y, hwf & o) {