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

src/api/python/z3.py

@@ -8944,7 +8944,31 @@ def fpFP(sgn, exp, sig, ctx=None):
     return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
 
 def fpToFP(a1, a2=None, a3=None, ctx=None):
-    """Create a Z3 floating-point conversion expression from other terms."""
+    """Create a Z3 floating-point conversion expression from other term sorts
+    to floating-point.
+
+    From a bit-vector term in IEEE 754-2008 format:
+    >>> x = FPVal(1.0, Float32())
+    >>> x_bv = fpToIEEEBV(x)
+    >>> simplify(fpToFP(x_bv, Float32()))
+    1
+
+    From a floating-point term with different precision:
+    >>> x = FPVal(1.0, Float32())
+    >>> x_db = fpToFP(RNE(), x, Float64())
+    >>> x_db.sort()
+    FPSort(11, 53)
+
+    From a real term:
+    >>> x_r = RealVal(1.5)
+    >>> simplify(fpToFP(RNE(), x_r, Float32()))
+    1.5
+
+    From a signed bit-vector term:
+    >>> x_signed = BitVecVal(-5, BitVecSort(32))
+    >>> simplify(fpToFP(RNE(), x_signed, Float32()))
+    -1.25*(2**2)
+    """
     ctx = _get_ctx(ctx)
     if is_bv(a1) and is_fp_sort(a2):
         return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)

src/ast/ast.h

@@ -972,7 +972,7 @@ public:
     */
     virtual bool is_unique_value(app * a) const { return false; }
 
-    virtual bool are_equal(app * a, app * b) const { return a == b && is_unique_value(a) && is_unique_value(b); }
+    virtual bool are_equal(app * a, app * b) const { return a == b; }
 
     virtual bool are_distinct(app * a, app * b) const { return a != b && is_unique_value(a) && is_unique_value(b); }
 

src/ast/rewriter/bool_rewriter.cpp

