From 1d425e55cd7e7b8547446b1423c23828ec8f73a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Jul 2026 19:16:07 -0700 Subject: [PATCH] bug fixes to ho_matching - offset alignment inv_var_shift, callback scopes should not be nested, allow bindings that are not ground Signed-off-by: Nikolaj Bjorner --- src/ast/euf/ho_matcher.cpp | 17 +++++------- src/smt/smt_quantifier.cpp | 54 +++++++++++++++++++++++++++----------- src/smt/smt_relevancy.cpp | 2 +- src/util/debug.cpp | 35 ++++++++++++++++++++++++ 4 files changed, 80 insertions(+), 28 deletions(-) diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index 03eb319614..5c48f77435 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -473,15 +473,6 @@ namespace euf { } } - // pat_vars[k] references the lambda binder for the k-th distinct - // index and must carry that index' sort, so the reconstructed - // select stays aligned with the flex head's array domain - // (pat_domain). The binder at forward position p has de Bruijn - // index num_bound-1-p (the outermost binder has the highest - // index). Emitting in forward slot order keeps the select - // arguments in the same order as pat_domain even when the - // indices have heterogeneous sorts (otherwise the array plugin - // rejects the ill-ordered select). for (unsigned k = 1; k < pat_args.size(); ++k) { unsigned db = num_bound - 1 - pat_pos[k]; pat_vars.push_back(m.mk_var(db, pat_args.get(k)->get_sort())); @@ -685,11 +676,15 @@ namespace euf { SASSERT(is_well_sorted(m, body)); } - void ho_matcher::add_binding(var* v, unsigned offset, expr* t) { + void ho_matcher::add_binding(var* v, unsigned offset, expr* _t) { SASSERT(v->get_idx() >= offset); + expr_ref t(_t, m); + inv_var_shifter vs(m); + vs(_t, offset, t); m_subst.set(v->get_idx() - offset, t); + SASSERT(is_well_sorted(m, t)); 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";); + TRACE(ho_matching, tout << "ho_matcher::add_binding: " << offset << " v" << v->get_idx() - offset << " -> " << mk_pp(t, m) << "\n";); m_trail.push(undo_set(m_subst, v->get_idx() - offset)); } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 57702daf32..26d2fa4919 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -21,6 +21,8 @@ Revision History: #include "ast/quantifier_stat.h" #include "ast/euf/ho_matcher.h" #include "ast/rewriter/var_subst.h" +#include "ast/well_sorted.h" +#include "ast/has_free_vars.h" #include "smt/smt_quantifier.h" #include "smt/smt_context.h" #include "smt/smt_model_finder.h" @@ -620,6 +622,7 @@ namespace smt { unsigned m_min_top_generation = 0; unsigned m_max_top_generation = 0; vector>* m_used_enodes = nullptr; + vector> m_matches; }; ho_match_state m_ho_state; unsigned m_stat_ho_refine = 0; // number of times ho-matching refinement is invoked @@ -660,11 +663,11 @@ namespace smt { quantifier_manager_plugin * mk_fresh() override { return alloc(default_qm_plugin); } - void on_ho_match(euf::ho_subst& s) { - ast_manager& m = m_context->get_manager(); - auto& st = m_ho_state; - auto* hoq = st.m_q; - auto* q = m_ho_matcher->hoq2q(hoq); + void on_ho_match(euf::ho_subst &s) { + ast_manager &m = m_context->get_manager(); + auto &st = m_ho_state; + auto *hoq = st.m_q; + auto *q = m_ho_matcher->hoq2q(hoq); expr_ref_vector binding(m); for (unsigned i = 0; i < s.size(); ++i) @@ -674,9 +677,14 @@ 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";); + TRACE( + ho_matching, tout << "num bound variables " << q->get_num_decls() << " for " << mk_bounded_pp(q, m) + << "\n" + << binding << "\n"; + for (unsigned i = 0; i < binding.size(); ++i) { + tout << i << " - " << mk_pp(binding.get(i)->get_sort(), m) << ": " << mk_ll_pp(binding.get(i), m) + << "\n"; + }); if (binding.size() > q->get_num_decls()) { // binding is indexed directly (binding[k] = value for var k), // so the substitution must use direct (non-standard) order to @@ -686,16 +694,18 @@ namespace smt { bool change = true; while (change) { change = false; - for (unsigned i = 1; i < binding.size(); ++i) { - if (!binding.get(i)) continue; + for (unsigned i = 0; i < binding.size(); ++i) { + if (!binding.get(i)) + continue; // A misaligned higher-order binding would build an // ill-sorted term. Abandon this refinement (no instance) // rather than aborting the whole solve. - if (!euf::ho_matcher::subst_sorts_match(m, binding.get(i), binding, false)) - return; + SASSERT(is_well_sorted(m, binding.get(i))); auto r = sub(binding.get(i), binding); change |= r != binding.get(i); binding[i] = r; + SASSERT(is_well_sorted(m, binding.get(i))); + TRACE(ho_matching, tout << "setting v" << i << " <- " << r << "\n"); } } binding.shrink(q->get_num_decls()); @@ -705,16 +715,26 @@ namespace smt { binding.reverse(); + st.m_matches.push_back({ q, binding }); + } + + void consume_ho_matches() { + for (auto const &[q, binding] : m_ho_state.m_matches) + consume_ho_match(q, binding); + m_ho_state.m_matches.reset(); + } + + void consume_ho_match(quantifier * q, expr_ref_vector const& binding) { + ast_manager &m = m_context->get_manager(); + auto &st = m_ho_state; // Create enodes for the refined bindings and add instance ptr_buffer new_bindings; unsigned max_gen = st.m_max_generation; + TRACE(ho_matching, tout << binding << "\n"); for (expr* e : binding) { if (!e) return; // incomplete binding - // A leftover free (de Bruijn) variable means the binding is - // incomplete/misaligned; adding such a term would raise - // "Formulas should not contain unbound variables". Skip it. - if (!is_ground(e)) + if (has_free_vars(e)) return; if (!m_context->e_internalized(e)) { m_context->internalize(e, false); @@ -760,12 +780,14 @@ namespace smt { m_ho_state.m_min_top_generation = min_top_gen; m_ho_state.m_max_top_generation = max_top_gen; m_ho_state.m_used_enodes = &used_enodes; + m_ho_state.m_matches.reset(); IF_VERBOSE(10, verbose_stream() << "try_ho_refine: q=" << mk_pp(qa, m) << "\n pat=" << mk_pp(pat, m) << "\n"; for (unsigned i = 0; i < num_bindings; ++i) verbose_stream() << " s[" << i << "] = " << mk_pp(s.get(i), m) << " sort=" << mk_pp(s.get(i)->get_sort(), m) << "\n";); m_ho_matcher->refine_ho_match(pat, s); + consume_ho_matches(); ++m_stat_ho_refine; return true; } diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index fcaf604558..0a7db2cb94 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -267,7 +267,7 @@ namespace smt { } } - bool is_relevant_core(expr * n) const { return m_is_relevant.contains(n->get_id()); } + bool is_relevant_core(expr * n) const { SASSERT(n); return m_is_relevant.contains(n->get_id()); } bool is_relevant(expr * n) const override { return !enabled() || is_relevant_core(n); diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 9cdc0472d2..4a2141c024 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -36,11 +36,46 @@ bool assertions_enabled() { return g_enable_assertions; } +#if defined(_WINDOWS) +#include +#include +#pragma comment(lib, "dbghelp.lib") +static void print_windows_backtrace() { + HANDLE process = GetCurrentProcess(); + SymSetOptions(SYMOPT_LOAD_LINES | SYMOPT_DEFERRED_LOADS | SYMOPT_UNDNAME); + SymInitialize(process, nullptr, TRUE); + void * stack[64]; + USHORT frames = RtlCaptureStackBackTrace(0, 64, stack, nullptr); + char buf[sizeof(SYMBOL_INFO) + 256 * sizeof(char)]; + SYMBOL_INFO * sym = reinterpret_cast(buf); + sym->SizeOfStruct = sizeof(SYMBOL_INFO); + sym->MaxNameLen = 255; + IMAGEHLP_LINE64 line64; + line64.SizeOfStruct = sizeof(IMAGEHLP_LINE64); + std::cerr << "----- backtrace -----\n"; + for (USHORT i = 0; i < frames; i++) { + DWORD64 addr = reinterpret_cast(stack[i]); + const char * name = "?"; + if (SymFromAddr(process, addr, nullptr, sym)) + name = sym->Name; + DWORD disp = 0; + std::cerr << i << ": " << name; + if (SymGetLineFromAddr64(process, addr, &disp, &line64)) + std::cerr << " (" << line64.FileName << ":" << line64.LineNumber << ")"; + std::cerr << "\n"; + } + std::cerr << "---------------------\n"; +} +#endif + void notify_assertion_violation(const char * fileName, int line, const char * condition) { std::cerr << "ASSERTION VIOLATION\n" "File: " << fileName << "\n" "Line: " << line << '\n' << condition << '\n'; +#if defined(_WINDOWS) + print_windows_backtrace(); +#endif #ifndef Z3DEBUG std::cerr << Z3_FULL_VERSION "\n" "Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new\n";