diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 9a7bc1856a8..a10af72a654 100644 --- a/RELEASE_NOTES.md +++ b/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 ============== diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index ba2b4b4a72c..8317b37c39b 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/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(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()); } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index fa359a9a7cd..25c4977e9f2 100644 --- a/src/ast/arith_decl_plugin.h +++ b/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(); } diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index f725fefc5b9..30cfe4cdbeb 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/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); +} diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 9126b97b7b8..89588ee0ea8 100644 --- a/src/ast/bv_decl_plugin.h +++ b/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); } diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 99bf8941bbd..f640b3ed074 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/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; diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 55156c53abf..3ad64acfdab 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/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()); diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index 2a4e5058d4f..0eb8b6b3713 100644 --- a/src/math/lp/lp_api.h +++ b/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); } }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 96b3c13c40e..a1b88bed1ca 100644 --- a/src/sat/sat_solver.cpp +++ b/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++; diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 7caccded641..e5d35a4f968 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -5,6 +5,7 @@ z3_add_component(sat_smt arith_internalize.cpp arith_sls.cpp arith_solver.cpp + arith_value.cpp array_axioms.cpp array_diagnostics.cpp array_internalize.cpp @@ -27,6 +28,7 @@ z3_add_component(sat_smt euf_proof_checker.cpp euf_relevancy.cpp euf_solver.cpp + intblast_solver.cpp fpa_solver.cpp pb_card.cpp pb_constraint.cpp diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 173ae28c89c..f004422a652 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -205,6 +205,80 @@ namespace arith { add_clause(dgez, neg); } + bool solver::check_band_term(app* n) { + unsigned sz; + expr* x, * y; + if (!ctx.is_relevant(expr2enode(n))) + return true; + VERIFY(a.is_band(n, sz, x, y)); + expr_ref vx(m), vy(m),vn(m); + if (!get_value(expr2enode(x), vx) || !get_value(expr2enode(y), vy) || !get_value(expr2enode(n), vn)) { + IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n"); + found_unsupported(n); + return true; + } + rational valn, valx, valy; + bool is_int; + if (!a.is_numeral(vn, valn, is_int) || !is_int || !a.is_numeral(vx, valx, is_int) || !is_int || !a.is_numeral(vy, valy, is_int) || !is_int) { + IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n"); + found_unsupported(n); + return true; + } + // verbose_stream() << "band: " << mk_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n"; + rational N = rational::power_of_two(sz); + valx = mod(valx, N); + valy = mod(valy, N); + SASSERT(0 <= valn && valn < N); + + // x mod 2^{i + 1} >= 2^i means the i'th bit is 1. + auto bitof = [&](expr* x, unsigned i) { + expr_ref r(m); + r = a.mk_ge(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), a.mk_int(rational::power_of_two(i))); + return mk_literal(r); + }; + for (unsigned i = 0; i < sz; ++i) { + bool xb = valx.get_bit(i); + bool yb = valy.get_bit(i); + bool nb = valn.get_bit(i); + if (xb && yb && !nb) + add_clause(~bitof(x, i), ~bitof(y, i), bitof(n, i)); + else if (nb && !xb) + add_clause(~bitof(n, i), bitof(x, i)); + else if (nb && !yb) + add_clause(~bitof(n, i), bitof(y, i)); + else + continue; + return false; + } + return true; + } + + bool solver::check_band_terms() { + for (app* n : m_band_terms) { + if (!check_band_term(n)) { + ++m_stats.m_band_axioms; + return false; + } + } + return true; + } + + /* + * 0 <= x&y < 2^sz + * x&y <= x + * x&y <= y + */ + void solver::mk_band_axiom(app* n) { + unsigned sz; + expr* x, * y; + VERIFY(a.is_band(n, sz, x, y)); + rational N = rational::power_of_two(sz); + add_clause(mk_literal(a.mk_ge(n, a.mk_int(0)))); + add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1)))); + add_clause(mk_literal(a.mk_le(n, a.mk_mod(x, a.mk_int(N))))); + add_clause(mk_literal(a.mk_le(n, a.mk_mod(y, a.mk_int(N))))); + } + void solver::mk_bound_axioms(api_bound& b) { theory_var v = b.get_var(); lp_api::bound_kind kind1 = b.get_bound_kind(); diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 3c628631730..decd49019e4 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -252,6 +252,12 @@ namespace arith { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } + else if (a.is_band(n)) { + m_band_terms.push_back(to_app(n)); + mk_band_axiom(to_app(n)); + ctx.push(push_back_vector(m_band_terms)); + ensure_arg_vars(to_app(n)); + } else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) { found_unsupported(n); ensure_arg_vars(to_app(n)); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 2be9b6b600c..eff25bc4a3b 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -619,17 +619,17 @@ namespace arith { } } - void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + bool solver::get_value(euf::enode* n, expr_ref& value) { theory_var v = n->get_th_var(get_id()); expr* o = n->get_expr(); - expr_ref value(m); + if (m.is_value(n->get_root()->get_expr())) { value = n->get_root()->get_expr(); } else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) { anum const& an = nl_value(v, m_nla->tmp1()); if (a.is_int(o) && !m_nla->am().is_int(an)) - value = a.mk_numeral(rational::zero(), a.is_int(o)); + value = a.mk_numeral(rational::zero(), a.is_int(o)); else value = a.mk_numeral(m_nla->am(), nl_value(v, m_nla->tmp1()), a.is_int(o)); } @@ -637,24 +637,35 @@ namespace arith { rational r = get_value(v); TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";); SASSERT("integer variables should have integer values: " && (ctx.get_config().m_arith_ignore_int || !a.is_int(o) || r.is_int() || m_not_handled != nullptr || m.limit().is_canceled())); - if (a.is_int(o) && !r.is_int()) + if (a.is_int(o) && !r.is_int()) r = floor(r); value = a.mk_numeral(r, o->get_sort()); } + else + return false; + + return true; + } + + + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + expr_ref value(m); + expr* o = n->get_expr(); + if (get_value(n, value)) + ; else if (a.is_arith_expr(o) && reflect(o)) { expr_ref_vector args(m); for (auto* arg : *to_app(o)) { if (m.is_value(arg)) args.push_back(arg); - else + else args.push_back(values.get(ctx.get_enode(arg)->get_root_id())); } value = m.mk_app(to_app(o)->get_decl(), args.size(), args.data()); ctx.get_rewriter()(value); } - else { - value = mdl.get_fresh_value(o->get_sort()); - } + else + value = mdl.get_fresh_value(n->get_sort()); mdl.register_value(value); values.set(n->get_root_id(), value); } @@ -1042,6 +1053,9 @@ namespace arith { if (!check_delayed_eqs()) return sat::check_result::CR_CONTINUE; + if (!int_undef && !check_band_terms()) + return sat::check_result::CR_CONTINUE; + if (ctx.get_config().m_arith_ignore_int && int_undef) return sat::check_result::CR_GIVEUP; if (m_not_handled != nullptr) { @@ -1192,7 +1206,8 @@ namespace arith { lia_check = l_undef; break; case lp::lia_move::continue_with_check: - lia_check = l_undef; + TRACE("arith", tout << "continue-with-check\n"); + lia_check = l_false; break; default: UNREACHABLE(); diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 20ae599c265..022dbeaead6 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -214,6 +214,7 @@ namespace arith { expr* m_not_handled = nullptr; ptr_vector m_underspecified; ptr_vector m_idiv_terms; + ptr_vector m_band_terms; vector > m_use_list; // bounds where variables are used. // attributes for incremental version: @@ -317,6 +318,7 @@ namespace arith { void mk_bound_axioms(api_bound& b); void mk_bound_axiom(api_bound& b1, api_bound& b2); void mk_power0_axioms(app* t, app* n); + void mk_band_axiom(app* n); void flush_bound_axioms(); void add_farkas_clause(sat::literal l1, sat::literal l2); @@ -408,6 +410,8 @@ namespace arith { bool check_delayed_eqs(); lbool check_lia(); lbool check_nla(); + bool check_band_terms(); + bool check_band_term(app* n); void add_lemmas(); void propagate_nla(); void add_equality(lpvar v, rational const& k, lp::explanation const& exp); @@ -522,6 +526,8 @@ namespace arith { bool add_eq(lpvar u, lpvar v, lp::explanation const& e, bool is_fixed); void consume(rational const& v, lp::constraint_index j); bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational& bval) const; + + bool get_value(euf::enode* n, expr_ref& val); }; diff --git a/src/sat/smt/arith_value.cpp b/src/sat/smt/arith_value.cpp new file mode 100644 index 00000000000..bb301808e40 --- /dev/null +++ b/src/sat/smt/arith_value.cpp @@ -0,0 +1,145 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + smt_arith_value.cpp + +Abstract: + + Utility to extract arithmetic values from context. + +Author: + + Nikolaj Bjorner (nbjorner) 2018-12-08. + +Revision History: + +--*/ + +#include "ast/ast_pp.h" +#include "sat/smt/arith_value.h" +#include "sat/smt/euf_solver.h" +#include "sat/smt/arith_solver.h" + +namespace arith { + + arith_value::arith_value(euf::solver& s) : + s(s), m(s.get_manager()), a(m) {} + + void arith_value::init() { + if (!as) + as = dynamic_cast(s.fid2solver(a.get_family_id())); + } + + bool arith_value::get_value(expr* e, rational& val) { + auto n = s.get_enode(e); + expr_ref _val(m); + init(); + return n && as->get_value(n, _val) && a.is_numeral(_val, val); + } + +#if 0 + bool arith_value::get_lo_equiv(expr* e, rational& lo, bool& is_strict) { + if (!s.get_enode(e)) + return false; + init(); + is_strict = false; + bool found = false; + bool is_strict1; + rational lo1; + for (auto sib : euf::enode_class(s.get_enode(e))) { + if (!as->get_lower(sib, lo1, is_strict1)) + continue; + if (!found || lo1 > lo || lo == lo1 && is_strict1) + lo = lo1, is_strict = is_strict1; + found = true; + } + CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m) << "\n";); + return found; + } + + bool arith_value::get_up_equiv(expr* e, rational& hi, bool& is_strict) { + if (!s.get_enode(e)) + return false; + init(); + is_strict = false; + bool found = false; + bool is_strict1; + rational hi1; + for (auto sib : euf::enode_class(s.get_enode(e))) { + if (!as->get_upper(sib, hi1, is_strict1)) + continue; + if (!found || hi1 < hi || hi == hi1 && is_strict1) + hi = hi1, is_strict = is_strict1; + found = true; + } + CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m) << "\n";); + return found; + } + + bool arith_value::get_up(expr* e, rational& up, bool& is_strict) const { + init(); + enode* n = s.get_enode(e); + is_strict = false; + return n && as->get_upper(n, up, is_strict); + } + + bool arith_value::get_lo(expr* e, rational& lo, bool& is_strict) const { + init(); + enode* n = s.get_enode(e); + is_strict = false; + return n && as->get_lower(n, lo, is_strict); + } + +#endif + + +#if 0 + + + bool arith_value::get_value_equiv(expr* e, rational& val) const { + if (!m_ctx->e_internalized(e)) return false; + expr_ref _val(m); + enode* next = m_ctx->get_enode(e), * n = next; + do { + e = next->get_expr(); + if (m_tha && m_tha->get_value(next, _val) && a.is_numeral(_val, val)) return true; + if (m_thi && m_thi->get_value(next, _val) && a.is_numeral(_val, val)) return true; + if (m_thr && m_thr->get_value(next, val)) return true; + next = next->get_next(); + } while (next != n); + TRACE("arith_value", tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";); + return false; + } + + expr_ref arith_value::get_lo(expr* e) const { + rational lo; + bool s = false; + if ((a.is_int_real(e) || b.is_bv(e)) && get_lo(e, lo, s) && !s) { + return expr_ref(a.mk_numeral(lo, e->get_sort()), m); + } + return expr_ref(e, m); + } + + expr_ref arith_value::get_up(expr* e) const { + rational up; + bool s = false; + if ((a.is_int_real(e) || b.is_bv(e)) && get_up(e, up, s) && !s) { + return expr_ref(a.mk_numeral(up, e->get_sort()), m); + } + return expr_ref(e, m); + } + + expr_ref arith_value::get_fixed(expr* e) const { + rational lo, up; + bool s = false; + if (a.is_int_real(e) && get_lo(e, lo, s) && !s && get_up(e, up, s) && !s && lo == up) { + return expr_ref(a.mk_numeral(lo, e->get_sort()), m); + } + return expr_ref(e, m); + } + +#endif + +}; diff --git a/src/sat/smt/arith_value.h b/src/sat/smt/arith_value.h new file mode 100644 index 00000000000..b858ff8965a --- /dev/null +++ b/src/sat/smt/arith_value.h @@ -0,0 +1,52 @@ + +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + arith_value.h + +Abstract: + + Utility to extract arithmetic values from context. + +Author: + + Nikolaj Bjorner (nbjorner) 2018-12-08. + +Revision History: + +--*/ +#pragma once + +#include "ast/arith_decl_plugin.h" + +namespace euf { + class solver; +} +namespace arith { + + class solver; + + class arith_value { + euf::solver& s; + ast_manager& m; + arith_util a; + solver* as = nullptr; + void init(); + public: + arith_value(euf::solver& s); + bool get_value(expr* e, rational& value); + +#if 0 + bool get_lo_equiv(expr* e, rational& lo, bool& strict); + bool get_up_equiv(expr* e, rational& up, bool& strict); + bool get_lo(expr* e, rational& lo, bool& strict); + bool get_up(expr* e, rational& up, bool& strict); + bool get_value_equiv(expr* e, rational& value); + expr_ref get_lo(expr* e); + expr_ref get_up(expr* e); + expr_ref get_fixed(expr* e); +#endif + }; +}; diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index daecb7325d6..52c4ed95386 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -400,7 +400,7 @@ namespace dt { return; } SASSERT(val == l_undef || (val == l_false && !d->m_constructor)); - ctx.push(set_vector_idx_trail(d->m_recognizers, c_idx)); + ctx.push(set_vector_idx_trail(d->m_recognizers, c_idx)); d->m_recognizers[c_idx] = recognizer; if (val == l_false) propagate_recognizer(v, recognizer); diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 943d0b3245f..f750f186d56 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -106,7 +106,6 @@ namespace euf { attach_node(mk_enode(e, 0, nullptr)); return true; } - bool solver::post_visit(expr* e, bool sign, bool root) { unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0; m_args.reset(); diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index b117ac1e32e..073d164be79 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -302,7 +302,7 @@ namespace euf { if (mval != sval) { if (r->bool_var() != sat::null_bool_var) out << "b" << r->bool_var() << " "; - out << bpp(r) << " :=\neval: " << sval << "\nmval: " << mval << "\n"; + out << bpp(r) << " :=\nvalue obtained from model: " << sval << "\nvalue of the root expression: " << mval << "\n"; continue; } if (!m.is_bool(val)) @@ -310,7 +310,7 @@ namespace euf { auto bval = s().value(r->bool_var()); bool tt = l_true == bval; if (tt != m.is_true(sval)) - out << bpp(r) << " :=\neval: " << sval << "\nmval: " << bval << "\n"; + out << bpp(r) << " :=\nvalue according to model: " << sval << "\nvalue of Boolean literal: " << bval << "\n"; } for (euf::enode* r : nodes) if (r) @@ -357,6 +357,7 @@ namespace euf { if (!tt && !mdl.is_true(e)) continue; CTRACE("euf", first, display_validation_failure(tout, mdl, n);); + CTRACE("euf", first, display(tout)); IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n);); (void)first; first = false; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 3ae4425fc12..ff11b074938 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -21,6 +21,7 @@ Module Name: #include "sat/smt/sat_smt.h" #include "sat/smt/pb_solver.h" #include "sat/smt/bv_solver.h" +#include "sat/smt/intblast_solver.h" #include "sat/smt/euf_solver.h" #include "sat/smt/array_solver.h" #include "sat/smt/arith_solver.h" @@ -134,8 +135,16 @@ namespace euf { special_relations_util sp(m); if (pb.get_family_id() == fid) ext = alloc(pb::solver, *this, fid); - else if (bvu.get_family_id() == fid) - ext = alloc(bv::solver, *this, fid); + else if (bvu.get_family_id() == fid) { + if (get_config().m_bv_solver == 0) + ext = alloc(bv::solver, *this, fid); + else if (get_config().m_bv_solver == 1) + throw default_exception("polysat solver is not integrated"); + else if (get_config().m_bv_solver == 2) + ext = alloc(intblast::solver, *this); + else + throw default_exception("unknown bit-vector solver. Accepted values 0 (bit blast), 1 (polysat), 2 (int blast)"); + } else if (au.get_family_id() == fid) ext = alloc(array::solver, *this, fid); else if (fpa.get_family_id() == fid) @@ -209,6 +218,15 @@ namespace euf { s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx)); } + lbool solver::resolve_conflict() { + for (auto* s : m_solvers) { + lbool r = s->resolve_conflict(); + if (r != l_undef) + return r; + } + return l_undef; + } + /** Retrieve set of literals r that imply r. Since the set of literals are retrieved modulo multiple theories in a single implication @@ -281,6 +299,26 @@ namespace euf { } } + void solver::get_eq_antecedents(enode* a, enode* b, literal_vector& r) { + m_egraph.begin_explain(); + m_explain.reset(); + m_egraph.explain_eq(m_explain, nullptr, a, b); + for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) { + size_t* e = m_explain[qhead]; + if (is_literal(e)) + r.push_back(get_literal(e)); + else { + size_t idx = get_justification(e); + auto* ext = sat::constraint_base::to_extension(idx); + SASSERT(ext != this); + sat::literal lit = sat::null_literal; + ext->get_antecedents(lit, idx, r, true); + } + } + m_egraph.end_explain(); + } + + void solver::get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) { for (auto lit : euf::th_explain::lits(jst)) r.push_back(lit); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index db99ec512b2..7d2d01473ea 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -363,11 +363,13 @@ namespace euf { bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); } size_t* to_justification(sat::literal l) { return to_ptr(l); } void set_conflict(th_explain* p) { set_conflict(p->to_index()); } + bool inconsistent() const { return s().inconsistent() || m_egraph.inconsistent(); } bool set_root(literal l, literal r) override; void flush_roots() override; void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override; + void get_eq_antecedents(enode* a, enode* b, literal_vector& r); void get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing); void add_eq_antecedent(bool probing, enode* a, enode* b); void explain_diseq(ptr_vector& ex, cc_justification* cc, enode* a, enode* b); @@ -378,6 +380,7 @@ namespace euf { bool get_case_split(bool_var& var, lbool& phase) override; void asserted(literal l) override; sat::check_result check() override; + lbool resolve_conflict() override; void push() override; void pop(unsigned n) override; void user_push() override; diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp new file mode 100644 index 00000000000..9d03d0ad086 --- /dev/null +++ b/src/sat/smt/intblast_solver.cpp @@ -0,0 +1,985 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + intblast_solver.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2023-12-10 + +--*/ + +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "ast/rewriter/bv_rewriter.h" +#include "params/bv_rewriter_params.hpp" +#include "sat/smt/intblast_solver.h" +#include "sat/smt/euf_solver.h" +#include "sat/smt/arith_value.h" + + +namespace intblast { + + solver::solver(euf::solver& ctx) : + th_euf_solver(ctx, symbol("intblast"), ctx.get_manager().get_family_id("bv")), + ctx(ctx), + s(ctx.s()), + m(ctx.get_manager()), + bv(m), + a(m), + m_translate(m), + m_args(m), + m_pinned(m) + {} + + euf::theory_var solver::mk_var(euf::enode* n) { + auto r = euf::th_euf_solver::mk_var(n); + ctx.attach_th_var(n, this, r); + TRACE("bv", tout << "mk-var: v" << r << " " << ctx.bpp(n) << "\n";); + return r; + } + + sat::literal solver::internalize(expr* e, bool sign, bool root) { + force_push(); + SASSERT(m.is_bool(e)); + if (!visit_rec(m, e, sign, root)) + return sat::null_literal; + sat::literal lit = expr2literal(e); + if (sign) + lit.neg(); + return lit; + } + + void solver::internalize(expr* e) { + force_push(); + visit_rec(m, e, false, false); + } + + bool solver::visit(expr* e) { + if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { + ctx.internalize(e); + return true; + } + m_stack.push_back(sat::eframe(e)); + return false; + } + + bool solver::visited(expr* e) { + euf::enode* n = expr2enode(e); + return n && n->is_attached_to(get_id()); + } + + + + bool solver::post_visit(expr* e, bool sign, bool root) { + euf::enode* n = expr2enode(e); + app* a = to_app(e); + if (visited(e)) + return true; + SASSERT(!n || !n->is_attached_to(get_id())); + if (!n) + n = mk_enode(e, false); + SASSERT(!n->is_attached_to(get_id())); + mk_var(n); + SASSERT(n->is_attached_to(get_id())); + internalize_bv(a); + return true; + } + + void solver::eq_internalized(euf::enode* n) { + expr* e = n->get_expr(); + expr* x, * y; + VERIFY(m.is_eq(n->get_expr(), x, y)); + SASSERT(bv.is_bv(x)); + if (!is_translated(e)) { + ensure_translated(x); + ensure_translated(y); + m_args.reset(); + m_args.push_back(a.mk_sub(translated(x), translated(y))); + set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); + } + m_preds.push_back(e); + ctx.push(push_back_vector(m_preds)); + } + + void solver::set_translated(expr* e, expr* r) { + SASSERT(r); + SASSERT(!is_translated(e)); + m_translate.setx(e->get_id(), r); + ctx.push(set_vector_idx_trail(m_translate, e->get_id())); + } + + void solver::internalize_bv(app* e) { + ensure_translated(e); + if (m.is_bool(e)) { + m_preds.push_back(e); + ctx.push(push_back_vector(m_preds)); + } + } + + bool solver::add_bound_axioms() { + if (m_vars_qhead == m_vars.size()) + return false; + ctx.push(value_trail(m_vars_qhead)); + for (; m_vars_qhead < m_vars.size(); ++m_vars_qhead) { + auto v = m_vars[m_vars_qhead]; + auto w = translated(v); + auto sz = rational::power_of_two(bv.get_bv_size(v->get_sort())); + auto lo = ctx.mk_literal(a.mk_ge(w, a.mk_int(0))); + auto hi = ctx.mk_literal(a.mk_le(w, a.mk_int(sz - 1))); + ctx.mark_relevant(lo); + ctx.mark_relevant(hi); + add_unit(lo); + add_unit(hi); + } + return true; + } + + bool solver::add_predicate_axioms() { + if (m_preds_qhead == m_preds.size()) + return false; + ctx.push(value_trail(m_preds_qhead)); + for (; m_preds_qhead < m_preds.size(); ++m_preds_qhead) { + expr* e = m_preds[m_preds_qhead]; + expr_ref r(translated(e), m); + ctx.get_rewriter()(r); + auto a = expr2literal(e); + auto b = mk_literal(r); + ctx.mark_relevant(b); +// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; + add_equiv(a, b); + } + return true; + } + + bool solver::unit_propagate() { + return add_bound_axioms() || add_predicate_axioms(); + } + + void solver::ensure_translated(expr* e) { + if (m_translate.get(e->get_id(), nullptr)) + return; + ptr_vector todo; + ast_fast_mark1 visited; + todo.push_back(e); + visited.mark(e); + for (unsigned i = 0; i < todo.size(); ++i) { + expr* e = todo[i]; + if (!is_app(e)) + continue; + app* a = to_app(e); + if (m.is_bool(e) && a->get_family_id() != bv.get_family_id()) + continue; + for (auto arg : *a) + if (!visited.is_marked(arg) && !m_translate.get(arg->get_id(), nullptr)) { + visited.mark(arg); + todo.push_back(arg); + } + } + std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); + for (expr* e : todo) + translate_expr(e); + } + + lbool solver::check_solver_state() { + sat::literal_vector literals; + uint_set selected; + for (auto const& clause : s.clauses()) { + if (any_of(*clause, [&](auto lit) { return selected.contains(lit.index()); })) + continue; + if (any_of(*clause, [&](auto lit) { return s.value(lit) == l_true && !is_bv(lit); })) + continue; + // TBD: if we associate "status" with clauses, we can also remove theory axioms from polysat + sat::literal selected_lit = sat::null_literal; + for (auto lit : *clause) { + if (s.value(lit) != l_true) + continue; + SASSERT(is_bv(lit)); + if (selected_lit == sat::null_literal || s.lvl(selected_lit) > s.lvl(lit)) + selected_lit = lit; + } + if (selected_lit == sat::null_literal) { + UNREACHABLE(); + return l_undef; + } + selected.insert(selected_lit.index()); + literals.push_back(selected_lit); + } + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + auto lit = s.trail_literal(i); + if (selected.contains(lit.index()) || !is_bv(lit)) + continue; + selected.insert(lit.index()); + literals.push_back(lit); + } + svector> bin; + s.collect_bin_clauses(bin, false, false); + for (auto [a, b] : bin) { + if (selected.contains(a.index())) + continue; + if (selected.contains(b.index())) + continue; + if (s.value(a) == l_true && !is_bv(a)) + continue; + if (s.value(b) == l_true && !is_bv(b)) + continue; + if (s.value(a) == l_false) + std::swap(a, b); + if (s.value(b) == l_true && s.value(a) == l_true && s.lvl(b) < s.lvl(a)) + std::swap(a, b); + selected.insert(a.index()); + literals.push_back(a); + } + + m_core.reset(); + m_is_plugin = false; + m_solver = mk_smt2_solver(m, s.params(), symbol::null); + + expr_ref_vector es(m); + for (auto lit : literals) + es.push_back(ctx.literal2expr(lit)); + + translate(es); + + for (auto e : m_vars) { + auto v = translated(e); + auto b = rational::power_of_two(bv.get_bv_size(e)); + m_solver->assert_expr(a.mk_le(a.mk_int(0), v)); + m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); + } + + IF_VERBOSE(10, verbose_stream() << "check\n"; + m_solver->display(verbose_stream()); + verbose_stream() << es << "\n"); + + lbool r = m_solver->check_sat(es); + + m_solver->collect_statistics(m_stats); + + IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); + + if (r == l_false) { + expr_ref_vector core(m); + m_solver->get_unsat_core(core); + obj_map e2index; + for (unsigned i = 0; i < es.size(); ++i) + e2index.insert(es.get(i), i); + for (auto e : core) { + unsigned idx = e2index[e]; + if (idx < literals.size()) + m_core.push_back(literals[idx]); + else + m_core.push_back(ctx.mk_literal(e)); + } + } + return r; + }; + + bool solver::is_bv(sat::literal lit) { + expr* e = ctx.bool_var2expr(lit.var()); + if (!e) + return false; + if (m.is_and(e) || m.is_or(e) || m.is_not(e) || m.is_implies(e) || m.is_iff(e)) + return false; + return any_of(subterms::all(expr_ref(e, m)), [&](auto* p) { return bv.is_bv_sort(p->get_sort()); }); + } + + void solver::sorted_subterms(expr_ref_vector& es, ptr_vector& sorted) { + expr_fast_mark1 visited; + for (expr* e : es) { + if (is_translated(e)) + continue; + sorted.push_back(e); + visited.mark(e); + } + for (unsigned i = 0; i < sorted.size(); ++i) { + expr* e = sorted[i]; + if (is_app(e)) { + app* a = to_app(e); + for (expr* arg : *a) { + if (!visited.is_marked(arg) && !is_translated(arg)) { + visited.mark(arg); + sorted.push_back(arg); + } + } + + // + // Add ground equalities to ensure the model is valid with respect to the current case splits. + // This may cause more conflicts than necessary. Instead could use intblast on the base level, but using literal + // assignment from complete level. + // E.g., force the solver to completely backtrack, check satisfiability using the assignment obtained under a complete assignment. + // If intblast is SAT, then force the model and literal assignment on the rest of the literals. + // + if (!is_ground(e)) + continue; + euf::enode* n = ctx.get_enode(e); + if (!n) + continue; + if (n == n->get_root()) + continue; + expr* r = n->get_root()->get_expr(); + es.push_back(m.mk_eq(e, r)); + r = es.back(); + if (!visited.is_marked(r) && !is_translated(r)) { + visited.mark(r); + sorted.push_back(r); + } + } + else if (is_quantifier(e)) { + quantifier* q = to_quantifier(e); + expr* b = q->get_expr(); + if (!visited.is_marked(b) && !is_translated(b)) { + visited.mark(b); + sorted.push_back(b); + } + } + } + std::stable_sort(sorted.begin(), sorted.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); + } + + void solver::translate(expr_ref_vector& es) { + ptr_vector todo; + + sorted_subterms(es, todo); + + for (expr* e : todo) + translate_expr(e); + + TRACE("bv", + for (expr* e : es) + tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated(e), m) << "\n"; + ); + + for (unsigned i = 0; i < es.size(); ++i) + es[i] = translated(es.get(i)); + } + + sat::check_result solver::check() { + // ensure that bv2int is injective + for (auto e : m_bv2int) { + euf::enode* n = expr2enode(e); + euf::enode* r1 = n->get_arg(0)->get_root(); + for (auto sib : euf::enode_class(n)) { + if (sib == n) + continue; + if (!bv.is_bv2int(sib->get_expr())) + continue; + if (sib->get_arg(0)->get_root() == r1) + continue; + auto a = eq_internalize(n, sib); + auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); + ctx.mark_relevant(a); + ctx.mark_relevant(b); + add_clause(~a, b, nullptr); + return sat::check_result::CR_CONTINUE; + } + } + // ensure that int2bv respects values + // bv2int(int2bv(x)) = x mod N + for (auto e : m_int2bv) { + auto n = expr2enode(e); + auto x = n->get_arg(0)->get_expr(); + auto bv2int = bv.mk_bv2int(e); + ctx.internalize(bv2int); + auto N = rational::power_of_two(bv.get_bv_size(e)); + auto xModN = a.mk_mod(x, a.mk_int(N)); + ctx.internalize(xModN); + auto nBv2int = ctx.get_enode(bv2int); + auto nxModN = ctx.get_enode(xModN); + if (nBv2int->get_root() != nxModN->get_root()) { + auto a = eq_internalize(nBv2int, nxModN); + ctx.mark_relevant(a); + add_unit(a); + return sat::check_result::CR_CONTINUE; + } + } + return sat::check_result::CR_DONE; + } + + expr* solver::umod(expr* bv_expr, unsigned i) { + expr* x = arg(i); + rational r; + rational N = bv_size(bv_expr); + if (a.is_numeral(x, r)) { + if (0 <= r && r < N) + return x; + return a.mk_int(mod(r, N)); + } + if (any_of(m_vars, [&](expr* v) { return translated(v) == x && bv.get_bv_size(v) == bv.get_bv_size(bv_expr); })) + return x; + return a.mk_mod(x, a.mk_int(N)); + } + + expr* solver::smod(expr* bv_expr, unsigned i) { + expr* x = arg(i); + auto N = bv_size(bv_expr); + auto shift = N / 2; + rational r; + if (a.is_numeral(x, r)) + return a.mk_int(mod(r + shift, N)); + return a.mk_mod(a.mk_add(x, a.mk_int(shift)), a.mk_int(N)); + } + + rational solver::bv_size(expr* bv_expr) { + return rational::power_of_two(bv.get_bv_size(bv_expr->get_sort())); + } + + void solver::translate_expr(expr* e) { + if (is_quantifier(e)) + translate_quantifier(to_quantifier(e)); + else if (is_var(e)) + translate_var(to_var(e)); + else { + app* ap = to_app(e); + if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) { + set_translated(e, e); + return; + } + m_args.reset(); + for (auto arg : *ap) + m_args.push_back(translated(arg)); + + if (ap->get_family_id() == basic_family_id) + translate_basic(ap); + else if (ap->get_family_id() == bv.get_family_id()) + translate_bv(ap); + else + translate_app(ap); + } + } + + void solver::translate_quantifier(quantifier* q) { + if (is_lambda(q)) + throw default_exception("lambdas are not supported in intblaster"); + if (m_is_plugin) { + set_translated(q, q); + return; + } + expr* b = q->get_expr(); + unsigned nd = q->get_num_decls(); + ptr_vector sorts; + for (unsigned i = 0; i < nd; ++i) { + auto s = q->get_decl_sort(i); + if (bv.is_bv_sort(s)) { + NOT_IMPLEMENTED_YET(); + sorts.push_back(a.mk_int()); + } + else + + sorts.push_back(s); + } + b = translated(b); + // TODO if sorts contain integer, then created bounds variables. + set_translated(q, m.update_quantifier(q, b)); + } + + void solver::translate_var(var* v) { + if (bv.is_bv_sort(v->get_sort())) + set_translated(v, m.mk_var(v->get_idx(), a.mk_int())); + else + set_translated(v, v); + } + + // Translate functions that are not built-in or bit-vectors. + // Base method uses fresh functions. + // Other method could use bv2int, int2bv axioms and coercions. + // f(args) = bv2int(f(int2bv(args')) + // + + void solver::translate_app(app* e) { + + if (m_is_plugin && m.is_bool(e)) { + set_translated(e, e); + return; + } + + bool has_bv_sort = bv.is_bv(e); + func_decl* f = e->get_decl(); + + for (unsigned i = 0; i < m_args.size(); ++i) + if (bv.is_bv(e->get_arg(i))) + m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i)); + + if (has_bv_sort) + m_vars.push_back(e); + + if (m_is_plugin) { + expr* r = m.mk_app(f, m_args); + if (has_bv_sort) { + ctx.push(push_back_vector(m_vars)); + r = bv.mk_bv2int(r); + } + set_translated(e, r); + return; + } + else if (has_bv_sort) { + if (f->get_family_id() != null_family_id) + throw default_exception("conversion for interpreted functions is not supported by intblast solver"); + func_decl* g = nullptr; + if (!m_new_funs.find(f, g)) { + g = m.mk_fresh_func_decl(e->get_decl()->get_name(), symbol("bv"), f->get_arity(), f->get_domain(), a.mk_int()); + m_new_funs.insert(f, g); + } + f = g; + m_pinned.push_back(f); + } + set_translated(e, m.mk_app(f, m_args)); + } + + void solver::translate_bv(app* e) { + + auto bnot = [&](expr* e) { + return a.mk_sub(a.mk_int(-1), e); + }; + + auto band = [&](expr_ref_vector const& args) { + expr* r = arg(0); + for (unsigned i = 1; i < args.size(); ++i) + r = a.mk_band(bv.get_bv_size(e), r, arg(i)); + return r; + }; + + auto rotate_left = [&](unsigned n) { + auto sz = bv.get_bv_size(e); + n = n % sz; + expr* r = arg(0); + if (n != 0 && sz != 1) { + // r[sz - n - 1 : 0] ++ r[sz - 1 : sz - n] + // r * 2^(sz - n) + (r div 2^n) mod 2^(sz - n)??? + // r * A + (r div B) mod A + auto N = bv_size(e); + auto A = rational::power_of_two(sz - n); + auto B = rational::power_of_two(n); + auto hi = a.mk_mul(r, a.mk_int(A)); + auto lo = a.mk_mod(a.mk_idiv(umod(e, 0), a.mk_int(B)), a.mk_int(A)); + r = a.mk_add(hi, lo); + } + return r; + }; + + expr* bv_expr = e; + expr* r = nullptr; + auto const& args = m_args; + switch (e->get_decl_kind()) { + case OP_BADD: + r = a.mk_add(args); + break; + case OP_BSUB: + r = a.mk_sub(args.size(), args.data()); + break; + case OP_BMUL: + r = a.mk_mul(args); + break; + case OP_ULEQ: + bv_expr = e->get_arg(0); + r = a.mk_le(umod(bv_expr, 0), umod(bv_expr, 1)); + break; + case OP_UGEQ: + bv_expr = e->get_arg(0); + r = a.mk_ge(umod(bv_expr, 0), umod(bv_expr, 1)); + break; + case OP_ULT: + bv_expr = e->get_arg(0); + r = a.mk_lt(umod(bv_expr, 0), umod(bv_expr, 1)); + break; + case OP_UGT: + bv_expr = e->get_arg(0); + r = a.mk_gt(umod(bv_expr, 0), umod(bv_expr, 1)); + break; + case OP_SLEQ: + bv_expr = e->get_arg(0); + r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1)); + break; + case OP_SGEQ: + r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1)); + break; + case OP_SLT: + bv_expr = e->get_arg(0); + r = a.mk_lt(smod(bv_expr, 0), smod(bv_expr, 1)); + break; + case OP_SGT: + bv_expr = e->get_arg(0); + r = a.mk_gt(smod(bv_expr, 0), smod(bv_expr, 1)); + break; + case OP_BNEG: + r = a.mk_uminus(arg(0)); + break; + case OP_CONCAT: { + unsigned sz = 0; + for (unsigned i = args.size(); i-- > 0;) { + expr* old_arg = e->get_arg(i); + expr* new_arg = umod(old_arg, i); + if (sz > 0) { + new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz))); + r = a.mk_add(r, new_arg); + } + else + r = new_arg; + sz += bv.get_bv_size(old_arg->get_sort()); + } + break; + } + case OP_EXTRACT: { + unsigned lo, hi; + expr* old_arg; + VERIFY(bv.is_extract(e, lo, hi, old_arg)); + r = arg(0); + if (lo > 0) + r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo))); + break; + } + case OP_BV_NUM: { + rational val; + unsigned sz; + VERIFY(bv.is_numeral(e, val, sz)); + r = a.mk_int(val); + break; + } + case OP_BUREM: + case OP_BUREM_I: { + expr* x = umod(e, 0), * y = umod(e, 1); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, a.mk_mod(x, y)); + break; + } + case OP_BUDIV: + case OP_BUDIV_I: { + expr* x = arg(0), * y = umod(e, 1); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y)); + break; + } + case OP_BUMUL_NO_OVFL: { + bv_expr = e->get_arg(0); + r = a.mk_lt(a.mk_mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr))); + break; + } + case OP_BSHL: { + expr* x = arg(0), * y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < bv.get_bv_size(e); ++i) + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r); + break; + } + case OP_BNOT: + r = bnot(arg(0)); + break; + case OP_BLSHR: { + expr* x = arg(0), * y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < bv.get_bv_size(e); ++i) + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); + break; + } + case OP_BOR: { + // p | q := (p + q) - band(p, q) + r = arg(0); + for (unsigned i = 1; i < args.size(); ++i) + r = a.mk_sub(a.mk_add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i))); + break; + } + case OP_BNAND: + r = bnot(band(args)); + break; + case OP_BAND: + r = band(args); + break; + case OP_BXNOR: + case OP_BXOR: { + // p ^ q := (p + q) - 2*band(p, q); + unsigned sz = bv.get_bv_size(e); + r = arg(0); + for (unsigned i = 1; i < args.size(); ++i) { + expr* q = arg(i); + r = a.mk_sub(a.mk_add(r, q), a.mk_mul(a.mk_int(2), a.mk_band(sz, r, q))); + } + if (e->get_decl_kind() == OP_BXNOR) + r = bnot(r); + break; + } + case OP_BASHR: { + // + // ashr(x, y) + // if y = k & x >= 0 -> x / 2^k + // if y = k & x < 0 -> (x / 2^k) - 1 + 2^{N-k} + // + unsigned sz = bv.get_bv_size(e); + rational N = bv_size(e); + expr* x = umod(e, 0), *y = umod(e, 1); + expr* signx = a.mk_ge(x, a.mk_int(N / 2)); + r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0)); + for (unsigned i = 0; i < sz; ++i) { + expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); + r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), + m.mk_ite(signx, a.mk_add(d, a.mk_int(- rational::power_of_two(sz-i))), d), + r); + } + break; + } + case OP_ZERO_EXT: + bv_expr = e->get_arg(0); + r = umod(bv_expr, 0); + SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr)); + break; + case OP_SIGN_EXT: { + bv_expr = e->get_arg(0); + r = umod(bv_expr, 0); + SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr)); + unsigned arg_sz = bv.get_bv_size(bv_expr); + unsigned sz = bv.get_bv_size(e); + rational N = rational::power_of_two(sz); + rational M = rational::power_of_two(arg_sz); + expr* signbit = a.mk_ge(r, a.mk_int(M / 2)); + r = m.mk_ite(signbit, a.mk_uminus(r), r); + break; + } + case OP_INT2BV: + m_int2bv.push_back(e); + ctx.push(push_back_vector(m_int2bv)); + r = arg(0); + break; + case OP_BV2INT: + m_bv2int.push_back(e); + ctx.push(push_back_vector(m_bv2int)); + r = umod(e->get_arg(0), 0); + break; + case OP_BCOMP: + bv_expr = e->get_arg(0); + r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0)); + break; + case OP_BSMOD_I: + case OP_BSMOD: { + expr* x = umod(e, 0), *y = umod(e, 1); + rational N = bv_size(e); + expr* signx = a.mk_ge(x, a.mk_int(N/2)); + expr* signy = a.mk_ge(y, a.mk_int(N/2)); + expr* u = a.mk_mod(x, y); + // u = 0 -> 0 + // y = 0 -> x + // x < 0, y < 0 -> -u + // x < 0, y >= 0 -> y - u + // x >= 0, y < 0 -> y + u + // x >= 0, y >= 0 -> u + r = a.mk_uminus(u); + r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), a.mk_add(u, y), r); + r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r); + r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r); + r = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); + break; + } + case OP_BSDIV_I: + case OP_BSDIV: { + // d = udiv(abs(x), abs(y)) + // y = 0, x > 0 -> 1 + // y = 0, x <= 0 -> -1 + // x = 0, y != 0 -> 0 + // x > 0, y < 0 -> -d + // x < 0, y > 0 -> -d + // x > 0, y > 0 -> d + // x < 0, y < 0 -> d + expr* x = umod(e, 0), * y = umod(e, 1); + rational N = bv_size(e); + expr* signx = a.mk_ge(x, a.mk_int(N / 2)); + expr* signy = a.mk_ge(y, a.mk_int(N / 2)); + x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x); + y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); + expr* d = a.mk_idiv(x, y); + r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r); + break; + } + case OP_BSREM_I: + case OP_BSREM: { + // y = 0 -> x + // else x - sdiv(x, y) * y + expr* x = umod(e, 0), * y = umod(e, 1); + rational N = bv_size(e); + expr* signx = a.mk_ge(x, a.mk_int(N / 2)); + expr* signy = a.mk_ge(y, a.mk_int(N / 2)); + expr* absx = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x); + expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); + expr* d = a.mk_idiv(absx, absy); + d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); + r = a.mk_sub(x, a.mk_mul(d, y)); + r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); + break; + } + case OP_ROTATE_LEFT: { + auto n = e->get_parameter(0).get_int(); + r = rotate_left(n); + break; + } + case OP_ROTATE_RIGHT: { + unsigned sz = bv.get_bv_size(e); + auto n = e->get_parameter(0).get_int(); + r = rotate_left(sz - n); + break; + } + case OP_EXT_ROTATE_LEFT: { + unsigned sz = bv.get_bv_size(e); + expr* y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < sz; ++i) + r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r); + break; + } + case OP_EXT_ROTATE_RIGHT: { + unsigned sz = bv.get_bv_size(e); + expr* y = umod(e, 1); + r = a.mk_int(0); + for (unsigned i = 0; i < sz; ++i) + r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r); + break; + } + case OP_REPEAT: { + unsigned n = e->get_parameter(0).get_int(); + expr* x = umod(e->get_arg(0), 0); + r = x; + rational N = bv_size(e->get_arg(0)); + rational N0 = N; + for (unsigned i = 1; i < n; ++i) + r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0; + break; + } + case OP_BREDOR: { + r = umod(e->get_arg(0), 0); + r = m.mk_not(m.mk_eq(r, a.mk_int(0))); + break; + } + case OP_BREDAND: { + rational N = bv_size(e->get_arg(0)); + r = umod(e->get_arg(0), 0); + r = m.mk_not(m.mk_eq(r, a.mk_int(N - 1))); + break; + } + default: + verbose_stream() << mk_pp(e, m) << "\n"; + NOT_IMPLEMENTED_YET(); + } + set_translated(e, r); + } + + void solver::translate_basic(app* e) { + if (m.is_eq(e)) { + bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); }); + if (has_bv_arg) { + expr* bv_expr = e->get_arg(0); + m_args[0] = a.mk_sub(arg(0), arg(1)); + set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0))); + } + else + set_translated(e, m.mk_eq(arg(0), arg(1))); + } + else if (m.is_ite(e)) + set_translated(e, m.mk_ite(arg(0), arg(1), arg(2))); + else if (m_is_plugin) + set_translated(e, e); + else + set_translated(e, m.mk_app(e->get_decl(), m_args)); + } + + rational solver::get_value(expr* e) const { + SASSERT(bv.is_bv(e)); + model_ref mdl; + m_solver->get_model(mdl); + expr_ref r(m); + r = translated(e); + rational val; + if (!mdl->eval_expr(r, r, true)) + return rational::zero(); + if (!a.is_numeral(r, val)) + return rational::zero(); + return val; + } + + void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { + if (m_is_plugin) + add_value_plugin(n, mdl, values); + else + add_value_solver(n, mdl, values); + } + + bool solver::add_dep(euf::enode* n, top_sort& dep) { + if (!is_app(n->get_expr())) + return false; + app* e = to_app(n->get_expr()); + if (n->num_args() == 0) { + dep.insert(n, nullptr); + return true; + } + if (e->get_family_id() != bv.get_family_id()) + return false; + for (euf::enode* arg : euf::enode_args(n)) + dep.add(n, arg->get_root()); + return true; + } + + // TODO: handle dependencies properly by using arithmetical model to retrieve values of translated + // bit-vectors directly. + void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) { + expr* e = n->get_expr(); + SASSERT(bv.is_bv(e)); + + if (bv.is_numeral(e)) { + values.setx(n->get_root_id(), e); + return; + } + + rational r, N = rational::power_of_two(bv.get_bv_size(e)); + expr* te = translated(e); + model_ref mdlr; + m_solver->get_model(mdlr); + expr_ref value(m); + if (mdlr->eval_expr(te, value, true) && a.is_numeral(value, r)) { + values.setx(n->get_root_id(), bv.mk_numeral(mod(r, N), bv.get_bv_size(e))); + return; + } + ctx.s().display(verbose_stream()); + verbose_stream() << "failed to evaluate " << mk_pp(te, m) << " " << value << "\n"; + UNREACHABLE(); + } + + void solver::add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values) { + expr_ref value(m); + if (n->interpreted()) + value = n->get_expr(); + else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) { + bv_rewriter rw(m); + expr_ref_vector args(m); + for (auto arg : euf::enode_args(n)) + args.push_back(values.get(arg->get_root_id())); + rw.mk_app(n->get_decl(), args.size(), args.data(), value); + } + else { + expr_ref bv2int(bv.mk_bv2int(n->get_expr()), m); + euf::enode* b2i = ctx.get_enode(bv2int); + if (!b2i) verbose_stream() << bv2int << "\n"; + SASSERT(b2i); + VERIFY(b2i); + arith::arith_value av(ctx); + rational r; + VERIFY(av.get_value(b2i->get_expr(), r)); + verbose_stream() << ctx.bpp(n) << " := " << r << "\n"; + value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr())); + } + values.set(n->get_root_id(), value); + TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); + } + + sat::literal_vector const& solver::unsat_core() { + return m_core; + } + + std::ostream& solver::display(std::ostream& out) const { + if (m_solver) + m_solver->display(out); + return out; + } + + void solver::collect_statistics(statistics& st) const { + st.copy(m_stats); + } + +} diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h new file mode 100644 index 00000000000..d59dac9355f --- /dev/null +++ b/src/sat/smt/intblast_solver.h @@ -0,0 +1,143 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + intblast_solver.h + +Abstract: + + Int-blast solver. + + check_solver_state assumes a full assignment to literals in + irredundant clauses. + It picks a satisfying Boolean assignment and + checks if it is feasible for bit-vectors using + an arithmetic solver. + + The solver plugin is self-contained. + + Internalize: + - internalize bit-vector terms bottom-up by updating m_translate. + - add axioms of the form: + - ule(b,a) <=> translate(ule(b, a)) + - let arithmetic solver handle bit-vector constraints. + - For shared b + - Ensure: int2bv(translate(b)) = b + - but avoid bit-blasting by ensuring int2bv is injective (mod N) during final check + +Author: + + Nikolaj Bjorner (nbjorner) 2023-12-10 + +--*/ +#pragma once + +#include "ast/arith_decl_plugin.h" +#include "ast/bv_decl_plugin.h" +#include "solver/solver.h" +#include "sat/smt/sat_th.h" +#include "util/statistics.h" + +namespace euf { + class solver; +} + +namespace intblast { + + class solver : public euf::th_euf_solver { + euf::solver& ctx; + sat::solver& s; + ast_manager& m; + bv_util bv; + arith_util a; + scoped_ptr<::solver> m_solver; + obj_map m_new_funs; + expr_ref_vector m_translate, m_args; + ast_ref_vector m_pinned; + sat::literal_vector m_core; + ptr_vector m_bv2int, m_int2bv; + statistics m_stats; + bool m_is_plugin = true; // when the solver is used as a plugin, then do not translate below quantifiers. + + bool is_bv(sat::literal lit); + void translate(expr_ref_vector& es); + void sorted_subterms(expr_ref_vector& es, ptr_vector& sorted); + + + + bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); } + expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; } + void set_translated(expr* e, expr* r); + expr* arg(unsigned i) { return m_args.get(i); } + + expr* umod(expr* bv_expr, unsigned i); + expr* smod(expr* bv_expr, unsigned i); + rational bv_size(expr* bv_expr); + + void translate_expr(expr* e); + void translate_bv(app* e); + void translate_basic(app* e); + void translate_app(app* e); + void translate_quantifier(quantifier* q); + void translate_var(var* v); + + void ensure_translated(expr* e); + void internalize_bv(app* e); + + unsigned m_vars_qhead = 0, m_preds_qhead = 0; + ptr_vector m_vars, m_preds; + bool add_bound_axioms(); + bool add_predicate_axioms(); + + euf::theory_var mk_var(euf::enode* n) override; + + void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values); + void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values); + + public: + solver(euf::solver& ctx); + + ~solver() override {} + + lbool check_solver_state(); + + sat::literal_vector const& unsat_core(); + + void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; + + bool add_dep(euf::enode* n, top_sort& dep) override; + + std::ostream& display(std::ostream& out) const override; + + void collect_statistics(statistics& st) const override; + + bool unit_propagate() override; + + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override {} + + sat::check_result check() override; + + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return out; } + + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out; } + + euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } + + void internalize(expr* e) override; + + bool visited(expr* e) override; + + bool post_visit(expr* e, bool sign, bool root) override; + + bool visit(expr* e) override; + + sat::literal internalize(expr* e, bool, bool) override; + + void eq_internalized(euf::enode* n) override; + + rational get_value(expr* e) const; + + }; + +} diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 300bef1fbd2..b882c1abfac 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -54,6 +54,7 @@ def_module_params(module_name='smt', ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'), ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'), ('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'), + ('bv.solver', UINT, 1, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index 734a983fb59..8a3ddcf3729 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -28,6 +28,7 @@ void theory_bv_params::updt_params(params_ref const & _p) { m_bv_enable_int2bv2int = p.bv_enable_int2bv(); m_bv_delay = p.bv_delay(); m_bv_size_reduce = p.bv_size_reduce(); + m_bv_solver = p.bv_solver(); } #define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; @@ -42,4 +43,5 @@ void theory_bv_params::display(std::ostream & out) const { DISPLAY_PARAM(m_bv_enable_int2bv2int); DISPLAY_PARAM(m_bv_delay); DISPLAY_PARAM(m_bv_size_reduce); + DISPLAY_PARAM(m_bv_solver); } diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 523459f0913..97428c8ba28 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -36,6 +36,7 @@ struct theory_bv_params { bool m_bv_watch_diseq = false; bool m_bv_delay = true; bool m_bv_size_reduce = false; + unsigned m_bv_solver = 0; theory_bv_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index cfc1f06f2f9..b794a44b5c7 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -915,7 +915,7 @@ namespace smt { } SASSERT(val == l_undef || (val == l_false && d->m_constructor == nullptr)); d->m_recognizers[c_idx] = recognizer; - m_trail_stack.push(set_vector_idx_trail(d->m_recognizers, c_idx)); + m_trail_stack.push(set_vector_idx_trail(d->m_recognizers, c_idx)); if (val == l_false) { propagate_recognizer(v, recognizer); } diff --git a/src/util/trail.h b/src/util/trail.h index 1aa7e44418a..43e6982342c 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -219,12 +219,12 @@ class push_back_vector : public trail { } }; -template +template class set_vector_idx_trail : public trail { - ptr_vector & m_vector; + V & m_vector; unsigned m_idx; public: - set_vector_idx_trail(ptr_vector & v, unsigned idx): + set_vector_idx_trail(V & v, unsigned idx): m_vector(v), m_idx(idx) { }