mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

fixes to ho-matcher

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-05 16:24:45 -07:00
parent 3ccf7a695b
commit 2d1a42d53f
2 changed files with 136 additions and 168 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/array_decl_plugin.h
View file

@ -245,6 +245,11 @@ public:
return mk_select(2, args); return mk_select(2, args);
} }
app* mk_select(expr* a, expr* i, expr* j) const {
expr* args[3] = { a, i, j };
return mk_select(3, args);
}
app * mk_select(unsigned num_args, expr * const * args) const { app * mk_select(unsigned num_args, expr * const * args) const {
return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args); return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args);
} }

299
src/test/ho_matcher.cpp
View file

@ -29,7 +29,7 @@ namespace euf {
bool m_in_scope = false; bool m_in_scope = false;
public: public:
void initialize_backtrack() { void set_init() {
m_state = state::init_s; m_state = state::init_s;
m_index = 0; m_index = 0;
m_in_scope = false; m_in_scope = false;
@ -42,6 +42,7 @@ namespace euf {
void set_app() { m_state = state::app_s; m_index = 0; } void set_app() { m_state = state::app_s; m_index = 0; }
void set_done() { m_state = state::done_s; } void set_done() { m_state = state::done_s; }
void inc_index() { ++m_index; } void inc_index() { ++m_index; }
void set_index(unsigned i) { m_index = i; }
unsigned index() const { return m_index; } unsigned index() const { return m_index; }
bool in_scope() const { return m_in_scope; } bool in_scope() const { return m_in_scope; }
void set_in_scope(bool f = true) { m_in_scope = f; } void set_in_scope(bool f = true) { m_in_scope = f; }
@ -70,26 +71,14 @@ namespace euf {
return !(*this == other); return !(*this == other);
} }
match_goal(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t) noexcept : base_offset(offset), pat(pat), t(t), level(level) {} match_goal(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t) noexcept :
match_goal(match_goal const& other) noexcept : base_offset(offset), pat(pat), t(t), level(level) {}
pat(other.pat), t(other.t), delta_offset(other.delta_offset),
base_offset(other.base_offset), level(other.level) {}
match_goal& operator=(match_goal const& other) noexcept {
if (this != &other) {
pat = other.pat;
t = other.t;
level = other.level;
base_offset = other.base_offset;
delta_offset = other.delta_offset;
}
return *this;
}
unsigned term_offset() const { return base_offset + delta_offset; } unsigned term_offset() const { return base_offset + delta_offset; }
unsigned pat_offset() const { return delta_offset; } unsigned pat_offset() const { return base_offset + delta_offset; }
std::ostream& display(std::ostream& out) const { std::ostream& display(std::ostream& out) const {
return out << "[" << level << ":" << delta_offset << "] " << pat << " ~ " << t << "\n"; return out << "[" << level << ":" << base_offset + delta_offset << "] " << pat << " ~ " << t << "\n";
} }
}; };
@ -327,8 +316,6 @@ namespace euf {
void add_binding(var* v, unsigned offset, expr* t); void add_binding(var* v, unsigned offset, expr* t);
expr_ref mk_project(unsigned i, sort* array_sort);
expr_ref mk_project(unsigned num_lambdas, unsigned xi, sort* array_sort); expr_ref mk_project(unsigned num_lambdas, unsigned xi, sort* array_sort);
void bind_lambdas(unsigned j, sort* s, expr_ref& body); void bind_lambdas(unsigned j, sort* s, expr_ref& body);
@ -358,6 +345,8 @@ namespace euf {
void operator()(expr *pat, expr *t, unsigned num_vars); void operator()(expr *pat, expr *t, unsigned num_vars);
void operator()(expr* pat, expr* t, unsigned num_bound, unsigned num_vars);
void reduce(match_goal& wi); void reduce(match_goal& wi);
trail_stack& trail() { return m_trail; } trail_stack& trail() { return m_trail; }
@ -407,15 +396,19 @@ namespace euf {
namespace euf { namespace euf {
void ho_matcher::operator()(expr* pat, expr* t, unsigned num_vars) { void ho_matcher::operator()(expr* pat, expr* t, unsigned num_vars) {
(*this)(pat, t, 0, num_vars);
}
void ho_matcher::operator()(expr* pat, expr* t, unsigned num_bound, unsigned num_vars) {
m_trail.push_scope(); m_trail.push_scope();
m_subst.resize(num_vars); m_subst.resize(num_vars);
m_goals.reset(); m_goals.reset();
m_goals.push(0, 0, pat, t); m_goals.push(0, num_bound, pat, t);
IF_VERBOSE(1, display(verbose_stream())); IF_VERBOSE(1, display(verbose_stream()));
while (true) { while (m.inc()) {
// Q, B -> Q', B'. Push work on the backtrack stack and new work items // Q, B -> Q', B'. Push work on the backtrack stack and new work items
// e, Bw -> Q', B'. Consume backtrack stack // e, Bw -> Q', B'. Consume backtrack stack
if (!m_goals.empty()) if (!m_goals.empty())
@ -442,10 +435,8 @@ namespace euf {
auto& wi = *m_backtrack.back(); auto& wi = *m_backtrack.back();
if (consume_work(wi)) { if (consume_work(wi)) {
IF_VERBOSE(3, display(verbose_stream() << "ho_matcher::consume_work: " << wi.pat << " =?= " << wi.t << " -> true\n");); IF_VERBOSE(3, display(verbose_stream() << "ho_matcher::consume_work: " << wi.pat << " =?= " << wi.t << " -> true\n"););
if (m_goals.empty()) { if (m_goals.empty())
m_on_match(m_subst); m_on_match(m_subst);
backtrack();
}
break; break;
} }
else { else {
@ -480,26 +471,28 @@ namespace euf {
auto p1 = m_subst.get(to_var(p)->get_idx() - o1); auto p1 = m_subst.get(to_var(p)->get_idx() - o1);
if (p1) if (p1)
return are_equal(0, p1, o2, t); return are_equal(0, p1, o2, t);
return l_undef;
} }
if (is_meta_var(t, o2)) { if (is_meta_var(t, o2)) {
auto t1 = m_subst.get(to_var(t)->get_idx() - o2); auto t1 = m_subst.get(to_var(t)->get_idx() - o2);
if (t1) if (t1)
return are_equal(o1, p, 0, t1); return are_equal(o1, p, 0, t1);
return l_undef;
} }
if (is_bound_var(p, o1) || is_bound_var(t, o2))
return to_lbool(p == t);
if (m_unitary.is_flex(o1, p)) { if (m_unitary.is_flex(o1, p)) {
expr_ref h = whnf(p, o1); expr_ref h = whnf(p, o1);
if (h != p) if (h != p)
return are_equal(o1, h, o2, t); return are_equal(o1, h, o2, t);
return l_undef;
} }
if (m_unitary.is_flex(o2, t)) { if (m_unitary.is_flex(o2, t)) {
expr_ref h = whnf(t, o2); expr_ref h = whnf(t, o2);
if (h != t) if (h != t)
return are_equal(o1, p, o2, h); return are_equal(o1, p, o2, h);
return l_undef;
} }
if (m_array.is_select(p)) if (m_array.is_select(p))
return l_undef; // TODO: interleave check with whnf expansion return l_undef; // TODO: interleave check with whnf expansion
@ -518,6 +511,9 @@ namespace euf {
} }
return l_true; return l_true;
} }
if (is_bound_var(p, o1) || is_bound_var(t, o2))
return to_lbool(p == t);
return l_undef; return l_undef;
} }
@ -588,29 +584,25 @@ namespace euf {
// We assume that m_rewriter should produce // We assume that m_rewriter should produce
// something amounting to weak-head normal form WHNF // something amounting to weak-head normal form WHNF
// TODO: also unfold binding
void ho_matcher::reduce(match_goal& wi) { void ho_matcher::reduce(match_goal& wi) {
bool change = true; while (true) {
while (change) {
change = false;
expr_ref r = whnf(wi.pat, wi.pat_offset()); expr_ref r = whnf(wi.pat, wi.pat_offset());
if (r != wi.pat) { if (r == wi.pat)
IF_VERBOSE(3, verbose_stream() << "ho_matcher::reduce: " << wi.pat << " -> " << r << "\n";); break;
wi.pat = r; IF_VERBOSE(3, verbose_stream() << "ho_matcher::reduce: " << wi.pat << " -> " << r << "\n";);
change = true; wi.pat = r;
} }
r = whnf(wi.t, wi.term_offset());
if (r != wi.t) { while (true) {
IF_VERBOSE(3, verbose_stream() << "ho_matcher::reduce: " << wi.t << " -> " << r << "\n";); expr_ref r = whnf(wi.t, wi.term_offset());
wi.t = r; if (r == wi.t)
change = true; break;
} IF_VERBOSE(3, verbose_stream() << "ho_matcher::reduce: " << wi.t << " -> " << r << "\n";);
} wi.t = r;
}
} }
bool ho_matcher::consume_work(match_goal &wi) { bool ho_matcher::consume_work(match_goal &wi) {
// IF_VERBOSE(1, display(verbose_stream() << "ho_matcher::consume_work: " << wi.pat << " =?= " << wi.t << "\n");); // IF_VERBOSE(1, display(verbose_stream() << "ho_matcher::consume_work: " << wi.pat << " =?= " << wi.t << "\n"););
@ -645,8 +637,7 @@ namespace euf {
if (is_meta_var(p, wi.pat_offset()) && is_closed(t, 0, wi.term_offset())) { if (is_meta_var(p, wi.pat_offset()) && is_closed(t, 0, wi.term_offset())) {
auto v = to_var(p); auto v = to_var(p);
auto idx = v->get_idx() - wi.pat_offset(); auto idx = v->get_idx() - wi.pat_offset();
if (m_subst.get(idx)) SASSERT(!m_subst.get(idx)); // reduce ensures meta variables are not in substitutions
return to_lbool(m_subst.get(idx) == t);
add_binding(v, wi.pat_offset(), t); add_binding(v, wi.pat_offset(), t);
wi.set_done(); wi.set_done();
return true; return true;
@ -676,7 +667,6 @@ namespace euf {
if (m_array.is_select(p) && m_unitary.is_flex(wi.pat_offset(), p) && is_pattern(p, wi.pat_offset(), t)) { if (m_array.is_select(p) && m_unitary.is_flex(wi.pat_offset(), p) && is_pattern(p, wi.pat_offset(), t)) {
auto lam = abstract_pattern(p, wi.pat_offset(), t); auto lam = abstract_pattern(p, wi.pat_offset(), t);
expr* v = p;
while (m_array.is_select(p)) while (m_array.is_select(p))
p = to_app(p)->get_arg(0); p = to_app(p)->get_arg(0);
SASSERT(is_meta_var(p, wi.pat_offset())); SASSERT(is_meta_var(p, wi.pat_offset()));
@ -686,6 +676,7 @@ namespace euf {
} }
// Flex head general case // Flex head general case
if (m_array.is_select(p) && m_unitary.is_flex(wi.pat_offset(), p)) { if (m_array.is_select(p) && m_unitary.is_flex(wi.pat_offset(), p)) {
ptr_vector<app> pats; ptr_vector<app> pats;
auto p1 = p; auto p1 = p;
@ -703,15 +694,17 @@ namespace euf {
unsigned i = 0; unsigned i = 0;
for (auto pa : pats) { for (auto pa : pats) {
for (auto pi : array_select_indices(pa)) { for (auto pi : array_select_indices(pa)) {
if (start <= i && pi->get_sort() == t->get_sort()) { if (start <= i && pi->get_sort() == t->get_sort()) {
auto eq = are_equal(wi.pat_offset(), pi, wi.term_offset(), t); auto eq = are_equal(wi.pat_offset(), pi, wi.term_offset(), t);
if (eq == l_false) if (eq == l_false) {
++i;
continue; continue;
}
auto e = mk_project(pats.size(), i, v->get_sort()); auto e = mk_project(pats.size(), i, v->get_sort());
add_binding(v, wi.pat_offset(), e); add_binding(v, wi.pat_offset(), e);
if (eq == l_undef) if (eq == l_undef)
m_goals.push(wi.level, wi.pat_offset(), pi, t); m_goals.push(wi.level, wi.pat_offset(), pi, t);
wi.inc_index(); wi.set_index(i + 1);
return true; return true;
} }
++i; ++i;
@ -719,7 +712,7 @@ namespace euf {
} }
} }
// TBD: H p1 p2 = \x . t not handled SASSERT(!is_lambda(t));
if (!is_app(t)) if (!is_app(t))
return false; return false;
@ -736,36 +729,44 @@ namespace euf {
m_trail.push(undo_resize(m_subst)); m_trail.push(undo_resize(m_subst));
} }
// H (p1) (p2) = f(t1, .., tn) // H (p1) (p2) = f(t1, .., tn)
// H -> \x1 \x2 f(H1(x1, x2), .., Hn(x1, x2)) // H -> \x1 \x2 f(H1(x1, x2), .., Hn(x1, x2))
// H1(p1, p2) = t1, .., Hn(p1, p2) = tn // H1(p1, p2) = t1, .., Hn(p1, p2) = tn
ptr_vector<sort> domain; ptr_vector<sort> domain, pat_domain;
ptr_vector<expr> pat_args; ptr_vector<expr> pat_args;
expr_ref_vector args(m), pat_vars(m), bound_args(m); expr_ref_vector args(m), pat_vars(m), bound_args(m);
vector<symbol> names; vector<symbol> names;
pat_args.push_back(nullptr); pat_args.push_back(nullptr);
pat_vars.push_back(nullptr); pat_vars.push_back(nullptr);
unsigned num_bound = 0; unsigned num_bound = 0;
expr_mark seen;
for (auto pat : pats) { for (auto pat : pats) {
for (auto pi : array_select_indices(pat)) { for (auto pi : array_select_indices(pat)) {
++num_bound;
domain.push_back(pi->get_sort()); domain.push_back(pi->get_sort());
pat_args.push_back(pi); names.push_back(symbol(num_bound));
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);
} }
} }
unsigned i = 0;
for (auto pat : pats) for (unsigned i = pat_args.size(); i-- > 1; ) {
for (auto pi : array_select_indices(pat)) auto pi = pat_args.get(i);
pat_vars.push_back(m.mk_var(num_bound - (--i), pi->get_sort())); pat_vars.push_back(m.mk_var(pat_args.size() - i - 1, pi->get_sort()));
}
for (auto ti : *ta) { for (auto ti : *ta) {
auto v = m.mk_var(m_subst.size() + wi.pat_offset(), m_array.mk_array_sort(domain.size(), domain.data(), ti->get_sort())); sort* v_sort = m_array.mk_array_sort(pat_domain.size(), pat_domain.data(), ti->get_sort());
auto v = m.mk_var(m_subst.size() + wi.pat_offset(), v_sort);
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); m_subst.resize(m_subst.size() + 1);
pat_args[0] = v; pat_args[0] = v;
auto sel = m_array.mk_select(pat_args.size(), pat_args.data()); auto sel = m_array.mk_select(pat_args.size(), pat_args.data());
m_goals.push(wi.level, wi.term_offset(), sel, ti); m_goals.push(wi.level, wi.term_offset(), sel, ti);
pat_vars[0] = v; pat_vars[0] = w;
sel = m_array.mk_select(pat_vars.size(), pat_vars.data()); sel = m_array.mk_select(pat_vars.size(), pat_vars.data());
bound_args.push_back(sel); bound_args.push_back(sel);
} }
@ -780,6 +781,7 @@ namespace euf {
lam = m.mk_lambda(sz, domain.data() + num_bound, names.data() + num_bound, lam); lam = m.mk_lambda(sz, domain.data() + num_bound, names.data() + num_bound, lam);
} }
add_binding(v, wi.pat_offset(), lam); add_binding(v, wi.pat_offset(), lam);
wi.set_done();
return true; return true;
} }
return false; return false;
@ -903,8 +905,7 @@ namespace euf {
} }
var_subst sub(m, false); var_subst sub(m, false);
expr_ref lam = sub(t, pat2bound); expr_ref lam = sub(t, pat2bound);
unsigned j = 0; for (unsigned i = pats.size(), j = 0; i-- > 0; ) {
for (unsigned i = pats.size(); i-- > 0; ) {
vector<symbol> names; vector<symbol> names;
ptr_vector<sort> sorts; ptr_vector<sort> sorts;
for (unsigned k = 1; k < pats[i]->get_num_args(); ++k) { for (unsigned k = 1; k < pats[i]->get_num_args(); ++k) {
@ -934,31 +935,15 @@ namespace euf {
return false; return false;
} }
// T1,.., Ti, .., Tn -> Ti => lambda x1, .., xn . xi
expr_ref ho_matcher::mk_project(unsigned i, sort* s) {
SASSERT(m_array.is_array(s));
unsigned sz = get_array_arity(s);
expr_ref body(m);
ptr_vector<sort> decl_sorts;
vector<symbol> decl_names;
SASSERT(i < sz);
for (unsigned j = 0; j < sz; ++j) {
decl_sorts.push_back(get_array_domain(s, j));
decl_names.push_back(symbol(j));
}
body = m.mk_var(sz - i - 1, get_array_domain(s, i));
return expr_ref(m.mk_lambda(sz, decl_sorts.data(), decl_names.data(), body), m);
}
// (T1, T2,.., Tn) -> (Tn+1,.., Ti,.., Tm) -> Ti => lambda x1...xn . lambda x_n+1,..x_m . x_i // (T1, T2,.., Tn) -> (Tn+1,.., Ti,.., Tm) -> Ti => lambda x1...xn . lambda x_n+1,..x_m . x_i
expr_ref ho_matcher::mk_project(unsigned num_lambdas, unsigned i, sort* s) { expr_ref ho_matcher::mk_project(unsigned num_lambdas, unsigned i, sort* s) {
SASSERT(num_lambdas > 1); SASSERT(num_lambdas > 0);
SASSERT(m_array.is_array(s)); SASSERT(m_array.is_array(s));
unsigned num_binders = 0; unsigned num_binders = 0;
expr_ref body(m); expr_ref body(m);
sort* a = s, * var_sort = nullptr; sort* a = s, * var_sort = nullptr;
unsigned j = i; unsigned j = i;
for (unsigned j = 0; j < num_lambdas; ++j) { for (unsigned k = 0; k < num_lambdas; ++k) {
auto arity = get_array_arity(a); auto arity = get_array_arity(a);
if (j >= arity) if (j >= arity)
j -= arity; j -= arity;
@ -967,13 +952,14 @@ namespace euf {
num_binders += arity; num_binders += arity;
a = get_array_range(a); a = get_array_range(a);
} }
SASSERT(var_sort);
body = m.mk_var(num_binders - i - 1, var_sort); body = m.mk_var(num_binders - i - 1, var_sort);
bind_lambdas(num_lambdas, s, body); bind_lambdas(num_lambdas, s, body);
return body; return body;
} }
void ho_matcher::bind_lambdas(unsigned j, sort* s, expr_ref& body) { void ho_matcher::bind_lambdas(unsigned j, sort* s, expr_ref& body) {
if (j > 0) if (j > 1)
bind_lambdas(j - 1, get_array_range(s), body); bind_lambdas(j - 1, get_array_range(s), body);
unsigned sz = get_array_arity(s); unsigned sz = get_array_arity(s);
ptr_vector<sort> decl_sorts; ptr_vector<sort> decl_sorts;
@ -985,7 +971,6 @@ namespace euf {
body = m.mk_lambda(sz, decl_sorts.data(), decl_names.data(), body); body = m.mk_lambda(sz, decl_sorts.data(), decl_names.data(), body);
} }
void ho_matcher::add_binding(var* v, unsigned offset, expr* t) { void ho_matcher::add_binding(var* v, unsigned offset, expr* t) {
SASSERT(v->get_idx() >= offset); SASSERT(v->get_idx() >= offset);
m_subst.set(v->get_idx() - offset, t); m_subst.set(v->get_idx() - offset, t);
@ -1031,19 +1016,20 @@ namespace euf {
} }
} }
match_goal* match_goals::pop() { match_goal* match_goals::pop() {
SASSERT(!empty()); SASSERT(!empty());
if (m_cheap) if (m_cheap)
return pop(m_cheap); return pop(m_cheap);
auto* wi = m_expensive; auto* wi = m_expensive;
do { do {
match_goal save_wi(wi->level, wi->term_offset(), wi->pat, wi->t); expr_ref pat(wi->pat), t(wi->t);
ho.reduce(*wi); ho.reduce(*wi);
if (*wi == save_wi) if (pat == wi->pat && t == wi->t)
continue; continue;
if (pat != wi->pat)
ho.trail().push(update_value(*wi, save_wi)); ho.trail().push(update_value(wi->pat, pat));
if (t != wi->t)
ho.trail().push(update_value(wi->t, t));
if (ho.is_cheap(*wi)) { if (ho.is_cheap(*wi)) {
dll_base<match_goal>::remove_from(m_expensive, wi); dll_base<match_goal>::remove_from(m_expensive, wi);
match_goal::push_to_front(m_cheap, wi); match_goal::push_to_front(m_cheap, wi);
@ -1063,7 +1049,7 @@ namespace euf {
SASSERT(ws); SASSERT(ws);
auto* wi = ws->pop(ws); auto* wi = ws->pop(ws);
ho.trail().push(insert_dll(ws, wi)); // insert wi into ws ho.trail().push(insert_dll(ws, wi)); // insert wi into ws
wi->initialize_backtrack(); wi->set_init();
return wi; return wi;
} }
@ -1119,6 +1105,7 @@ namespace euf {
args.push_back(zero); args.push_back(zero);
expr_ref t(m.mk_app(m_f, args), m); expr_ref t(m.mk_app(m_f, args), m);
m_matcher.add_pattern(pat.get()); m_matcher.add_pattern(pat.get());
IF_VERBOSE(0, verbose_stream() << "test2 " << pat << " ~ " << t << "\n");
m_matcher(pat, t, 2); m_matcher(pat, t, 2);
} }
@ -1137,6 +1124,7 @@ namespace euf {
args.push_back(zero); args.push_back(zero);
expr_ref t(m.mk_app(m_f, args), m); expr_ref t(m.mk_app(m_f, args), m);
m_matcher.add_pattern(pat.get()); m_matcher.add_pattern(pat.get());
IF_VERBOSE(0, verbose_stream() << "test2 " << pat << " ~ " << t << "\n");
m_matcher(pat, t, 1); m_matcher(pat, t, 1);
} }
@ -1148,6 +1136,7 @@ namespace euf {
expr_ref one(m_arith.mk_int(1), m); expr_ref one(m_arith.mk_int(1), m);
expr_ref p(m_array.mk_select(v0, one), m); expr_ref p(m_array.mk_select(v0, one), m);
m_matcher.add_pattern(p.get()); m_matcher.add_pattern(p.get());
IF_VERBOSE(0, verbose_stream() << "test3 " << p << " ~ " << zero << "\n");
m_matcher(p, zero, 1); m_matcher(p, zero, 1);
} }
@ -1158,6 +1147,7 @@ namespace euf {
expr_ref one(m_arith.mk_int(1), m); expr_ref one(m_arith.mk_int(1), m);
expr_ref p(m_array.mk_select(v0, one), m); expr_ref p(m_array.mk_select(v0, one), m);
m_matcher.add_pattern(p.get()); m_matcher.add_pattern(p.get());
IF_VERBOSE(0, verbose_stream() << "test4 " << p << " ~ " << one << "\n");
m_matcher(p, one, 1); m_matcher(p, one, 1);
} }
@ -1193,96 +1183,69 @@ namespace euf {
m_matcher(pat, s, 4); m_matcher(pat, s, 4);
} }
// // test patterns
// H (2, 0) = f(2)
// G (1) (2, 0) = f(1, 2)
// G (1) (2, 1) = f(1, 2) // not unitary
// H (0, 1) = f(2) // fail
void test6() {
sort_ref intint2int(m_array.mk_array_sort(m_int, m_int, m_int), m);
func_decl_ref f1(m.mk_func_decl(symbol("f"), m_int, m_int), m);
func_decl_ref f2(m.mk_func_decl(symbol("f"), m_int, m_int, m_int), m);
expr_ref v0(m.mk_var(0, m_int), m);
expr_ref v1(m.mk_var(1, m_int), m);
expr_ref v2(m.mk_var(2, m_int), m);
expr_ref H(m.mk_var(3, intint2int), m);
expr* args[3] = { H.get(), v2, v0 };
expr_ref pat(m_array.mk_select(3, args), m);
expr_ref t(m.mk_app(f1.get(), v2), m);
IF_VERBOSE(0, verbose_stream() << "test6a: " << pat << " =?= " << t << "\n";);
m_matcher.add_pattern(pat.get());
m_matcher(pat, t, 3, 1);
expr* args2[3] = { H.get(), v1, v0 };
pat = m_array.mk_select(3, args2);
t = m.mk_app(f2.get(), v0, v1);
IF_VERBOSE(0, verbose_stream() << "test6b: " << pat << " =?= " << t << "\n";);
m_matcher.add_pattern(pat.get());
m_matcher(pat, t, 3, 1);
sort_ref int2intt(m_array.mk_array_sort(m_int, intint2int), m);
expr_ref(m.mk_var(3, int2intt), m);
expr_ref G(m.mk_var(3, int2intt), m);
pat = m_array.mk_select(G.get(), v1);
pat = m_array.mk_select(pat.get(), v2, v0);
t = m.mk_app(f2.get(), v1, v2);
IF_VERBOSE(0, verbose_stream() << "test6c: " << pat << " =?= " << t << "\n";);
m_matcher.add_pattern(pat.get());
m_matcher(pat, t, 3, 1);
pat = m_array.mk_select(G, v1);
pat = m_array.mk_select(pat, v2, v1);
IF_VERBOSE(0, verbose_stream() << "test6d: " << pat << " =?= " << t << "\n";);
m_matcher.add_pattern(pat.get());
m_matcher(pat, t, 3, 1);
pat = m_array.mk_select(H, v0, v2);
IF_VERBOSE(0, verbose_stream() << "test6e: " << pat << " =?= " << t << "\n";);
m_matcher.add_pattern(pat.get());
m_matcher(pat, t, 3, 1);
}
}; };
#if 0
void ho_matcher::apps(unsigned sz, sort* const* domain, expr_ref_vector& ts,
vector<expr_ref_vector>& sts, unsigned_vector& sts_start, unsigned_vector& sts_end) {
vector<unsigned_vector> starts, ends;
for (unsigned i = 0; i < sz; ++i) {
unsigned_vector sts_start_i, sts_end_i;
expr_ref_vector sts_i(m);
expr* t = nullptr; // TODO
apps(domain[sz - i - 1], t, sz - i - 1, ts, sts_i, sts_start_i, sts_end_i);
starts.push_back(sts_start_i);
ends.push_back(sts_end_i);
sts.push_back(sts_i);
}
// perform another level of blend helper.
}
// all possible abstactions for subterms of type s in t.
void ho_matcher::apps(sort* s, expr* t, unsigned i, expr_ref_vector& ts, expr_ref_vector& sts, unsigned_vector& sts_start, unsigned_vector& sts_end) {
var_ref v(m.mk_var(i, s), m);
for (auto st : subterms::all(expr_ref(t, m))) { // ground vs non-ground?
if (st->get_sort() == s) {
sts.push_back(st);
unsigned start = ts.size();
// abstract st in t
abstract(st, t, v.get(), ts, start);
sts_start.push_back(start);
sts_end.push_back(ts.size());
}
}
}
// abstract 1, 2, .. occurrences of s in t
// return list of ts
void ho_matcher::abstract(expr* s, expr* t, var* v, expr_ref_vector& ts, unsigned& start) {
if (is_app(t) && get_depth(s) > get_depth(t)) {
auto ta = to_app(t);
unsigned_vector pos;
for (auto arg : *ta) {
pos.push_back(ts.size());
// abstract(s, arg, v, ts);
}
pos.push_back(ts.size());
//
// now merge the sub-intervals ts_1, .., ts_n
// where each sub-interval starts at pos_1, ., pos_n
// into terms f(ts_1[i], .., ts_n[j]) for i, j
// remove intermediary terms from ts after the merge.
//
expr_ref_vector args(m);
blend_helper(ts, pos, ta->get_decl(), 0, args);
start = pos.back();
return;
}
ts.push_back(t);
if (s == t)
ts.push_back(v);
}
void ho_matcher::blend_helper(expr_ref_vector& ts, unsigned_vector const& pos, func_decl* f, unsigned i, expr_ref_vector& args) {
if (i == pos.size() - 1) {
ts.push_back(m.mk_app(f, args));
return;
}
for (unsigned j = pos[i]; j < pos[i + 1]; ++j) {
args.push_back(ts.get(j));
blend_helper(ts, pos, f, i + 1, args);
args.pop_back();
}
}
#endif
} }
void tst_ho_matcher() { void tst_ho_matcher() {
euf::test_ho_matcher tm; euf::test_ho_matcher tm;
try { try {
tm.test1(); tm.test1();
tm.test2(); tm.test2();
tm.test3(); tm.test3();
tm.test4(); tm.test4();
tm.test5(); tm.test5();
tm.test6();
} }
catch (std::exception const& ex) { catch (std::exception const& ex) {
std::cout << ex.what() << "\n"; std::cout << ex.what() << "\n";
} }
} }