mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

Fix quasi-macro variable checks. Fixes #3029.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2020-03-04 16:40:36 +00:00
parent fcbf660592
commit 19ed465696
No known key found for this signature in database
GPG key ID: BCF6360F86294467
3 changed files with 35 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -104,7 +104,7 @@ void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const {
void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const { void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const {
switch (num_args) { switch (num_args) {
case 0: case 0:
r = mk_zero(s); r = mk_zero(s);
break; break;
case 1: case 1:
@ -176,8 +176,8 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const {
*/ */
bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const { bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
expr * lhs = nullptr, * rhs = nullptr; expr * lhs = nullptr, * rhs = nullptr;
if (m_manager.is_eq(n, lhs, rhs) && if (m_manager.is_eq(n, lhs, rhs) &&
is_macro_head(lhs, num_decls) && is_macro_head(lhs, num_decls) &&
!is_forbidden(to_app(lhs)->get_decl()) && !is_forbidden(to_app(lhs)->get_decl()) &&
!occurs(to_app(lhs)->get_decl(), rhs)) { !occurs(to_app(lhs)->get_decl(), rhs)) {
head = to_app(lhs); head = to_app(lhs);
@ -208,7 +208,7 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const { bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
expr * lhs = nullptr, * rhs = nullptr; expr * lhs = nullptr, * rhs = nullptr;
if (m_manager.is_eq(n, lhs, rhs) && if (m_manager.is_eq(n, lhs, rhs) &&
is_macro_head(rhs, num_decls) && is_macro_head(rhs, num_decls) &&
!is_forbidden(to_app(rhs)->get_decl()) && !is_forbidden(to_app(rhs)->get_decl()) &&
!occurs(to_app(rhs)->get_decl(), lhs)) { !occurs(to_app(rhs)->get_decl(), lhs)) {
head = to_app(rhs); head = to_app(rhs);
@ -331,7 +331,7 @@ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, ap
where t is a ground term, (f X) is the head. where t is a ground term, (f X) is the head.
*/ */
bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def) { bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def) {
if (!is_forall(n)) if (!is_forall(n))
return false; return false;
TRACE("macro_util", tout << "processing: " << mk_pp(n, m_manager) << "\n";); TRACE("macro_util", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
expr * body = to_quantifier(n)->get_expr(); expr * body = to_quantifier(n)->get_expr();
@ -366,7 +366,7 @@ 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) const { bool macro_util::is_quasi_macro_head(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) {
@ -374,20 +374,22 @@ bool macro_util::is_quasi_macro_head(expr * n, unsigned num_decls) const {
sbuffer<bool> found_vars; sbuffer<bool> found_vars;
found_vars.resize(num_decls, false); found_vars.resize(num_decls, false);
unsigned num_found_vars = 0; unsigned num_found_vars = 0;
expr_free_vars fv;
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(n)->get_arg(i); expr * arg = to_app(n)->get_arg(i);
if (is_var(arg)) { if (occurs(to_app(n)->get_decl(), arg))
unsigned idx = to_var(arg)->get_idx(); return false;
if (idx >= num_decls) else
return false; fv.accumulate(arg);
if (found_vars[idx] == false) { }
found_vars[idx] = true; if (def)
num_found_vars++; fv.accumulate(def);
} for (unsigned i = 0; i < fv.size(); i++) {
} if (i >= num_decls || !fv.contains(i))
else { continue; // Quasi-macros may have new variables.
if (occurs(to_app(n)->get_decl(), arg)) if (found_vars[i] == false) {
return false; found_vars[i] = true;
num_found_vars++;
} }
} }
return num_found_vars == num_decls; return num_found_vars == num_decls;
@ -437,7 +439,8 @@ 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));
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);
} }
@ -926,6 +929,3 @@ void macro_util::collect_macro_candidates(quantifier * q, macro_candidates & r)
collect_macro_candidates_core(n, num_decls, r); collect_macro_candidates_core(n, num_decls, r);
} }
} }

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

@ -112,7 +112,7 @@ 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) const; bool is_quasi_macro_head(expr * n, unsigned num_decls, expr * def = NULL) 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;

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

@ -23,7 +23,7 @@ Revision History:
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) : quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) :
m_manager(m), m_manager(m),
m_macro_manager(mm), m_macro_manager(mm),
m_rewriter(m), m_rewriter(m),
m_new_vars(m), m_new_vars(m),
@ -293,22 +293,22 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) { bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl; TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl;
for (unsigned i = 0 ; i < n ; i++) for (unsigned i = 0 ; i < n ; i++)
tout << i << ": " << mk_pp(exprs[i].get_fml(), m_manager) << std::endl; ); tout << i << ": " << mk_pp(exprs[i].get_fml(), m_manager) << std::endl; );
bool res = false; bool res = false;
m_occurrences.reset(); m_occurrences.reset();
// Find out how many non-ground appearances for each uninterpreted function there are // Find out how many non-ground appearances for each uninterpreted function there are
for ( unsigned i = 0 ; i < n ; i++ ) for ( unsigned i = 0 ; i < n ; i++ )
find_occurrences(exprs[i].get_fml()); find_occurrences(exprs[i].get_fml());
TRACE("quasi_macros", tout << "Occurrences: " << std::endl; TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
for (occurrences_map::iterator it = m_occurrences.begin(); for (occurrences_map::iterator it = m_occurrences.begin();
it != m_occurrences.end(); it != m_occurrences.end();
it++) it++)
tout << it->m_key->get_name() << ": " << it->m_value << std::endl; ); tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
// Find all macros // Find all macros
for ( unsigned i = 0 ; i < n ; i++ ) { for ( unsigned i = 0 ; i < n ; i++ ) {
app_ref a(m_manager); app_ref a(m_manager);
@ -329,17 +329,17 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
return res; return res;
} }
void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps) { void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps) {
for ( unsigned i = 0 ; i < n ; i++ ) { for ( unsigned i = 0 ; i < n ; i++ ) {
expr_ref r(m_manager), rs(m_manager); expr_ref r(m_manager), rs(m_manager);
proof_ref pr(m_manager), ps(m_manager); proof_ref pr(m_manager), ps(m_manager);
expr_dependency_ref dep(m_manager); expr_dependency_ref dep(m_manager);
proof * p = m_manager.proofs_enabled() ? prs[i] : nullptr; proof * p = m_manager.proofs_enabled() ? prs[i] : nullptr;
m_macro_manager.expand_macros(exprs[i], p, deps[i], r, pr, dep); m_macro_manager.expand_macros(exprs[i], p, deps[i], r, pr, dep);
m_rewriter(r); m_rewriter(r);
new_exprs.push_back(r); new_exprs.push_back(r);
new_prs.push_back(ps); new_prs.push_back(ps);
new_deps.push_back(dep); new_deps.push_back(dep);
} }
} }
@ -348,7 +348,7 @@ bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const *
if (find_macros(n, exprs)) { if (find_macros(n, exprs)) {
apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps); apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps);
return true; return true;
} }
else { else {
// just copy them over // just copy them over
for ( unsigned i = 0 ; i < n ; i++ ) { for ( unsigned i = 0 ; i < n ; i++ ) {
@ -360,7 +360,7 @@ bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const *
} }
} }
void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) { void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
for ( unsigned i = 0 ; i < n ; i++ ) { for ( unsigned i = 0 ; i < n ; i++ ) {
expr_ref r(m_manager), rs(m_manager); expr_ref r(m_manager), rs(m_manager);
proof_ref pr(m_manager), ps(m_manager); proof_ref pr(m_manager), ps(m_manager);
@ -382,5 +382,5 @@ bool quasi_macros::operator()(unsigned n, justified_expr const* fmls, vector<jus
new_fmls.push_back(fmls[i]); new_fmls.push_back(fmls[i]);
} }
return false; return false;
} }
} }