From 7df5c941243376530764d3a6e5f82cac90b6d893 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Sep 2020 11:22:48 -0700 Subject: [PATCH] additional bit-vector propagators Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 26 ++-- src/sat/sat_probing.cpp | 1 + src/sat/sat_probing.h | 3 +- src/sat/sat_solver.cpp | 21 +++- src/sat/sat_solver.h | 1 + src/sat/smt/bv_ackerman.cpp | 2 +- src/sat/smt/bv_internalize.cpp | 72 +++++++---- src/sat/smt/bv_invariant.cpp | 22 ++++ src/sat/smt/bv_solver.cpp | 217 +++++++++++++++++++++++++------- src/sat/smt/bv_solver.h | 84 ++++++++++--- src/sat/smt/euf_internalize.cpp | 6 + src/sat/smt/euf_solver.cpp | 62 ++++++--- src/sat/smt/sat_th.cpp | 1 - src/sat/smt/sat_th.h | 10 +- src/sat/tactic/goal2sat.cpp | 9 +- src/smt/smt_context.cpp | 1 + src/smt/theory_bv.cpp | 6 + 17 files changed, 423 insertions(+), 121 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 80e50c61561..c2ff7939d09 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -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; } diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index 2ca17e344da..510593bbf0a 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -237,6 +237,7 @@ namespace sat { if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit) m_cached_bins.finalize(); + flet _probing(m_active, true); report rpt(*this); bool r = true; m_counter = 0; diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h index 986bad6a8d6..dd75d21bfbc 100644 --- a/src/sat/sat_probing.h +++ b/src/sat/sat_probing.h @@ -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 diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index daa4b3e5aa7..3219d7d605f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -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; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 00ade9465f6..abd4a66d292 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -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; diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index 1d7ebfe13ee..beee6a558fc 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -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) { diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 6a46dbe45d5..376d4c69e94 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -42,6 +42,16 @@ namespace bv { } }; + class solver::add_eq_occurs_trail : public trail { + 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 { 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 _red(m_is_redundant, true); + flet _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())); } } diff --git a/src/sat/smt/bv_invariant.cpp b/src/sat/smt/bv_invariant.cpp index 73db67894be..82fde885e1e 100644 --- a/src/sat/smt/bv_invariant.cpp +++ b/src/sat/smt/bv_invariant.cpp @@ -16,6 +16,7 @@ Module Name: --*/ #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. diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index a356f5890e6..e022fcb918b 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -69,7 +69,7 @@ namespace bv { m_fixed_var_table.find(key, v2) && v2 < static_cast(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(i + 1); + } + if (num_undef > 1 && get_config().m_bv_eq_axioms) + return; + } + 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)); } - if (s().at_search_lvl()) { + 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(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)); } } diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index a70c9d48a4d..76fe5207526 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -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 bool_var2atom; @@ -160,15 +210,16 @@ namespace bv { vector 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 m_power2; - literal_vector m_tmp_literals; - svector m_prop_queue; - unsigned_vector m_prop_queue_lim; - unsigned m_prop_queue_head { 0 }; + mutable vector m_power2; + literal_vector m_tmp_literals; + svector 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& 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; diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 5bc32013ce3..fd1ba52f493 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -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); } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 416a2388d1b..23dff1f5a3f 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -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 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 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 { diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 4173bae8ece..e0450cd897b 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -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()); } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 18d435fe821..eed5d7cb027 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -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); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 12228e8a58a..59fba823cc7 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -669,13 +669,14 @@ struct goal2sat::imp : public sat::sat_internalizer { } struct scoped_stack { + imp& i; sat::literal_vector& r; unsigned rsz; svector& 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()); } }; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 20f931e7e46..a5d8e6caf26 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 6fa32f3fa7e..6b7db2d8fc9 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -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());