mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 11:35:42 +00:00
Code Activity

fix HO-matcher imitation curry-order and instance-assembly ordering bugs

Browse source 
The higher-order matcher produced ill-typed instantiations that aborted
the solve (sort-mismatch / unbound-variable exceptions), making
smt.ho_matching=true net-negative on the TPTP THF benchmarks.

Two root causes:

1. Imitation rule (ho_matcher.cpp): the select chain 'pats' is collected
   outermost-first, i.e. in reverse application order. The imitating
   lambda must curry arguments in application order (first-applied select
   binds the outermost lambda). Reversing 'pats' before building the
   domain/argument/body vectors and the lambda-wrapping loop makes the
   constructed lambda's sort agree with the flex head variable. Fixes
   unit-test ho_matcher test6c/test6d (previously asserted at
   add_binding: v->get_sort() == t->get_sort()).

2. Instance assembly (smt_quantifier.cpp on_ho_match): the fixpoint
   binding substitution used var_subst with the default std_order=true
   while the binding vector is directly indexed (binding[k] = value for
   var k). This resolved chained HO variable references against the wrong
   slots and built ill-sorted terms (assertion at rewriter_def.h:52).
   Use direct (std_order=false) substitution to match the binding layout.

Also adds defensive guards as belt-and-suspenders: subst_sorts_match
skips sort-inconsistent substitutions, an is_ground check skips bindings
with leftover de Bruijn variables, and on_ho_match catches z3_exception
to skip an unusable heuristic instance rather than aborting the solve
(re-raising only on cancellation/resource-limit).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-05 17:25:01 -07:00
parent 72d27e1cbb
commit 6c8a5cd853
3 changed files with 91 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -421,6 +421,16 @@ namespace euf {
// H (p1) (p2) = f(t1, .., tn)
// H -> \x1 \x2 f(H1(x1, x2), .., Hn(x1, x2))
// H1(p1, p2) = t1, .., Hn(p1, p2) = tn
//
// The select chain `pats` was collected from the outermost
// select down to the flex head, i.e. in reverse order of
// application. The imitating lambda must curry the arguments in
// application order (the first-applied select binds the
// outermost lambda), so process the applications inner-to-outer.
// Without this the constructed lambda has the argument arities
// in the wrong nesting order and its sort disagrees with the
// flex head variable (producing an ill-typed binding).
pats.reverse();
ptr_vector<sort> domain, pat_domain;
ptr_vector<expr> pat_args;
expr_ref_vector args(m), pat_vars(m), bound_args(m);
@ -824,6 +834,16 @@ namespace euf {
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]) {
// Defensive: if the abstraction-variable indices in the stored
// pattern do not line up (sort-wise) with the current substitution,
// building the refined term would be ill-typed and abort the solve.
// Skip the whole refinement; a missed heuristic instance is sound.
if (!subst_sorts_match(m, pat, s, true)) {
m_trail.pop_scope(1);
return;
}
}
for (auto [v, pat] : m_pat2abs[fo_pat]) {
var_subst sub(m, true);
auto pat_refined = sub(pat, s);
@ -835,6 +855,41 @@ namespace euf {
m_trail.pop_scope(1);
}
bool ho_matcher::subst_sorts_match(ast_manager& m, expr* t, expr_ref_vector const& s, bool std_order) {
unsigned sz = s.size();
ptr_buffer<expr> es;
svector<unsigned> offs;
es.push_back(t);
offs.push_back(0);
while (!es.empty()) {
expr* e = es.back(); es.pop_back();
unsigned off = offs.back(); offs.pop_back();
if (is_var(e)) {
unsigned idx = to_var(e)->get_idx();
if (idx < off)
continue;
unsigned k = idx - off;
if (k >= sz)
continue;
expr* r = std_order ? s.get(sz - k - 1) : s.get(k);
if (r && r->get_sort() != e->get_sort())
return false;
}
else if (is_app(e)) {
for (expr* arg : *to_app(e)) {
es.push_back(arg);
offs.push_back(off);
}
}
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
es.push_back(q->get_expr());
offs.push_back(off + q->get_num_decls());
}
}
return true;
}
std::ostream& ho_matcher::display(std::ostream& out) const {
m_subst.display(out << "subst\n");
m_goals.display(out << "goals\n");

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

@ -400,6 +400,13 @@ namespace euf {
void refine_ho_match(app* p, expr_ref_vector& s);
// Returns true iff applying the substitution s to t (with the given
// variable ordering) is sort-safe: every free variable of t that is
// bound by s maps to a value of the same sort. Used to defensively
// skip higher-order matches whose bindings would produce ill-typed
// instantiation terms (which would otherwise abort the whole solve).
static bool subst_sorts_match(ast_manager& m, expr* t, expr_ref_vector const& s, bool std_order);
bool is_free(app* p, unsigned i) const { return m_hopat2free_vars[p].contains(i); }
quantifier* hoq2q(quantifier* q) const { return m_hoq2q[q]; }

30
src/smt/smt_quantifier.cpp
View file

@ -667,6 +667,21 @@ 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();
try {
on_ho_match_core(s);
}
catch (z3_exception &) {
// A higher-order binding produced an ill-typed or otherwise
// unusable instantiation term. Adding a heuristic HO instance is
// optional, so we skip this match rather than aborting the solve.
// Re-raise only if the failure was due to cancellation/resource limits.
if (!m.inc())
throw;
}
}
void on_ho_match_core(euf::ho_subst& s) {
ast_manager& m = m_context->get_manager();
auto& st = m_ho_state;
auto* hoq = st.m_q;
@ -684,12 +699,20 @@ namespace smt {
<< "\n"
<< binding << "\n";);
if (binding.size() > q->get_num_decls()) {
var_subst sub(m);
// binding is indexed directly (binding[k] = value for var k),
// so the substitution must use direct (non-standard) order to
// resolve chained HO variable references; the sort guard below
// is checked with the matching order.
var_subst sub(m, false);
bool change = true;
while (change) {
change = false;
for (unsigned i = 1; i < binding.size(); ++i) {
if (!binding.get(i)) continue;
// Skip ill-typed substitutions: a misaligned higher-order
// binding would build an ill-sorted term and abort the solve.
if (!euf::ho_matcher::subst_sorts_match(m, binding.get(i), binding, false))
return;
auto r = sub(binding.get(i), binding);
change |= r != binding.get(i);
binding[i] = r;
@ -708,6 +731,11 @@ namespace smt {
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))
return;
if (!m_context->e_internalized(e)) {
m_context->internalize(e, false);
}