diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index a740167ad3..e52a65144c 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -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 domain, pat_domain; ptr_vector 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 es; + svector 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"); diff --git a/src/ast/euf/ho_matcher.h b/src/ast/euf/ho_matcher.h index 0235559261..e513332fe2 100644 --- a/src/ast/euf/ho_matcher.h +++ b/src/ast/euf/ho_matcher.h @@ -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]; } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 311c7a82d5..3af5953a96 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -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); }