diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index 305a7b626..735de4d75 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -69,7 +69,7 @@ namespace arith { } std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { - return euf::th_propagation::from_index(idx).display(out); + return euf::th_explain::from_index(idx).display(out); } std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index d07390810..e1d99b9d8 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -318,7 +318,7 @@ namespace arith { reset_evidence(); for (auto const& ev : e) set_evidence(ev.ci(), m_core, m_eqs); - auto* jst = euf::th_propagation::propagate(*this, m_core, m_eqs, n1, n2); + auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2); ctx.propagate(n1, n2, jst->to_index()); } @@ -718,7 +718,7 @@ namespace arith { set_evidence(ci4, m_core, m_eqs); enode* x = var2enode(v1); enode* y = var2enode(v2); - auto* jst = euf::th_propagation::propagate(*this, m_core, m_eqs, x, y); + auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y); ctx.propagate(x, y, jst->to_index()); } @@ -1141,7 +1141,7 @@ namespace arith { add_clause(m_core2); } else { - auto* jst = euf::th_propagation::propagate(*this, core, eqs, lit); + auto* jst = euf::th_explain::propagate(*this, core, eqs, lit); ctx.propagate(lit, jst->to_index()); } } @@ -1419,7 +1419,7 @@ namespace arith { } void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) { - auto& jst = euf::th_propagation::from_index(idx); + auto& jst = euf::th_explain::from_index(idx); ctx.get_antecedents(l, jst, r, probing); } diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index 2c6c7faf2..4dfa3fef2 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -105,7 +105,7 @@ namespace dt { add_unit(eq_internalize(e1, e2)); else if (s().value(antecedent) == l_true) { euf::enode* n2 = e_internalize(e2); - ctx.propagate(n1, n2, euf::th_propagation::propagate(*this, antecedent, n1, n2)); + ctx.propagate(n1, n2, euf::th_explain::propagate(*this, antecedent, n1, n2)); } else add_clause(~antecedent, eq_internalize(e1, e2)); @@ -160,7 +160,7 @@ namespace dt { literal l = ctx.enode2literal(r); SASSERT(s().value(l) == l_false); clear_mark(); - ctx.set_conflict(euf::th_propagation::conflict(*this, ~l, c, r->get_arg(0))); + ctx.set_conflict(euf::th_explain::conflict(*this, ~l, c, r->get_arg(0))); } /** @@ -315,7 +315,7 @@ namespace dt { break; } } - ctx.set_conflict(euf::th_propagation::conflict(*this, m_lits)); + ctx.set_conflict(euf::th_explain::conflict(*this, m_lits)); } @@ -462,7 +462,7 @@ namespace dt { } TRACE("dt", tout << "propagate " << num_unassigned << " eqs: " << eqs.size() << "\n";); if (num_unassigned == 0) - ctx.set_conflict(euf::th_propagation::conflict(*this, m_lits, eqs)); + ctx.set_conflict(euf::th_explain::conflict(*this, m_lits, eqs)); else if (num_unassigned == 1) { // propagate remaining recognizer SASSERT(!m_lits.empty()); @@ -476,7 +476,7 @@ namespace dt { app_ref rec_app(m.mk_app(rec, n->get_expr()), m); consequent = mk_literal(rec_app); } - ctx.propagate(consequent, euf::th_propagation::propagate(*this, m_lits, eqs, consequent)); + ctx.propagate(consequent, euf::th_explain::propagate(*this, m_lits, eqs, consequent)); } else if (get_config().m_dt_lazy_splits == 0 || (!srt->is_infinite() && get_config().m_dt_lazy_splits == 1)) // there are more than 2 unassigned recognizers... @@ -493,7 +493,7 @@ namespace dt { auto* con1 = d1->m_constructor; auto* con2 = d2->m_constructor; if (con1 && con2 && con1->get_decl() != con2->get_decl()) - ctx.set_conflict(euf::th_propagation::conflict(*this, con1, con2)); + ctx.set_conflict(euf::th_explain::conflict(*this, con1, con2)); else if (con2 && !con1) { ctx.push(set_ptr_trail(d1->m_constructor)); // check whether there is a recognizer in d1 that conflicts with con2; @@ -663,7 +663,7 @@ namespace dt { if (res) { clear_mark(); - ctx.set_conflict(euf::th_propagation::conflict(*this, m_used_eqs)); + ctx.set_conflict(euf::th_explain::conflict(*this, m_used_eqs)); TRACE("dt", tout << "occurs check conflict: " << ctx.bpp(n) << "\n";); } return res; @@ -704,7 +704,7 @@ namespace dt { } void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) { - auto& jst = euf::th_propagation::from_index(idx); + auto& jst = euf::th_explain::from_index(idx); ctx.get_antecedents(l, jst, r, probing); } diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h index 528e2c508..785912170 100644 --- a/src/sat/smt/dt_solver.h +++ b/src/sat/smt/dt_solver.h @@ -140,7 +140,7 @@ namespace dt { sat::check_result check() override; std::ostream& display(std::ostream& out) const override; - std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return euf::th_propagation::from_index(idx).display(out); } + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return euf::th_explain::from_index(idx).display(out); } std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return display_justification(out, idx); } void collect_statistics(statistics& st) const override; euf::th_solver* clone(euf::solver& ctx) override; diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index b742809e5..42fc8ccde 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -126,7 +126,7 @@ namespace euf { } } - void solver::log_justification(literal l, th_propagation const& jst) { + void solver::log_justification(literal l, th_explain const& jst) { literal_vector lits; unsigned nv = s().num_vars(); expr_ref_vector eqs(m); @@ -138,11 +138,11 @@ namespace euf { return lit; }; - for (auto lit : euf::th_propagation::lits(jst)) + for (auto lit : euf::th_explain::lits(jst)) lits.push_back(~lit); if (l != sat::null_literal) lits.push_back(l); - for (auto eq : euf::th_propagation::eqs(jst)) + for (auto eq : euf::th_explain::eqs(jst)) lits.push_back(~add_lit(eq)); if (jst.lit_consequent() != sat::null_literal && jst.lit_consequent() != l) lits.push_back(jst.lit_consequent()); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index b8ceb7fc2..1f2531d20 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -218,10 +218,10 @@ namespace euf { log_antecedents(l, r); } - void solver::get_antecedents(literal l, th_propagation& jst, literal_vector& r, bool probing) { - for (auto lit : euf::th_propagation::lits(jst)) + void solver::get_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) { + for (auto lit : euf::th_explain::lits(jst)) r.push_back(lit); - for (auto eq : euf::th_propagation::eqs(jst)) + for (auto eq : euf::th_explain::eqs(jst)) add_antecedent(eq.first, eq.second); if (!probing && use_drat()) diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 84a926650..112a8a35d 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -167,7 +167,7 @@ namespace euf { // proofs void log_antecedents(std::ostream& out, literal l, literal_vector const& r); void log_antecedents(literal l, literal_vector const& r); - void log_justification(literal l, th_propagation const& jst); + void log_justification(literal l, th_explain const& jst); void drat_log_decl(func_decl* f); void drat_log_expr(expr* n); void drat_log_expr1(expr* n); @@ -282,15 +282,15 @@ namespace euf { bool propagate(enode* a, enode* b, ext_justification_idx idx); void set_conflict(ext_justification_idx idx); - void propagate(literal lit, th_propagation* p) { propagate(lit, p->to_index()); } - bool propagate(enode* a, enode* b, th_propagation* p) { return propagate(a, b, p->to_index()); } - void set_conflict(th_propagation* p) { set_conflict(p->to_index()); } + void propagate(literal lit, th_explain* p) { propagate(lit, p->to_index()); } + bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); } + void set_conflict(th_explain* p) { set_conflict(p->to_index()); } 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_antecedents(literal l, th_propagation& jst, literal_vector& r, bool probing); + void get_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing); void add_antecedent(enode* a, enode* b); void add_diseq_antecedent(enode* a, enode* b); void asserted(literal l) override; diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 3faad5855..da668643d 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -225,73 +225,73 @@ namespace euf { return ctx.s().rand()(); } - size_t th_propagation::get_obj_size(unsigned num_lits, unsigned num_eqs) { - return sat::constraint_base::obj_size(sizeof(th_propagation) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs); + size_t th_explain::get_obj_size(unsigned num_lits, unsigned num_eqs) { + return sat::constraint_base::obj_size(sizeof(th_explain) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs); } - th_propagation::th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& p) { + th_explain::th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& p) { m_consequent = c; m_eq = p; m_num_literals = n_lits; m_num_eqs = n_eqs; - m_literals = reinterpret_cast(reinterpret_cast(this) + sizeof(th_propagation)); + m_literals = reinterpret_cast(reinterpret_cast(this) + sizeof(th_explain)); for (unsigned i = 0; i < n_lits; ++i) m_literals[i] = lits[i]; - m_eqs = reinterpret_cast(reinterpret_cast(this) + sizeof(th_propagation) + sizeof(literal) * n_lits); + m_eqs = reinterpret_cast(reinterpret_cast(this) + sizeof(th_explain) + sizeof(literal) * n_lits); for (unsigned i = 0; i < n_eqs; ++i) m_eqs[i] = eqs[i]; } - th_propagation* th_propagation::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y) { + th_explain* th_explain::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y) { region& r = th.ctx.get_region(); void* mem = r.allocate(get_obj_size(n_lits, n_eqs)); sat::constraint_base::initialize(mem, &th); - return new (sat::constraint_base::ptr2mem(mem)) th_propagation(n_lits, lits, n_eqs, eqs, c, enode_pair(x, y)); + return new (sat::constraint_base::ptr2mem(mem)) th_explain(n_lits, lits, n_eqs, eqs, c, enode_pair(x, y)); } - th_propagation* th_propagation::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent) { + th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent) { return mk(th, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), consequent, nullptr, nullptr); } - th_propagation* th_propagation::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y) { + th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y) { return mk(th, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), sat::null_literal, x, y); } - th_propagation* th_propagation::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) { + th_explain* th_explain::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) { return mk(th, 1, &lit, 0, nullptr, sat::null_literal, x, y); } - th_propagation* th_propagation::conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs) { + th_explain* th_explain::conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs) { return conflict(th, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr()); } - th_propagation* th_propagation::conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) { + th_explain* th_explain::conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) { return mk(th, n_lits, lits, n_eqs, eqs, sat::null_literal, nullptr, nullptr); } - th_propagation* th_propagation::conflict(th_euf_solver& th, enode_pair_vector const& eqs) { + th_explain* th_explain::conflict(th_euf_solver& th, enode_pair_vector const& eqs) { return conflict(th, 0, nullptr, eqs.size(), eqs.c_ptr()); } - th_propagation* th_propagation::conflict(th_euf_solver& th, sat::literal lit) { + th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit) { return conflict(th, 1, &lit, 0, nullptr); } - th_propagation* th_propagation::conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) { + th_explain* th_explain::conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) { enode_pair eq(x, y); return conflict(th, 1, &lit, 1, &eq); } - th_propagation* th_propagation::conflict(th_euf_solver& th, euf::enode* x, euf::enode* y) { + th_explain* th_explain::conflict(th_euf_solver& th, euf::enode* x, euf::enode* y) { enode_pair eq(x, y); return conflict(th, 0, nullptr, 1, &eq); } - std::ostream& th_propagation::display(std::ostream& out) const { - for (auto lit : euf::th_propagation::lits(*this)) + std::ostream& th_explain::display(std::ostream& out) const { + for (auto lit : euf::th_explain::lits(*this)) out << lit << " "; - for (auto eq : euf::th_propagation::eqs(*this)) + for (auto eq : euf::th_explain::eqs(*this)) out << eq.first->get_expr_id() << " == " << eq.second->get_expr_id() << " "; if (m_consequent != sat::null_literal) out << "--> " << m_consequent; diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 52ff3e3cc..67b15e8e3 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -165,7 +165,7 @@ namespace euf { for (; m_num_scopes > 0; --m_num_scopes) push_core(); } - friend class th_propagation; + friend class th_explain; public: th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id); @@ -191,36 +191,41 @@ namespace euf { unsigned random(); }; - - class th_propagation { - sat::literal m_consequent { sat::null_literal }; - enode_pair m_eq { enode_pair() }; + /** + * General purpose, eager explanation object. Explanations are conjunctions of literals and equalities. + * Used literals and equalities are stored in the object and retrieved on demand for conflict resolution + * It is "eager" in the sense that relevant literals are accumulated when the explanation is created. + * This is not a real problem for conflicts, but a theory has an option to implement custom lazy explanations + * that retrieve literals on demand. + */ + class th_explain { + sat::literal m_consequent { sat::null_literal }; // literal consequent for propagations + enode_pair m_eq { enode_pair() }; // equality consequent for propagations unsigned m_num_literals; unsigned m_num_eqs; sat::literal* m_literals; enode_pair* m_eqs; static size_t get_obj_size(unsigned num_lits, unsigned num_eqs); - th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq); - static th_propagation* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y); + th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq); + static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y); public: - static th_propagation* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs); - static th_propagation* conflict(th_euf_solver& th, sat::literal_vector const& lits) { return conflict(th, lits.size(), lits.c_ptr(), 0, nullptr); } - static th_propagation* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs); - static th_propagation* conflict(th_euf_solver& th, enode_pair_vector const& eqs); - static th_propagation* conflict(th_euf_solver& th, sat::literal lit); - static th_propagation* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y); - static th_propagation* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y); - static th_propagation* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y); - static th_propagation* propagate(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal consequent); - static th_propagation* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent); - static th_propagation* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y); + static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs); + static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits) { return conflict(th, lits.size(), lits.c_ptr(), 0, nullptr); } + static th_explain* conflict(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs); + static th_explain* conflict(th_euf_solver& th, enode_pair_vector const& eqs); + static th_explain* conflict(th_euf_solver& th, sat::literal lit); + static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y); + static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y); + static th_explain* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y); + static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent); + static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y); sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); } - static th_propagation& from_index(size_t idx) { - return *reinterpret_cast(sat::constraint_base::from_index(idx)->mem()); + static th_explain& from_index(size_t idx) { + return *reinterpret_cast(sat::constraint_base::from_index(idx)->mem()); } sat::extension& ext() const { @@ -230,17 +235,17 @@ namespace euf { std::ostream& display(std::ostream& out) const; class lits { - th_propagation const& th; + th_explain const& th; public: - lits(th_propagation const& th) : th(th) {} + lits(th_explain const& th) : th(th) {} sat::literal const* begin() const { return th.m_literals; } sat::literal const* end() const { return th.m_literals + th.m_num_literals; } }; class eqs { - th_propagation const& th; + th_explain const& th; public: - eqs(th_propagation const& th) : th(th) {} + eqs(th_explain const& th) : th(th) {} enode_pair const* begin() const { return th.m_eqs; } enode_pair const* end() const { return th.m_eqs + th.m_num_eqs; } };