merge

src/api/java/ASTVector.java

@@ -119,4 +119,12 @@ public class ASTVector extends Z3Object
         getContext().getASTVectorDRQ().add(o);
         super.decRef(o);
     }
+
+    BoolExpr[] ToBoolArray() {
+        int n = size();
+        BoolExpr[] res = new BoolExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = new BoolExpr(getContext(), get(i).getNativeObject());
+        return res;	
+    }
 }

src/api/java/Fixedpoint.java

@@ -298,11 +298,7 @@ public class Fixedpoint extends Z3Object
 
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
                 getContext().nCtx(), getNativeObject()));
-        int n = v.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
+	return v.ToBoolArray();
     }
 
     /**
@@ -315,11 +311,7 @@ public class Fixedpoint extends Z3Object
 
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
                 getContext().nCtx(), getNativeObject()));
-        int n = v.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
+	return v.ToBoolArray();
     }
 
     /**

src/api/java/InterpolationContext.java

@@ -90,7 +90,7 @@ public class InterpolationContext extends Context
     public class ComputeInterpolantResult 
     {
         public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
-        public ASTVector interp = null;
+        public BoolExpr[] interp = null;
         public Model model = null;
     };
     
@@ -109,8 +109,10 @@ public class InterpolationContext extends Context
         ComputeInterpolantResult res = new ComputeInterpolantResult();
         Native.LongPtr n_i = new Native.LongPtr();
         Native.LongPtr n_m = new Native.LongPtr();
-        res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
-        if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value);
+        res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
+        if (res.status == Z3_lbool.Z3_L_FALSE) {
+	    res.interp = (new ASTVector(this, n_i.value)).ToBoolArray();
+	}
         if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
         return res;
     }

src/api/java/Solver.java

@@ -190,11 +190,7 @@ public class Solver extends Z3Object
     {
         ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
                 getContext().nCtx(), getNativeObject()));
-        int n = assrts.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject());
-        return res;
+	return assrts.ToBoolArray();
     }
 
     /**

src/ast/ast.cpp

@@ -2043,7 +2043,13 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2
 }
 
 app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
-    SASSERT(decl->get_arity() == num_args || decl->is_right_associative() || decl->is_left_associative() || decl->is_chainable());
+    if (decl->get_arity() != num_args && !decl->is_right_associative() && 
+        !decl->is_left_associative() && !decl->is_chainable()) {
+        std::ostringstream buffer;
+        buffer << "Wrong number of arguments (" << num_args 
+               << ") passed to function " << mk_pp(decl, *this);        
+        throw ast_exception(buffer.str().c_str());
+    }
     app * r = 0;
     if (num_args > 2 && !decl->is_flat_associative()) {
         if (decl->is_right_associative()) {

src/ast/fpa/fpa2bv_converter.cpp

@@ -1072,7 +1072,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
     
     result = y;
     mk_ite(lt, x, result, result);
-    mk_ite(both_zero, pzero, result, result);
+    mk_ite(both_zero, y, result, result);
     mk_ite(y_is_nan, x, result, result);
     mk_ite(x_is_nan, y, result, result);
 
@@ -1102,7 +1102,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
 
     result = y;
     mk_ite(gt, x, result, result);
-    mk_ite(both_zero, pzero, result, result);
+    mk_ite(both_zero, y, result, result);
     mk_ite(y_is_nan, x, result, result);
     mk_ite(x_is_nan, y, result, result);
 
@@ -1586,9 +1586,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
     mk_nzero(f, nzero); 
     mk_pzero(f, pzero);
 
-    expr_ref x_is_zero(m), x_is_pos(m);
+    expr_ref x_is_zero(m), x_is_pos(m), x_is_neg(m);
     mk_is_zero(x, x_is_zero);
     mk_is_pos(x, x_is_pos);
+    mk_is_neg(x, x_is_neg);
     
     dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero);
     dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos);    
@@ -1655,9 +1656,13 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
     mk_ite(c422, xone, v42, v42);
     mk_ite(c421, xzero, v42, v42);
     
-    mk_ite(m.mk_eq(a_sgn, one_1), nzero, pone, v4);
-    mk_ite(m.mk_or(rm_is_rte, rm_is_rta), v42, v4, v4);
-    mk_ite(m.mk_or(rm_is_rtz, rm_is_rtn), xzero, v4, v4);
+    expr_ref v4_rtn(m), v4_rtp(m);
+    mk_ite(x_is_neg, nzero, pone, v4_rtp);
+    mk_ite(x_is_neg, none, pzero, v4_rtn);
+
+    mk_ite(rm_is_rtp, v4_rtp, v42, v4);
+    mk_ite(rm_is_rtn, v4_rtn, v4, v4);
+    mk_ite(rm_is_rtz, xzero, v4, v4);
 
     SASSERT(is_well_sorted(m, v4));
     
@@ -3039,6 +3044,13 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
     m_simp.mk_not(sig_is_zero, sig_is_not_zero);
     m_simp.mk_eq(exp, top_exp, exp_is_top);
     m_simp.mk_and(exp_is_top, sig_is_not_zero, result);
+
+    // Inject auxiliary lemmas that fix e to the one and only NaN value, 
+    // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
+    // has a value to propagate.
+    m_extra_assertions.push_back(m.mk_eq(sgn, m_bv_util.mk_numeral(0, 1)));
+    m_extra_assertions.push_back(m.mk_eq(exp, top_exp));
+    m_extra_assertions.push_back(m.mk_eq(sig, m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(sig))));
 }
 
 void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) {

src/ast/rewriter/fpa_rewriter.cpp

@@ -412,7 +412,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
         return BR_DONE;
     }
     if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
-        result = m_util.mk_pzero(m().get_sort(arg1));
+        result = arg2;
         return BR_DONE;
     }
 
@@ -421,7 +421,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
                         m().mk_ite(mk_eq_nan(arg2),
                         arg1,
                         m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
-                        m_util.mk_pzero(m().get_sort(arg1)),
+                        arg2,
                         m().mk_ite(m_util.mk_lt(arg1, arg2),
                         arg1,
                         arg2))));
@@ -438,7 +438,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
         return BR_DONE;
     }
     if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
-        result = m_util.mk_pzero(m().get_sort(arg1));
+        result = arg2;
         return BR_DONE;
     }
 
@@ -447,7 +447,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
                         m().mk_ite(mk_eq_nan(arg2),
                         arg1,
                         m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
-                        m_util.mk_pzero(m().get_sort(arg1)),
+                        arg2,
                         m().mk_ite(m_util.mk_gt(arg1, arg2),
                         arg1,
                         arg2))));

src/math/euclid/euclidean_solver.cpp

@@ -717,7 +717,7 @@ struct euclidean_solver::imp {
                 elim_unit();
             else
                 decompose_and_elim();
-            TRACE("euclidean_solver_step", display(tout);); 
+            TRACE("euclidean_solver", display(tout);); 
             if (inconsistent()) return false;
         }
         return true;

src/muz/transforms/dl_mk_quantifier_instantiation.h

@@ -26,8 +26,9 @@ Revision History:
 #define _DL_MK_QUANTIFIER_INSTANTIATION_H_
 
 
-#include"dl_rule_transformer.h"
-#include"expr_safe_replace.h"
+#include "dl_rule_transformer.h"
+#include "expr_safe_replace.h"
+#include "union_find.h"
 
 
 namespace datalog {
@@ -37,75 +38,12 @@ namespace datalog {
     class mk_quantifier_instantiation : public rule_transformer::plugin {
         typedef svector<std::pair<expr*,expr*> > term_pairs;
 
-        class union_find {
-            unsigned_vector   m_find;
-            unsigned_vector   m_size;
-            unsigned_vector   m_next;
-
-            void ensure_size(unsigned v) {
-                while (v >= get_num_vars()) {
-                    mk_var();
-                }
-            }
-        public:
-            unsigned mk_var() {
-                unsigned r = m_find.size();
-                m_find.push_back(r);
-                m_size.push_back(1);
-                m_next.push_back(r);
-                return r;
-            }
-            unsigned get_num_vars() const { return m_find.size(); }
-            
-            unsigned find(unsigned v) const {
-                if (v >= get_num_vars()) {
-                    return v;
-                }
-                while (true) {
-                    unsigned new_v = m_find[v];
-                    if (new_v == v)
-                        return v;
-                    v = new_v;
-                }
-            }
-            
-            unsigned next(unsigned v) const { 
-                if (v >= get_num_vars()) {
-                    return v;
-                }
-                return m_next[v]; 
-            }
-            
-            bool is_root(unsigned v) const { 
-                return v >= get_num_vars() || m_find[v] == v; 
-            }
-            
-            void merge(unsigned v1, unsigned v2) {
-                unsigned r1 = find(v1);
-                unsigned r2 = find(v2);
-                if (r1 == r2)
-                    return;
-                ensure_size(v1);
-                ensure_size(v2);
-                if (m_size[r1] > m_size[r2])
-                    std::swap(r1, r2);
-                m_find[r1] = r2;
-                m_size[r2] += m_size[r1];
-                std::swap(m_next[r1], m_next[r2]);
-            }
-
-            void reset() {
-                m_find.reset();
-                m_next.reset();
-                m_size.reset();
-            }
-        };
 
         ast_manager&      m;
         context&          m_ctx;
         expr_safe_replace m_var2cnst; 
         expr_safe_replace m_cnst2var;
-        union_find        m_uf;
+        basic_union_find  m_uf;
         ptr_vector<expr>  m_todo;
         ptr_vector<expr>  m_terms;
         ptr_vector<expr>  m_binding;

src/smt/theory_arith_int.h

@@ -1041,8 +1041,8 @@ namespace smt {
                     num_args = 1;
                     args     = &n;
                 }
-                for (unsigned j = 0; j < num_args; j++) {
-                    expr * arg = args[j];
+                for (unsigned i = 0; i < num_args; i++) {
+                    expr * arg = args[i];
                     expr * pp;
                     rational a_val;
                     get_monomial(arg, a_val, pp);

src/tactic/fpa/qffp_tactic.cpp

@@ -37,6 +37,7 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
                                 mk_smt_tactic(),
                                 and_then(
                                      mk_fpa2bv_tactic(m, p),
+                                     mk_propagate_values_tactic(m, p),
                                      using_params(mk_simplify_tactic(m, p), simp_p),                                 
                                      mk_bit_blaster_tactic(m, p),
                                      using_params(mk_simplify_tactic(m, p), simp_p),                                 

src/util/hwf.cpp

@@ -306,7 +306,7 @@ void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
 #pragma fp_contract(on)
 #endif
 
-void hwf_manager::fused_mul_add(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o) {
+void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o) {
     // CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium, 
     // Intel Sandybridge and AMD Bulldozers support that (via AVX).
 
@@ -315,11 +315,8 @@ void hwf_manager::fused_mul_add(mpf_rounding_mode rm, hwf const & x, hwf const &
     set_rounding_mode(rm);
     o.value = x.value * y.value + z.value;
 #else
-    // NOT_IMPLEMENTED_YET();
-    // Just a dummy for now:
-    hwf t;
-    mul(rm, x, y, t);
-    add(rm, t, z, o);
+    set_rounding_mode(rm);
+    o.value = ::fma(x.value, y.value, z.value);
 #endif
 }
 
@@ -338,8 +335,38 @@ void hwf_manager::sqrt(mpf_rounding_mode rm, hwf const & x, hwf & o) {
 
 void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o) {
     set_rounding_mode(rm);
-    modf(x.value, &o.value);
-    // Note: on x64, this sometimes produces an SNAN instead of a QNAN?
+    // CMW: modf is not the right function here.
+    // modf(x.value, &o.value);
+
+    // According to the Intel Architecture manual, the x87-instrunction FRNDINT is the 
+    // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions.
+#ifdef _WINDOWS
+#ifdef USE_INTRINSICS
+    switch (rm) {
+    case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break;
+    case 2: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_POS_INF)); break;
+    case 3: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEG_INF)); break;
+    case 4: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_ZERO)); break;
+    case 1:
+        UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware!
+        break;
+    default:
+        UNREACHABLE(); // Unknown rounding mode.
+    }
+#else
+    double xv = x.value;
+    double & ov = o.value;
+
+    __asm {
+        fld     xv
+        frndint
+        fstp    ov // Store result away.
+    }
+#endif
+#else
+    // Linux, OSX.
+    o.value = nearbyint(x.value);
+#endif
 }
 
 void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) {

src/util/hwf.h

@@ -105,7 +105,7 @@ public:
     void mul(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & o);
     void div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & o);    
 
-    void fused_mul_add(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o);
+    void fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o);
 
     void sqrt(mpf_rounding_mode rm, hwf const & x, hwf & o);
 

src/util/mpf.cpp

@@ -1006,11 +1006,22 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
     else if (is_zero(x))
         mk_zero(x.ebits, x.sbits, x.sign, o); // -0.0 -> -0.0, says IEEE754, Sec 5.9.
     else if (x.exponent < 0) {
-        if (rm == MPF_ROUND_TOWARD_ZERO ||
-            rm == MPF_ROUND_TOWARD_NEGATIVE)
+        if (rm == MPF_ROUND_TOWARD_ZERO)
             mk_zero(x.ebits, x.sbits, x.sign, o);
-        else if (rm == MPF_ROUND_NEAREST_TEVEN ||
-                 rm == MPF_ROUND_NEAREST_TAWAY) {
+        else if (rm == MPF_ROUND_TOWARD_NEGATIVE) {
+            if (x.sign)
+                mk_one(x.ebits, x.sbits, true, o);
+            else
+                mk_zero(x.ebits, x.sbits, false, o);
+        }
+        else if (rm == MPF_ROUND_TOWARD_POSITIVE) {
+            if (x.sign)
+                mk_zero(x.ebits, x.sbits, true, o);
+            else
+                mk_one(x.ebits, x.sbits, false, o);
+        }
+        else {
+            SASSERT(rm == MPF_ROUND_NEAREST_TEVEN || rm == MPF_ROUND_NEAREST_TAWAY);
             bool tie = m_mpz_manager.is_zero(x.significand) && x.exponent == -1;
             TRACE("mpf_dbg", tout << "tie = " << tie << std::endl;);
             if (tie && rm == MPF_ROUND_NEAREST_TEVEN)
@@ -1019,15 +1030,8 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
                 mk_one(x.ebits, x.sbits, x.sign, o);
             else if (x.exponent < -1)
                 mk_zero(x.ebits, x.sbits, x.sign, o);
-            else 
-                mk_one(x.ebits, x.sbits, x.sign, o);
-        }
-        else {
-            SASSERT(rm == MPF_ROUND_TOWARD_POSITIVE);
-            if (x.sign) 
-                mk_nzero(x.ebits, x.sbits, o);
             else
-                mk_one(x.ebits, x.sbits, false, o);
+                mk_one(x.ebits, x.sbits, x.sign, o);
         }
     }
     else if (x.exponent >= x.sbits - 1)

src/util/mpn.h

@@ -27,7 +27,9 @@ Revision History:
 typedef unsigned int mpn_digit;
 
 class mpn_manager {
+#ifndef _NO_OMP_
     omp_nest_lock_t m_lock;
+#endif
 #define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock);
 #define MPN_END_CRITICAL() omp_unset_nest_lock(&m_lock);
 

src/util/union_find.h

@@ -173,5 +173,71 @@ public:
 #endif
 };
 
+
+class basic_union_find {
+    unsigned_vector   m_find;
+    unsigned_vector   m_size;
+    unsigned_vector   m_next;
+    
+    void ensure_size(unsigned v) {
+        while (v >= get_num_vars()) {
+            mk_var();
+        }
+    }
+ public:
+    unsigned mk_var() {
+        unsigned r = m_find.size();
+        m_find.push_back(r);
+        m_size.push_back(1);
+        m_next.push_back(r);
+        return r;
+    }
+    unsigned get_num_vars() const { return m_find.size(); }
+    
+    unsigned find(unsigned v) const {
+        if (v >= get_num_vars()) {
+            return v;
+        }
+        while (true) {
+            unsigned new_v = m_find[v];
+            if (new_v == v)
+                return v;
+            v = new_v;
+        }
+    }
+    
+    unsigned next(unsigned v) const { 
+        if (v >= get_num_vars()) {
+            return v;
+        }
+        return m_next[v]; 
+    }
+    
+    bool is_root(unsigned v) const { 
+        return v >= get_num_vars() || m_find[v] == v; 
+    }
+    
+    void merge(unsigned v1, unsigned v2) {
+        unsigned r1 = find(v1);
+        unsigned r2 = find(v2);
+        if (r1 == r2)
+            return;
+        ensure_size(v1);
+        ensure_size(v2);
+        if (m_size[r1] > m_size[r2])
+            std::swap(r1, r2);
+        m_find[r1] = r2;
+        m_size[r2] += m_size[r1];
+        std::swap(m_next[r1], m_next[r2]);
+    }
+    
+    void reset() {
+        m_find.reset();
+        m_next.reset();
+        m_size.reset();
+    }
+};
+
+
 #endif /* _UNION_FIND_H_ */