mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 14:17:47 +00:00
Code Activity

add lambda-t case in addition to p-lambda case

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-29 01:15:59 -07:00
parent b74e35f4fb
commit 48bcee8e62
1 changed files with 38 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -315,7 +315,6 @@ namespace euf {
break;
}
// v >= offset
// v - offset |-> t
if (is_meta_var(p, wi.pat_offset()) && is_closed(t, 0, wi.term_offset())) {
@ -326,7 +325,6 @@ namespace euf {
return true;
}
// N = \ x. T => ((shift1 N) x) = T
if (is_lambda(t) && !is_lambda(p)) {
auto q = to_quantifier(t);
@ -345,6 +343,43 @@ namespace euf {
return true;
}
// \x . N = T => N = ((shift1 T) x)
if (is_lambda(p) && !is_lambda(t)) {
auto q = to_quantifier(p);
auto p_body = q->get_expr();
auto nd = q->get_num_decls();
var_shifter vs(m);
expr_ref r(m);
vs(t, nd, r);
expr_ref_vector args(m);
args.push_back(r);
for (unsigned i = 0; i < nd; ++i)
args.push_back(m.mk_var(nd - 1 - i, q->get_decl_sort(i)));
r = m_array.mk_select(args);
m_goals.push(wi.level, wi.term_offset() + nd, p_body, r);
wi.set_done();
return true;
}
//
// lambda x . p == lambda x . t
//
if (is_quantifier(p) && is_quantifier(t)) {
auto qp = to_quantifier(p);
auto qt = to_quantifier(t);
unsigned pd = qp->get_num_decls();
unsigned td = qt->get_num_decls();
if (qp->get_kind() != qt->get_kind())
return false;
if (pd != td)
return false;
for (unsigned i = 0; i < pd; ++i)
if (qp->get_decl_sort(i) != qt->get_decl_sort(i))
return false;
m_goals.push(wi.level, wi.term_offset() + td, qp->get_expr(), qt->get_expr());
return true;
}
// Flex head unitary
// H(pat) = t
@ -484,25 +519,7 @@ namespace euf {
m_goals.push(wi.level, wi.term_offset(), tp->get_arg(i), ta->get_arg(i));
return true;
}
//
// lambda x . p == lambda x . t
//
if (is_quantifier(p) && is_quantifier(t)) {
auto qp = to_quantifier(p);
auto qt = to_quantifier(t);
unsigned pd = qp->get_num_decls();
unsigned td = qt->get_num_decls();
if (qp->get_kind() != qt->get_kind())
return false;
if (pd != td)
return false;
for (unsigned i = 0; i < pd; ++i)
if (qp->get_decl_sort(i) != qt->get_decl_sort(i))
return false;
m_goals.push(wi.level, wi.term_offset() + td, qp->get_expr(), qt->get_expr());
return true;
}
return false;
}