Merge branch 'master' of https://github.com/Z3Prover/z3

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), tie2(m), tie2_c(m), div_last(m), v51(m);
-	expr_ref tie_pttrn(m_bv_util.mk_concat(one_1, m_bv_util.mk_numeral(0, sbits - 1)), 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);
+    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);
-    expr_ref div_last_eq_1(m.mk_eq(div_last, one_1), m);
+    div_last_eq_1 = m.mk_eq(div_last, one_1);
-    expr_ref rte_and_dl_eq_1(m.mk_and(rm_is_rte, div_last_eq_1), m);
+    rte_and_dl_eq_1 = m.mk_and(rm_is_rte, div_last_eq_1);
-    expr_ref rte_and_dl_eq_1_or_rta(m.mk_or(rte_and_dl_eq_1, rm_is_rta), m);
+    rte_and_dl_eq_1_or_rta = m.mk_or(rte_and_dl_eq_1, rm_is_rta);
-    expr_ref tie_pttrn_ule_rem(m_bv_util.mk_ule(tie_pttrn, rem), m);
+    tie_pttrn_ule_rem = m_bv_util.mk_ule(tie_pttrn, rem);
-    expr_ref tie2_c(m.mk_ite(tie2, rte_and_dl_eq_1_or_rta, tie_pttrn_ule_rem), m);
+    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);

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;

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<func_decl, expr*> const & c2bit, bound_manager const & bm):
     m(_m) {
     obj_map<func_decl, expr*>::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<func_decl_pair>::iterator it = m_c2bit.begin();
+    svector<func_decl_pair>::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;
 }

src/tactic/arith/pb2bv_model_converter.h

@@ -28,6 +28,7 @@ class pb2bv_model_converter : public model_converter {
     ast_manager &             m;    
     svector<func_decl_pair>   m_c2bit;
 public:
+    pb2bv_model_converter(ast_manager & _m);
     pb2bv_model_converter(ast_manager & _m, obj_map<func_decl, expr*> const & c2bit, bound_manager const & bm);
     virtual ~pb2bv_model_converter();
     virtual void operator()(model_ref & md);

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

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) {