mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

fix loop bug in ho_matching and add throttle configurations

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-07 09:20:14 -07:00
parent d9d3be959c
commit b2f0d0682a
7 changed files with 35 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/euf/ho_matcher.cpp
View file

@ -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;
}

6
src/ast/euf/ho_matcher.h
View file

@ -315,6 +315,8 @@ namespace euf {
match_goals m_goals;
unitary_patterns m_unitary;
ptr_vector<match_goal> 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<app, app*> m_pat2hopat, m_hopat2pat;
@ -386,6 +388,10 @@ namespace euf {
void set_on_match(std::function<void(ho_subst&)>& 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);

2
src/params/smt_params.cpp
View file

@ -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<phase_selection>(p.phase_selection());

2
src/params/smt_params.h
View file

@ -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;

2
src/params/smt_params_helper.pyg
View file

@ -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'),

9
src/smt/smt_model_finder.cpp
View file

@ -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)

1
src/smt/smt_quantifier.cpp
View file

@ -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<void(euf::ho_subst&)> on_match = [this](euf::ho_subst& s) {
on_ho_match(s);
};