From b2f0d0682aaef74c6b9c62419c2ff28912c8168f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Jul 2026 09:20:14 -0700 Subject: [PATCH] fix loop bug in ho_matching and add throttle configurations --- src/ast/euf/ho_matcher.cpp | 14 ++++++++++++++ src/ast/euf/ho_matcher.h | 6 ++++++ src/params/smt_params.cpp | 2 ++ src/params/smt_params.h | 2 ++ src/params/smt_params_helper.pyg | 2 ++ src/smt/smt_model_finder.cpp | 9 ++++++++- src/smt/smt_quantifier.cpp | 1 + 7 files changed, 35 insertions(+), 1 deletion(-) diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index 4a793e2159..03eb319614 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -67,7 +67,15 @@ namespace euf { void ho_matcher::search() { IF_VERBOSE(10, display(verbose_stream())); + + unsigned budget = m_max_iterations; while (m.inc()) { + if (budget-- == 0) { + IF_VERBOSE(2, verbose_stream() << "ho_matcher: search budget exhausted\n"); + while (!m_backtrack.empty()) + backtrack(); + break; + } // Q, B -> Q', B'. Push work on the backtrack stack and new work items // e, Bw -> Q', B'. Consume backtrack stack if (!m_goals.empty()) @@ -271,6 +279,11 @@ namespace euf { if (wi.is_done()) return false; + if (wi.level > m_max_depth) { + wi.set_done(); + return false; + } + reduce(wi); auto t = wi.t; @@ -349,6 +362,7 @@ namespace euf { if (qp->get_decl_sort(i) != qt->get_decl_sort(i)) return false; m_goals.push(wi.level, wi.term_offset() + td, qp->get_expr(), qt->get_expr()); + wi.set_done(); return true; } diff --git a/src/ast/euf/ho_matcher.h b/src/ast/euf/ho_matcher.h index e513332fe2..1c952bcbbd 100644 --- a/src/ast/euf/ho_matcher.h +++ b/src/ast/euf/ho_matcher.h @@ -315,6 +315,8 @@ namespace euf { match_goals m_goals; unitary_patterns m_unitary; ptr_vector m_backtrack; + unsigned m_max_depth = 10; // bound on imitation/projection depth (secondary safety cap) + unsigned m_max_iterations = 10000; // per-search expansion-step budget to guarantee termination mutable array_rewriter m_rewriter; array_util m_array; obj_map m_pat2hopat, m_hopat2pat; @@ -386,6 +388,10 @@ namespace euf { void set_on_match(std::function& on_match) { m_on_match = on_match; } + void set_max_depth(unsigned d) { m_max_depth = d; } + + void set_max_iterations(unsigned n) { m_max_iterations = n; } + void operator()(expr *pat, expr *t, unsigned num_vars); void operator()(expr* pat, expr* t, unsigned num_bound, unsigned num_vars); diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index a64075204c..bd58aeb311 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -28,6 +28,8 @@ void smt_params::updt_local_params(params_ref const & _p) { m_relevancy_lvl = p.relevancy(); m_ematching = p.ematching(); m_ho_matching = p.ho_matching(); + m_ho_matching_bound = p.ho_matching_bound(); + m_term_enumeration = p.term_enumeration(); m_induction = p.induction(); m_clause_proof = p.clause_proof(); m_phase_selection = static_cast(p.phase_selection()); diff --git a/src/params/smt_params.h b/src/params/smt_params.h index 7b5efa9919..3d696504ee 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -110,6 +110,8 @@ struct smt_params : public preprocessor_params, bool m_new_core2th_eq = true; bool m_ematching = true; bool m_ho_matching = false; + unsigned m_ho_matching_bound = 10000; + bool m_term_enumeration = true; bool m_induction = false; bool m_clause_proof = false; symbol m_proof_log; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index d3f164f3bb..8dc181a2f9 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -11,6 +11,8 @@ def_module_params(module_name='smt', ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'), ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'), ('ho_matching', BOOL, False, 'higher-order matching for quantifier instantiation'), + ('ho_matching_bound', UINT, 10000, 'per-problem expansion-step budget of the higher-order matching search; bounds the (undecidable) HO unification to guarantee termination'), + ('term_enumeration', BOOL, True, 'use term enumeration to populate instantiation sets for higher-order variables during model-based quantifier instantiation'), ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory'), ('phase_caching_on', UINT, 400, 'number of conflicts while phase caching is on'), ('phase_caching_off', UINT, 100, 'number of conflicts while phase caching is off'), diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 4d06e09d71..62fab4b14c 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1411,10 +1411,14 @@ namespace smt { } void populate_inst_sets(quantifier *q, auf_solver &s, context *ctx) override { + bool use_term_enum = ctx->get_fparams().m_term_enumeration; + if (!use_term_enum) + return; node *S = s.get_uvar(q, m_var_i); sort *srt = S->get_sort(); IF_VERBOSE(3, verbose_stream() << "ho_var::populate_inst_sets: " << q->get_id() << " " << mk_pp(srt, m) << "\n";); + term_enumeration tn(m); // Add ground terms of type S. // Add productions for functions in E-graph @@ -1423,6 +1427,7 @@ namespace smt { ast_mark visited; tn.add_production(m.mk_true()); tn.add_production(m.mk_false()); + for (enode *n : ctx->enodes()) { if (!ctx->is_relevant(n)) continue; @@ -1431,6 +1436,8 @@ namespace smt { TRACE(model_finder, tout << "inserting " << mk_pp(e, m) << " into inst set\n"); S->insert(e, n->get_generation()); } + else if (!use_term_enum) + continue; else if (is_app(e) && to_app(e)->get_decl()->is_skolem()) ; else if (is_uninterp_const(e)) { @@ -1446,7 +1453,7 @@ namespace smt { tn.add_production(f); } } - + unsigned max_count = 20; for (auto t : tn.enum_terms(srt)) { if (max_count == 0) diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index b7dcb70623..156f9ef80a 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -657,6 +657,7 @@ namespace smt { if (m_fparams->m_ho_matching) { m_ho_matcher = alloc(euf::ho_matcher, m, m_context->get_trail_stack()); + m_ho_matcher->set_max_iterations(m_fparams->m_ho_matching_bound); std::function on_match = [this](euf::ho_subst& s) { on_ho_match(s); };