From 0b56db7f0773f43ee2ff9e19c91aed0b889e434a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 May 2026 09:01:48 -0700 Subject: [PATCH] fix #9657 --- src/ast/euf/ho_matcher.cpp | 9 +++++---- src/ast/euf/ho_matcher.h | 7 +++++-- src/ast/rewriter/rewriter_def.h | 2 +- src/smt/smt_quantifier.cpp | 14 ++++++++++---- 4 files changed, 21 insertions(+), 11 deletions(-) diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index b44f5888a..38787a9c9 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -92,7 +92,7 @@ namespace euf { while (!m_backtrack.empty()) { auto& wi = *m_backtrack.back(); bool st = consume_work(wi); - IF_VERBOSE(3, display(verbose_stream() << "ho_matcher::consume_work: " << wi.pat << " =?= " << wi.t << " -> " << (st?"true":"false") << "\n");); + TRACE(ho_matching, display(tout << "ho_matcher::consume_work: " << mk_bounded_pp(wi.pat, m) << " =?= " << mk_bounded_pp(wi.t, m) << " -> " << (st?"true":"false") << "\n");); if (st) { if (m_goals.empty()) m_on_match(m_subst); @@ -653,7 +653,8 @@ namespace euf { void ho_matcher::add_binding(var* v, unsigned offset, expr* t) { SASSERT(v->get_idx() >= offset); m_subst.set(v->get_idx() - offset, t); - IF_VERBOSE(10, verbose_stream() << "ho_matcher::add_binding: v" << v->get_idx() - offset << " -> " << mk_pp(t, m) << "\n";); + SASSERT(v->get_sort() == t->get_sort()); + TRACE(ho_matching, tout << "ho_matcher::add_binding: v" << v->get_idx() - offset << " -> " << mk_pp(t, m) << "\n";); m_trail.push(undo_set(m_subst, v->get_idx() - offset)); } @@ -821,13 +822,13 @@ namespace euf { m_subst.set(idx, s.get(i)); } - IF_VERBOSE(10, verbose_stream() << "refine " << mk_pp(p, m) << "\n" << s << "\n"); + TRACE(ho_matching, tout << "refine " << mk_pp(p, m) << "\n" << s << "\n"); unsigned num_bound = 0, level = 0; for (auto [v, pat] : m_pat2abs[fo_pat]) { var_subst sub(m, true); auto pat_refined = sub(pat, s); - IF_VERBOSE(10, verbose_stream() << mk_pp(pat, m) << " -> " << pat_refined << "\n"); + TRACE(ho_matching, tout << mk_pp(pat, m) << " -> " << pat_refined << "\n"); m_goals.push(level, num_bound, pat_refined, m_subst.get(v)); } diff --git a/src/ast/euf/ho_matcher.h b/src/ast/euf/ho_matcher.h index 82f64ef3f..a0a28d7b9 100644 --- a/src/ast/euf/ho_matcher.h +++ b/src/ast/euf/ho_matcher.h @@ -25,6 +25,7 @@ Author: #include "ast/for_each_expr.h" #include "ast/reg_decl_plugins.h" #include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" #include "ast/rewriter/array_rewriter.h" #include "ast/rewriter/var_subst.h" @@ -88,13 +89,15 @@ namespace euf { } match_goal(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t) noexcept : - base_offset(offset), pat(pat), t(t), level(level) {} + base_offset(offset), pat(pat), t(t), level(level) { + SASSERT(pat->get_sort() == t->get_sort()); + } unsigned term_offset() const { return base_offset + delta_offset; } unsigned pat_offset() const { return base_offset + delta_offset; } std::ostream& display(std::ostream& out) const { - return out << "[" << level << ":" << base_offset + delta_offset << "] " << pat << " ~ " << t << "\n"; + return out << "[" << level << ":" << base_offset + delta_offset << "] " << mk_bounded_pp(pat, pat.m()) << " ~ " << mk_bounded_pp(t, t.m()) << "\n"; } }; diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 7a395006d..ad4702de5 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -668,7 +668,7 @@ template void rewriter_tpl::display_bindings(std::ostream& out) { for (unsigned i = 0; i < m_bindings.size(); ++i) { if (m_bindings[i]) - out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << ";\n"; + out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << " : " << mk_pp(m_bindings[i]->get_sort(), m()) << ";\n"; } } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index c96d741ce..3bfa45785 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -677,12 +677,15 @@ namespace smt { // The HO quantifier has extra vars at higher indices; drop them. // Binding is indexed by var index: binding[i] = value for var i. // First substitute any remaining vars, then keep only original vars. + TRACE(ho_matching, tout << "num bound variables " << q->get_num_decls() << " for " << mk_bounded_pp(q, m) + << "\n" + << binding << "\n";); if (binding.size() > q->get_num_decls()) { var_subst sub(m); bool change = true; while (change) { change = false; - for (unsigned i = 0; i < binding.size(); ++i) { + for (unsigned i = 1; i < binding.size(); ++i) { if (!binding.get(i)) continue; auto r = sub(binding.get(i), binding); change |= r != binding.get(i); @@ -691,12 +694,15 @@ namespace smt { } binding.shrink(q->get_num_decls()); } + if (binding.size() < q->get_num_decls()) + return; + + binding.reverse(); // Create enodes for the refined bindings and add instance ptr_buffer new_bindings; unsigned max_gen = st.m_max_generation; - for (unsigned i = 0; i < q->get_num_decls(); ++i) { - expr* e = binding.get(i); + for (expr* e : binding) { if (!e) return; // incomplete binding if (!m_context->e_internalized(e)) { @@ -711,7 +717,7 @@ namespace smt { TRACE(ho_matching, tout << "ho_match refined for " << mk_pp(q, m) << "\n"; for (unsigned i = 0; i < new_bindings.size(); ++i) - tout << " binding[" << i << "] = " << mk_pp(new_bindings[i]->get_expr(), m) << "\n";); + tout << " binding[" << i << "] = " << mk_bounded_pp(new_bindings[i]->get_expr(), m) << "\n";); vector> used_enodes; m_context->add_instance(q, nullptr, new_bindings.size(), new_bindings.data(),