mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

Add intblast solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-15 13:50:38 -08:00
parent 0520558fc0
commit 9293923b8a
28 changed files with 1621 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
RELEASE_NOTES.md
View file

@ -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
==============

31
src/ast/arith_decl_plugin.cpp
View file

@ -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());
}

65
src/ast/arith_decl_plugin.h
View file

@ -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();
}

5
src/ast/bv_decl_plugin.cpp
View file

@ -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);
}

29
src/ast/bv_decl_plugin.h
View file

@ -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); }

7
src/ast/euf/euf_bv_plugin.cpp
View file

@ -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;

2
src/math/dd/dd_pdd.cpp
View file

@ -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());

2
src/math/lp/lp_api.h
View file

@ -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);
}
};

15
src/sat/sat_solver.cpp
View file

@ -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) {
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);
@ -2555,6 +2559,7 @@ namespace sat {
SASSERT(lvl(c_var) < m_conflict_lvl);
}
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";);
@ -2811,6 +2816,7 @@ namespace sat {
if (not_l != null_literal) {
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++;

2
src/sat/smt/CMakeLists.txt
View file

@ -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

74
src/sat/smt/arith_axioms.cpp
View file

@ -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();

6
src/sat/smt/arith_internalize.cpp
View file

@ -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));

27
src/sat/smt/arith_solver.cpp
View file

@ -619,10 +619,10 @@ 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();
}
@ -641,6 +641,18 @@ namespace arith {
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)) {
@ -652,9 +664,8 @@ namespace arith {
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();

6
src/sat/smt/arith_solver.h
View file

@ -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);
};

145
src/sat/smt/arith_value.cpp Normal file
View file

@ -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
};

52
src/sat/smt/arith_value.h Normal file
View file

@ -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
};
};

2
src/sat/smt/dt_solver.cpp
View file

@ -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);

1
src/sat/smt/euf_internalize.cpp
View file

@ -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();

5
src/sat/smt/euf_model.cpp
View file

@ -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;

42
src/sat/smt/euf_solver.cpp
View file

@ -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);

3
src/sat/smt/euf_solver.h
View file

@ -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;

985
src/sat/smt/intblast_solver.cpp Normal file
View file

@ -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);
}
}

143
src/sat/smt/intblast_solver.h Normal file
View file

@ -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;
};
}

1
src/smt/params/smt_params_helper.pyg
View file

@ -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'),

2
src/smt/params/theory_bv_params.cpp
View file

@ -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);
}

1
src/smt/params/theory_bv_params.h
View file

@ -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);
}

2
src/smt/theory_datatype.cpp
View file

@ -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);
}

6
src/util/trail.h
View file

@ -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) {
}