From 19ed46569695beaad063db0a75ebd9d93b2e14aa Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 4 Mar 2020 16:40:36 +0000 Subject: [PATCH] Fix quasi-macro variable checks. Fixes #3029. --- src/ast/macros/macro_util.cpp | 44 ++++++++++++++++----------------- src/ast/macros/macro_util.h | 2 +- src/ast/macros/quasi_macros.cpp | 24 +++++++++--------- 3 files changed, 35 insertions(+), 35 deletions(-) diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index b7b1efd39..5bfac48ac 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -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 { switch (num_args) { - case 0: + case 0: r = mk_zero(s); break; 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 { expr * lhs = nullptr, * rhs = nullptr; - if (m_manager.is_eq(n, lhs, rhs) && - is_macro_head(lhs, num_decls) && + if (m_manager.is_eq(n, 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); @@ -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 { expr * lhs = nullptr, * rhs = nullptr; 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()) && !occurs(to_app(rhs)->get_decl(), lhs)) { 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. */ 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; TRACE("macro_util", tout << "processing: " << mk_pp(n, m_manager) << "\n";); 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. */ -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) && to_app(n)->get_family_id() == null_family_id && 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 found_vars; found_vars.resize(num_decls, false); unsigned num_found_vars = 0; + expr_free_vars fv; 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; + if (occurs(to_app(n)->get_decl(), arg)) + return false; + else + fv.accumulate(arg); + } + if (def) + fv.accumulate(def); + for (unsigned i = 0; i < fv.size(); i++) { + if (i >= num_decls || !fv.contains(i)) + continue; // Quasi-macros may have new variables. + if (found_vars[i] == false) { + found_vars[i] = true; + num_found_vars++; } } 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 { 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)); 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); } } - - - diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h index fecdeb97f..57ad2d851 100644 --- a/src/ast/macros/macro_util.h +++ b/src/ast/macros/macro_util.h @@ -112,7 +112,7 @@ public: 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_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 mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const; diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index 56faf39e8..e104c408b 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -23,7 +23,7 @@ Revision History: #include "ast/rewriter/var_subst.h" quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) : - m_manager(m), + m_manager(m), m_macro_manager(mm), m_rewriter(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) { 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; ); bool res = false; m_occurrences.reset(); - + // Find out how many non-ground appearances for each uninterpreted function there are for ( unsigned i = 0 ; i < n ; i++ ) find_occurrences(exprs[i].get_fml()); TRACE("quasi_macros", tout << "Occurrences: " << std::endl; - for (occurrences_map::iterator it = m_occurrences.begin(); - it != m_occurrences.end(); + for (occurrences_map::iterator it = m_occurrences.begin(); + it != m_occurrences.end(); it++) tout << it->m_key->get_name() << ": " << it->m_value << std::endl; ); - + // Find all macros for ( unsigned i = 0 ; i < n ; i++ ) { app_ref a(m_manager); @@ -329,17 +329,17 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) { 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++ ) { expr_ref r(m_manager), rs(m_manager); proof_ref pr(m_manager), ps(m_manager); expr_dependency_ref dep(m_manager); proof * p = m_manager.proofs_enabled() ? prs[i] : nullptr; - + m_macro_manager.expand_macros(exprs[i], p, deps[i], r, pr, dep); m_rewriter(r); new_exprs.push_back(r); - new_prs.push_back(ps); + new_prs.push_back(ps); 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)) { apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps); return true; - } + } else { // just copy them over 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& new_fmls) { +void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector& new_fmls) { for ( unsigned i = 0 ; i < n ; i++ ) { expr_ref r(m_manager), rs(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