mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
extend macro detection to negated equivalences #5496
This commit is contained in:
Nikolaj Bjorner
parent
f03d756e08
commit
e6264a80ff
|
|
@ -126,7 +126,7 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen
|
|||
}
|
||||
|
||||
app * head;
|
||||
expr * definition;
|
||||
expr_ref definition(m);
|
||||
bool revert = false;
|
||||
get_head_def(q, f, head, definition, revert);
|
||||
|
||||
|
|
@ -190,21 +190,22 @@ void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) {
|
|||
}
|
||||
|
||||
|
||||
void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def, bool& revert) const {
|
||||
app * body = to_app(q->get_expr());
|
||||
void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const {
|
||||
expr * body = q->get_expr();
|
||||
expr * lhs = nullptr, *rhs = nullptr;
|
||||
bool is_not = m.is_not(body, body);
|
||||
VERIFY(m.is_eq(body, lhs, rhs));
|
||||
SASSERT(is_app_of(lhs, d) || is_app_of(rhs, d));
|
||||
SASSERT(!is_app_of(lhs, d) || !is_app_of(rhs, d));
|
||||
if (is_app_of(lhs, d)) {
|
||||
revert = false;
|
||||
head = to_app(lhs);
|
||||
def = rhs;
|
||||
def = is_not ? m.mk_not(rhs) : rhs;
|
||||
}
|
||||
else {
|
||||
revert = true;
|
||||
head = to_app(rhs);
|
||||
def = lhs;
|
||||
def = is_not ? m.mk_not(lhs) : lhs;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -215,7 +216,7 @@ void macro_manager::display(std::ostream & out) {
|
|||
quantifier * q = nullptr;
|
||||
m_decl2macro.find(f, q);
|
||||
app * head;
|
||||
expr * def;
|
||||
expr_ref def(m);
|
||||
bool r;
|
||||
get_head_def(q, f, head, def, r);
|
||||
SASSERT(q);
|
||||
|
|
@ -227,7 +228,7 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
|
|||
func_decl * f = m_decls.get(i);
|
||||
quantifier * q = m_macros.get(i);
|
||||
app * head;
|
||||
expr * def;
|
||||
expr_ref def(m);
|
||||
bool r;
|
||||
get_head_def(q, f, head, def, r);
|
||||
TRACE("macro_bug",
|
||||
|
|
@ -298,7 +299,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
|
|||
TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
|
||||
if (mm.m_decl2macro.find(d, q)) {
|
||||
app * head = nullptr;
|
||||
expr * def = nullptr;
|
||||
expr_ref def(m);
|
||||
bool revert = false;
|
||||
mm.get_head_def(q, d, head, def, revert);
|
||||
unsigned num = n->get_num_args();
|
||||
|
|
@ -320,6 +321,14 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
|
|||
r = rr;
|
||||
if (m.proofs_enabled()) {
|
||||
expr_ref instance = s(q->get_expr(), num, subst_args.data());
|
||||
expr* eq, * lhs, * rhs;
|
||||
if (m.is_not(instance, eq) && m.is_eq(eq, lhs, rhs)) {
|
||||
if (revert)
|
||||
instance = m.mk_eq(m.mk_not(lhs), rhs);
|
||||
else
|
||||
instance = m.mk_eq(lhs, m.mk_not(rhs));
|
||||
}
|
||||
SASSERT(m.is_eq(instance));
|
||||
proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.data());
|
||||
proof * q_pr = mm.m_decl2macro_pr.find(d);
|
||||
proof * prs[2] = { qi_pr, q_pr };
|
||||
|
|
|
|||
|
|
@ -84,7 +84,7 @@ public:
|
|||
func_decl * get_macro_func_decl(unsigned i) const { return m_decls.get(i); }
|
||||
func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
|
||||
quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; }
|
||||
void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def, bool& revert) const;
|
||||
void get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const;
|
||||
void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -184,6 +184,14 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
|
|||
def = rhs;
|
||||
return true;
|
||||
}
|
||||
if (m_manager.is_not(n, lhs) && m_manager.is_eq(lhs, lhs, rhs) &&
|
||||
is_macro_head(lhs, num_decls) &&
|
||||
!is_forbidden(to_app(lhs)->get_decl()) &&
|
||||
!occurs(to_app(lhs)->get_decl(), rhs)) {
|
||||
head = to_app(lhs);
|
||||
def = m_manager.mk_not(rhs);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -215,6 +223,14 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h
|
|||
def = lhs;
|
||||
return true;
|
||||
}
|
||||
if (m_manager.is_not(n, n) && m_manager.is_eq(n, lhs, rhs) &&
|
||||
is_macro_head(rhs, num_decls) &&
|
||||
!is_forbidden(to_app(rhs)->get_decl()) &&
|
||||
!occurs(to_app(rhs)->get_decl(), lhs)) {
|
||||
head = to_app(rhs);
|
||||
def = m_manager.mk_not(lhs);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -148,6 +148,15 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool quasi_macros::is_quasi_def(quantifier* q, expr* lhs, expr* rhs) const {
|
||||
return
|
||||
is_non_ground_uninterp(lhs) &&
|
||||
is_unique(to_app(lhs)->get_decl()) &&
|
||||
!depends_on(rhs, to_app(lhs)->get_decl()) &&
|
||||
fully_depends_on(to_app(lhs), q);
|
||||
}
|
||||
|
||||
|
||||
bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
|
||||
// Our definition of a quasi-macro:
|
||||
// Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
|
||||
|
|
@ -158,27 +167,39 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
|
|||
quantifier * q = to_quantifier(e);
|
||||
expr * qe = q->get_expr(), *lhs = nullptr, *rhs = nullptr;
|
||||
if (m.is_eq(qe, lhs, rhs)) {
|
||||
if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
|
||||
!depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
|
||||
a = to_app(lhs);
|
||||
if (is_quasi_def(q, lhs, rhs)) {
|
||||
a = to_app(lhs);
|
||||
t = rhs;
|
||||
return true;
|
||||
} else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
|
||||
!depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
|
||||
a = to_app(rhs);
|
||||
} else if (is_quasi_def(q, rhs, lhs)) {
|
||||
a = to_app(rhs);
|
||||
t = lhs;
|
||||
return true;
|
||||
}
|
||||
} else if (m.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
|
||||
}
|
||||
else if (m.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
|
||||
is_unique(to_app(lhs)->get_decl())) { // this is like f(...) = false
|
||||
a = to_app(lhs);
|
||||
t = m.mk_false();
|
||||
return true;
|
||||
} else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
|
||||
}
|
||||
else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
|
||||
a = to_app(qe);
|
||||
t = m.mk_true();
|
||||
return true;
|
||||
}
|
||||
else if (m.is_not(qe, lhs) && m.is_eq(lhs, lhs, rhs) && m.is_bool(lhs)) {
|
||||
if (is_quasi_def(q, lhs, rhs)) {
|
||||
a = to_app(lhs);
|
||||
t = m.mk_not(rhs);
|
||||
return true;
|
||||
} else if (is_quasi_def(q, rhs, lhs)) {
|
||||
a = to_app(rhs);
|
||||
t = m.mk_not(lhs);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
return false;
|
||||
|
|
|
|||
|
|
@ -49,6 +49,7 @@ class quasi_macros {
|
|||
bool depends_on(expr * e, func_decl * f) const;
|
||||
|
||||
bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const;
|
||||
bool is_quasi_def(quantifier* q, expr* lhs, expr* rhs) const;
|
||||
bool quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro);
|
||||
|
||||
void find_occurrences(expr * e);
|
||||
|
|
|
|||
Loading…
Reference in a new issue