diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index e52a65144..4a793e215 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -43,6 +43,7 @@ Author: --*/ #include "ast/euf/ho_matcher.h" +#include "ast/well_sorted.h" @@ -373,6 +374,9 @@ namespace euf { pats.push_back(to_app(p1)); p1 = to_app(p1)->get_arg(0); } + // innermost select is a meta variable, + // order patterns from inner-most application to outer-most. + pats.reverse(); auto v = to_var(p1); if (wi.is_init()) wi.set_project(); @@ -430,32 +434,44 @@ namespace euf { // 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; + svector pat_pos; // forward binder position (in domain) of each distinct index expr_ref_vector args(m), pat_vars(m), bound_args(m); vector names; pat_args.push_back(nullptr); pat_vars.push_back(nullptr); + pat_pos.push_back(0); // placeholder for the flex-head slot 0 unsigned num_bound = 0; expr_mark seen; for (auto pat : pats) { for (auto pi : array_select_indices(pat)) { + if (!seen.is_marked(pi)) { + pat_domain.push_back(pi->get_sort()); + pat_args.push_back(pi); + pat_pos.push_back(num_bound); + seen.mark(pi); + } ++num_bound; domain.push_back(pi->get_sort()); names.push_back(symbol(num_bound)); - if (seen.is_marked(pi)) - continue; - pat_domain.push_back(pi->get_sort()); - pat_args.push_back(pi); - seen.mark(pi); } } - for (unsigned i = pat_args.size(); i-- > 1; ) { - auto pi = pat_args.get(i); - pat_vars.push_back(m.mk_var(pat_args.size() - i - 1, pi->get_sort())); - } + // 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())); + } for (auto ti : *ta) { sort* v_sort = m_array.mk_array_sort(pat_domain.size(), pat_domain.data(), ti->get_sort()); @@ -463,7 +479,8 @@ namespace euf { auto w = m.mk_var(m_subst.size() + wi.pat_offset() + num_bound, v_sort); // shifted by number of bound m_subst.resize(m_subst.size() + 1); pat_args[0] = v; - auto sel = m_array.mk_select(pat_args.size(), pat_args.data()); + expr_ref sel(m); + sel = m_array.mk_select(pat_args.size(), pat_args.data()); m_goals.push(wi.level + 1, wi.term_offset(), sel, ti); pat_vars[0] = w; sel = m_array.mk_select(pat_vars.size(), pat_vars.data()); @@ -479,6 +496,7 @@ namespace euf { num_bound -= sz; lam = m.mk_lambda(sz, domain.data() + num_bound, names.data() + num_bound, lam); } + add_binding(v, wi.pat_offset(), lam); wi.set_done(); return true; @@ -591,6 +609,7 @@ namespace euf { } lam = m.mk_lambda(names.size(), sorts.data(), names.data(), lam); } + SASSERT(is_well_sorted(m, lam)); return lam; } @@ -632,6 +651,8 @@ namespace euf { SASSERT(var_sort); body = m.mk_var(num_binders - i - 1, var_sort); bind_lambdas(num_lambdas, s, body); + SASSERT(body->get_sort() == s); + SASSERT(is_well_sorted(m, body)); return body; } @@ -646,6 +667,8 @@ namespace euf { decl_names.push_back(symbol(i)); } body = m.mk_lambda(sz, decl_sorts.data(), decl_names.data(), body); + SASSERT(s == body->get_sort()); + SASSERT(is_well_sorted(m, body)); } void ho_matcher::add_binding(var* v, unsigned offset, expr* t) { @@ -665,7 +688,6 @@ namespace euf { } auto is_ho = any_of(subterms::all(expr_ref(p, m)), [&](expr* t) { return m_unitary.is_flex(0, t) || - // m.is_lambda_def(t) || is_lambda(t); }); if (!is_ho) @@ -684,8 +706,7 @@ namespace euf { todo.pop_back(); continue; } - if ((m_unitary.is_flex(0, t) && lvl > 1) || // m.is_lambda_def(t) || - is_lambda(t)) { + if ((m_unitary.is_flex(0, t) && lvl > 1) || is_lambda(t)) { if (!contains_pat2abs) m_pat2abs.insert_if_not_there(p, svector>()).push_back({ nb, t }); auto v = m.mk_var(nb++, t->get_sort()); @@ -817,6 +838,7 @@ namespace euf { auto& abs = m_pat2abs[fo_pat]; verbose_stream() << " m_pat2abs size: " << abs.size() << "\n"; for (auto [v, pat] : abs) verbose_stream() << " v=" << v << " pat=" << mk_pp(pat, m) << "\n";); + unsigned base_scope = m_trail.get_num_scopes(); m_trail.push_scope(); m_subst.resize(0); m_subst.resize(s.size()); @@ -835,12 +857,18 @@ namespace euf { 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 a binding's sort disagrees with the pattern variable it would + // fill, substituting it would build an ill-sorted term. This can + // arise for deeply nested multi-select patterns whose de Bruijn + // remapping does not line up, or when E-matching delivers a + // candidate binding whose sort is incompatible with the abstracted + // higher-order pattern. Discard this refinement candidate (produce + // no instance) instead of aborting the whole solve. if (!subst_sorts_match(m, pat, s, true)) { m_trail.pop_scope(1); + IF_VERBOSE(0, verbose_stream() << "refine_ho_match: sorts do not match for " << mk_pp(pat, m) << " and " + << s << "\n";); + UNREACHABLE(); return; } } @@ -850,8 +878,8 @@ namespace euf { TRACE(ho_matching, tout << mk_pp(pat, m) << " -> " << pat_refined << "\n"); m_goals.push(level, num_bound, pat_refined, m_subst.get(v)); } - search(); + m_trail.pop_scope(1); } @@ -908,6 +936,7 @@ namespace euf { }; void match_goals::push(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t) { + SASSERT(pat->get_sort() == t->get_sort()); match_goal* wi = new (ho.trail().get_region()) match_goal(level, offset, pat, t); ho.trail().push(retire_match_goal(*wi)); // reset on undo wi->init(wi); diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 5d3ddf1dd..55135ba59 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -21,6 +21,7 @@ Notes: #include "ast/ast_util.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" +#include "ast/well_sorted.h" #include "ast/rewriter/var_subst.h" #include "params/array_rewriter_params.hpp" #include "util/util.h" @@ -818,6 +819,7 @@ expr_ref array_rewriter::expand_store(expr* s) { result = m().mk_ite(mk_and(eqs), tmp, result); } result = m().mk_lambda(sorts.size(), sorts.data(), names.data(), result); + SASSERT(is_well_sorted(m(), result)); return result; } diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index ad4702de5..b9e4b4f27 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -21,6 +21,7 @@ Notes: #include "ast/rewriter/rewriter.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" +#include "ast/well_sorted.h" #include "ast/ast_pp.h" template @@ -552,6 +553,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { SASSERT(fr.m_spos + num_children == result_stack().size()); expr * const * it = result_stack().data() + fr.m_spos; expr * new_body = *it; + SASSERT(is_well_sorted(m_manager, q)); unsigned num_pats = q->get_num_patterns(); unsigned num_no_pats = q->get_num_no_patterns(); expr_ref_vector new_pats(m_manager, num_pats, q->get_patterns()); @@ -604,6 +606,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { if (!m_cfg.reduce_quantifier(q, new_body, new_pats.data(), new_no_pats.data(), m_r, m_pr)) { if (fr.m_new_child) { m_r = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body); + SASSERT(is_well_sorted(m(), m_r)); } else { TRACE(rewriter_reuse, tout << "reusing:\n" << mk_ismt2_pp(q, m()) << "\n";); diff --git a/src/ast/well_sorted.cpp b/src/ast/well_sorted.cpp index cb8b8b93d..36aed7215 100644 --- a/src/ast/well_sorted.cpp +++ b/src/ast/well_sorted.cpp @@ -25,31 +25,57 @@ Revision History: #include "util/warning.h" #include "ast/ast_smt2_pp.h" + namespace { struct well_sorted_proc { - ast_manager & m_manager; - bool m_error; + ast_manager & m; + bool m_error; + ptr_vector m_binding; - well_sorted_proc(ast_manager & m):m_manager(m), m_error(false) {} - - void operator()(var * v) {} + well_sorted_proc(ast_manager & m):m(m), m_error(false) {} - void operator()(quantifier * n) { - expr const * e = n->get_expr(); - if (!is_lambda(n) && !m_manager.is_bool(e)) { - warning_msg("quantifier's body must be a boolean."); - m_error = true; - UNREACHABLE(); + void check(expr* e) { + for (auto term : subterms::ground(expr_ref(e, m))) { + if (is_app(term)) + check_app(to_app(term)); + else if (is_var(term)) + check_var(to_var(term)); + else if (is_quantifier(term)) + check_quantifier(to_quantifier(term)); } } - void operator()(app * n) { + void check_quantifier(quantifier * n) { + if (!is_lambda(n) && !m.is_bool(n->get_expr())) { + warning_msg("quantifier's body must be a boolean."); + m_error = true; + // UNREACHABLE(); + } + unsigned sz = m_binding.size(); + m_binding.append(n->get_num_decls(), n->get_decl_sorts()); + check(n->get_expr()); + m_binding.shrink(sz); + } + + void check_var(var* v) { + if (v->get_idx() >= m_binding.size()) { + return; + } + sort *s = m_binding[m_binding.size() - v->get_idx() - 1]; + if (s != v->get_sort()) { + warning_msg("variable sort does not match binding sort."); + m_error = true; + // UNREACHABLE(); + } + } + + void check_app(app * n) { unsigned num_args = n->get_num_args(); func_decl * decl = n->get_decl(); if (num_args != decl->get_arity() && !decl->is_associative() && !decl->is_right_associative() && !decl->is_left_associative()) { - TRACE(ws, tout << "unexpected number of arguments.\n" << mk_ismt2_pp(n, m_manager);); + TRACE(ws, tout << "unexpected number of arguments.\n" << mk_ismt2_pp(n, m);); warning_msg("unexpected number of arguments."); m_error = true; return; @@ -59,19 +85,20 @@ struct well_sorted_proc { sort * actual_sort = n->get_arg(i)->get_sort(); sort * expected_sort = decl->is_associative() ? decl->get_domain(0) : decl->get_domain(i); if (expected_sort != actual_sort) { - TRACE(tc, tout << "sort mismatch on argument #" << i << ".\n" << mk_ismt2_pp(n, m_manager); - tout << "Sort mismatch for argument " << i+1 << " of " << mk_ismt2_pp(n, m_manager, false) << "\n"; - tout << "Expected sort: " << mk_pp(expected_sort, m_manager) << "\n"; - tout << "Actual sort: " << mk_pp(actual_sort, m_manager) << "\n"; - tout << "Function sort: " << mk_pp(decl, m_manager) << "."; + TRACE(tc, tout << "sort mismatch on argument #" << i << ".\n" << mk_ismt2_pp(n, m); + tout << "Sort mismatch for argument " << i+1 << " of " << mk_ismt2_pp(n, m, false) << "\n"; + tout << "Expected sort: " << mk_pp(expected_sort, m) << "\n"; + tout << "Actual sort: " << mk_pp(actual_sort, m) << "\n"; + tout << "Function sort: " << mk_pp(decl, m) << "."; ); std::ostringstream strm; - strm << "Sort mismatch for argument " << i+1 << " of " << mk_ll_pp(n, m_manager, false) << "\n"; - strm << "Expected sort: " << mk_pp(expected_sort, m_manager) << '\n'; - strm << "Actual sort: " << mk_pp(actual_sort, m_manager) << '\n'; - strm << "Function sort: " << mk_pp(decl, m_manager) << '.'; + strm << "Sort mismatch for argument " << i+1 << " of " << mk_ll_pp(n, m, false) << "\n"; + strm << "Expected sort: " << mk_pp(expected_sort, m) << '\n'; + strm << "Actual sort: " << mk_pp(actual_sort, m) << '\n'; + strm << "Function sort: " << mk_pp(decl, m) << '.'; warning_msg("%s", std::move(strm).str().c_str()); m_error = true; + // UNREACHABLE(); return; } } @@ -82,7 +109,11 @@ struct well_sorted_proc { bool is_well_sorted(ast_manager const & m, expr * n) { well_sorted_proc p(const_cast(m)); - for_each_expr(p, n); + p.check(n); + if (p.m_error) { + IF_VERBOSE(0, verbose_stream() << "expression is not well sorted.\n" << mk_pp(n, const_cast(m)) << "\n";); + IF_VERBOSE(0, verbose_stream() << mk_ll_pp(n, const_cast(m)) << "\n";); + } return !p.m_error; } diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 1bfd0e011..8ab6b3167 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -18,6 +18,7 @@ #include "ast/expr_abstract.h" #include "ast/ast_util.h" #include "ast/polymorphism_util.h" +#include "ast/well_sorted.h" #include "ast/rewriter/expr_safe_replace.h" #include "solver/solver.h" #include "cmd_context/cmd_context.h" @@ -2461,6 +2462,7 @@ class tptp_parser { m_has_conjecture = true; f = m.mk_not(f); } + SASSERT(is_well_sorted(m, f)); m_cmd.assert_expr(f); } catch (z3_exception const& ex) { // Sort mismatch or other semantic error in this formula — skip it. diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 423669e0a..4d06e09d7 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -42,10 +42,6 @@ Revision History: namespace smt { - // Instrumentation: counts terms produced by ho_var term-enumeration - // (mf::ho_var::populate_inst_sets). One increment per enumerated term - // inserted into an instantiation set. Reset per model_finder instance. - static unsigned g_ho_var_term_enum = 0; namespace mf { @@ -1173,6 +1169,7 @@ namespace smt { virtual char const* get_kind() const = 0; virtual bool is_equal(qinfo const* qi) const = 0; virtual void display(std::ostream& out) const { out << "[" << get_kind() << "]"; } + virtual void collect_statistics(::statistics &st) const {} // AUF fragment solver virtual void process_auf(quantifier* q, auf_solver& s, context* ctx) = 0; @@ -1385,10 +1382,15 @@ namespace smt { class ho_var : public qinfo { unsigned m_var_i; + unsigned m_ho_var_term_enum = 0; public: ho_var(ast_manager& m, unsigned i) : qinfo(m), m_var_i(i) { } + void collect_statistics(::statistics &st) const override { + st.update("mbqi.ho-var-term-enum", m_ho_var_term_enum); + } + char const *get_kind() const override { return "ho_var"; } @@ -1453,7 +1455,7 @@ namespace smt { unsigned generation = 0; // todo - inherited from sub-term of t? TRACE(model_finder, tout << "ho_var: adding term " << mk_ismt2_pp(t, m) << " to instantiation set of S" << std::endl;); - ++g_ho_var_term_enum; + ++m_ho_var_term_enum; S->insert(t, generation); } } @@ -1779,6 +1781,11 @@ namespace smt { public: typedef ptr_vector::const_iterator macro_iterator; + void collect_statistics(::statistics &st) const { + for (auto *qi : m_qinfo_vect) + qi->collect_statistics(st); + } + static quantifier_ref mk_flat(ast_manager& m, quantifier* q) { if (has_quantifiers(q->get_expr())) { proof_ref pr(m); @@ -2415,7 +2422,6 @@ namespace smt { m_auf_solver(alloc(auf_solver, m)), m_dependencies(m), m_new_constraints(m) { - g_ho_var_term_enum = 0; } model_finder::~model_finder() { @@ -2423,7 +2429,10 @@ namespace smt { } void model_finder::collect_statistics(::statistics & st) const { - st.update("ho-var term-enum", g_ho_var_term_enum); + // Retrieve the ho-var term-enumeration counters from the embedded + // qinfo objects (mf::ho_var) held by each registered quantifier_info. + for (auto const &[k, v] : m_q2info) + v->collect_statistics(st); } void model_finder::checkpoint() { diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 3af5953a9..b7dcb7062 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -657,7 +657,7 @@ namespace smt { if (m_fparams->m_ho_matching) { m_ho_matcher = alloc(euf::ho_matcher, m, m_context->get_trail_stack()); - std::function on_match = [&](euf::ho_subst& s) { + std::function on_match = [this](euf::ho_subst& s) { on_ho_match(s); }; m_ho_matcher->set_on_match(on_match); @@ -667,21 +667,6 @@ 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; @@ -709,8 +694,9 @@ namespace smt { 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. + // 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; auto r = sub(binding.get(i), binding); @@ -770,6 +756,7 @@ namespace smt { for (unsigned i = 0; i < num_bindings; ++i) s.push_back(bindings[i]->get_expr()); + unsigned num_instances = m_stat_ho_instances; m_ho_state.m_q = qa; m_ho_state.m_pat = pat; m_ho_state.m_num_bindings = num_bindings; diff --git a/src/test/ho_matcher.cpp b/src/test/ho_matcher.cpp index dccd8af08..a6dee5891 100644 --- a/src/test/ho_matcher.cpp +++ b/src/test/ho_matcher.cpp @@ -170,6 +170,147 @@ namespace euf { m_matcher.add_pattern(pat.get()); m_matcher(pat, t, 3, 1); } + + // Structural regression test derived from TPTP ANA067^1 (which fails + // under smt.ho_matching=true inside the full solver). + // pattern: (select (select v0 v3) v2) with v0 a doubly-nested array (flex head) + // term: (select K ...) matched term is itself array-sorted. + // Exercises imitation/projection of a flex head against an array-sorted + // term. The matcher must build only well-sorted bindings; the debug + // asserts in match_goals::push and mk_project catch any regression that + // commits an ill-sorted (extra array level) lambda/select. + void test7() { + sort_ref r(m_arith.mk_real(), m); + sort_ref arr_rb(m_array.mk_array_sort(r, m.mk_bool_sort()), m); // (Array Real Bool) + sort_ref arr_r_rb(m_array.mk_array_sort(r, arr_rb), m); // (Array Real (Array Real Bool)) + sort_ref arr_r_r_rb(m_array.mk_array_sort(r, arr_r_rb), m); // v0 sort + + expr_ref v0(m.mk_var(0, arr_r_r_rb), m); + expr_ref v2(m.mk_var(2, r), m); + expr_ref v3(m.mk_var(3, r), m); + expr_ref pat(m_array.mk_select(v0, v3), m); + pat = m_array.mk_select(pat, v2); + + expr_ref K(m.mk_const(symbol("K"), arr_r_rb), m); + expr_ref b(m.mk_const(symbol("b"), r), m); + expr_ref t(m_array.mk_select(K, b), m); + + IF_VERBOSE(0, verbose_stream() << "test7: " << pat << " =?= " << t << "\n";); + m_matcher.add_pattern(pat.get()); + m_matcher(pat, t, 5); + + // Faithful variant: the term index argument is itself + // (select fun (lambda (t) c)) as in ANA067^1, i.e. a term whose + // subterm is a function(array)-valued lambda. This forces the + // matcher to decompose/imitate against a lambda-bearing term. + sort_ref arr_rr(m_array.mk_array_sort(r, r), m); // (Array Real Real) + sort_ref fun_sort(m_array.mk_array_sort(arr_rr, r), m); // (Array (Array Real Real) Real) + symbol tt("t"); + sort* r_s = r.get(); + expr_ref c0(m.mk_const(symbol("c0"), r), m); + expr_ref lam(m.mk_lambda(1, &r_s, &tt, c0), m); // (lambda (t Real) c0) + expr_ref fun(m.mk_const(symbol("fun"), fun_sort), m); + expr_ref idx(m_array.mk_select(fun, lam), m); // : Real + expr_ref t2(m_array.mk_select(K, idx), m); + IF_VERBOSE(0, verbose_stream() << "test7b: " << pat << " =?= " << t2 << "\n";); + m_matcher.add_pattern(pat.get()); + m_matcher(pat, t2, 5); + } + + // Structural regression test derived from TPTP PHI008^4 (which fails + // under smt.ho_matching=true inside the full solver). + // pattern: (select v3 v4) v3 flex head, v4 a flex arg of an array sort + // term: (select P ...) P a concrete array constant. + // Exercises projecting/imitating a flex head over a function(array)-sorted + // argument (incl. a lambda-valued term arg). The matcher must build only + // well-sorted bindings; debug asserts guard against regressions. + void test8() { + sort_ref i(m.mk_uninterpreted_sort(symbol("qML_i")), m); + sort_ref mu(m.mk_uninterpreted_sort(symbol("qML_mu")), m); + sort_ref arr_ib(m_array.mk_array_sort(i, m.mk_bool_sort()), m); // (Array qML_i Bool) + sort_ref arr_mu_ib(m_array.mk_array_sort(mu, arr_ib), m); // (Array qML_mu (Array qML_i Bool)) + sort_ref p_sort(m_array.mk_array_sort(arr_mu_ib, arr_ib), m); // P sort + + expr_ref v3(m.mk_var(3, p_sort), m); + expr_ref v4(m.mk_var(4, arr_mu_ib), m); + expr_ref pat(m_array.mk_select(v3, v4), m); + + expr_ref P(m.mk_const(symbol("P"), p_sort), m); + expr_ref ell(m.mk_const(symbol("ell"), arr_mu_ib), m); + expr_ref t(m_array.mk_select(P, ell), m); + + IF_VERBOSE(0, verbose_stream() << "test8: " << pat << " =?= " << t << "\n";); + m_matcher.add_pattern(pat.get()); + m_matcher(pat, t, 9); + + // Variant with a lambda-valued term argument, mirroring PHI008's + // (select scott_P (lambda (Y) (lambda (Z) ...))) goal that forces + // the matcher to decompose a flex head against a lambda term. + symbol yv("Y"); + sort* mu_s = mu.get(); + expr_ref cbody(m.mk_const(symbol("C"), arr_ib), m); + expr_ref lam(m.mk_lambda(1, &mu_s, &yv, cbody), m); // (lambda (Y qML_mu) C) : arr_mu_ib + expr_ref t2(m_array.mk_select(P, lam), m); + IF_VERBOSE(0, verbose_stream() << "test8b: " << pat << " =?= " << t2 << "\n";); + m_matcher.add_pattern(pat.get()); + m_matcher(pat, t2, 9); + } + + // Structural regression test for the ITP127-style shape (fails under + // smt.ho_matching=true inside the full solver). The flex head H has an + // applied result sort that is *itself* an array (monomo = (Array d Bool)). + // Matching (select (select H x1) x2) =?= f where f is array-sorted is a + // case where imitation could build a lambda with an extra array level + // (an ill-sorted select). The matcher must build only well-sorted + // bindings; debug asserts guard against regressions. + void test9() { + sort_ref c(m.mk_uninterpreted_sort(symbol("c")), m); + sort_ref d(m.mk_uninterpreted_sort(symbol("d")), m); + sort_ref monomo(m_array.mk_array_sort(d, m.mk_bool_sort()), m); // (Array d Bool) + sort_ref h1(m_array.mk_array_sort(c, monomo), m); // (Array c monomo) + sort_ref h2(m_array.mk_array_sort(c, h1), m); // (Array c (Array c monomo)) + + expr_ref H(m.mk_var(0, h2), m); + expr_ref x1(m.mk_var(1, c), m); + expr_ref x2(m.mk_var(2, c), m); + expr_ref pat(m_array.mk_select(H, x1), m); + pat = m_array.mk_select(pat, x2); // (select (select H x1) x2) : monomo + + expr_ref f(m.mk_const(symbol("f"), monomo), m); // f : (Array d Bool) + IF_VERBOSE(0, verbose_stream() << "test9: " << pat << " =?= " << f << "\n";); + m_matcher.add_pattern(pat.get()); + m_matcher(pat, f, 3); + } + + // Faithful isolation test for the refine-time sort guard used by + // ho_matcher::refine_ho_match (throws "sort mismatch ..." on failure). + // Mirrors the SEV510^1 family where a bound-variable binding's sort + // disagrees with the pattern variable it would fill. subst_sorts_match + // must detect the mismatch (return false) and accept the matching case. + void test10() { + sort_ref int2int(m_array.mk_array_sort(m_int, m_int), m); + // pattern (select v0 v1): v0 is the array (idx 0), v1 the index (idx 1) + expr_ref v0(m.mk_var(0, int2int), m); + expr_ref v1(m.mk_var(1, m_int), m); + expr_ref pat(m_array.mk_select(v0, v1), m); + + // std_order=true: var idx maps to s[size-idx-1], so idx0->s[1], idx1->s[0]. + expr_ref arr(m.mk_const(symbol("arr"), int2int), m); + expr_ref i0(m_arith.mk_int(0), m); + + // Well-sorted substitution: idx0 -> arr (array), idx1 -> 0 (int). + expr_ref_vector s_ok(m); + s_ok.push_back(i0); // s[0] -> var idx 1 (Int) OK + s_ok.push_back(arr); // s[1] -> var idx 0 (Array) OK + VERIFY(ho_matcher::subst_sorts_match(m, pat, s_ok, true)); + + // Ill-sorted substitution: idx0 (array var) bound to an Int -> mismatch. + expr_ref_vector s_bad(m); + s_bad.push_back(i0); // s[0] -> var idx 1 (Int) OK + s_bad.push_back(i0); // s[1] -> var idx 0 expects Array, got Int -> mismatch + VERIFY(!ho_matcher::subst_sorts_match(m, pat, s_bad, true)); + IF_VERBOSE(0, verbose_stream() << "test10: subst_sorts_match detects sort mismatch\n";); + } }; } @@ -183,6 +324,10 @@ void tst_ho_matcher() { tm.test4(); tm.test5(); tm.test6(); + tm.test7(); + tm.test8(); + tm.test9(); + tm.test10(); } catch (std::exception const& ex) { std::cout << ex.what() << "\n";