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

Fix quasi-macro detection

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2020-03-04 18:06:38 +00:00
parent 67497ba897
commit 6b12da0b45
No known key found for this signature in database
GPG key ID: BCF6360F86294467
2 changed files with 33 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/ast/macros/macro_util.cpp
View file

@ -366,7 +366,36 @@ bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t
Return true if \c n is a quasi-macro. Store the macro head in \c head, and the conditions to apply the macro in \c cond. Return true if \c n is a quasi-macro. Store the macro head in \c head, and the conditions to apply the macro in \c cond.
*/ */
bool macro_util::is_quasi_macro_head(expr * n, unsigned num_decls, expr * def) const { bool macro_util::is_quasi_macro_head(expr * n, unsigned num_decls) const {
if (is_app(n) &&
to_app(n)->get_family_id() == null_family_id &&
to_app(n)->get_num_args() >= num_decls) {
unsigned num_args = to_app(n)->get_num_args();
sbuffer<bool> found_vars;
found_vars.resize(num_decls, false);
unsigned num_found_vars = 0;
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(n)->get_arg(i);
if (is_var(arg)) {
unsigned idx = to_var(arg)->get_idx();
if (idx >= num_decls)
return false;
if (found_vars[idx] == false) {
found_vars[idx] = true;
num_found_vars++;
}
}
else {
if (occurs(to_app(n)->get_decl(), arg))
return false;
}
}
return num_found_vars == num_decls;
}
return false;
}
bool macro_util::is_quasi_macro_ok(expr * n, unsigned num_decls, expr * def) const {
if (is_app(n) && if (is_app(n) &&
to_app(n)->get_family_id() == null_family_id && to_app(n)->get_family_id() == null_family_id &&
to_app(n)->get_num_args() >= num_decls) { to_app(n)->get_num_args() >= num_decls) {
@ -440,7 +469,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl
void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const { void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const {
TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n";); TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n";);
SASSERT(is_macro_head(head, head->get_num_args()) || SASSERT(is_macro_head(head, head->get_num_args()) ||
is_quasi_macro_head(head, head->get_num_args(), def)); is_quasi_macro_ok(head, head->get_num_args(), def));
SASSERT(!occurs(head->get_decl(), def)); SASSERT(!occurs(head->get_decl(), def));
normalize_expr(head, num_decls, def, interp); normalize_expr(head, num_decls, def, interp);
} }

3
src/ast/macros/macro_util.h
View file

@ -112,7 +112,8 @@ public:
bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t); bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t);
bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def); bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def);
bool is_quasi_macro_head(expr * n, unsigned num_decls, expr * def = NULL) const; bool is_quasi_macro_head(expr * n, unsigned num_decls) const;
bool is_quasi_macro_ok(expr * n, unsigned num_decls, expr * def) const;
void quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decls, app_ref & head, expr_ref & cond) const; void quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decls, app_ref & head, expr_ref & cond) const;
void mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const; void mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const;