mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

import master branch

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-16 16:56:09 -08:00
parent b1597fd499
commit 0353177fe0
5 changed files with 65 additions and 84 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/arith_decl_plugin.h
View file

@ -309,14 +309,13 @@ public:
bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); } 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) const { return is_app_of(n, arith_family_id, OP_ARITH_BAND); }
bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) { bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_BAND, sz, x, y); }
if (!is_band(n)) bool is_shl(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_SHL); }
return false; bool is_shl(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_SHL, sz, x, y); }
x = to_app(n)->get_arg(0); bool is_lshr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_LSHR); }
y = to_app(n)->get_arg(1); bool is_lshr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_LSHR, sz, x, y); }
sz = to_app(n)->get_parameter(0).get_int(); bool is_ashr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_ASHR); }
return true; bool is_ashr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_ASHR, sz, x, y); }
}
bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); } 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_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); }

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

@ -129,11 +129,7 @@ namespace lp_api {
st.update("arith-gomory-cuts", m_gomory_cuts); st.update("arith-gomory-cuts", m_gomory_cuts);
st.update("arith-assume-eqs", m_assume_eqs); st.update("arith-assume-eqs", m_assume_eqs);
st.update("arith-branch", m_branch); st.update("arith-branch", m_branch);
<<<<<<< HEAD
st.update("arith-bv-axioms", m_bv_axioms); st.update("arith-bv-axioms", m_bv_axioms);
=======
st.update("arith-band-axioms", m_band_axioms);
>>>>>>> c72780d9b (b-and, stats, reinsert variable to heap, debugging)
} }
}; };

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