@@ -671,7 +671,7 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) {
 #endif
 
 br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
-    if (lhs == rhs) {
+    if (m().are_equal(lhs, rhs)) {
         result = m().mk_true();
         return BR_DONE;
     }

src/muz/pdr/pdr_sym_mux.h

@@ -23,6 +23,7 @@ Revision History:
 #include "ast.h"
 #include "map.h"
 #include "vector.h"
+#include <vector>
 
 class model_core;
 
@@ -46,7 +47,7 @@ private:
     mutable unsigned       m_next_sym_suffix_idx;
     mutable symbols        m_used_suffixes;
     /** Here we have default suffixes for each of the variants */
-    vector<std::string>    m_suffixes;
+    std::vector<std::string>    m_suffixes;
 
 
     /**

src/smt/tactic/smt_tactic.cpp

@@ -99,7 +99,7 @@ public:
         m_ctx(0),
         m_callback(0) {
         updt_params_core(p);
-        TRACE("smt_tactic", tout << this << "\np: " << p << "\n";);
+        TRACE("smt_tactic", tout << "p: " << p << "\n";);
     }
 
     virtual tactic * translate(ast_manager & m) {
@@ -120,13 +120,12 @@ public:
     }
 
     virtual void updt_params(params_ref const & p) {
-        TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";);
+        TRACE("smt_tactic", tout << "updt_params: " << p << "\n";);
         updt_params_core(p);
         fparams().updt_params(p);
-        symbol logic = p.get_sym(symbol("logic"), symbol::null);
-        if (logic != symbol::null) {
-            if (m_ctx) m_ctx->set_logic(logic);
-            m_logic = logic;
+        m_logic = p.get_sym(symbol("logic"), m_logic);
+        if (m_logic != symbol::null && m_ctx) {
+            m_ctx->set_logic(m_logic);
         }
         SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
     }

src/solver/tactic2solver.cpp

@@ -128,8 +128,8 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
     ast_manager & m = m_assertions.m();
     m_result = alloc(simple_check_sat_result, m);
     m_tactic->cleanup();
-    m_tactic->updt_params(m_params);
     m_tactic->set_logic(m_logic);
+    m_tactic->updt_params(m_params); // parameters are allowed to overwrite logic.
     goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
 
     unsigned sz = m_assertions.size();

src/test/model_evaluator.cpp

@@ -26,13 +26,19 @@ void tst_model_evaluator() {
     expr_ref vB0(m.mk_var(0, m.mk_bool_sort()), m);
     expr_ref vB1(m.mk_var(1, m.mk_bool_sort()), m);
     expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m);
-    expr_ref f01(m.mk_app(f, vI0, vB1), m);
-    expr_ref g01(m.mk_app(g, vI0, vB1), m);
-    expr_ref h01(m.mk_app(h, vI0, vB1), m);
+    expr* vI0p = vI0.get();
+    expr* vI1p = vI1.get();
+    expr* vB0p = vB0.get();
+    expr* vB1p = vB1.get();
+    expr* vB2p = vB2.get();
+
+    expr_ref f01(m.mk_app(f, vI0p, vB1p), m);
+    expr_ref g01(m.mk_app(g, vI0p, vB1p), m);
+    expr_ref h01(m.mk_app(h, vI0p, vB1p), m);
     func_interp* fi = alloc(func_interp, m, 2);
     func_interp* gi = alloc(func_interp, m, 2);
     func_interp* hi = alloc(func_interp, m, 2);
-    hi->set_else(m.mk_ite(vB1, m.mk_app(f, vI0, vB1), m.mk_app(g, vI0, vB1)));
+    hi->set_else(m.mk_ite(vB1p, m.mk_app(f, vI0p, vB1p), m.mk_app(g, vI0p, vB1p)));
     mdl.register_decl(h, hi);
     
 
@@ -42,23 +48,23 @@ void tst_model_evaluator() {
 
     {
         symbol nI("N");
-        fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(F, vI1, vB2))), vI0, a.mk_int(1)));
-        gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(G, vI1, vB2))), a.mk_int(2), vI0));
+        fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(F, vI1p, vB2p))), vI0p, a.mk_int(1)));
+        gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(G, vI1p, vB2p))), a.mk_int(2), vI0p));
         mdl.register_decl(g, gi);
         mdl.register_decl(f, fi);
         model_pp(std::cout, mdl);
-        e = m.mk_app(h, vI0, vB1);
+        e = m.mk_app(h, vI0p, vB1p);
         eval(e, v);
         std::cout << e << " " << v << "\n";
     }
 
     {
-        fi->set_else(m.mk_app(F, vI0, vB1));
-        gi->set_else(m.mk_app(G, vI0, vB1));
+        fi->set_else(m.mk_app(F, vI0p, vB1p));
+        gi->set_else(m.mk_app(G, vI0p, vB1p));
         mdl.register_decl(g, gi);
         mdl.register_decl(h, hi);
         model_pp(std::cout, mdl);
-        e = m.mk_app(h, vI0, vB1);
+        e = m.mk_app(h, vI0p, vB1p);
         eval(e, v);
         std::cout << e << " " << v << "\n";
     }

src/util/mpn.cpp

@@ -226,7 +226,7 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
                                   mpn_sbuffer & n_denom) const
 {    
     size_t d = 0;
-    while (((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
+    while (lden > 0 && ((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
     SASSERT(d < DIGIT_BITS);
     
     n_numer.resize(lnum+1);
@@ -239,7 +239,8 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
         for (size_t i = 0; i < lden; i++)
             n_denom[i] = denom[i];
     }
-    else {
+    else if (lnum != 0) {
+        SASSERT(lden > 0);
         mpn_digit q = FIRST_BITS(d, numer[lnum-1]);
         n_numer[lnum] = q;
         for (size_t i = lnum-1; i > 0; i--)
@@ -249,6 +250,9 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
             n_denom[i] = denom[i] << d | FIRST_BITS(d, denom[i-1]);
         n_denom[0] = denom[0] << d;   
     }
+    else {
+        d = 0;
+    }
 
     TRACE("mpn_norm", tout << "Normalized: n_numer="; display_raw(tout, n_numer.c_ptr(), n_numer.size()); 
                       tout << " n_denom="; display_raw(tout, n_denom.c_ptr(), n_denom.size()); tout << std::endl; );

src/util/version.h.in

@@ -0,0 +1,5 @@
+// automatically generated file.
+#define Z3_MAJOR_VERSION   @Z3_VERSION_MAJOR@
+#define Z3_MINOR_VERSION   @Z3_VERSION_MINOR@
+#define Z3_BUILD_NUMBER    @Z3_VERSION_PATCH@
+#define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@