From 1de25ed09c0f3cf80d921a208946e0a15fa63c3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Dec 2023 19:43:51 -0800 Subject: [PATCH] pending files --- src/ast/euf/euf_egraph.cpp | 47 ++++++++++++++++++++++---------------- src/sat/sat_solver.cpp | 31 ++++++++++++------------- src/sat/smt/euf_solver.cpp | 12 +++++++--- 3 files changed, 50 insertions(+), 40 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 154106e2399..c32a8173933 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -81,14 +81,14 @@ namespace euf { } void egraph::reinsert_equality(enode* p) { - SASSERT(p->is_equality()); + SASSERT(p->is_equality()); if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) queue_literal(p, nullptr); } - void egraph::queue_literal(enode* p, enode* ante) { + void egraph::queue_literal(enode* p, enode* ante) { if (m_on_propagate_literal) - m_to_merge.push_back({ p, ante }); + m_to_merge.push_back(to_merge(p, ante)); } void egraph::force_push() { @@ -180,6 +180,7 @@ namespace euf { } void egraph::add_literal(enode* n, enode* ante) { + TRACE("euf", tout << "propagate " << bpp(n) << " " << bpp(ante) << "\n"); if (!m_on_propagate_literal) return; if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits; @@ -518,7 +519,7 @@ namespace euf { void egraph::remove_parents(enode* r) { TRACE("euf", tout << bpp(r) << "\n"); - DEBUG_CODE(for (enode* p : enode_parents(r)) SASSERT(!p->is_marked1()); ); + SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); })); for (enode* p : enode_parents(r)) { if (p->is_marked1()) continue; @@ -545,7 +546,7 @@ namespace euf { if (p->cgc_enabled()) { auto [p_other, comm] = insert_table(p); SASSERT(m_table.contains_ptr(p) == (p_other == p)); - TRACE("euf", tout << "other " << bpp(p_other) << "\n";); + CTRACE("euf", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n"); if (p_other != p) m_to_merge.push_back(to_merge(p_other, p, comm)); else @@ -606,20 +607,26 @@ namespace euf { bool egraph::propagate() { force_push(); - for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) { - auto const& w = m_to_merge[i]; - switch (w.t) { - case to_merge_plain: - case to_merge_comm: - merge(w.a, w.b, justification::congruence(w.commutativity(), m_congruence_timestamp++)); - break; - case to_justified: - merge(w.a, w.b, w.j); - break; - case to_add_literal: - add_literal(w.a, w.b); - break; - } + unsigned i = 0; + bool change = true; + while (change) { + change = false; + propagate_plugins(); + for (; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) { + auto const& w = m_to_merge[i]; + switch (w.t) { + case to_merge_plain: + case to_merge_comm: + merge(w.a, w.b, justification::congruence(w.commutativity(), m_congruence_timestamp++)); + break; + case to_justified: + merge(w.a, w.b, w.j); + break; + case to_add_literal: + add_literal(w.a, w.b); + break; + } + } } m_to_merge.reset(); return @@ -635,7 +642,7 @@ namespace euf { m_updates.push_back(update_record(false, update_record::inconsistent())); m_n1 = n1; m_n2 = n2; - TRACE("euf", tout << "conflict " << bpp(n1) << " " << bpp(n2) << " " << j << "\n"); + TRACE("euf", tout << "conflict " << bpp(n1) << " " << bpp(n2) << " " << j << " " << n1->get_root()->value() << " " << n2->get_root()->value() << "\n"); m_justification = j; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b899ee47990..ba5170c7f73 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -962,6 +962,8 @@ namespace sat { // ----------------------- bool solver::propagate_core(bool update) { + if (m_ext && (!is_probing() || at_base_lvl())) + m_ext->unit_propagate(); while (m_qhead < m_trail.size() && !m_inconsistent) { do { checkpoint(); @@ -1783,7 +1785,7 @@ namespace sat { } bool solver::should_propagate() const { - return !inconsistent() && m_qhead < m_trail.size(); + return !inconsistent() && (m_qhead < m_trail.size() || (m_ext && m_ext->should_propagate())); } lbool solver::final_check() { @@ -2533,17 +2535,8 @@ namespace sat { case justification::EXT_JUSTIFICATION: { fill_ext_antecedents(consequent, js, false); TRACE("sat", tout << "ext antecedents: " << m_ext_antecedents << "\n";); - for (literal l : m_ext_antecedents) - process_antecedent(l, num_marks); - -#if 0 - if (m_ext_antecedents.size() <= 1) { - for (literal& l : m_ext_antecedents) - l.neg(); - m_ext_antecedents.push_back(consequent); - mk_clause(m_ext_antecedents.size(), m_ext_antecedents.c_ptr(), sat::status::redundant()); - } -#endif + for (literal l : m_ext_antecedents) + process_antecedent(l, num_marks); break; } default: @@ -2822,25 +2815,27 @@ namespace sat { switch (js.get_kind()) { case justification::NONE: level = std::max(level, js.level()); - return level; + break; case justification::BINARY: level = update_max_level(js.get_literal(), level, unique_max); - return level; + break; case justification::CLAUSE: for (literal l : get_clause(js)) level = update_max_level(l, level, unique_max); - return level; + break; case justification::EXT_JUSTIFICATION: if (not_l != null_literal) not_l.neg(); fill_ext_antecedents(not_l, js, true); for (literal l : m_ext_antecedents) level = update_max_level(l, level, unique_max); - return level; + break; default: UNREACHABLE(); - return 0; + break; } + TRACE("sat", tout << "max-level " << level << " " << unique_max << "\n"); + return level; } /** @@ -3493,6 +3488,8 @@ namespace sat { SASSERT(!inconsistent()); TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";); SASSERT(m_qhead == m_trail.size()); + if (m_ext) + m_ext->unit_propagate(); m_scopes.push_back(scope()); scope & s = m_scopes.back(); m_scope_lvl++; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 8e4bd765d54..f4a563876c7 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -435,6 +435,9 @@ namespace euf { } + bool solver::should_propagate() { + return m_egraph.can_propagate(); + } bool solver::unit_propagate() { bool propagated = false; @@ -477,6 +480,7 @@ namespace euf { SASSERT(m.is_bool(e)); size_t cnstr; literal lit; + if (!ante) { VERIFY(m.is_eq(e, a, b)); cnstr = eq_constraint().to_index(); @@ -494,7 +498,7 @@ namespace euf { if (val == l_undef) { SASSERT(m.is_value(ante->get_expr())); val = m.is_true(ante->get_expr()) ? l_true : l_false; - } + } auto& c = lit_constraint(ante); cnstr = c.to_index(); lit = literal(v, val == l_false); @@ -1012,8 +1016,10 @@ namespace euf { return out << "euf conflict"; case constraint::kind_t::eq: return out << "euf equality propagation"; - case constraint::kind_t::lit: - return out << "euf literal propagation " << m_egraph.bpp(c.node()) ; + case constraint::kind_t::lit: { + euf::enode* n = c.node(); + return out << "euf literal propagation " << (sat::literal(n->bool_var(), n->value() == l_false)) << " " << m_egraph.bpp(n); + } default: UNREACHABLE(); return out;