diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index 75b4e55f4..b17e1ce28 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -106,7 +106,7 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) { if (!m_deps.insert(f, s)) { return false; } - + // add macro m_decl2macro.insert(f, m); m_decls.push_back(f); @@ -117,8 +117,8 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) { } TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";); - - // Nothing's forbidden anymore; if something's bad, we detected it earlier. + + // Nothing's forbidden anymore; if something's bad, we detected it earlier. // mark_forbidden(m->get_expr()); return true; } @@ -144,7 +144,7 @@ namespace macro_manager_ns { \brief Mark all func_decls used in exprs as forbidden. */ void macro_manager::mark_forbidden(unsigned n, expr * const * exprs) { - expr_mark visited; + expr_mark visited; macro_manager_ns::proc p(m_forbidden_set, m_forbidden); for (unsigned i = 0; i < n; i++) for_each_expr(p, visited, exprs[i]); @@ -187,9 +187,9 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter app * head; expr * def; get_head_def(q, f, head, def); - TRACE("macro_bug", + TRACE("macro_bug", tout << f->get_name() << "\n" << mk_pp(head, m_manager) << "\n" << mk_pp(q, m_manager) << "\n";); - m_util.mk_macro_interpretation(head, def, interp); + m_util.mk_macro_interpretation(head, q->get_num_decls(), def, interp); return f; } @@ -237,7 +237,7 @@ void macro_manager::macro_expander::reduce1_quantifier(quantifier * q) { erase_patterns = true; } for (unsigned i = 0; !erase_patterns && i < q->get_num_no_patterns(); i++) { - if (q->get_no_pattern(i) != new_q->get_no_pattern(i)) + if (q->get_no_pattern(i) != new_q->get_no_pattern(i)) erase_patterns = true; } } @@ -254,7 +254,7 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref return false; app * n = to_app(_n); quantifier * q = 0; - func_decl * d = n->get_decl(); + func_decl * d = n->get_decl(); TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";); if (m_macro_manager.m_decl2macro.find(d, q)) { TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";); @@ -308,7 +308,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref if (r.get() == old_n.get()) return; old_n = r; - old_pr = new_pr; + old_pr = new_pr; } } else { diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 97b44d4cd..99732871c 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -405,7 +405,7 @@ bool macro_util::is_quasi_macro_head(expr * n, unsigned num_decls) const { \brief Convert a quasi-macro head into a macro head, and store the conditions under which it is valid in cond. */ -void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, app_ref & head, expr_ref & cond) const { +void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decls, app_ref & head, expr_ref & cond) const { unsigned num_args = qhead->get_num_args(); sbuffer found_vars; found_vars.resize(num_decls, false); @@ -431,6 +431,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, } get_basic_simp()->mk_and(new_conds.size(), new_conds.c_ptr(), cond); head = m_manager.mk_app(qhead->get_decl(), new_args.size(), new_args.c_ptr()); + num_decls = next_var_idx; } /** @@ -440,10 +441,10 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, See normalize_expr */ -void macro_util::mk_macro_interpretation(app * head, expr * def, expr_ref & interp) const { +void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const { SASSERT(is_macro_head(head, head->get_num_args())); SASSERT(!occurs(head->get_decl(), def)); - normalize_expr(head, def, interp); + normalize_expr(head, num_decls, def, interp); } /** @@ -456,36 +457,27 @@ void macro_util::mk_macro_interpretation(app * head, expr * def, expr_ref & inte f(x_1, x_2) --> f(x_0, x_1) f(x_3, x_2) --> f(x_0, x_1) */ -void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const { - expr_ref_buffer var_mapping(m_manager); +void macro_util::normalize_expr(app * head, unsigned num_decls, expr * t, expr_ref & norm_t) const { + expr_ref_buffer var_mapping(m_manager); + var_mapping.resize(num_decls); bool changed = false; unsigned num_args = head->get_num_args(); - unsigned max_var_idx = 0; - for (unsigned i = 0; i < num_args; i++) { - var const * v = to_var(head->get_arg(i)); - if (v->get_idx() > max_var_idx) - max_var_idx = v->get_idx(); - } TRACE("macro_util", tout << "head: " << mk_pp(head, m_manager) << "\n"; tout << "applying substitution to:\n" << mk_bounded_pp(t, m_manager) << "\n";); for (unsigned i = 0; i < num_args; i++) { var * v = to_var(head->get_arg(i)); - if (v->get_idx() != i) { + unsigned vi = v->get_idx(); + SASSERT(vi < num_decls); + if (vi != i) { changed = true; var_ref new_var(m_manager.mk_var(i, v->get_sort()), m_manager); - var_mapping.setx(max_var_idx - v->get_idx(), new_var); + var_mapping.setx(num_decls - vi - 1, new_var); } else - var_mapping.setx(max_var_idx - i, v); + var_mapping.setx(num_decls - i - 1, v); } - for (unsigned i = num_args; i <= max_var_idx; i++) - // CMW: Won't be used, but dictates a larger binding size, - // so that the indexes between here and in the rewriter match. - // It's possible that we don't see the true max idx of all vars here. - var_mapping.setx(max_var_idx - i, 0); - if (changed) { // REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution. var_subst subst(m_manager, true); @@ -573,7 +565,7 @@ bool is_hint_atom(expr * lhs, expr * rhs) { return !occurs(to_app(lhs)->get_decl(), rhs) && vars_of_is_subset(rhs, vars); } -void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref & new_head) { +void hint_to_macro_head(ast_manager & m, app * head, unsigned & num_decls, app_ref & new_head) { unsigned num_args = head->get_num_args(); ptr_buffer new_args; sbuffer found_vars; @@ -595,6 +587,7 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref new_args.push_back(new_var); } new_head = m.mk_app(head->get_decl(), new_args.size(), new_args.c_ptr()); + num_decls = next_var_idx; } /** @@ -671,12 +664,12 @@ void macro_util::macro_candidates::insert(func_decl * f, expr * def, expr * cond // // ----------------------------- -void macro_util::insert_macro(app * head, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r) { +void macro_util::insert_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r) { expr_ref norm_def(m_manager); expr_ref norm_cond(m_manager); - normalize_expr(head, def, norm_def); + normalize_expr(head, num_decls, def, norm_def); if (cond != 0) - normalize_expr(head, cond, norm_cond); + normalize_expr(head, num_decls, cond, norm_cond); else if (!hint) norm_cond = m_manager.mk_true(); SASSERT(!hint || norm_cond.get() == 0); @@ -698,11 +691,14 @@ void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, } else { hint_to_macro_head(m_manager, head, num_decls, new_head); + TRACE("macro_util", + tout << "hint macro head: " << mk_ismt2_pp(new_head, m_manager) << std::endl; + tout << "hint macro def: " << mk_ismt2_pp(def, m_manager) << std::endl; ); } - insert_macro(new_head, def, new_cond, ineq, satisfy_atom, hint, r); + insert_macro(new_head, num_decls, def, new_cond, ineq, satisfy_atom, hint, r); } else { - insert_macro(head, def, cond, ineq, satisfy_atom, hint, r); + insert_macro(head, num_decls, def, cond, ineq, satisfy_atom, hint, r); } } @@ -879,6 +875,9 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls, */ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, macro_candidates & r) { expr* lhs, *rhs; + + TRACE("macro_util", tout << "Candidate check for: " << mk_ismt2_pp(atom, m_manager) << std::endl;); + if (m_manager.is_eq(atom, lhs, rhs) || m_manager.is_iff(atom, lhs, rhs)) { if (is_quasi_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h index 18b00c1f7..033f6ecb4 100644 --- a/src/ast/macros/macro_util.h +++ b/src/ast/macros/macro_util.h @@ -74,9 +74,9 @@ private: void collect_arith_macros(expr * n, unsigned num_decls, unsigned max_macros, bool allow_cond_macros, macro_candidates & r); - void normalize_expr(app * head, expr * t, expr_ref & norm_t) const; - void insert_macro(app * head, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r); - void insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, + void normalize_expr(app * head, unsigned num_decls, expr * t, expr_ref & norm_t) const; + void insert_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r); + void insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r); expr * m_curr_clause; // auxiliary var used in collect_macro_candidates. @@ -105,7 +105,7 @@ public: bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const; bool is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const; bool is_simple_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref & def) const { - return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def); + return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def); } bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const; @@ -113,20 +113,20 @@ public: bool inv; return is_arith_macro(n, num_decls, head, def, inv); } - + 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; - 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, expr * def, expr_ref & interp) const; + void mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const; void collect_macro_candidates(expr * atom, unsigned num_decls, macro_candidates & r); void collect_macro_candidates(quantifier * q, macro_candidates & r); // - // Auxiliary goodness that allows us to manipulate BV and Arith polynomials. + // Auxiliary goodness that allows us to manipulate BV and Arith polynomials. // bool is_bv(expr * n) const; bool is_bv_sort(sort * s) const;