diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 9a7bc1856..a10af72a6 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 ba2b4b4a7..8317b37c3 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<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());
}
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index fa359a9a7..25c4977e9 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 @@ public:
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 @@ public:
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 @@ public:
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 @@ public:
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 @@ public:
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 f725fefc5..30cfe4cdb 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 9126b97b7..89588ee0e 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -386,9 +386,31 @@ public:
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 @@ public:
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 @@ public:
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 99bf8941b..f640b3ed0 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 55156c53a..3ad64acfd 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 2a4e5058d..0eb8b6b37 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 96b3c13c4..a1b88bed1 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 7caccded6..e5d35a4f9 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 173ae28c8..f004422a6 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 3c6286317..decd49019 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 2be9b6b60..eff25bc4a 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 20ae599c2..022dbeaea 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<app> m_underspecified;
ptr_vector<expr> m_idiv_terms;
+ ptr_vector<app> m_band_terms;
vector<ptr_vector<api_bound> > 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 000000000..bb301808e
--- /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<arith::solver*>(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 000000000..b858ff896
--- /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 daecb7325..52c4ed953 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<enode>(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 943d0b324..f750f186d 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 b117ac1e3..073d164be 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 3ae4425fc..ff11b0749 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -21,6 +21,7 @@ Author:
#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<size_t>(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 db99ec512..7d2d01473 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<size_t>& 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 000000000..9d03d0ad0
--- /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<expr> 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<std::pair<sat::literal, sat::literal>> 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<expr, unsigned> 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<expr>& 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<expr> 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<sort> 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<euf::enode>& 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 000000000..d59dac935
--- /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<func_decl, func_decl*> m_new_funs;
+ expr_ref_vector m_translate, m_args;
+ ast_ref_vector m_pinned;
+ sat::literal_vector m_core;
+ ptr_vector<app> 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<expr>& 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<expr> 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<euf::enode>& 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 300bef1fb..b882c1abf 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 734a983fb..8a3ddcf37 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 523459f09..97428c8ba 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 cfc1f06f2..b794a44b5 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<enode>(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 1aa7e4441..43e698234 100644
--- a/src/util/trail.h
+++ b/src/util/trail.h
@@ -219,12 +219,12 @@ public:
}
};
-template<typename T>
+template<typename V>
class set_vector_idx_trail : public trail {
- ptr_vector<T> & m_vector;
+ V & m_vector;
unsigned m_idx;
public:
- set_vector_idx_trail(ptr_vector<T> & v, unsigned idx):
+ set_vector_idx_trail(V & v, unsigned idx):
m_vector(v),
m_idx(idx) {
}