mirror of
https://github.com/Z3Prover/z3
synced 2026-07-19 05:25:48 +00:00
bugfixes to front-end and matcher
This commit is contained in:
Nikolaj Bjorner
parent
6c8a5cd853
commit
470e966791
8 changed files with 275 additions and 67 deletions
|
|
@ -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<sort> domain, pat_domain;
|
||||
ptr_vector<expr> pat_args;
|
||||
svector<unsigned> pat_pos; // forward binder position (in domain) of each distinct index
|
||||
expr_ref_vector args(m), pat_vars(m), bound_args(m);
|
||||
vector<symbol> 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<std::pair<unsigned, expr*>>()).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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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<typename Config>
|
||||
|
|
@ -552,6 +553,7 @@ void rewriter_tpl<Config>::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<Config>::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";);
|
||||
|
|
|
|||
|
|
@ -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<sort> 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<ast_manager&>(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<ast_manager&>(m)) << "\n";);
|
||||
IF_VERBOSE(0, verbose_stream() << mk_ll_pp(n, const_cast<ast_manager &>(m)) << "\n";);
|
||||
}
|
||||
return !p.m_error;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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<cond_macro>::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() {
|
||||
|
|
|
|||
|
|
@ -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<void(euf::ho_subst&)> on_match = [&](euf::ho_subst& s) {
|
||||
std::function<void(euf::ho_subst&)> 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;
|
||||
|
|
|
|||
|
|
@ -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";
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue