diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 70803b361..a28d9c608 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -28,7 +28,7 @@ Revision History: #include "ast/rewriter/bool_rewriter.h" macro_util::macro_util(ast_manager & m): - m_manager(m), + m(m), m_bv(m), m_arith(m), m_arith_rw(m), @@ -176,7 +176,7 @@ 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) && + if (m.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)) { @@ -184,13 +184,13 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he def = rhs; return true; } - if (m_manager.is_not(n, lhs) && m_manager.is_eq(lhs, lhs, rhs) && - m_manager.is_bool(lhs) && + if (m.is_not(n, lhs) && m.is_eq(lhs, lhs, rhs) && + m.is_bool(lhs) && is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && !occurs(to_app(lhs)->get_decl(), rhs)) { head = to_app(lhs); - def = m_manager.mk_not(rhs); + def = m.mk_not(rhs); return true; } return false; @@ -216,7 +216,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) && + if (m.is_eq(n, lhs, rhs) && is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) && !occurs(to_app(rhs)->get_decl(), lhs)) { @@ -224,13 +224,13 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h def = lhs; return true; } - if (m_manager.is_not(n, n) && m_manager.is_eq(n, lhs, rhs) && - m_manager.is_bool(lhs) && + if (m.is_not(n, n) && m.is_eq(n, lhs, rhs) && + m.is_bool(lhs) && is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) && !occurs(to_app(rhs)->get_decl(), lhs)) { head = to_app(rhs); - def = m_manager.mk_not(lhs); + def = m.mk_not(lhs); return true; } return false; @@ -262,7 +262,7 @@ bool macro_util::poly_contains_head(expr * n, func_decl * f, expr * exception) c bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const { // TODO: obsolete... we should move to collect_arith_macro_candidates - if (!m_manager.is_eq(n) && !m_arith.is_le(n) && !m_arith.is_ge(n)) + if (!m.is_eq(n) && !m_arith.is_le(n) && !m_arith.is_ge(n)) return false; expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); @@ -306,7 +306,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex if (h == nullptr) return false; head = to_app(h); - expr_ref tmp(m_manager); + expr_ref tmp(m); tmp = m_arith.mk_add(args.size(), args.data()); if (inv) mk_sub(tmp, rhs, def); @@ -321,12 +321,12 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex */ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t) { expr* lhs = nullptr, *rhs = nullptr; - if (!m_manager.is_eq(n, lhs, rhs)) + if (!m.is_eq(n, lhs, rhs)) return false; if (!is_ground(lhs) && !is_ground(rhs)) return false; sort * s = lhs->get_sort(); - if (m_manager.is_uninterp(s)) + if (m.is_uninterp(s)) return false; sort_size sz = s->get_num_elements(); if (sz.is_finite() && sz.size() == 1) @@ -351,11 +351,11 @@ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, ap bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def) { if (!is_forall(n)) return false; - TRACE("macro_util", tout << "processing: " << mk_pp(n, m_manager) << "\n";); + TRACE("macro_util", tout << "processing: " << mk_pp(n, m) << "\n";); expr * body = to_quantifier(n)->get_expr(); unsigned num_decls = to_quantifier(n)->get_num_decls(); expr * lhs, *rhs; - if (!m_manager.is_iff(body, lhs, rhs)) + if (!m.is_iff(body, lhs, rhs)) return false; if (is_pseudo_head(lhs, num_decls, head, t) && !is_forbidden(head->get_decl()) && @@ -466,14 +466,14 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl continue; } } - var * new_var = m_manager.mk_var(next_var_idx, arg->get_sort()); + var * new_var = m.mk_var(next_var_idx, arg->get_sort()); next_var_idx++; - expr * new_cond = m_manager.mk_eq(new_var, arg); + expr * new_cond = m.mk_eq(new_var, arg); new_args.push_back(new_var); new_conds.push_back(new_cond); } - bool_rewriter(m_manager).mk_and(new_conds.size(), new_conds.data(), cond); - head = m_manager.mk_app(qhead->get_decl(), new_args.size(), new_args.data()); + bool_rewriter(m).mk_and(new_conds.size(), new_conds.data(), cond); + head = m.mk_app(qhead->get_decl(), new_args.size(), new_args.data()); num_decls = next_var_idx; } @@ -485,7 +485,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl See normalize_expr */ 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" << mk_pp(def, m_manager) << "\n";); + TRACE("macro_util", tout << mk_pp(head, m) << "\n" << mk_pp(def, m) << "\n";); SASSERT(is_macro_head(head, head->get_num_args()) || is_quasi_macro_ok(head, head->get_num_args(), def)); SASSERT(!occurs(head->get_decl(), def)); @@ -503,20 +503,20 @@ void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * f(x_3, x_2) --> f(x_0, x_1) */ void macro_util::normalize_expr(app * head, unsigned num_decls, expr * t, expr_ref & norm_t) const { - expr_ref_buffer var_mapping(m_manager); + expr_ref_buffer var_mapping(m); var_mapping.resize(num_decls); bool changed = false; unsigned num_args = head->get_num_args(); TRACE("macro_util", - tout << "head: " << mk_pp(head, m_manager) << "\n"; - tout << "applying substitution to:\n" << mk_bounded_pp(t, m_manager) << "\n";); + tout << "head: " << mk_pp(head, m) << "\n"; + tout << "applying substitution to:\n" << mk_bounded_pp(t, m) << "\n";); for (unsigned i = 0; i < num_args; i++) { var * v = to_var(head->get_arg(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_ref new_var(m.mk_var(i, v->get_sort()), m); var_mapping.setx(num_decls - vi - 1, new_var); } else @@ -525,13 +525,13 @@ void macro_util::normalize_expr(app * head, unsigned num_decls, expr * t, expr_r if (changed) { // REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution. - var_subst subst(m_manager, true); + var_subst subst(m, true); TRACE("macro_util", - tout << "head: " << mk_pp(head, m_manager) << "\n"; - tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n"; + tout << "head: " << mk_pp(head, m) << "\n"; + tout << "applying substitution to:\n" << mk_ll_pp(t, m) << "\nsubstitution:\n"; for (unsigned i = 0; i < var_mapping.size(); i++) { if (var_mapping[i] != 0) - tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager); + tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m); }); norm_t = subst(t, var_mapping.size(), var_mapping.data()); } @@ -642,8 +642,8 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned & num_decls, app_r is_hint_head(head, vars) must also return true */ bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) { - TRACE("macro_util", tout << "is_poly_hint n:\n" << mk_pp(n, m_manager) << "\nhead:\n" << mk_pp(head, m_manager) << "\nexception:\n"; - if (exception) tout << mk_pp(exception, m_manager); else tout << ""; + TRACE("macro_util", tout << "is_poly_hint n:\n" << mk_pp(n, m) << "\nhead:\n" << mk_pp(head, m) << "\nexception:\n"; + if (exception) tout << mk_pp(exception, m); else tout << ""; tout << "\n";); ptr_buffer vars; if (!is_hint_head(head, vars)) { @@ -664,7 +664,7 @@ bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) { for (unsigned i = 0; i < num_args; i++) { expr * arg = args[i]; if (arg != exception && (occurs(f, arg) || !vars_of_is_subset(arg, vars))) { - TRACE("macro_util", tout << "failed because of:\n" << mk_pp(arg, m_manager) << "\n";); + TRACE("macro_util", tout << "failed because of:\n" << mk_pp(arg, m) << "\n";); return false; } } @@ -710,36 +710,36 @@ void macro_util::macro_candidates::insert(func_decl * f, expr * def, expr * cond // ----------------------------- 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); + expr_ref norm_def(m); + expr_ref norm_cond(m); normalize_expr(head, num_decls, def, norm_def); if (cond != nullptr) normalize_expr(head, num_decls, cond, norm_cond); else if (!hint) - norm_cond = m_manager.mk_true(); + norm_cond = m.mk_true(); SASSERT(!hint || norm_cond.get() == 0); r.insert(head->get_decl(), norm_def.get(), norm_cond.get(), ineq, satisfy_atom, hint); } void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r) { - TRACE("macro_util", tout << expr_ref(head, m_manager) << "\n";); + TRACE("macro_util", tout << expr_ref(head, m) << "\n";); if (!is_macro_head(head, head->get_num_args())) { - app_ref new_head(m_manager); - expr_ref extra_cond(m_manager); - expr_ref new_cond(m_manager); + app_ref new_head(m); + expr_ref extra_cond(m); + expr_ref new_cond(m); if (!hint) { quasi_macro_head_to_macro_head(head, num_decls, new_head, extra_cond); if (cond == nullptr) new_cond = extra_cond; else - bool_rewriter(m_manager).mk_and(cond, extra_cond, new_cond); + bool_rewriter(m).mk_and(cond, extra_cond, new_cond); } else { - hint_to_macro_head(m_manager, head, num_decls, new_head); + hint_to_macro_head(m, 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; ); + tout << "hint macro head: " << mk_ismt2_pp(new_head, m) << std::endl; + tout << "hint macro def: " << mk_ismt2_pp(def, m) << std::endl; ); } insert_macro(new_head, num_decls, def, new_cond, ineq, satisfy_atom, hint, r); } @@ -751,10 +751,10 @@ void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, bool macro_util::rest_contains_decl(func_decl * f, expr * except_lit) { if (m_curr_clause == nullptr) return false; - SASSERT(is_clause(m_manager, m_curr_clause)); - unsigned num_lits = get_clause_num_literals(m_manager, m_curr_clause); + SASSERT(is_clause(m, m_curr_clause)); + unsigned num_lits = get_clause_num_literals(m, m_curr_clause); for (unsigned i = 0; i < num_lits; i++) { - expr * l = get_clause_literal(m_manager, m_curr_clause, i); + expr * l = get_clause_literal(m, m_curr_clause, i); if (l != except_lit && occurs(f, l)) return true; } @@ -764,20 +764,20 @@ bool macro_util::rest_contains_decl(func_decl * f, expr * except_lit) { void macro_util::get_rest_clause_as_cond(expr * except_lit, expr_ref & extra_cond) { if (m_curr_clause == nullptr) return; - SASSERT(is_clause(m_manager, m_curr_clause)); - expr_ref_buffer neg_other_lits(m_manager); - unsigned num_lits = get_clause_num_literals(m_manager, m_curr_clause); + SASSERT(is_clause(m, m_curr_clause)); + expr_ref_buffer neg_other_lits(m); + unsigned num_lits = get_clause_num_literals(m, m_curr_clause); for (unsigned i = 0; i < num_lits; i++) { - expr * l = get_clause_literal(m_manager, m_curr_clause, i); + expr * l = get_clause_literal(m, m_curr_clause, i); if (l != except_lit) { - expr_ref neg_l(m_manager); - bool_rewriter(m_manager).mk_not(l, neg_l); + expr_ref neg_l(m); + bool_rewriter(m).mk_not(l, neg_l); neg_other_lits.push_back(neg_l); } } if (neg_other_lits.empty()) return; - bool_rewriter(m_manager).mk_and(neg_other_lits.size(), neg_other_lits.data(), extra_cond); + bool_rewriter(m).mk_and(neg_other_lits.size(), neg_other_lits.data(), extra_cond); } void macro_util::collect_poly_args(expr * n, expr * exception, ptr_buffer & args) { @@ -800,14 +800,14 @@ void macro_util::collect_poly_args(expr * n, expr * exception, ptr_buffer } void macro_util::add_arith_macro_candidate(app * head, unsigned num_decls, expr * def, expr * atom, bool ineq, bool hint, macro_candidates & r) { - expr_ref cond(m_manager); + expr_ref cond(m); if (!hint) get_rest_clause_as_cond(atom, cond); insert_quasi_macro(head, num_decls, def, cond, ineq, true, hint, r); } void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * atom, unsigned num_decls, bool is_ineq, macro_candidates & r) { - if (!is_add(lhs) && m_manager.is_eq(atom)) // this case is a simple macro. + if (!is_add(lhs) && m.is_eq(atom)) // this case is a simple macro. return; ptr_buffer args; unsigned lhs_num_args; @@ -837,9 +837,9 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a if (_is_arith_macro || _is_poly_hint) { collect_poly_args(lhs, arg, args); - expr_ref rest(m_manager); + expr_ref rest(m); mk_add(args.size(), args.data(), arg->get_sort(), rest); - expr_ref def(m_manager); + expr_ref def(m); mk_sub(rhs, rest, def); // If is_poly_hint, rhs may contain variables that do not occur in to_app(arg). // So, we should re-check. @@ -858,9 +858,9 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a if (_is_arith_macro || _is_poly_hint) { collect_poly_args(lhs, arg, args); - expr_ref rest(m_manager); + expr_ref rest(m); mk_add(args.size(), args.data(), arg->get_sort(), rest); - expr_ref def(m_manager); + expr_ref def(m); mk_sub(rest, rhs, def); // If is_poly_hint, rhs may contain variables that do not occur in to_app(neg_arg). // So, we should re-check. @@ -872,12 +872,12 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a } void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls, macro_candidates & r) { - TRACE("macro_util", tout << "collect_arith_macro_candidates:\n" << mk_pp(atom, m_manager) << "\n";); - if (!m_manager.is_eq(atom) && !is_le_ge(atom)) + TRACE("macro_util", tout << "collect_arith_macro_candidates:\n" << mk_pp(atom, m) << "\n";); + if (!m.is_eq(atom) && !is_le_ge(atom)) return; expr * lhs = to_app(atom)->get_arg(0); expr * rhs = to_app(atom)->get_arg(1); - bool is_ineq = !m_manager.is_eq(atom); + bool is_ineq = !m.is_eq(atom); collect_arith_macro_candidates(lhs, rhs, atom, num_decls, is_ineq, r); collect_arith_macro_candidates(rhs, lhs, atom, num_decls, is_ineq, r); } @@ -921,14 +921,14 @@ 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;); + TRACE("macro_util", tout << "Candidate check for: " << mk_ismt2_pp(atom, m) << std::endl;); auto insert_quasi = [&](expr* lhs, expr* rhs) { if (is_quasi_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && !occurs(to_app(lhs)->get_decl(), rhs) && !rest_contains_decl(to_app(lhs)->get_decl(), atom)) { - expr_ref cond(m_manager); + expr_ref cond(m); get_rest_clause_as_cond(atom, cond); insert_quasi_macro(to_app(lhs), num_decls, rhs, cond, false, true, false, r); return true; @@ -941,16 +941,16 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, insert_quasi_macro(to_app(lhs), num_decls, rhs, nullptr, false, true, true, r); }; - if (m_manager.is_eq(atom, lhs, rhs)) { + if (m.is_eq(atom, lhs, rhs)) { if (!insert_quasi(lhs, rhs)) insert_hint(lhs, rhs); if (!insert_quasi(rhs, lhs)) insert_hint(rhs, lhs); } expr* atom2; - if (m_manager.is_not(atom, atom2) && m_manager.is_eq(atom2, lhs, rhs) && m_manager.is_bool(lhs)) { - expr_ref nlhs(m_manager.mk_not(lhs), m_manager); - expr_ref nrhs(m_manager.mk_not(rhs), m_manager); + if (m.is_not(atom, atom2) && m.is_eq(atom2, lhs, rhs) && m.is_bool(lhs)) { + expr_ref nlhs(m.mk_not(lhs), m); + expr_ref nrhs(m.mk_not(rhs), m); if (!insert_quasi(lhs, nrhs)) insert_hint(lhs, nrhs); if (!insert_quasi(rhs, nlhs)) @@ -973,11 +973,11 @@ void macro_util::collect_macro_candidates(quantifier * q, macro_candidates & r) return; unsigned num_decls = q->get_num_decls(); SASSERT(m_curr_clause == 0); - if (is_clause(m_manager, n)) { + if (is_clause(m, n)) { m_curr_clause = n; - unsigned num_lits = get_clause_num_literals(m_manager, n); + unsigned num_lits = get_clause_num_literals(m, n); for (unsigned i = 0; i < num_lits; i++) - collect_macro_candidates_core(get_clause_literal(m_manager, n, i), num_decls, r); + collect_macro_candidates_core(get_clause_literal(m, n, i), num_decls, r); m_curr_clause = nullptr; } else { diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h index 17b409c12..b714bd9e5 100644 --- a/src/ast/macros/macro_util.h +++ b/src/ast/macros/macro_util.h @@ -56,7 +56,7 @@ public: }; private: - ast_manager & m_manager; + ast_manager & m; bv_util m_bv; arith_util m_arith; mutable arith_rewriter m_arith_rw;