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

additional bit-vector propagators (#4695)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-18 12:38:29 -07:00 committed by GitHub
parent 549753845e
commit 8691ef1d4d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
17 changed files with 423 additions and 121 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/ast/euf/euf_egraph.cpp
View file

@ -573,30 +573,30 @@ namespace euf {
std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
out << n->get_expr_id() << " := ";
if (!n->is_root())
out << "[" << n->get_root()->get_expr_id() << "] ";
expr* f = n->get_expr();
if (is_app(f))
out << mk_bounded_pp(f, m, 1);
out << mk_bounded_pp(f, m, 1) << " ";
else if (is_quantifier(f))
out << "q:" << f->get_id();
out << "q:" << f->get_id() << " ";
else
out << "v:" << f->get_id();
out << "\n";
out << "v:" << f->get_id() << " ";
if (!n->is_root())
out << "[r " << n->get_root()->get_expr_id() << "] ";
if (!n->m_parents.empty()) {
out << " parents ";
out << "[p";
for (enode* p : enode_parents(n))
out << p->get_expr_id() << " ";
out << "\n";
out << " " << p->get_expr_id();
out << "] ";
}
if (n->has_th_vars()) {
out << " theories ";
out << "[t";
for (auto v : enode_th_vars(n))
out << v.get_id() << ":" << v.get_var() << " ";
out << "\n";
out << " " << v.get_id() << ":" << v.get_var();
out << "] ";
}
if (n->m_target && m_display_justification)
n->m_justification.display(out << " = " << n->m_target->get_expr_id() << " j: ", m_display_justification) << "\n";
n->m_justification.display(out << "[j " << n->m_target->get_expr_id() << " ", m_display_justification) << "] ";
out << "\n";
return out;
}

1
src/sat/sat_probing.cpp
View file

@ -237,6 +237,7 @@ namespace sat {
if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit)
m_cached_bins.finalize();
flet<bool> _probing(m_active, true);
report rpt(*this);
bool r = true;
m_counter = 0;

3
src/sat/sat_probing.h
View file

@ -31,7 +31,7 @@ namespace sat {
unsigned m_stopped_at; // where did it stop
literal_set m_assigned; // literals assigned in the first branch
literal_vector m_to_assert;
bool m_active { false };
// counters
int m_counter; // track cost
@ -78,6 +78,7 @@ namespace sat {
void collect_statistics(statistics & st) const;
void reset_statistics();
bool active() const { return m_active; }
// return the literals implied by l.
// return 0, if the cache is not available

21
src/sat/sat_solver.cpp
View file

@ -1934,12 +1934,24 @@ namespace sat {
}
log_stats();
m_simplifications++;
IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";);
TRACE("sat", tout << "simplify\n";);
pop(scope_lvl());
struct report {
solver& s;
stopwatch m_watch;
report(solver& s):s(s) {
m_watch.start();
s.log_stats();
IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << s.m_simplifications << ")\n";);
}
~report() {
m_watch.stop();
s.log_stats();
}
};
report _rprt(*this);
SASSERT(at_base_lvl());
m_cleaner(m_config.m_force_cleanup);
@ -3943,9 +3955,8 @@ namespace sat {
break;
}
case justification::EXT_JUSTIFICATION:
if (m_ext) {
m_ext->display_justification(out << " ", js.get_ext_justification_idx());
}
if (m_ext)
m_ext->display_justification(out, js.get_ext_justification_idx());
break;
default:
break;

1
src/sat/sat_solver.h
View file

@ -662,6 +662,7 @@ namespace sat {
public:
void set_should_simplify() { m_next_simplify = m_conflicts_since_init; }
bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit; }
bool is_probing() const { return m_probing.active(); }
public:
void user_push() override;

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

@ -110,7 +110,7 @@ namespace bv {
}
if (glue < max_glue)
v.m_glue = 2*glue <= sz ? 0 : glue;
v.m_glue = (sz > 6 && 2*glue <= sz) ? 0 : glue;
}
void ackerman::remove(vv* p) {

72
src/sat/smt/bv_internalize.cpp
View file

@ -42,6 +42,16 @@ namespace bv {
}
};
class solver::add_eq_occurs_trail : public trail<euf::solver> {
solver::bit_atom* m_atom;
public:
add_eq_occurs_trail(solver::bit_atom* a) :m_atom(a) {}
void undo(euf::solver& euf) override {
SASSERT(m_atom->m_eqs);
m_atom->m_eqs = m_atom->m_eqs->m_next;
}
};
class solver::mk_atom_trail : public trail<euf::solver> {
solver& th;
sat::bool_var m_var;
@ -242,10 +252,15 @@ namespace bv {
}
solver::bit_atom* solver::mk_bit_atom(sat::bool_var bv) {
bit_atom* b = new (get_region()) bit_atom();
insert_bv2a(bv, b);
ctx.push(mk_atom_trail(bv, *this));
return b;
atom* a = get_bv2a(bv);
if (a)
return a->is_bit() ? &a->to_bit() : nullptr;
else {
bit_atom* b = new (get_region()) bit_atom();
insert_bv2a(bv, b);
ctx.push(mk_atom_trail(bv, *this));
return b;
}
}
void solver::set_bit_eh(theory_var v, literal l, unsigned idx) {
@ -253,20 +268,14 @@ namespace bv {
if (s().value(l) != l_undef && s().lvl(l) == 0)
register_true_false_bit(v, idx);
else {
atom* a = get_bv2a(l.var());
if (a && !a->is_bit())
;
else if (a) {
bit_atom* b = &a->to_bit();
find_new_diseq_axioms(*b, v, idx);
ctx.push(add_var_pos_trail(b));
bit_atom* b = mk_bit_atom(l.var());
if (b) {
if (b->m_occs)
find_new_diseq_axioms(*b, v, idx);
if (!b->is_fresh())
ctx.push(add_var_pos_trail(b));
b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
}
else {
bit_atom* b = mk_bit_atom(l.var());
SASSERT(!b->m_occs);
b->m_occs = new (get_region()) var_pos_occ(v, idx);
}
}
}
@ -570,12 +579,34 @@ namespace bv {
}
}
void solver::eq_internalized(euf::enode* n) {
SASSERT(m.is_eq(n->get_expr()));
theory_var v1 = n->get_arg(0)->get_th_var(get_id());
theory_var v2 = n->get_arg(1)->get_th_var(get_id());
SASSERT(v1 != euf::null_theory_var);
SASSERT(v2 != euf::null_theory_var);
unsigned sz = m_bits[v1].size();
for (unsigned i = 0; i < sz; ++i) {
eq_internalized(m_bits[v1][i].var(), i, v1, v2, n);
eq_internalized(m_bits[v2][i].var(), i, v2, v1, n);
}
}
void solver::eq_internalized(sat::bool_var b, unsigned idx, theory_var v1, theory_var v2, euf::enode* n) {
bit_atom* a = mk_bit_atom(b);
if (a) {
if (!a->is_fresh())
ctx.push(add_eq_occurs_trail(a));
a->m_eqs = new (get_region()) eq_occurs(idx, v1, v2, n, a->m_eqs);
}
}
void solver::assert_ackerman(theory_var v1, theory_var v2) {
if (v1 == v2)
return;
if (v1 > v2)
std::swap(v1, v2);
flet<bool> _red(m_is_redundant, true);
flet<bool> _red(m_is_redundant, true);
++m_stats.m_ackerman;
expr* o1 = var2expr(v1);
expr* o2 = var2expr(v2);
@ -584,6 +615,7 @@ namespace bv {
unsigned sz = m_bits[v1].size();
TRACE("bv", tout << "ackerman-eq: " << s().scope_lvl() << " " << oe << "\n";);
literal_vector eqs;
eqs.push_back(oeq);
for (unsigned i = 0; i < sz; ++i) {
literal l1 = m_bits[v1][i];
literal l2 = m_bits[v2][i];
@ -592,14 +624,10 @@ namespace bv {
e2 = bv.mk_bit2bool(o2, i);
expr_ref e = mk_eq(e1, e2);
literal eq = ctx.internalize(e, false, false, m_is_redundant);
add_clause(l1, ~l2, ~eq);
add_clause(~l1, l2, ~eq);
add_clause(l1, l2, eq);
add_clause(~l1, ~l2, eq);
add_clause(eq, ~oeq);
eqs.push_back(~eq);
}
eqs.push_back(oeq);
TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);
s().add_clause(eqs.size(), eqs.c_ptr(), sat::status::th(m_is_redundant, get_id()));
}
}

22
src/sat/smt/bv_invariant.cpp
View file

@ -16,6 +16,7 @@ Author:
--*/
#include "sat/smt/bv_solver.h"
#include "sat/smt/euf_solver.h"
namespace bv {
@ -32,6 +33,27 @@ namespace bv {
}
}
void solver::check_missing_propagation() const {
for (euf::enode* n : ctx.get_egraph().nodes()) {
expr* e = n->get_expr(), *a = nullptr, *b = nullptr;
if (m.is_eq(e, a, b) && bv.is_bv(a) && s().value(expr2literal(e)) == l_undef) {
theory_var v1 = n->get_arg(0)->get_th_var(get_id());
theory_var v2 = n->get_arg(1)->get_th_var(get_id());
SASSERT(v1 != euf::null_theory_var);
SASSERT(v2 != euf::null_theory_var);
unsigned sz = m_bits[v1].size();
for (unsigned i = 0; i < sz; ++i) {
lbool val1 = s().value(m_bits[v1][i]);
lbool val2 = s().value(m_bits[v2][i]);
if (val1 != l_undef && val2 != l_undef && val1 != val2) {
IF_VERBOSE(0, verbose_stream() << "missing " << mk_bounded_pp(e, m) << "\n");
break;
}
}
}
}
}
/**
\brief Check whether m_zero_one_bits is an accurate summary of the bits in the
equivalence class rooted by v.

217
src/sat/smt/bv_solver.cpp
View file

@ -69,7 +69,7 @@ namespace bv {
m_fixed_var_table.find(key, v2) &&
v2 < static_cast<int>(get_num_vars()) &&
is_bv(v2) &&
get_bv_size(v2) == sz &&
m_bits[v2].size() == sz &&
get_fixed_value(v2, val2) && val1 == val2;
if (!is_current)
@ -79,7 +79,7 @@ namespace bv {
TRACE("bv", tout << "detected equality: v" << v1 << " = v" << v2 << "\n" << pp(v1) << pp(v2););
m_stats.m_num_th2core_eq++;
add_fixed_eq(v1, v2);
ctx.propagate(var2enode(v1), var2enode(v2), mk_bit2bv_justification(v1, v2));
ctx.propagate(var2enode(v1), var2enode(v2), mk_bit2eq_justification(v1, v2));
}
}
@ -137,7 +137,7 @@ namespace bv {
for (auto vp : a) {
theory_var v2 = vp.first;
unsigned idx2 = vp.second;
if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v))
if (idx == idx2 && m_bits[v2].size() == m_bits[v].size() && m_bits[v2][idx2] == l )
mk_new_diseq_axiom(v, v2, idx);
}
}
@ -149,8 +149,6 @@ namespace bv {
if (!get_config().m_bv_eq_axioms)
return;
// TBD: disabled until new literal creation is supported
return;
SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2););
m_stats.m_num_diseq_static++;
@ -195,7 +193,7 @@ namespace bv {
void solver::new_eq_eh(euf::th_eq const& eq) {
force_push();
TRACE("bv", tout << "new eq " << eq.v1() << " == " << eq.v2() << "\n";);
TRACE("bv", tout << "new eq " << mk_bounded_pp(var2expr(eq.v1()), m) << " == " << mk_bounded_pp(var2expr(eq.v2()), m) << "\n";);
if (is_bv(eq.v1()))
m_find.merge(eq.v1(), eq.v2());
}
@ -204,11 +202,13 @@ namespace bv {
theory_var v1 = ne.v1(), v2 = ne.v2();
if (!is_bv(v1))
return;
if (!get_config().m_bv_eq_axioms)
if (s().is_probing())
return;
TRACE("bv", tout << "diff: " << v1 << " != " << v2 << "\n";);
TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
unsigned sz = m_bits[v1].size();
unsigned num_undef = 0;
int undef_idx = 0;
for (unsigned i = 0; i < sz; ++i) {
sat::literal a = m_bits[v1][i];
sat::literal b = m_bits[v2][i];
@ -218,12 +218,41 @@ namespace bv {
auto vb = s().value(b);
if (va != l_undef && vb != l_undef && va != vb)
return;
if (va == l_undef) {
++num_undef;
undef_idx = i + 1;
}
if (vb == l_undef) {
++num_undef;
undef_idx = -static_cast<int>(i + 1);
}
if (num_undef > 1 && get_config().m_bv_eq_axioms)
return;
}
if (s().at_search_lvl()) {
if (num_undef == 0)
return;
else if (num_undef == 1) {
if (undef_idx < 0) {
undef_idx = -undef_idx;
std::swap(v1, v2);
}
undef_idx--;
sat::literal consequent = m_bits[v1][undef_idx];
sat::literal b = m_bits[v2][undef_idx];
sat::literal antecedent = ~expr2literal(ne.eq());
SASSERT(s().value(antecedent) == l_true);
SASSERT(s().value(consequent) == l_undef);
SASSERT(s().value(b) != l_undef);
if (s().value(b) == l_true)
consequent.neg();
++m_stats.m_num_nbit2core;
s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent));
}
else if (s().at_search_lvl()) {
force_push();
assert_ackerman(v1, v2);
}
else
else
m_ackerman.used_diseq_eh(v1, v2);
}
@ -236,12 +265,41 @@ namespace bv {
auto& c = bv_justification::from_index(idx);
TRACE("bv", display_constraint(tout, idx););
switch (c.m_kind) {
case bv_justification::kind_t::bv2bit:
case bv_justification::kind_t::eq2bit:
SASSERT(s().value(c.m_antecedent) == l_true);
r.push_back(c.m_antecedent);
ctx.add_antecedent(var2enode(c.m_v1), var2enode(c.m_v2));
break;
case bv_justification::kind_t::bit2bv:
case bv_justification::kind_t::ne2bit: {
r.push_back(c.m_antecedent);
SASSERT(s().value(c.m_antecedent) == l_true);
SASSERT(c.m_consequent == l);
unsigned idx = c.m_idx;
for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) {
sat::literal a = m_bits[c.m_v1][i];
sat::literal b = m_bits[c.m_v2][i];
SASSERT(a == b || s().value(a) != l_undef);
SASSERT(i == idx || s().value(a) == s().value(b));
if (a == b)
continue;
if (i == idx) {
if (s().value(b) == l_false)
b.neg();
r.push_back(b);
continue;
}
if (s().value(a) == l_false) {
a.neg();
b.neg();
}
r.push_back(a);
r.push_back(b);
}
break;
}
case bv_justification::kind_t::bit2eq:
SASSERT(m_bits[c.m_v1].size() == m_bits[c.m_v2].size());
for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) {
sat::literal a = m_bits[c.m_v1][i];
@ -258,6 +316,25 @@ namespace bv {
r.push_back(b);
}
break;
case bv_justification::kind_t::bit2ne: {
SASSERT(c.m_consequent.sign());
sat::bool_var v = c.m_consequent.var();
expr* eq = bool_var2expr(v);
SASSERT(m.is_eq(eq));
euf::enode* n = expr2enode(eq);
theory_var v1 = n->get_arg(0)->get_th_var(get_id());
theory_var v2 = n->get_arg(1)->get_th_var(get_id());
sat::literal a = m_bits[v1][c.m_idx];
sat::literal b = m_bits[v2][c.m_idx];
lbool val_a = s().value(a);
lbool val_b = s().value(b);
SASSERT(val_a != l_undef && val_b != l_undef && val_a != val_b);
if (val_a == l_false) a.neg();
if (val_b == l_false) b.neg();
r.push_back(a);
r.push_back(b);
break;
}
}
if (!probing && ctx.use_drat())
log_drat(c);
@ -274,42 +351,41 @@ namespace bv {
ctx.get_drat().def_add_arg(e2->get_id());
ctx.get_drat().def_end();
ctx.get_drat().bool_def(leq.var(), eq->get_id());
sat::literal_vector lits;
auto add_bit = [&](sat::literal lit) {
if (s().value(lit) == l_true)
lit.neg();
lits.push_back(lit);
};
switch (c.m_kind) {
case bv_justification::kind_t::bv2bit:
case bv_justification::kind_t::eq2bit:
lits.push_back(~leq);
lits.push_back(~c.m_antecedent);
lits.push_back(c.m_consequent);
break;
case bv_justification::kind_t::bit2bv:
case bv_justification::kind_t::ne2bit:
get_antecedents(c.m_consequent, c.to_index(), lits, true);
lits.push_back(c.m_consequent);
break;
case bv_justification::kind_t::bit2eq:
get_antecedents(leq, c.to_index(), lits, true);
for (auto& lit : lits)
lit.neg();
lits.push_back(leq);
for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) {
sat::literal a = m_bits[c.m_v1][i];
sat::literal b = m_bits[c.m_v2][i];
if (a != b) {
add_bit(a);
add_bit(b);
}
}
break;
case bv_justification::kind_t::bit2ne:
get_antecedents(c.m_consequent, c.to_index(), lits, true);
for (auto& lit : lits)
lit.neg();
lits.push_back(c.m_consequent);
break;
}
ctx.get_drat().add(lits, status());
ctx.get_drat().log_gc_var(leq.var());
ctx.get_drat().log_gc_var(leq.var()); // TBD, a proper way would be to delete the lemma after use.
}
void solver::asserted(literal l) {
atom* a = get_bv2a(l.var());
TRACE("bv", tout << "asserted: " << l << "\n";);
if (a && a->is_bit()) {
force_push();
for (auto vp : a->to_bit())
m_prop_queue.push_back(vp);
m_prop_queue.push_back(propagation_item(&a->to_bit()));
}
}
@ -318,11 +394,34 @@ namespace bv {
return false;
force_push();
ctx.push(value_trail<euf::solver, unsigned>(m_prop_queue_head));
for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head)
propagate_bits(m_prop_queue[m_prop_queue_head]);
for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
auto const p = m_prop_queue[m_prop_queue_head];
if (p.m_atom) {
for (auto vp : *p.m_atom)
propagate_bits(vp);
for (auto const& eq : p.m_atom->eqs())
propagate_eq_occurs(eq);
}
else
propagate_bits(p.m_vp);
}
// check_missing_propagation();
return true;
}
void solver::propagate_eq_occurs(eq_occurs const& occ) {
auto lit = expr2literal(occ.m_node->get_expr());
if (s().value(lit) != l_undef)
return;
lbool val1 = s().value(m_bits[occ.m_v1][occ.m_idx]);
lbool val2 = s().value(m_bits[occ.m_v2][occ.m_idx]);
SASSERT(val1 != l_undef);
if (val1 != val2 && val2 != l_undef) {
++m_stats.m_num_th2core_diseq;
s().assign(~lit, mk_bit2ne_justification(occ.m_idx, ~lit));
}
}
void solver::propagate_bits(var_pos entry) {
theory_var v1 = entry.first;
unsigned idx = entry.second;
@ -453,11 +552,25 @@ namespace bv {
std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
auto& c = bv_justification::from_index(idx);
theory_var v1 = c.m_v1;
theory_var v2 = c.m_v2;
unsigned cidx = c.m_idx;
switch (c.m_kind) {
case bv_justification::kind_t::bv2bit:
return out << c.m_consequent << " <= " << c.m_antecedent << " v" << c.m_v1 << " == v" << c.m_v2 << "\n";
case bv_justification::kind_t::bit2bv:
return out << m_bits[c.m_v1] << " == " << m_bits[c.m_v2] << " => v" << c.m_v1 << " == v" << c.m_v2 << "\n";
case bv_justification::kind_t::eq2bit:
return out << "bv <- " << c.m_antecedent << " v" << v1 << " == v" << v2;
case bv_justification::kind_t::bit2eq:
return out << "bv " << m_bits[v1] << " == " << m_bits[v2] << " -> v" << v1 << " == v" << v2;
case bv_justification::kind_t::bit2ne: {
expr* e = bool_var2expr(c.m_consequent.var());
SASSERT(m.is_eq(e));
euf::enode* n = expr2enode(e);
v1 = n->get_arg(0)->get_th_var(get_id());
v2 = n->get_arg(1)->get_th_var(get_id());
return out << "bv <- v" << v1 << "[" << cidx << "] != v" << v2 << "[" << cidx << "] " << m_bits[v1][cidx] << " != " << m_bits[v2][cidx];
}
case bv_justification::kind_t::ne2bit:
return out << "bv <- " << m_bits[v1] << " != " << m_bits[v2] << " @" << cidx;
break;
default:
UNREACHABLE();
break;
@ -469,8 +582,10 @@ namespace bv {
st.update("bv conflicts", m_stats.m_num_conflicts);
st.update("bv diseqs", m_stats.m_num_diseq_static);
st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
st.update("bv bit2core", m_stats.m_num_bit2core);
st.update("bv->core eq", m_stats.m_num_th2core_eq);
st.update("bv eq2bit", m_stats.m_num_bit2core);
st.update("bv ne2bit", m_stats.m_num_nbit2core);
st.update("bv bit2eq", m_stats.m_num_th2core_eq);
st.update("bv bit2ne", m_stats.m_num_th2core_diseq);
st.update("bv ackerman", m_stats.m_ackerman);
}
@ -575,26 +690,40 @@ namespace bv {
}
}
sat::justification solver::mk_bv2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) {
sat::justification solver::mk_eq2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) {
void* mem = get_region().allocate(bv_justification::get_obj_size());
sat::constraint_base::initialize(mem, this);
auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2, c, a);
return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
}
sat::ext_justification_idx solver::mk_bit2bv_justification(theory_var v1, theory_var v2) {
sat::ext_justification_idx solver::mk_bit2eq_justification(theory_var v1, theory_var v2) {
void* mem = get_region().allocate(bv_justification::get_obj_size());
sat::constraint_base::initialize(mem, this);
auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2);
return constraint->to_index();
}
sat::justification solver::mk_bit2ne_justification(unsigned idx, sat::literal c) {
void* mem = get_region().allocate(bv_justification::get_obj_size());
sat::constraint_base::initialize(mem, this);
auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(idx, c);
return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
}
sat::justification solver::mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a) {
void* mem = get_region().allocate(bv_justification::get_obj_size());
sat::constraint_base::initialize(mem, this);
auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(idx, v1, v2, c, a);
return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
}
void solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
m_stats.m_num_bit2core++;
SASSERT(ctx.s().value(antecedent) == l_true);
SASSERT(m_bits[v2][idx].var() == consequent.var());
SASSERT(consequent.var() != antecedent.var());
s().assign(consequent, mk_bv2bit_justification(v1, v2, consequent, antecedent));
s().assign(consequent, mk_eq2bit_justification(v1, v2, consequent, antecedent));
if (s().value(consequent) == l_false) {
m_stats.m_num_conflicts++;
SASSERT(s().inconsistent());
@ -615,7 +744,7 @@ namespace bv {
if (a && a->is_bit())
for (auto curr : a->to_bit())
if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx)
m_prop_queue.push_back(curr);
m_prop_queue.push_back(propagation_item(curr));
}
}

84
src/sat/smt/bv_solver.h
View file

@ -43,23 +43,29 @@ namespace bv {
friend class ackerman;
struct stats {
unsigned m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
unsigned m_num_diseq_static, m_num_diseq_dynamic, m_num_conflicts;
unsigned m_num_bit2core, m_num_th2core_eq, m_num_th2core_diseq, m_num_nbit2core;
unsigned m_ackerman;
void reset() { memset(this, 0, sizeof(stats)); }
stats() { reset(); }
};
struct bv_justification {
enum kind_t { bv2bit, bit2bv };
enum kind_t { eq2bit, ne2bit, bit2eq, bit2ne };
kind_t m_kind;
theory_var m_v1;
theory_var m_v2;
theory_var m_v1{ euf::null_theory_var };
theory_var m_v2 { euf::null_theory_var };
unsigned m_idx{ UINT_MAX };
sat::literal m_consequent;
sat::literal m_antecedent;
bv_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
m_kind(kind_t::bv2bit), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
m_kind(bv_justification::kind_t::eq2bit), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
bv_justification(theory_var v1, theory_var v2):
m_kind(kind_t::bit2bv), m_v1(v1), m_v2(v2) {}
m_kind(bv_justification::kind_t::bit2eq), m_v1(v1), m_v2(v2) {}
bv_justification(unsigned idx, sat::literal c) :
m_kind(bv_justification::kind_t::bit2ne), m_idx(idx), m_consequent(c) {}
bv_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
m_kind(bv_justification::kind_t::ne2bit), m_idx(idx), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
sat::ext_constraint_idx to_index() const {
return sat::constraint_base::mem2base(this);
}
@ -69,8 +75,10 @@ namespace bv {
static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(bv_justification)); }
};
sat::justification mk_bv2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a);
sat::ext_justification_idx mk_bit2bv_justification(theory_var v1, theory_var v2);
sat::justification mk_eq2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a);
sat::ext_justification_idx mk_bit2eq_justification(theory_var v1, theory_var v2);
sat::justification mk_bit2ne_justification(unsigned idx, sat::literal c);
sat::justification mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a);
void log_drat(bv_justification const& c);
@ -125,13 +133,46 @@ namespace bv {
bool operator!=(var_pos_it const& other) const { return !(*this == other); }
};
struct eq_occurs {
unsigned m_idx;
theory_var m_v1;
theory_var m_v2;
euf::enode* m_node;
eq_occurs* m_next;
eq_occurs(unsigned idx, theory_var v1, theory_var v2, euf::enode* n, eq_occurs* next = nullptr):
m_idx(idx), m_v1(v1), m_v2(v2), m_node(n), m_next(next) {}
};
class eq_occurs_it {
eq_occurs* m_first;
public:
eq_occurs_it(eq_occurs* c) : m_first(c) {}
eq_occurs operator*() { return *m_first; }
eq_occurs_it& operator++() { m_first = m_first->m_next; return *this; }
eq_occurs_it operator++(int) { eq_occurs_it tmp = *this; ++* this; return tmp; }
bool operator==(eq_occurs_it const& other) const { return m_first == other.m_first; }
bool operator!=(eq_occurs_it const& other) const { return !(*this == other); }
};
struct bit_atom : public atom {
var_pos_occ * m_occs;
bit_atom():m_occs(nullptr) {}
eq_occurs * m_eqs;
bit_atom():m_occs(nullptr), m_eqs(nullptr) {}
~bit_atom() override {}
bool is_bit() const override { return true; }
var_pos_it begin() const { return var_pos_it(m_occs); }
var_pos_it end() const { return var_pos_it(nullptr); }
bool is_fresh() const { return !m_occs && !m_eqs; }
class eqs_iterator {
bit_atom const& a;
public:
eqs_iterator(bit_atom const& a):a(a) {}
eq_occurs_it begin() const { return eq_occurs_it(a.m_eqs); }
eq_occurs_it end() const { return eq_occurs_it(nullptr); }
};
eqs_iterator eqs() const { return eqs_iterator(*this); }
};
struct def_atom : public atom {
@ -142,8 +183,17 @@ namespace bv {
bool is_bit() const override { return false; }
};
struct propagation_item {
var_pos m_vp { var_pos(0, 0) };
bit_atom* m_atom{ nullptr };
explicit propagation_item(bit_atom* a) : m_atom(a) {}
explicit propagation_item(var_pos const& vp) : m_vp(vp) {}
};
class bit_trail;
class add_var_pos_trail;
class add_eq_occurs_trail;
class mk_atom_trail;
class bit_occs_trail;
typedef ptr_vector<atom> bool_var2atom;
@ -160,15 +210,16 @@ namespace bv {
vector<zero_one_bits> m_zero_one_bits; // per var, see comment in the struct zero_one_bit
bool_var2atom m_bool_var2atom;
value2var m_fixed_var_table;
mutable vector<rational> m_power2;
literal_vector m_tmp_literals;
svector<var_pos> m_prop_queue;
unsigned_vector m_prop_queue_lim;
unsigned m_prop_queue_head { 0 };
mutable vector<rational> m_power2;
literal_vector m_tmp_literals;
svector<propagation_item> m_prop_queue;
unsigned_vector m_prop_queue_lim;
unsigned m_prop_queue_head { 0 };
sat::solver* m_solver;
sat::solver& s() { return *m_solver; }
sat::solver const& s() const { return *m_solver; }
// internalize
void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); }
@ -191,6 +242,8 @@ namespace bv {
void register_true_false_bit(theory_var v, unsigned i);
void add_bit(theory_var v, sat::literal lit);
bit_atom* mk_bit_atom(sat::bool_var bv);
void eq_internalized(sat::bool_var b, unsigned idx, theory_var v1, theory_var v2, euf::enode* n);
void set_bit_eh(theory_var v, literal l, unsigned idx);
void init_bits(expr* e, expr_ref_vector const & bits);
void mk_bits(theory_var v);
@ -227,10 +280,12 @@ namespace bv {
bool merge_zero_one_bits(theory_var r1, theory_var r2);
void assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
void propagate_bits(var_pos entry);
void propagate_eq_occurs(eq_occurs const& occ);
numeral const& power2(unsigned i) const;
// invariants
bool check_zero_one_bits(theory_var v);
void check_missing_propagation() const;
void validate_atoms() const;
public:
@ -282,6 +337,7 @@ namespace bv {
bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override { return false; }
sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
void internalize(expr* e, bool redundant) override;
void eq_internalized(euf::enode* n) override;
euf::theory_var mk_var(euf::enode* n) override;
void apply_sort_cnstr(euf::enode * n, sort * s) override;

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

@ -93,6 +93,12 @@ namespace euf {
if (s_ext && s_ext != e_ext)
s_ext->apply_sort_cnstr(n, m.get_sort(e));
}
expr* a = nullptr, * b = nullptr;
if (m.is_eq(e, a, b) && m.get_sort(a)->get_family_id() != null_family_id) {
auto* s_ext = sort2solver(m.get_sort(a));
if (s_ext)
s_ext->eq_internalized(n);
}
axiomatize_basic(n);
}

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

@ -352,6 +352,7 @@ namespace euf {
return sat::check_result::CR_CONTINUE;
if (give_up)
return sat::check_result::CR_GIVEUP;
TRACE("after_search", s().display(tout););
return sat::check_result::CR_DONE;
}
@ -390,34 +391,47 @@ namespace euf {
}
}
/**
* After a pop has completed, re-initialize the association between Boolean variables
* and the theories by re-creating the expression/variable mapping used for Booleans
* and replaying internalization.
*/
void solver::finish_reinit() {
SASSERT(s().get_vars_to_reinit().size() == m_reinit_exprs.size());
if (s().get_vars_to_reinit().empty())
return;
struct scoped_set_replay {
solver& s;
obj_map<expr, sat::bool_var> m;
scoped_set_replay(solver& s) :s(s) {
s.si.set_expr2var_replay(&m);
}
~scoped_set_replay() {
s.si.set_expr2var_replay(nullptr);
}
};
scoped_set_replay replay(*this);
unsigned i = 0;
obj_map<expr, sat::bool_var> expr2var_replay;
for (sat::bool_var v : s().get_vars_to_reinit()) {
expr* e = m_reinit_exprs.get(i++);
if (!e)
continue;
expr2var_replay.insert(e, v);
if (e)
replay.m.insert(e, v);
}
if (expr2var_replay.empty())
if (replay.m.empty())
return;
si.set_expr2var_replay(&expr2var_replay);
TRACE("euf", for (auto const& kv : expr2var_replay) tout << "replay: " << kv.m_value << " " << mk_bounded_pp(kv.m_key, m) << "\n";);
for (auto const& kv : expr2var_replay) {
TRACE("euf", for (auto const& kv : replay.m) tout << "replay: " << kv.m_value << " " << mk_bounded_pp(kv.m_key, m) << "\n";);
for (auto const& kv : replay.m) {
sat::literal lit;
expr* e = kv.m_key;
if (si.is_bool_op(e))
lit = literal(expr2var_replay[e], false);
lit = literal(replay.m[e], false);
else
lit = si.internalize(kv.m_key, true);
VERIFY(lit.var() == kv.m_value);
attach_lit(lit, kv.m_key);
}
si.set_expr2var_replay(nullptr);
TRACE("euf", tout << "replay done\n";);
}
@ -439,9 +453,13 @@ namespace euf {
}
lbool solver::get_phase(bool_var v) {
TRACE("euf", tout << "phase: " << v << "\n";);
auto* ext = bool_var2solver(v);
if (ext)
return ext->get_phase(v);
expr* e = bool_var2expr(v);
if (e && m.is_eq(e))
return l_true;
return l_undef;
}
@ -481,14 +499,28 @@ namespace euf {
std::ostream& solver::display_justification_ptr(std::ostream& out, size_t* j) const {
if (is_literal(j))
return out << get_literal(j) << " ";
return out << "sat: " << get_literal(j);
else
return display_justification(out, get_justification(j)) << " ";
return display_justification(out, get_justification(j));
}
std::ostream& solver::display_justification(std::ostream& out, ext_justification_idx idx) const {
auto* ext = sat::constraint_base::to_extension(idx);
if (ext != this)
if (ext == this) {
constraint& c = constraint::from_idx(idx);
switch (c.kind()) {
case constraint::kind_t::conflict:
return out << "euf conflict";
case constraint::kind_t::eq:
return out << "euf equality propagation";
case constraint::kind_t::lit:
return out << "euf literal propagation";
default:
UNREACHABLE();
return out;
}
}
else
return ext->display_justification(out, idx);
return out;
}
@ -497,7 +529,7 @@ namespace euf {
auto* ext = sat::constraint_base::to_extension(idx);
if (ext != this)
return ext->display_constraint(out, idx);
return out;
return display_justification(out, idx);
}
void solver::collect_statistics(statistics& st) const {

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

@ -99,7 +99,6 @@ namespace euf {
}
void th_euf_solver::push_core() {
TRACE("euf", tout << "push-core\n";);
m_var2enode_lim.push_back(m_var2enode.size());
}

10
src/sat/smt/sat_th.h
View file

@ -52,6 +52,11 @@ namespace euf {
*/
virtual void apply_sort_cnstr(enode * n, sort * s) {}
/**
\record that an equality has been internalized.
*/
virtual void eq_internalized(enode* n) {}
};
class th_decompile {
@ -138,7 +143,10 @@ namespace euf {
virtual void push_core();
virtual void pop_core(unsigned n);
void force_push() { for (; m_num_scopes > 0; --m_num_scopes) push_core(); }
void force_push() {
CTRACE("euf", m_num_scopes > 0, tout << "push-core " << m_num_scopes << "\n";);
for (; m_num_scopes > 0; --m_num_scopes) push_core();
}
public:
th_euf_solver(euf::solver& ctx, euf::theory_id id);

9
src/sat/tactic/goal2sat.cpp
View file

@ -669,13 +669,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
struct scoped_stack {
imp& i;
sat::literal_vector& r;
unsigned rsz;
svector<frame>& frames;
unsigned fsz;
bool is_root;
scoped_stack(imp& x, bool is_root) :
r(x.m_result_stack), rsz(r.size()), frames(x.m_frame_stack), fsz(frames.size()), is_root(is_root)
i(x), r(i.m_result_stack), rsz(r.size()), frames(x.m_frame_stack), fsz(frames.size()), is_root(is_root)
{}
~scoped_stack() {
if (frames.size() > fsz) {
@ -683,9 +684,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
r.shrink(rsz);
return;
}
SASSERT(frames.size() == fsz);
SASSERT(!is_root || rsz == r.size());
SASSERT(is_root || rsz + 1 == r.size());
SASSERT(i.m.limit().is_canceled() || frames.size() == fsz);
SASSERT(i.m.limit().is_canceled() || !is_root || rsz == r.size());
SASSERT(i.m.limit().is_canceled() || is_root || rsz + 1 == r.size());
}
};

1
src/smt/smt_context.cpp
View file

@ -3854,6 +3854,7 @@ namespace smt {
TRACE("final_check_result", tout << "fcs: " << fcs << " last_search_failure: " << m_last_search_failure << "\n";);
switch (fcs) {
case FC_DONE:
log_stats();
return l_true;
case FC_CONTINUE:
break;

6
src/smt/theory_bv.cpp
View file

@ -1178,6 +1178,12 @@ namespace smt {
literal arg = ctx.get_literal(diff);
lits.push_back(arg);
}
TRACE("bv",
tout << mk_pp(get_enode(v1)->get_owner(), m) << " = " << mk_pp(get_enode(v2)->get_owner(), m) << " "
<< ctx.get_scope_level()
<< "\n";
ctx.display_literals_smt2(tout, lits););
m_stats.m_num_diseq_dynamic++;
scoped_trace_stream st(*this, lits);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());