From 35b1d094251c53066abf374190e9dd41fef9e966 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Jul 2025 04:50:43 +0200 Subject: [PATCH] working on ho-matcher --- src/ast/euf/ho_matcher.cpp | 13 +++-- src/ast/euf/ho_matcher.h | 2 +- src/ast/simplifiers/euf_completion.cpp | 54 ++++++++++++++----- .../portfolio/euf_completion_tactic.cpp | 2 + 4 files changed, 49 insertions(+), 22 deletions(-) diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index 7be2a8943..4a313ee61 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -636,15 +636,15 @@ namespace euf { } - quantifier* ho_matcher::compile_ho_pattern(quantifier* q, app*& p) { + std::pair ho_matcher::compile_ho_pattern(quantifier* q, app* p) { app* p1 = nullptr; if (m_pat2hopat.find(p, p)) { q = m_q2hoq[q]; - return q; + return { q, p }; } auto is_ho = any_of(subterms::all(expr_ref(p, m)), [&](expr* t) { return m_unitary.is_flex(0, t); }); if (!is_ho) - return q; + return { q, p }; ptr_vector todo; ptr_buffer bound; expr_ref_vector cache(m); @@ -684,7 +684,7 @@ namespace euf { } if (is_quantifier(t)) { m_pat2abs.remove(p); - return q; + return { q, p }; } } p1 = to_app(cache.get(p->get_id())); @@ -738,9 +738,8 @@ namespace euf { trail().push(insert_map(m_pat2abs, p)); trail().push(insert_map(m_q2hoq, q)); trail().push(insert_map(m_hoq2q, q1)); - trail().push(insert_map(m_hopat2free_vars, p1)); - p = p1; - return q1; + trail().push(insert_map(m_hopat2free_vars, p1)); + return { q1, p1 }; } bool ho_matcher::is_ho_pattern(app* p) { diff --git a/src/ast/euf/ho_matcher.h b/src/ast/euf/ho_matcher.h index 3bd5b9d2f..47de6d4e2 100644 --- a/src/ast/euf/ho_matcher.h +++ b/src/ast/euf/ho_matcher.h @@ -386,7 +386,7 @@ namespace euf { void operator()(expr* pat, expr* t, unsigned num_bound, unsigned num_vars); - quantifier* compile_ho_pattern(quantifier* q, app*& p); + std::pair compile_ho_pattern(quantifier* q, app* p); bool is_ho_pattern(app* p); diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index 03410d95a..9ff6ecc13 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -98,28 +98,36 @@ namespace euf { [&](ho_subst& s) { IF_VERBOSE(1, s.display(verbose_stream() << "on-match\n") << "\n"); auto& b = *m_ho_binding; - auto* hopat = b.m_pattern; auto* hoq = b.m_q; auto* q = m_matcher.hoq2q(hoq); // shrink binding expr_ref_vector binding(m); for (unsigned i = 0; i < s.size(); ++i) binding.push_back(s.get(i)); - binding.reverse(); + if (binding.size() > q->get_num_decls()) { bool change = true; while (change) { change = false; - for (unsigned i = binding.size(); i-- > 0;) { - var_subst sub(m, false); + for (unsigned i = 1; i < binding.size();) { + var_subst sub(m); auto r = sub(binding.get(i), binding); change |= r != binding.get(i); + m_rewriter(r); binding[i] = r; } } + binding.reverse(); + binding.shrink(q->get_num_decls()); + binding.reverse(); + } + else { + for (unsigned i = 0; i < binding.size();) { + expr_ref r(binding.get(i), m); + m_rewriter(r); + binding[i] = r; + } } - binding.shrink(q->get_num_decls()); - binding.reverse(); IF_VERBOSE(1, verbose_stream() << binding << "\n"); apply_binding(b, q, binding); @@ -226,7 +234,7 @@ namespace euf { void completion::add_egraph() { m_nodes_to_canonize.reset(); unsigned sz = qtail(); - + for (unsigned i = qhead(); i < sz; ++i) { auto [f, p, d] = m_fmls[i](); @@ -264,23 +272,36 @@ namespace euf { }; expr* x, * y; if (m.is_eq(f, x, y)) { - enode* a = mk_enode(x); - enode* b = mk_enode(y); - + expr_ref x1(x, m); + expr_ref y1(y, m); + m_rewriter(x1); + m_rewriter(y1); + enode* a = mk_enode(x1); + enode* b = mk_enode(y1); + if (a->get_root() == b->get_root()) + return; m_egraph.merge(a, b, to_ptr(push_pr_dep(pr, d))); add_children(a); add_children(b); m_should_propagate = true; + if (m_side_condition_solver) + m_side_condition_solver->add_constraint(f, pr, d); } else if (m.is_not(f, f)) { enode* n = mk_enode(f); + if (m.is_false(n->get_root()->get_expr())) + return; auto j = to_ptr(push_pr_dep(pr, d)); m_egraph.new_diseq(n, j); add_children(n); m_should_propagate = true; + if (m_side_condition_solver) + m_side_condition_solver->add_constraint(f, pr, d); } else { enode* n = mk_enode(f); + if (m.is_true(n->get_root()->get_expr())) + return; m_egraph.merge(n, m_tt, to_ptr(push_pr_dep(pr, d))); add_children(n); if (is_forall(f)) { @@ -296,20 +317,24 @@ namespace euf { for (unsigned i = 0; i < q->get_num_patterns(); ++i) { auto p = to_app(q->get_pattern(i)); - auto q1 = m_matcher.compile_ho_pattern(q, p); + auto [q1, p1] = m_matcher.compile_ho_pattern(q, p); ptr_vector ground; mam::ground_subterms(p, ground); + if (p1 != p) + mam::ground_subterms(p1, ground); for (expr* g : ground) mk_enode(g); - m_mam->add_pattern(q1, p); + m_mam->add_pattern(q, p); + if (p != p1) + m_mam->add_pattern(q1, p1); } m_q2dep.insert(q, { pr, d}); get_trail().push(insert_obj_map(m_q2dep, q)); } add_rule(f, pr, d); + if (!is_forall(f) && !m.is_implies(f) && m_side_condition_solver) + m_side_condition_solver->add_constraint(f, pr, d); } - if (m_side_condition_solver) - m_side_condition_solver->add_constraint(f, pr, d); } lbool completion::eval_cond(expr* f, proof_ref& pr, expr_dependency*& d) { @@ -357,6 +382,7 @@ namespace euf { body.push_back(x); flatten_and(body); unsigned j = 0; + flet _propagate_with_solver(m_propagate_with_solver, true); for (auto f : body) { switch (eval_cond(f, pr_i, d)) { diff --git a/src/tactic/portfolio/euf_completion_tactic.cpp b/src/tactic/portfolio/euf_completion_tactic.cpp index a2d00ff74..f9a799948 100644 --- a/src/tactic/portfolio/euf_completion_tactic.cpp +++ b/src/tactic/portfolio/euf_completion_tactic.cpp @@ -79,6 +79,7 @@ public: bool is_true(expr* f, proof_ref& pr, expr_dependency*& d) override { d = nullptr; + init_solver(); solver::scoped_push _sp(*m_solver); m_fmls.reset(); m_fmls.push_back(m.mk_not(f)); @@ -113,6 +114,7 @@ public: } void solve_for(vector& sol) override { + init_solver(); vector ss; for (auto [v, t, g] : sol) ss.push_back({ v, t, g });