Add intblast solver

RELEASE_NOTES.md

@@ -12,6 +12,12 @@ Version 4.next
 
 Version 4.12.5
 ==============
+- Fixes to pypi setup and build for MacOS distributions
+- A new theory solver "int-blast" enabled by using:
+  - sat.smt=true smt.bv.solver=2
+  - It solves a few bit-vector problems not handled by bit-blasting, especially if the bit-widths are large.
+  - It is based on encoding bit-vector constraints to non-linear integer arithemtic.
+
 
 Version 4.12.4
 ==============

src/ast/arith_decl_plugin.cpp

@@ -523,6 +523,12 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
                                        func_decl_info(m_family_id, k, num_parameters, parameters));
     }
+    if (k == OP_ARITH_BAND) {
+        if (arity != 2 || domain[0] != m_int_decl || domain[1] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) 
+            m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer");
+        return m_manager->mk_func_decl(symbol("band"), 2, domain, m_int_decl,
+            func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
 
     if (m_manager->int_real_coercions() && use_coercion(k)) {
         return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl));
@@ -548,6 +554,14 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
                                        func_decl_info(m_family_id, k, num_parameters, parameters));
     }
+    if (k == OP_ARITH_BAND) {
+        if (num_args != 2 || args[0]->get_sort() != m_int_decl || args[1]->get_sort() != m_int_decl || num_parameters != 1 || !parameters[0].is_int())
+            m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer");
+        sort* domain[2] = { m_int_decl, m_int_decl };
+        return m_manager->mk_func_decl(symbol("band"), 2, domain, m_int_decl,
+            func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
+
     if (m_manager->int_real_coercions() && use_coercion(k)) {
         return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl));
     }
@@ -693,7 +707,16 @@ expr * arith_decl_plugin::get_some_value(sort * s) {
     return mk_numeral(rational(0), s == m_int_decl);
 }
 
-bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int) const {
+bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const {
+    if (is_irrational_algebraic_numeral(n)) {
+        scoped_anum an(am());
+        is_irrational_algebraic_numeral2(n, an);
+        if (am().is_rational(an)) {
+            am().to_rational(an, val);
+            is_int = val.is_int();
+            return true;
+        }
+    }
     if (!is_app_of(n, arith_family_id, OP_NUM))
         return false;
     func_decl * decl = to_app(n)->get_decl();
@@ -724,7 +747,7 @@ bool arith_recognizers::is_int_expr(expr const *e) const {
         if (is_to_real(e)) {
             // pass
         }
-        else if (is_numeral(e, r) && r.is_int()) {
+        else if (is_numeral(e) && is_int(e)) {
             // pass
         }
         else if (is_add(e) || is_mul(e)) {
@@ -747,14 +770,14 @@ void arith_util::init_plugin() {
     m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(arith_family_id));
 }
 
-bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) {
+bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) const {
     if (!is_app_of(n, arith_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM))
         return false;
     am().set(val, to_irrational_algebraic_numeral(n));
     return true;
 }
 
-algebraic_numbers::anum const & arith_util::to_irrational_algebraic_numeral(expr const * n) {
+algebraic_numbers::anum const & arith_util::to_irrational_algebraic_numeral(expr const * n) const {
     SASSERT(is_irrational_algebraic_numeral(n));
     return plugin().aw().to_anum(to_app(n)->get_decl());
 }

src/ast/arith_decl_plugin.h

@@ -70,6 +70,8 @@ enum arith_op_kind {
     OP_ASINH,
     OP_ACOSH,
     OP_ATANH,
+    // Bit-vector functions
+    OP_ARITH_BAND,
     // constants
     OP_PI,
     OP_E,
@@ -235,26 +237,10 @@ class arith_recognizers {
     family_id get_family_id() const { return arith_family_id; }
 
     bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == arith_family_id; }
-    bool is_irrational_algebraic_numeral(expr const * n) const;
-    bool is_unsigned(expr const * n, unsigned& u) const { 
-        rational val;
-        bool is_int = true;
-        return is_numeral(n, val, is_int) && is_int && val.is_unsigned() && (u = val.get_unsigned(), true); 
-    }
-    bool is_numeral(expr const * n, rational & val, bool & is_int) const;
-    bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
-    bool is_numeral(expr const * n) const { return is_app_of(n, arith_family_id, OP_NUM); }
-    bool is_zero(expr const * n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
-    bool is_minus_one(expr * n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
-    // return true if \c n is a term of the form (* -1 r)
-    bool is_times_minus_one(expr * n, expr * & r) const {
-        if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
-            r = to_app(n)->get_arg(1);
-            return true;
-        }
-        return false;
-    }
 
+    bool is_irrational_algebraic_numeral(expr const* n) const;
+
+    bool is_numeral(expr const* n) const { return is_app_of(n, arith_family_id, OP_NUM); }
     bool is_int_expr(expr const * e) const;
 
     bool is_le(expr const * n) const { return is_app_of(n, arith_family_id, OP_LE); }
@@ -309,6 +295,16 @@ class arith_recognizers {
     bool is_int_real(sort const * s) const { return s->get_family_id() == arith_family_id; }
     bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); }
 
+    bool is_band(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_BAND); }
+    bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) {
+        if (!is_band(n))
+            return false;
+        x = to_app(n)->get_arg(0);
+        y = to_app(n)->get_arg(1);
+        sz = to_app(n)->get_parameter(0).get_int();
+        return true;
+    }
+
     bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); }
     bool is_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); }
     bool is_tan(expr const* n) const { return is_app_of(n, arith_family_id, OP_TAN); }