@ -410,13 +410,8 @@ namespace arith {
bool check_delayed_eqs(); bool check_delayed_eqs();
lbool check_lia(); lbool check_lia();
lbool check_nla(); lbool check_nla();
<<<<<<< HEAD
bool check_bv_terms(); bool check_bv_terms();
bool check_bv_term(app* n); bool check_bv_term(app* n);
=======
bool check_band_terms();
bool check_band_term(app* n);
>>>>>>> b72575148 (axioms for b-and)
void add_lemmas(); void add_lemmas();
void propagate_nla(); void propagate_nla();
void add_equality(lpvar v, rational const& k, lp::explanation const& exp); void add_equality(lpvar v, rational const& k, lp::explanation const& exp);

91
src/sat/smt/intblast_solver.cpp
View file

@ -104,10 +104,10 @@ namespace intblast {
ctx.push(push_back_vector(m_preds)); ctx.push(push_back_vector(m_preds));
} }
void solver::set_translated(expr* e, expr* r) { void solver::set_translated(expr* e, expr* r) {
SASSERT(r); SASSERT(r);
SASSERT(!is_translated(e)); SASSERT(!is_translated(e));
m_translate.setx(e->get_id(), r); m_translate.setx(e->get_id(), r);
ctx.push(set_vector_idx_trail(m_translate, e->get_id())); ctx.push(set_vector_idx_trail(m_translate, e->get_id()));
} }
@ -148,7 +148,7 @@ namespace intblast {
auto a = expr2literal(e); auto a = expr2literal(e);
auto b = mk_literal(r); auto b = mk_literal(r);
ctx.mark_relevant(b); ctx.mark_relevant(b);
// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; // verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
add_equiv(a, b); add_equiv(a, b);
} }
return true; return true;
@ -157,7 +157,7 @@ namespace intblast {
bool solver::unit_propagate() { bool solver::unit_propagate() {
return add_bound_axioms() || add_predicate_axioms(); return add_bound_axioms() || add_predicate_axioms();
} }
void solver::ensure_translated(expr* e) { void solver::ensure_translated(expr* e) {
if (m_translate.get(e->get_id(), nullptr)) if (m_translate.get(e->get_id(), nullptr))
return; return;
@ -179,7 +179,7 @@ namespace intblast {
} }
} }
std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
for (expr* e : todo) for (expr* e : todo)
translate_expr(e); translate_expr(e);
} }
@ -305,6 +305,28 @@ namespace intblast {
sorted.push_back(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)) { else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e); quantifier* q = to_quantifier(e);
@ -325,6 +347,7 @@ namespace intblast {
for (expr* e : todo) for (expr* e : todo)
translate_expr(e); translate_expr(e);
TRACE("bv", TRACE("bv",
for (expr* e : es) for (expr* e : es)
tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated(e), m) << "\n"; tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated(e), m) << "\n";
@ -334,7 +357,7 @@ namespace intblast {
es[i] = translated(es.get(i)); es[i] = translated(es.get(i));
} }
sat::check_result solver::check() { sat::check_result solver::check() {
// ensure that bv2int is injective // ensure that bv2int is injective
for (auto e : m_bv2int) { for (auto e : m_bv2int) {
euf::enode* n = expr2enode(e); euf::enode* n = expr2enode(e);
@ -346,10 +369,10 @@ namespace intblast {
continue; continue;
if (sib->get_arg(0)->get_root() == r1) if (sib->get_arg(0)->get_root() == r1)
continue; continue;
auto a = eq_internalize(n, sib); auto a = eq_internalize(n, sib);
auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
ctx.mark_relevant(a); ctx.mark_relevant(a);
ctx.mark_relevant(b); ctx.mark_relevant(b);
add_clause(~a, b, nullptr); add_clause(~a, b, nullptr);
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
} }
@ -367,13 +390,13 @@ namespace intblast {
auto nBv2int = ctx.get_enode(bv2int); auto nBv2int = ctx.get_enode(bv2int);
auto nxModN = ctx.get_enode(xModN); auto nxModN = ctx.get_enode(xModN);
if (nBv2int->get_root() != nxModN->get_root()) { if (nBv2int->get_root() != nxModN->get_root()) {
auto a = eq_internalize(nBv2int, nxModN); auto a = eq_internalize(nBv2int, nxModN);
ctx.mark_relevant(a); ctx.mark_relevant(a);
add_unit(a); add_unit(a);
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
} }
} }
return sat::check_result::CR_DONE; return sat::check_result::CR_DONE;
} }
expr* solver::umod(expr* bv_expr, unsigned i) { expr* solver::umod(expr* bv_expr, unsigned i) {
@ -481,8 +504,8 @@ namespace intblast {
m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i)); m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i));
if (has_bv_sort) if (has_bv_sort)
m_vars.push_back(e); m_vars.push_back(e);
if (m_is_plugin) { if (m_is_plugin) {
expr* r = m.mk_app(f, m_args); expr* r = m.mk_app(f, m_args);
if (has_bv_sort) { if (has_bv_sort) {
@ -503,7 +526,7 @@ namespace intblast {
f = g; f = g;
m_pinned.push_back(f); m_pinned.push_back(f);
} }
set_translated(e, m.mk_app(f, m_args)); set_translated(e, m.mk_app(f, m_args));
} }
void solver::translate_bv(app* e) { void solver::translate_bv(app* e) {
@ -535,7 +558,7 @@ namespace intblast {
r = a.mk_add(hi, lo); r = a.mk_add(hi, lo);
} }
return r; return r;
}; };
expr* bv_expr = e; expr* bv_expr = e;
expr* r = nullptr; expr* r = nullptr;
@ -682,7 +705,6 @@ namespace intblast {
} }
} }
break; break;
}
case OP_BOR: { case OP_BOR: {
// p | q := (p + q) - band(p, q) // p | q := (p + q) - band(p, q)
IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
@ -744,11 +766,11 @@ namespace intblast {
r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(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; break;
case OP_BSMOD_I: case OP_BSMOD_I:
case OP_BSMOD: { case OP_BSMOD: {
expr* x = umod(e, 0), * y = umod(e, 1); expr* x = umod(e, 0), *y = umod(e, 1);
rational N = bv_size(e); rational N = bv_size(e);
expr* signx = a.mk_ge(x, a.mk_int(N / 2)); expr* signx = a.mk_ge(x, a.mk_int(N/2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2)); expr* signy = a.mk_ge(y, a.mk_int(N/2));
expr* u = a.mk_mod(x, y); expr* u = a.mk_mod(x, y);
// u = 0 -> 0 // u = 0 -> 0
// y = 0 -> x // y = 0 -> x
@ -756,14 +778,14 @@ namespace intblast {
// x < 0, y >= 0 -> y - u // x < 0, y >= 0 -> y - u
// x >= 0, y < 0 -> y + u // x >= 0, y < 0 -> y + u
// x >= 0, y >= 0 -> u // x >= 0, y >= 0 -> u
r = a.mk_uminus(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(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(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_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(u, a.mk_int(0)), a.mk_int(0), r);
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
break; break;
} }
case OP_BSDIV_I: case OP_BSDIV_I:
case OP_BSDIV: { case OP_BSDIV: {
// d = udiv(abs(x), abs(y)) // d = udiv(abs(x), abs(y))
@ -799,7 +821,7 @@ namespace intblast {
d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); 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 = a.mk_sub(x, a.mk_mul(d, y));
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
break; break;
} }
case OP_ROTATE_LEFT: { case OP_ROTATE_LEFT: {
auto n = e->get_parameter(0).get_int(); auto n = e->get_parameter(0).get_int();
@ -812,11 +834,11 @@ namespace intblast {
r = rotate_left(sz - n); r = rotate_left(sz - n);
break; break;
} }
case OP_EXT_ROTATE_LEFT: { case OP_EXT_ROTATE_LEFT: {
unsigned sz = bv.get_bv_size(e); unsigned sz = bv.get_bv_size(e);
expr* y = umod(e, 1); expr* y = umod(e, 1);
r = a.mk_int(0); r = a.mk_int(0);
for (unsigned i = 0; i < sz; ++i) for (unsigned i = 0; i < sz; ++i)
r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r); r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r);
break; break;
} }
@ -824,7 +846,7 @@ namespace intblast {
unsigned sz = bv.get_bv_size(e); unsigned sz = bv.get_bv_size(e);
expr* y = umod(e, 1); expr* y = umod(e, 1);
r = a.mk_int(0); r = a.mk_int(0);
for (unsigned i = 0; i < sz; ++i) for (unsigned i = 0; i < sz; ++i)
r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r); r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r);
break; break;
} }
@ -837,7 +859,7 @@ namespace intblast {
for (unsigned i = 1; i < n; ++i) for (unsigned i = 1; i < n; ++i)
r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0; r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0;
break; break;
} }
case OP_BREDOR: { case OP_BREDOR: {
r = umod(e->get_arg(0), 0); r = umod(e->get_arg(0), 0);
r = m.mk_not(m.mk_eq(r, a.mk_int(0))); r = m.mk_not(m.mk_eq(r, a.mk_int(0)));
@ -855,6 +877,7 @@ namespace intblast {
} }
set_translated(e, r); set_translated(e, r);
} }
void solver::translate_basic(app* e) { void solver::translate_basic(app* e) {
if (m.is_eq(e)) { if (m.is_eq(e)) {
bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); }); bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); });
@ -896,7 +919,7 @@ namespace intblast {
} }
bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
if (!is_app(n->get_expr())) if (!is_app(n->get_expr()))
return false; return false;
app* e = to_app(n->get_expr()); app* e = to_app(n->get_expr());
if (n->num_args() == 0) { if (n->num_args() == 0) {
@ -915,7 +938,7 @@ namespace intblast {
void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) { void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) {
expr* e = n->get_expr(); expr* e = n->get_expr();
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
if (bv.is_numeral(e)) { if (bv.is_numeral(e)) {
values.setx(n->get_root_id(), e); values.setx(n->get_root_id(), e);
return; return;
@ -955,8 +978,8 @@ namespace intblast {
arith::arith_value av(ctx); arith::arith_value av(ctx);
rational r; rational r;
VERIFY(av.get_value(b2i->get_expr(), 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())); value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr()));
verbose_stream() << ctx.bpp(n) << " := " << value << "\n";
} }
values.set(n->get_root_id(), value); values.set(n->get_root_id(), value);
TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");

34
src/sat/smt/intblast_solver.h
View file

@ -66,35 +66,6 @@ namespace intblast {
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);
bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); } 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; } 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); void set_translated(expr* e, expr* r);
@ -165,10 +136,7 @@ namespace intblast {
void eq_internalized(euf::enode* n) override; void eq_internalized(euf::enode* n) override;
sat::literal_vector const& unsat_core(); rational get_value(expr* e) const;
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
}; };