mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Bugfix for quasi-macros, many thanks to Nuno Lopez finding this bug and for suggesting a fix!

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-06-25 13:25:23 +01:00
parent 3209cd2ded
commit 7158e814d1
2 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/macros/quasi_macros.cpp
View file

@ -41,7 +41,7 @@ void quasi_macros::find_occurrences(expr * e) {
// we remember whether we have seen an expr once, or more than once; // we remember whether we have seen an expr once, or more than once;
// when we see it the second time, we don't have to visit it another time, // when we see it the second time, we don't have to visit it another time,
// as we are only intersted in finding unique function applications. // as we are only interested in finding unique function applications.
m_visited_once.reset(); m_visited_once.reset();
m_visited_more.reset(); m_visited_more.reset();
@ -61,7 +61,7 @@ void quasi_macros::find_occurrences(expr * e) {
case AST_VAR: break; case AST_VAR: break;
case AST_QUANTIFIER: m_todo.push_back(to_quantifier(cur)->get_expr()); break; case AST_QUANTIFIER: m_todo.push_back(to_quantifier(cur)->get_expr()); break;
case AST_APP: case AST_APP:
if (is_uninterp(cur) && !is_ground(cur)) { if (is_non_ground_uninterp(cur)) {
func_decl * f = to_app(cur)->get_decl(); func_decl * f = to_app(cur)->get_decl();
m_occurrences.insert_if_not_there(f, 0); m_occurrences.insert_if_not_there(f, 0);
occurrences_map::iterator it = m_occurrences.find_iterator(f); occurrences_map::iterator it = m_occurrences.find_iterator(f);
@ -76,6 +76,10 @@ void quasi_macros::find_occurrences(expr * e) {
} }
}; };
bool quasi_macros::is_non_ground_uninterp(expr const * e) const {
return is_non_ground(e) && is_uninterp(e);
}
bool quasi_macros::is_unique(func_decl * f) const { bool quasi_macros::is_unique(func_decl * f) const {
return m_occurrences.find(f) == 1; return m_occurrences.find(f) == 1;
} }
@ -149,6 +153,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
// Our definition of a quasi-macro: // 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, // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
// f[X] contains all universally quantified variables, and f does not occur in T[X]. // f[X] contains all universally quantified variables, and f does not occur in T[X].
TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;);
if (is_quantifier(e) && to_quantifier(e)->is_forall()) { if (is_quantifier(e) && to_quantifier(e)->is_forall()) {
quantifier * q = to_quantifier(e); quantifier * q = to_quantifier(e);
@ -157,23 +162,23 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
expr * lhs = to_app(qe)->get_arg(0); expr * lhs = to_app(qe)->get_arg(0);
expr * rhs = to_app(qe)->get_arg(1); expr * rhs = to_app(qe)->get_arg(1);
if (is_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) && 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)) { !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
a = to_app(lhs); a = to_app(lhs);
t = rhs; t = rhs;
return true; return true;
} else if (is_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) && } 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)) { !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
a = to_app(rhs); a = to_app(rhs);
t = lhs; t = lhs;
return true; return true;
} }
} else if (m_manager.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0)) && } else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) &&
is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false
a = to_app(to_app(qe)->get_arg(0)); a = to_app(to_app(qe)->get_arg(0));
t = m_manager.mk_false(); t = m_manager.mk_false();
return true; return true;
} else if (is_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); a = to_app(qe);
t = m_manager.mk_true(); t = m_manager.mk_true();
return true; return true;

1
src/ast/macros/quasi_macros.h
View file

@ -45,6 +45,7 @@ class quasi_macros {
expr_mark m_visited_more; expr_mark m_visited_more;
bool is_unique(func_decl * f) const; bool is_unique(func_decl * f) const;
bool is_non_ground_uninterp(expr const * e) const;
bool fully_depends_on(app * a, quantifier * q) const; bool fully_depends_on(app * a, quantifier * q) const;
bool depends_on(expr * e, func_decl * f) const; bool depends_on(expr * e, func_decl * f) const;