@@ -387,13 +383,32 @@ class arith_util : public arith_recognizers {
         return *m_plugin;
     }
 
-    algebraic_numbers::manager & am() {
+    algebraic_numbers::manager & am() const {
         return plugin().am();
     }
 
+    // return true if \c n is a term of the form (* -1 r)
+    bool is_zero(expr const* n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
+    bool is_minus_one(expr* n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
+    bool is_times_minus_one(expr* n, expr*& r) const {
+        if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
+            r = to_app(n)->get_arg(1);
+            return true;
+        }
+        return false;
+    }
+    bool is_unsigned(expr const* n, unsigned& u) const {
+        rational val;
+        bool is_int = true;
+        return is_numeral(n, val, is_int) && is_int && val.is_unsigned() && (u = val.get_unsigned(), true);
+    }
+    bool is_numeral(expr const* n) const { return arith_recognizers::is_numeral(n); }
+    bool is_numeral(expr const* n, rational& val, bool& is_int) const;
+    bool is_numeral(expr const* n, rational& val) const { bool is_int; return is_numeral(n, val, is_int); }
+
     bool convert_int_numerals_to_real() const { return plugin().convert_int_numerals_to_real(); }
-    bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val);
-    algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
+    bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) const;
+    algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n) const;
 
     sort * mk_int() { return m_manager.mk_sort(arith_family_id, INT_SORT); }
     sort * mk_real() { return m_manager.mk_sort(arith_family_id, REAL_SORT); }
@@ -471,6 +486,8 @@ class arith_util : public arith_recognizers {
     app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER, arg1, arg2); }
     app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); }
 
+    app* mk_band(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, 2, args); }
+
     app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); }
     app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); }
     app * mk_tan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TAN, arg); }
