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

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);
+    expr_ref v4_rtn(m), v4_rtp(m);
-    mk_ite(m.mk_or(rm_is_rte, rm_is_rta), v42, v4, v4);
+    mk_ite(x_is_neg, nzero, pone, v4_rtp);
-    mk_ite(m.mk_or(rm_is_rtz, rm_is_rtn), xzero, v4, v4);
+    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/interp/iz3mgr.cpp

@@ -556,6 +556,20 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
     extract_lcd(rats);
 }
 
+void iz3mgr::get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats){
+    symb s = sym(proof);
+    int numps = s->get_num_parameters();
+    rats.resize(numps-2);
+    for(int i = 2; i < numps; i++){
+        rational r;
+        bool ok = s->get_parameter(i).is_rational(r);
+        if(!ok)
+            throw "Bad Farkas coefficient";
+        rats[i-2] = r;
+    }
+    extract_lcd(rats);
+}
+
 void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& coeffs){
     std::vector<rational> rats;
     get_assign_bounds_coeffs(proof,rats);

src/interp/iz3mgr.h

@@ -424,6 +424,8 @@ class iz3mgr  {
 
     void get_farkas_coeffs(const ast &proof, std::vector<rational>& rats);
 
+    void get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats);
+
     void get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& rats);
 
     void get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& rats);

src/interp/iz3translate.cpp

@@ -1021,6 +1021,12 @@ public:
                 my_coeffs.push_back(make_int(c));
                 my_prem_cons.push_back(conc(prem(proof,i)));
             }
+            else if(c.is_neg()){
+                int j = (i % 2 == 0) ? i + 1 : i - 1;
+                my_prems.push_back(prems[j]);
+                my_coeffs.push_back(make_int(-coeffs[j]));
+                my_prem_cons.push_back(conc(prem(proof,j)));
+            }
         }
         ast my_con = sum_inequalities(my_coeffs,my_prem_cons);
 
@@ -1884,7 +1890,7 @@ public:
                     }
                     case GCDTestKind: {
                         std::vector<rational> farkas_coeffs;
-                        get_farkas_coeffs(proof,farkas_coeffs);
+                        get_broken_gcd_test_coeffs(proof,farkas_coeffs);
                         if(farkas_coeffs.size() != nprems){
                             pfgoto(proof);
                             throw unsupported();

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 "dl_rule_transformer.h"
-#include"expr_safe_replace.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/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

@@ -338,8 +338,39 @@ 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);
+    // CMW: modf is not the right function here.
-    // Note: on x64, this sometimes produces an SNAN instead of a QNAN?
+    // 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 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
+    NOT_IMPLEMENTED_YET();
+#endif
+
+#if 0
+    double xv = x.value;
+    double & ov = o.value;
+
+    __asm {
+        fld     xv
+        frndint
+        fstp    ov // Store result away.
+    }
+
+#endif
 }
 
 void hwf_manager::rem(hwf const & x, hwf const & y, 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 ||
+        if (rm == MPF_ROUND_TOWARD_ZERO)
-            rm == MPF_ROUND_TOWARD_NEGATIVE)
             mk_zero(x.ebits, x.sbits, x.sign, o);
-        else if (rm == MPF_ROUND_NEAREST_TEVEN ||
+        else if (rm == MPF_ROUND_TOWARD_NEGATIVE) {
-                 rm == MPF_ROUND_NEAREST_TAWAY) {
+            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/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_ */