From 7566f088f9298db9ea36174a68b22949d1ac0679 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Jun 2025 15:02:34 +0200 Subject: [PATCH] vtable Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/euf_completion.cpp | 140 +++++++++++++++++- .../portfolio/euf_completion_tactic.cpp | 2 +- 2 files changed, 137 insertions(+), 5 deletions(-) diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index 50a221e4c..78c0d2595 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -21,7 +21,6 @@ if it is smallest in a well-order, such as a ground Knuth-Bendix order. A basic approach is terms that are of smallest depth, are values can be chosen as simplest. Ties between equal-depth terms can be resolved arbitrarily. - Algorithm for extracting canonical form from an E-graph: * Compute function canon(t) that maps every term in E to a canonical, least with respect to well-order relative to the congruence closure. @@ -36,6 +35,25 @@ Algorithm for extracting canonical form from an E-graph: * We claim the new formula is equivalent. * The dependencies for each rewrite can be computed by following the equality justification data-structure. +Conditional saturation: +- forall X . Body => Head +- propagate when (all assertions in) Body is merged with True +- Possible efficient approaches: + - use on_merge? + - or bit set in nodes with Body? + - register Boolean reduction rules to EUF? + - register function "body_of" and monitor merges based on function? + +Delayed solver invocation +- So far default code for checking rules + - EUF check should be on demand, see note on conditional saturation + +Mam optimization? + match(p, t, S) = suppose all variables in p are bound in S, check equality using canonization of p[S], otherwise prune instances from S. + + + + --*/ @@ -75,6 +93,16 @@ namespace euf { m_egraph.set_on_make(_on_make); } + completion::~completion() { + reset_rules(); + } + + void completion::reset_rules() { + for (auto r : m_rules) + dealloc(r); + m_rules.reset(); + } + void completion::reduce() { m_has_new_eq = true; for (unsigned rounds = 0; m_has_new_eq && rounds <= 3 && !m_fmls.inconsistent(); ++rounds) { @@ -85,6 +113,7 @@ namespace euf { read_egraph(); IF_VERBOSE(11, verbose_stream() << "(euf.completion :rounds " << rounds << ")\n"); } + reset_rules(); } void completion::add_egraph() { @@ -96,14 +125,19 @@ namespace euf { add_constraint(f, d); } m_should_propagate = true; - while (m_should_propagate) { + while (m_should_propagate && m.inc() && !m_egraph.inconsistent()) { m_should_propagate = false; m_egraph.propagate(); m_mam->propagate(); + IF_VERBOSE(11, verbose_stream() << "propagate " << m_stats.m_num_instances << "\n"); + if (!m_should_propagate) + check_rules(); } } void completion::add_constraint(expr* f, expr_dependency* d) { + if (m_egraph.inconsistent()) + return; auto add_children = [&](enode* n) { for (auto* ch : enode_args(n)) m_nodes_to_canonize.push_back(ch); @@ -140,10 +174,110 @@ namespace euf { get_trail().push(insert_obj_map(m_q2dep, q)); } } + add_rule(f, d); } + if (m_side_condition_solver) + m_side_condition_solver->add_constraint(f, d); + } + + lbool completion::eval_cond(expr* f, expr_dependency*& d) { + auto n = mk_enode(f); + if (m.is_true(n->get_root()->get_expr())) { + d = m.mk_join(d, explain_eq(n, n->get_root())); + return l_true; + } + if (m.is_false(n->get_root()->get_expr())) + return l_false; + + expr* g = nullptr; + if (m.is_not(f, g)) { + n = mk_enode(g); + if (m.is_false(n->get_root()->get_expr())) { + d = m.mk_join(d, explain_eq(n, n->get_root())); + return l_true; + } + } + if (m_side_condition_solver) { + expr_dependency* sd = nullptr; + if (m_side_condition_solver->is_true(f, sd)) { + add_constraint(f, sd); + d = m.mk_join(d, sd); + return l_true; + } + } + return l_undef; + } + + void completion::add_rule(expr* f, expr_dependency* d) { + expr* x = nullptr, * y = nullptr; + if (!m.is_implies(f, x, y)) + return; + expr_ref_vector body(m); + expr_ref head(y, m); + body.push_back(x); + flatten_and(body); + unsigned j = 0; + for (auto f : body) { + switch (eval_cond(f, d)) { + case l_true: + break; + case l_false: + return; + case l_undef: + body[j++] = f; + break; + } + } + body.shrink(j); + if (body.empty()) { + add_constraint(head, d); + return; + } + m_rules.push_back(alloc(ground_rule, body, head, d)); + } + + void completion::check_rules() { + unsigned j = 0; + for (auto& r : m_rules) { + switch (check_rule(*r)) { + case l_true: + dealloc(r); + break; // remove rule, it is activated + case l_false: + dealloc(r); + break; // remove rule, premise is false + case l_undef: + m_rules[j++] = r; + break; + } + } + m_rules.shrink(j); + } + + lbool completion::check_rule(ground_rule& r) { + unsigned j = 0; + for (auto* f : r.m_body) { + switch (eval_cond(f, r.m_dep)) { + case l_true: + break; + case l_false: + return l_false; + default: + r.m_body[j++] = f; + break; + } + } + r.m_body.shrink(j); + if (r.m_body.empty()) { + add_constraint(r.m_head, r.m_dep); + return l_true; + } + return l_undef; } void completion::on_binding(quantifier* q, app* pat, enode* const* binding, unsigned mg, unsigned ming, unsigned mx) { + if (m_egraph.inconsistent()) + return; var_subst subst(m); expr_ref_vector _binding(m); for (unsigned i = 0; i < q->get_num_decls(); ++i) @@ -156,14 +290,12 @@ namespace euf { } void completion::read_egraph() { - if (m_egraph.inconsistent()) { auto* d = explain_conflict(); dependent_expr de(m, m.mk_false(), nullptr, d); m_fmls.update(0, de); return; } - unsigned sz = qtail(); for (unsigned i = qhead(); i < sz; ++i) { auto [f, p, d] = m_fmls[i](); diff --git a/src/tactic/portfolio/euf_completion_tactic.cpp b/src/tactic/portfolio/euf_completion_tactic.cpp index b8784d8f5..c61b678f1 100644 --- a/src/tactic/portfolio/euf_completion_tactic.cpp +++ b/src/tactic/portfolio/euf_completion_tactic.cpp @@ -75,5 +75,5 @@ static euf::completion* mk_completion(ast_manager& m, dependent_expr_state& s, p tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) { return alloc(dependent_expr_state_tactic, m, p, - [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(euf::completion, m, s); }); + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return mk_completion(m, s, p); }); }