@@ -498,11 +515,11 @@ class arith_util : public arith_recognizers {
        if none of them are numerals, then the left-hand-side has a smaller id than the right hand side.
     */
     app * mk_eq(expr * lhs, expr * rhs) {
-        if (is_numeral(lhs) || (!is_numeral(rhs) && lhs->get_id() > rhs->get_id()))
+        if (arith_recognizers::is_numeral(lhs) || (!arith_recognizers::is_numeral(rhs) && lhs->get_id() > rhs->get_id()))
             std::swap(lhs, rhs);
         if (lhs == rhs)
             return m_manager.mk_true();
-        if (is_numeral(lhs) && is_numeral(rhs)) {
+        if (arith_recognizers::is_numeral(lhs) && arith_recognizers::is_numeral(rhs)) {
             SASSERT(lhs != rhs);
             return m_manager.mk_false();
         }

src/ast/bv_decl_plugin.cpp

@@ -942,3 +942,8 @@ app * bv_util::mk_bv2int(expr* e) {
     parameter p(s);
     return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
 }
+
+app* bv_util::mk_int2bv(unsigned sz, expr* e) {
+    parameter p(sz);
+    return m_manager.mk_app(get_fid(), OP_INT2BV, 1, &p, 1, &e);
+}

src/ast/bv_decl_plugin.h

@@ -386,9 +386,31 @@ class bv_recognizers {
     bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); }
     bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
     bool is_bv_umul_no_ovfl(expr const* e) const { return is_app_of(e, get_fid(), OP_BUMUL_NO_OVFL); }
+    bool is_redand(expr const* e) const { return is_app_of(e, get_fid(), OP_BREDAND); }
+    bool is_redor(expr const* e) const { return is_app_of(e, get_fid(), OP_BREDOR); }
+    bool is_comp(expr const* e) const { return is_app_of(e, get_fid(), OP_BCOMP); }
+    bool is_rotate_left(expr const* e) const { return is_app_of(e, get_fid(), OP_ROTATE_LEFT); }
+    bool is_rotate_right(expr const* e) const { return is_app_of(e, get_fid(), OP_ROTATE_RIGHT); }
+    bool is_ext_rotate_left(expr const* e) const { return is_app_of(e, get_fid(), OP_EXT_ROTATE_LEFT); }
+    bool is_ext_rotate_right(expr const* e) const { return is_app_of(e, get_fid(), OP_EXT_ROTATE_RIGHT); }
+
+    bool is_rotate_left(expr const* e, unsigned& n, expr*& x) const {
+        return is_rotate_left(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true);
+    }
+    bool is_rotate_right(expr const* e, unsigned& n, expr*& x) const {
+        return is_rotate_right(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true);
+    }
+    bool is_int2bv(expr const* e, unsigned& n, expr*& x) const {
+        return is_int2bv(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true);
+    }
 
     MATCH_UNARY(is_bv_not);
+    MATCH_UNARY(is_redand);
+    MATCH_UNARY(is_redor);
 
+    MATCH_BINARY(is_ext_rotate_left);
+    MATCH_BINARY(is_ext_rotate_right);
+    MATCH_BINARY(is_comp);
     MATCH_BINARY(is_bv_add);
     MATCH_BINARY(is_bv_sub);
     MATCH_BINARY(is_bv_mul);
@@ -411,6 +433,12 @@ class bv_recognizers {
     MATCH_BINARY(is_bv_sdiv);
     MATCH_BINARY(is_bv_udiv);
     MATCH_BINARY(is_bv_smod);
+    MATCH_BINARY(is_bv_and);
+    MATCH_BINARY(is_bv_or);
+    MATCH_BINARY(is_bv_xor);
+    MATCH_BINARY(is_bv_nand);
+    MATCH_BINARY(is_bv_nor);
+
 
     MATCH_BINARY(is_bv_uremi);
     MATCH_BINARY(is_bv_sremi);
@@ -516,6 +544,7 @@ class bv_util : public bv_recognizers {
     app * mk_bv_lshr(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_BLSHR, arg1, arg2); }
 
     app * mk_bv2int(expr* e);
+    app * mk_int2bv(unsigned sz, expr* e);
 
     // TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return`
     app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); }

src/ast/euf/euf_bv_plugin.cpp

@@ -104,8 +104,8 @@ namespace euf {
     }
 
     void bv_plugin::merge_eh(enode* x, enode* y) {
-        SASSERT(x == x->get_root());
-        SASSERT(x == y->get_root());
+        if (!bv.is_bv(x->get_expr()))
+            return;
 
         TRACE("bv", tout << "merge_eh " << g.bpp(x) << " == " << g.bpp(y) << "\n");
         SASSERT(!m_internal);
@@ -343,7 +343,8 @@ namespace euf {
         enode* hi = mk_extract(n, cut, w - 1);
         enode* lo = mk_extract(n, 0, cut - 1);        
         auto& i = info(n);
-        SASSERT(i.value);
+        if (!i.value)
+            i.value = n;
         i.hi = hi;
         i.lo = lo;
         i.cut = cut;

src/math/dd/dd_pdd.cpp

@@ -1807,7 +1807,9 @@ namespace dd {
     pdd& pdd::operator=(pdd const& other) { 
         if (m != other.m) {
             verbose_stream() << "pdd manager confusion: " << *this << " (mod 2^" << power_of_2() << ") := " << other << " (mod 2^" << other.power_of_2() << ")\n";
+            UNREACHABLE();
             // TODO: in the end, this operator should probably be changed to also update the manager. But for now I want to detect such confusions.
+            reset(*other.m);
         }
         SASSERT_EQ(power_of_2(), other.power_of_2());
         VERIFY_EQ(power_of_2(), other.power_of_2());

src/math/lp/lp_api.h

@@ -108,6 +108,7 @@ namespace lp_api {
         unsigned m_gomory_cuts;
         unsigned m_assume_eqs;
         unsigned m_branch;
+        unsigned m_band_axioms;
         stats() { reset(); }
         void reset() {
             memset(this, 0, sizeof(*this));
@@ -128,6 +129,7 @@ namespace lp_api {
             st.update("arith-gomory-cuts", m_gomory_cuts);
             st.update("arith-assume-eqs", m_assume_eqs);
             st.update("arith-branch", m_branch);
+            st.update("arith-band-axioms", m_band_axioms);
         }
     };
 

src/sat/sat_solver.cpp

@@ -879,7 +879,6 @@ namespace sat {
         m_conflict = c;
         m_not_l    = not_l;
         TRACE("sat", display(display_justification(tout << "conflict " << not_l << " ", c) << "\n"));
-        TRACE("sat", display_watches(tout));
     }
 
     void solver::assign_core(literal l, justification j) {
@@ -1720,6 +1719,9 @@ namespace sat {
             if (next == null_bool_var)
                 return false;
         }
+        else {
+            SASSERT(value(next) == l_undef);
+        }
         push();
         m_stats.m_decision++;
 
@@ -1729,11 +1731,14 @@ namespace sat {
             phase = guess(next) ? l_true: l_false;
 
         literal next_lit(next, false);
+        SASSERT(value(next_lit) == l_undef);
 
         if (m_ext && m_ext->decide(next, phase)) {
+
             if (used_queue)
                 m_case_split_queue.unassign_var_eh(next);
             next_lit = literal(next, false);
+            SASSERT(value(next_lit) == l_undef);
         }
 
         if (phase == l_undef)
@@ -2429,9 +2434,8 @@ namespace sat {
         m_conflicts_since_restart++;
         m_conflicts_since_gc++;
         m_stats.m_conflict++;
-        if (m_step_size > m_config.m_step_size_min) {
-            m_step_size -= m_config.m_step_size_dec;
-        }
+        if (m_step_size > m_config.m_step_size_min)
+            m_step_size -= m_config.m_step_size_dec;        
 
         bool unique_max;
         m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);        
@@ -2554,7 +2558,8 @@ namespace sat {
                     }
                     SASSERT(lvl(c_var) < m_conflict_lvl);
                 }
-                CTRACE("sat", idx == 0, 
+                CTRACE("sat", idx == 0,
+                       tout << "conflict level " << m_conflict_lvl << "\n";
                        for (literal lit : m_trail)
                            if (is_marked(lit.var()))
                                tout << "missed " << lit << "@" << lvl(lit) << "\n";);
@@ -2809,8 +2814,9 @@ namespace sat {
         unsigned level = 0;
 
         if (not_l != null_literal) {
-            level = lvl(not_l);            
+            level = lvl(not_l);
         }      
+        TRACE("sat", tout << "level " << not_l << " is " << level << " " << js << "\n");
 
         switch (js.get_kind()) {
         case justification::NONE:
@@ -3485,11 +3491,10 @@ namespace sat {
     //
     // -----------------------
     void solver::push() {
+        SASSERT(!m_ext || !m_ext->can_propagate());
         SASSERT(!inconsistent());
         TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";);
         SASSERT(m_qhead == m_trail.size());
-        if (m_ext) 
-            m_ext->unit_propagate();
         m_scopes.push_back(scope());
         scope & s = m_scopes.back();
         m_scope_lvl++;