From cf7bba62880c3f9a215d20e05b757a16a5da0a23 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Dec 2022 07:53:32 -0800 Subject: [PATCH] use ast_manager as an attribute --- src/ast/rewriter/arith_rewriter.cpp | 226 +++++++++---------- src/ast/rewriter/arith_rewriter.h | 24 +- src/ast/rewriter/bv_rewriter.cpp | 321 +++++++++++++-------------- src/ast/rewriter/bv_rewriter.h | 13 +- src/ast/rewriter/poly_rewriter.h | 1 - src/ast/rewriter/poly_rewriter_def.h | 42 ++-- 6 files changed, 311 insertions(+), 316 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index cdf09d7f388..c2a9b4cf4cd 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -24,7 +24,7 @@ Module Name: seq_util& arith_rewriter_core::seq() { if (!m_seq) { - m_seq = alloc(seq_util, m()); + m_seq = alloc(seq_util, m); } return *m_seq; } @@ -93,9 +93,9 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_TANH: SASSERT(num_args == 1); st = mk_tanh_core(args[0], result); break; default: st = BR_FAILED; break; } - CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m()); - for (unsigned i = 0; i < num_args; ++i) tout << mk_pp(args[i], m()) << " "; - tout << "\n==>\n" << mk_pp(result.get(), m()) << "\n"; + CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m); + for (unsigned i = 0; i < num_args; ++i) tout << mk_pp(args[i], m) << " "; + tout << "\n==>\n" << mk_pp(result.get(), m) << "\n"; if (is_app(result)) tout << "args: " << to_app(result)->get_num_args() << "\n"; ); return st; @@ -133,7 +133,7 @@ bool arith_rewriter::div_polynomial(expr * t, numeral const & g, const_treatment SASSERT(!g.is_one()); unsigned sz; expr * const * ms = get_monomials(t, sz); - expr_ref_buffer new_args(m()); + expr_ref_buffer new_args(m); numeral a; for (unsigned i = 0; i < sz; i++) { expr * arg = ms[i]; @@ -196,10 +196,10 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & switch (kind) { case LE: c = floor(c); break; case GE: c = ceil(c); break; - case EQ: result = m().mk_false(); return true; + case EQ: result = m.mk_false(); return true; } } - expr_ref k(m_util.mk_numeral(c, is_int), m()); + expr_ref k(m_util.mk_numeral(c, is_int), m); switch (kind) { case LE: result = m_util.mk_le(pp, k); return true; case GE: result = m_util.mk_ge(pp, k); return true; @@ -223,24 +223,24 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & if (c.is_neg()) { switch (kind) { case EQ: - case LE: result = m().mk_false(); return true; - case GE: result = m().mk_true(); return true; + case LE: result = m.mk_false(); return true; + case GE: result = m.mk_true(); return true; } } if (c.is_zero() && kind == GE) { - result = m().mk_true(); + result = m.mk_true(); return true; } if (c.is_pos() && c >= abs(b)) { switch (kind) { - case LE: result = m().mk_true(); return true; + case LE: result = m.mk_true(); return true; case EQ: - case GE: result = m().mk_false(); return true; + case GE: result = m.mk_false(); return true; } } // mod x b <= b - 1 if (c + rational::one() == abs(b) && kind == LE) { - result = m().mk_true(); + result = m.mk_true(); return true; } } @@ -304,7 +304,7 @@ br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, exp if (kind != LE && kind != GE) return BR_FAILED; rational bound(0), r1, r2; - expr_ref narg(m()); + expr_ref narg(m); bool has_bound = true; if (!m_util.is_numeral(arg2, r2)) return BR_FAILED; @@ -335,47 +335,47 @@ br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, exp if (kind == GE && r1 > r2) return BR_FAILED; if (kind == LE && r1 > r2) { - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } if (kind == GE && r1 < r2) { - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } SASSERT(r1 == r2); - expr_ref zero(m_util.mk_numeral(rational(0), arg1->get_sort()), m()); + expr_ref zero(m_util.mk_numeral(rational(0), arg1->get_sort()), m); if (r1.is_zero() && m_util.is_mul(arg1)) { - expr_ref_buffer eqs(m()); + expr_ref_buffer eqs(m); ptr_buffer args; flat_mul(arg1, args); for (expr* arg : args) { if (m_util.is_numeral(arg)) continue; - eqs.push_back(m().mk_eq(arg, zero)); + eqs.push_back(m.mk_eq(arg, zero)); } - result = m().mk_or(eqs); + result = m.mk_or(eqs); return BR_REWRITE2; } if (kind == LE && m_util.is_add(arg1)) { - expr_ref_buffer leqs(m()); + expr_ref_buffer leqs(m); for (expr* arg : *to_app(arg1)) { if (!m_util.is_numeral(arg)) leqs.push_back(m_util.mk_le(arg, zero)); } - result = m().mk_and(leqs); + result = m.mk_and(leqs); return BR_REWRITE2; } if (kind == GE && m_util.is_add(arg1)) { - expr_ref_buffer geqs(m()); + expr_ref_buffer geqs(m); for (expr* arg : *to_app(arg1)) { if (!m_util.is_numeral(arg)) geqs.push_back(m_util.mk_ge(arg, zero)); } - result = m().mk_and(geqs); + result = m.mk_and(geqs); return BR_REWRITE2; } @@ -399,8 +399,8 @@ bool arith_rewriter::elim_to_real_var(expr * var, expr_ref & new_var) { bool arith_rewriter::elim_to_real_mon(expr * monomial, expr_ref & new_monomial) { if (m_util.is_mul(monomial)) { - expr_ref_buffer new_vars(m()); - expr_ref new_var(m()); + expr_ref_buffer new_vars(m); + expr_ref new_var(m); unsigned num = to_app(monomial)->get_num_args(); for (unsigned i = 0; i < num; i++) { if (!elim_to_real_var(to_app(monomial)->get_arg(i), new_var)) @@ -417,8 +417,8 @@ bool arith_rewriter::elim_to_real_mon(expr * monomial, expr_ref & new_monomial) bool arith_rewriter::elim_to_real_pol(expr * p, expr_ref & new_p) { if (m_util.is_add(p)) { - expr_ref_buffer new_monomials(m()); - expr_ref new_monomial(m()); + expr_ref_buffer new_monomials(m); + expr_ref new_monomial(m); for (expr* arg : *to_app(p)) { if (!elim_to_real_mon(arg, new_monomial)) return false; @@ -507,14 +507,14 @@ br_status arith_rewriter::reduce_power(expr * arg1, expr * arg2, op_kind kind, e switch (kind) { case LE: result = m_util.mk_le(new_arg1, new_arg2); return BR_REWRITE1; case GE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_REWRITE1; - default: result = m().mk_eq(new_arg1, new_arg2); return BR_REWRITE1; + default: result = m.mk_eq(new_arg1, new_arg2); return BR_REWRITE1; } } br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) { expr *orig_arg1 = arg1, *orig_arg2 = arg2; - expr_ref new_arg1(m()); - expr_ref new_arg2(m()); + expr_ref new_arg1(m); + expr_ref new_arg2(m); if ((is_zero(arg1) && is_reduce_power_target(arg2, kind == EQ)) || (is_zero(arg2) && is_reduce_power_target(arg1, kind == EQ))) return reduce_power(arg1, arg2, kind, result); @@ -524,29 +524,29 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin arg1 = new_arg1; arg2 = new_arg2; } - expr_ref new_new_arg1(m()); - expr_ref new_new_arg2(m()); + expr_ref new_new_arg1(m); + expr_ref new_new_arg2(m); if (m_elim_to_real && elim_to_real(arg1, arg2, new_new_arg1, new_new_arg2)) { arg1 = new_new_arg1; arg2 = new_new_arg2; - CTRACE("elim_to_real", m_elim_to_real, tout << "after_elim_to_real\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";); + CTRACE("elim_to_real", m_elim_to_real, tout << "after_elim_to_real\n" << mk_ismt2_pp(arg1, m) << "\n" << mk_ismt2_pp(arg2, m) << "\n";); if (st == BR_FAILED) st = BR_DONE; } numeral a1, a2; if (is_numeral(arg1, a1) && is_numeral(arg2, a2)) { switch (kind) { - case LE: result = a1 <= a2 ? m().mk_true() : m().mk_false(); return BR_DONE; - case GE: result = a1 >= a2 ? m().mk_true() : m().mk_false(); return BR_DONE; - default: result = a1 == a2 ? m().mk_true() : m().mk_false(); return BR_DONE; + case LE: result = a1 <= a2 ? m.mk_true() : m.mk_false(); return BR_DONE; + case GE: result = a1 >= a2 ? m.mk_true() : m.mk_false(); return BR_DONE; + default: result = a1 == a2 ? m.mk_true() : m.mk_false(); return BR_DONE; } } #define ANUM_LE_GE_EQ() { \ switch (kind) { \ - case LE: result = am.le(v1, v2) ? m().mk_true() : m().mk_false(); return BR_DONE; \ - case GE: result = am.ge(v1, v2) ? m().mk_true() : m().mk_false(); return BR_DONE; \ - default: result = am.eq(v1, v2) ? m().mk_true() : m().mk_false(); return BR_DONE; \ + case LE: result = am.le(v1, v2) ? m.mk_true() : m.mk_false(); return BR_DONE; \ + case GE: result = am.ge(v1, v2) ? m.mk_true() : m.mk_false(); return BR_DONE; \ + default: result = am.eq(v1, v2) ? m.mk_true() : m.mk_false(); return BR_DONE; \ } \ } @@ -593,12 +593,12 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin if (!first && !g.is_one() && num_consts <= 1) { bool is_sat = div_polynomial(arg1, g, (kind == LE ? CT_CEIL : (kind == GE ? CT_FLOOR : CT_FALSE)), new_arg1); if (!is_sat) { - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } is_sat = div_polynomial(arg2, g, (kind == LE ? CT_FLOOR : (kind == GE ? CT_CEIL : CT_FALSE)), new_arg2); if (!is_sat) { - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } arg1 = new_arg1.get(); @@ -607,25 +607,25 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin } } expr* c = nullptr, *t = nullptr, *e = nullptr; - if (m().is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) { + if (m.is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) { switch (kind) { - case LE: result = a1 <= a2 ? m().mk_or(c, m_util.mk_le(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_le(e, arg2)); return BR_REWRITE2; - case GE: result = a1 >= a2 ? m().mk_or(c, m_util.mk_ge(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_ge(e, arg2)); return BR_REWRITE2; - case EQ: result = a1 == a2 ? m().mk_or(c, m().mk_eq(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_eq(e, arg2)); return BR_REWRITE2; + case LE: result = a1 <= a2 ? m.mk_or(c, m_util.mk_le(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_le(e, arg2)); return BR_REWRITE2; + case GE: result = a1 >= a2 ? m.mk_or(c, m_util.mk_ge(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_ge(e, arg2)); return BR_REWRITE2; + case EQ: result = a1 == a2 ? m.mk_or(c, m.mk_eq(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_eq(e, arg2)); return BR_REWRITE2; } } - if (m().is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) { + if (m.is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) { switch (kind) { - case LE: result = a1 <= a2 ? m().mk_or(m().mk_not(c), m_util.mk_le(t, arg2)) : m().mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2; - case GE: result = a1 >= a2 ? m().mk_or(m().mk_not(c), m_util.mk_ge(t, arg2)) : m().mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2; - case EQ: result = a1 == a2 ? m().mk_or(m().mk_not(c), m().mk_eq(t, arg2)) : m().mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2; + case LE: result = a1 <= a2 ? m.mk_or(m.mk_not(c), m_util.mk_le(t, arg2)) : m.mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2; + case GE: result = a1 >= a2 ? m.mk_or(m.mk_not(c), m_util.mk_ge(t, arg2)) : m.mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2; + case EQ: result = a1 == a2 ? m.mk_or(m.mk_not(c), m.mk_eq(t, arg2)) : m.mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2; } } - if (m().is_ite(arg1, c, t, e) && arg1->get_ref_count() == 1) { + if (m.is_ite(arg1, c, t, e) && arg1->get_ref_count() == 1) { switch (kind) { - case LE: result = m().mk_ite(c, m_util.mk_le(t, arg2), m_util.mk_le(e, arg2)); return BR_REWRITE2; - case GE: result = m().mk_ite(c, m_util.mk_ge(t, arg2), m_util.mk_ge(e, arg2)); return BR_REWRITE2; - case EQ: result = m().mk_ite(c, m().mk_eq(t, arg2), m().mk_eq(e, arg2)); return BR_REWRITE2; + case LE: result = m.mk_ite(c, m_util.mk_le(t, arg2), m_util.mk_le(e, arg2)); return BR_REWRITE2; + case GE: result = m.mk_ite(c, m_util.mk_ge(t, arg2), m_util.mk_ge(e, arg2)); return BR_REWRITE2; + case EQ: result = m.mk_ite(c, m.mk_eq(t, arg2), m.mk_eq(e, arg2)); return BR_REWRITE2; } } if (m_util.is_to_int(arg2) && is_numeral(arg1)) { @@ -642,7 +642,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin return BR_REWRITE1; case EQ: result = m_util.mk_ge(t, m_util.mk_numeral(a2, false)); - result = m().mk_and(m_util.mk_lt(t, m_util.mk_numeral(a2+1, false)), result); + result = m.mk_and(m_util.mk_lt(t, m_util.mk_numeral(a2+1, false)), result); return BR_REWRITE3; } } @@ -663,7 +663,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin switch (kind) { case LE: result = m_util.mk_le(arg1, arg2); return BR_DONE; case GE: result = m_util.mk_ge(arg1, arg2); return BR_DONE; - default: result = m().mk_eq(arg1, arg2); return BR_DONE; + default: result = m.mk_eq(arg1, arg2); return BR_DONE; } } return BR_FAILED; @@ -674,7 +674,7 @@ br_status arith_rewriter::mk_le_core(expr * arg1, expr * arg2, expr_ref & result } br_status arith_rewriter::mk_lt_core(expr * arg1, expr * arg2, expr_ref & result) { - result = m().mk_not(m_util.mk_le(arg2, arg1)); + result = m.mk_not(m_util.mk_le(arg2, arg1)); return BR_REWRITE2; } @@ -683,7 +683,7 @@ br_status arith_rewriter::mk_ge_core(expr * arg1, expr * arg2, expr_ref & result } br_status arith_rewriter::mk_gt_core(expr * arg1, expr * arg2, expr_ref & result) { - result = m().mk_not(m_util.mk_le(arg1, arg2)); + result = m.mk_not(m_util.mk_le(arg1, arg2)); return BR_REWRITE2; } @@ -694,7 +694,7 @@ bool arith_rewriter::is_arith_term(expr * n) const { br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { br_status st = BR_FAILED; if (m_eq2ineq) { - result = m().mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2)); + result = m.mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2)); st = BR_REWRITE2; } else if (m_arith_lhs || is_arith_term(arg1) || is_arith_term(arg2)) { @@ -724,7 +724,7 @@ br_status arith_rewriter::mk_and_core(unsigned n, expr* const* args, expr_ref& r } if (rest.size() < n - 1) { rest.push_back(arg0); - result = m().mk_and(rest); + result = m.mk_and(rest); return BR_REWRITE1; } } @@ -742,8 +742,8 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) { rational a, b; rational g = gcd(p, k, a, b); if (g == 1) { - expr_ref nb(m_util.mk_numeral(b, true), m()); - result = m().mk_eq(m_util.mk_mod(u, y), + expr_ref nb(m_util.mk_numeral(b, true), m); + result = m.mk_eq(m_util.mk_mod(u, y), m_util.mk_mod(m_util.mk_mul(nb, arg2), y)); return true; } @@ -752,7 +752,7 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) { } expr_ref arith_rewriter::neg_monomial(expr* e) const { - expr_ref_vector args(m()); + expr_ref_vector args(m); rational a1; if (m_util.is_numeral(e, a1)) args.push_back(m_util.mk_numeral(-a1, e->get_sort())); @@ -773,10 +773,10 @@ expr_ref arith_rewriter::neg_monomial(expr* e) const { args.push_back(e); } if (args.size() == 1) { - return expr_ref(args.back(), m()); + return expr_ref(args.back(), m); } else { - return expr_ref(m_util.mk_mul(args.size(), args.data()), m()); + return expr_ref(m_util.mk_mul(args.size(), args.data()), m); } } @@ -793,7 +793,7 @@ bool arith_rewriter::is_neg_poly(expr* t, expr_ref& neg) const { expr * t2 = to_app(t)->get_arg(0); if (m_util.is_mul(t2) && is_numeral(to_app(t2)->get_arg(0), r) && r.is_neg()) { - expr_ref_vector args1(m()); + expr_ref_vector args1(m); for (expr* e1 : *to_app(t)) { args1.push_back(neg_monomial(e1)); } @@ -826,7 +826,7 @@ bool arith_rewriter::is_anum_simp_target(unsigned num_args, expr * const * args) br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, expr_ref & result) { if (is_anum_simp_target(num_args, args)) { - expr_ref_buffer new_args(m()); + expr_ref_buffer new_args(m); anum_manager & am = m_util.am(); scoped_anum r(am); scoped_anum arg(am); @@ -864,7 +864,7 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex new_args.push_back(m_util.mk_numeral(am, r, false)); br_status st = poly_rewriter::mk_add_core(new_args.size(), new_args.data(), result); if (st == BR_FAILED) { - result = m().mk_app(get_fid(), OP_ADD, new_args.size(), new_args.data()); + result = m.mk_app(get_fid(), OP_ADD, new_args.size(), new_args.data()); return BR_DONE; } return st; @@ -876,7 +876,7 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) { if (is_anum_simp_target(num_args, args)) { - expr_ref_buffer new_args(m()); + expr_ref_buffer new_args(m); anum_manager & am = m_util.am(); scoped_anum r(am); scoped_anum arg(am); @@ -913,7 +913,7 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex br_status st = poly_rewriter::mk_mul_core(new_args.size(), new_args.data(), result); if (st == BR_FAILED) { - result = m().mk_app(get_fid(), OP_MUL, new_args.size(), new_args.data()); + result = m.mk_app(get_fid(), OP_MUL, new_args.size(), new_args.data()); return BR_DONE; } return st; @@ -998,7 +998,7 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul else { numeral k(1); k /= v2; - result = m().mk_app(get_fid(), OP_MUL, + result = m.mk_app(get_fid(), OP_MUL, m_util.mk_numeral(k, false), arg1); return BR_REWRITE1; @@ -1028,8 +1028,8 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul v1 /= v2; result = m_util.mk_mul(m_util.mk_numeral(v1, false), m_util.mk_div(b, d)); - expr_ref z(m_util.mk_real(0), m()); - result = m().mk_ite(m().mk_eq(d, z), m_util.mk_div(arg1, z), result); + expr_ref z(m_util.mk_real(0), m); + result = m.mk_ite(m.mk_eq(d, z), m_util.mk_div(arg1, z), result); return BR_REWRITE2; } } @@ -1039,7 +1039,7 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul } br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) { - result = m().mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0)); + result = m.mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0)); return BR_REWRITE2; } @@ -1063,12 +1063,12 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu return BR_FAILED; } if (arg1 == arg2) { - expr_ref zero(m_util.mk_int(0), m()); - result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); + expr_ref zero(m_util.mk_int(0), m); + result = m.mk_ite(m.mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); return BR_REWRITE3; } if (m_util.is_numeral(arg2, v2, is_int) && v2.is_pos() && m_util.is_add(arg1)) { - expr_ref_buffer args(m()); + expr_ref_buffer args(m); bool change = false; rational add(0); for (expr* arg : *to_app(arg1)) { @@ -1083,15 +1083,15 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu } } if (change) { - result = m_util.mk_idiv(m().mk_app(to_app(arg1)->get_decl(), args.size(), args.data()), arg2); + result = m_util.mk_idiv(m.mk_app(to_app(arg1)->get_decl(), args.size(), args.data()), arg2); result = m_util.mk_add(m_util.mk_numeral(add, true), result); TRACE("div_bug", tout << "mk_div result: " << result << "\n";); return BR_REWRITE3; } } if (divides(arg1, arg2, result)) { - expr_ref zero(m_util.mk_int(0), m()); - result = m().mk_ite(m().mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result); + expr_ref zero(m_util.mk_int(0), m); + result = m.mk_ite(m.mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result); return BR_REWRITE_FULL; } return BR_FAILED; @@ -1150,17 +1150,17 @@ expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) { flat_mul(den, args2); remove_divisor(arg, args1); remove_divisor(arg, args2); - expr_ref zero(m_util.mk_int(0), m()); + expr_ref zero(m_util.mk_int(0), m); num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.data()); den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.data()); - expr_ref d(m_util.mk_idiv(num, den), m()); - expr_ref nd(m_util.mk_idiv(m_util.mk_uminus(num), m_util.mk_uminus(den)), m()); - return expr_ref(m().mk_ite(m().mk_eq(zero, arg), + expr_ref d(m_util.mk_idiv(num, den), m); + expr_ref nd(m_util.mk_idiv(m_util.mk_uminus(num), m_util.mk_uminus(den)), m); + return expr_ref(m.mk_ite(m.mk_eq(zero, arg), m_util.mk_idiv(zero, zero), - m().mk_ite(m_util.mk_ge(arg, zero), + m.mk_ite(m_util.mk_ge(arg, zero), d, nd)), - m()); + m); } void arith_rewriter::flat_mul(expr* e, ptr_buffer& args) { @@ -1208,8 +1208,8 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul } if (arg1 == arg2 && !m_util.is_numeral(arg2)) { - expr_ref zero(m_util.mk_int(0), m()); - result = m().mk_ite(m().mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero); + expr_ref zero(m_util.mk_int(0), m); + result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero); return BR_DONE; } @@ -1222,8 +1222,8 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul // propagate mod inside only if there is something to reduce. if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { - TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";); - expr_ref_buffer args(m()); + TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m) << "\n" << mk_ismt2_pp(arg2, m) << "\n";); + expr_ref_buffer args(m); bool change = false; for (expr* arg : *to_app(arg1)) { rational arg_v; @@ -1246,8 +1246,8 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul if (!change) { return BR_FAILED; // did not find any target for applying simplification } - result = m_util.mk_mod(m().mk_app(to_app(arg1)->get_decl(), args.size(), args.data()), arg2); - TRACE("mod_bug", tout << "mk_mod result: " << mk_ismt2_pp(result, m()) << "\n";); + result = m_util.mk_mod(m.mk_app(to_app(arg1)->get_decl(), args.size(), args.data()), arg2); + TRACE("mod_bug", tout << "mk_mod result: " << mk_ismt2_pp(result, m) << "\n";); return BR_REWRITE3; } @@ -1290,10 +1290,10 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul } else if (m_elim_rem) { expr * mod = m_util.mk_mod(arg1, arg2); - result = m().mk_ite(m_util.mk_ge(arg2, m_util.mk_numeral(rational(0), true)), + result = m.mk_ite(m_util.mk_ge(arg2, m_util.mk_numeral(rational(0), true)), mod, m_util.mk_uminus(mod)); - TRACE("elim_rem", tout << "result: " << mk_ismt2_pp(result, m()) << "\n";); + TRACE("elim_rem", tout << "result: " << mk_ismt2_pp(result, m) << "\n";); return BR_REWRITE3; } return BR_FAILED; @@ -1322,7 +1322,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res bool is_num_y = m_util.is_numeral(arg2, y); auto ensure_real = [&](expr* e) { return m_util.is_int(e) ? m_util.mk_to_real(e) : e; }; - TRACE("arith", tout << mk_pp(arg1, m()) << " " << mk_pp(arg2, m()) << "\n";); + TRACE("arith", tout << mk_pp(arg1, m) << " " << mk_pp(arg2, m) << "\n";); if (is_num_x && x.is_one()) { result = m_util.mk_numeral(x, false); return BR_DONE; @@ -1377,7 +1377,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res if (is_num_y && y.is_minus_one()) { result = m_util.mk_div(m_util.mk_real(1), ensure_real(arg1)); - result = m().mk_ite(m().mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))), + result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))), m_util.mk_real(0), result); return BR_REWRITE2; @@ -1387,7 +1387,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res // (^ t -k) --> (^ (/ 1 t) k) result = m_util.mk_power(m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1), m_util.mk_numeral(-y, false)); - result = m().mk_ite(m().mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))), + result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))), m_util.mk_real(0), result); return BR_REWRITE3; @@ -1504,7 +1504,7 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { // Try to apply simplifications such as: // (to_int (+ 1.0 (to_real x)) y) --> (+ 1 x (to_int y)) - expr_ref_buffer int_args(m()), real_args(m()); + expr_ref_buffer int_args(m), real_args(m); for (expr* c : *to_app(arg)) { if (m_util.is_numeral(c, a) && a.is_int()) { int_args.push_back(m_util.mk_numeral(a, true)); @@ -1520,17 +1520,17 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { return BR_FAILED; if (real_args.empty()) { - result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.data()); + result = m.mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.data()); return BR_REWRITE1; } if (!int_args.empty() && m_util.is_add(arg)) { decl_kind k = to_app(arg)->get_decl()->get_decl_kind(); - expr_ref t1(m().mk_app(get_fid(), k, int_args.size(), int_args.data()), m()); - expr_ref t2(m().mk_app(get_fid(), k, real_args.size(), real_args.data()), m()); + expr_ref t1(m.mk_app(get_fid(), k, int_args.size(), int_args.data()), m); + expr_ref t2(m.mk_app(get_fid(), k, real_args.size(), real_args.data()), m); int_args.reset(); int_args.push_back(t1); int_args.push_back(m_util.mk_to_int(t2)); - result = m().mk_app(get_fid(), k, int_args.size(), int_args.data()); + result = m.mk_app(get_fid(), k, int_args.size(), int_args.data()); return BR_REWRITE3; } } @@ -1550,9 +1550,9 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) { for (expr* e : *to_app(arg)) new_args.push_back(m_util.mk_to_real(e)); if (m_util.is_add(arg)) - result = m().mk_app(get_fid(), OP_ADD, new_args.size(), new_args.data()); + result = m.mk_app(get_fid(), OP_ADD, new_args.size(), new_args.data()); else - result = m().mk_app(get_fid(), OP_MUL, new_args.size(), new_args.data()); + result = m.mk_app(get_fid(), OP_MUL, new_args.size(), new_args.data()); return BR_REWRITE2; } } @@ -1562,23 +1562,23 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) { br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) { numeral a; if (m_util.is_numeral(arg, a)) { - result = a.is_int() ? m().mk_true() : m().mk_false(); + result = a.is_int() ? m.mk_true() : m.mk_false(); return BR_DONE; } else if (m_util.is_to_real(arg)) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } else { - result = m().mk_eq(m().mk_app(get_fid(), OP_TO_REAL, - m().mk_app(get_fid(), OP_TO_INT, arg)), + result = m.mk_eq(m.mk_app(get_fid(), OP_TO_REAL, + m.mk_app(get_fid(), OP_TO_INT, arg)), arg); return BR_REWRITE3; } } br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) { - result = m().mk_ite(m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg))), arg, m_util.mk_uminus(arg)); + result = m.mk_ite(m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg))), arg, m_util.mk_uminus(arg)); return BR_REWRITE2; } @@ -1647,9 +1647,9 @@ bool arith_rewriter::is_pi_integer(expr * t) { a = c; b = d; } - TRACE("tan", tout << "is_pi_integer " << mk_ismt2_pp(t, m()) << "\n"; - tout << "a: " << mk_ismt2_pp(a, m()) << "\n"; - tout << "b: " << mk_ismt2_pp(b, m()) << "\n";); + TRACE("tan", tout << "is_pi_integer " << mk_ismt2_pp(t, m) << "\n"; + tout << "a: " << mk_ismt2_pp(a, m) << "\n"; + tout << "b: " << mk_ismt2_pp(b, m) << "\n";); return (m_util.is_pi(a) && m_util.is_to_real(b)) || (m_util.is_to_real(a) && m_util.is_pi(b)); @@ -1861,7 +1861,7 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) { } if (is_pi_multiple(arg, k)) { - expr_ref n(m()), d(m()); + expr_ref n(m), d(m); n = mk_sin_value(k); if (n.get() == nullptr) goto end; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index c80226d0cf7..3cd9d6165a4 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -25,13 +25,13 @@ Module Name: class arith_rewriter_core { protected: typedef rational numeral; + ast_manager& m; arith_util m_util; scoped_ptr m_seq; - bool m_expand_power{ false }; - bool m_mul2power{ false }; - bool m_expand_tan{ false }; + bool m_expand_power = false; + bool m_mul2power = false; + bool m_expand_tan = false; - ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } seq_util& seq(); @@ -47,7 +47,7 @@ class arith_rewriter_core { app* mk_power(expr* x, rational const& r, sort* s); expr* coerce(expr* x, sort* s); public: - arith_rewriter_core(ast_manager & m):m_util(m) {} + arith_rewriter_core(ast_manager & m):m(m), m_util(m) {} bool is_zero(expr * n) const { return m_util.is_zero(n); } }; @@ -120,7 +120,7 @@ class arith_rewriter : public poly_rewriter { br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { if (mk_app_core(f, num_args, args, result) == BR_FAILED) - result = m().mk_app(f, num_args, args); + result = m.mk_app(f, num_args, args); } br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result); @@ -159,30 +159,30 @@ class arith_rewriter : public poly_rewriter { br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result); void mk_div(expr * arg1, expr * arg2, expr_ref & result) { if (mk_div_core(arg1, arg2, result) == BR_FAILED) - result = m().mk_app(get_fid(), OP_DIV, arg1, arg2); + result = m.mk_app(get_fid(), OP_DIV, arg1, arg2); } void mk_idiv(expr * arg1, expr * arg2, expr_ref & result) { if (mk_idiv_core(arg1, arg2, result) == BR_FAILED) - result = m().mk_app(get_fid(), OP_IDIV, arg1, arg2); + result = m.mk_app(get_fid(), OP_IDIV, arg1, arg2); } void mk_mod(expr * arg1, expr * arg2, expr_ref & result) { if (mk_mod_core(arg1, arg2, result) == BR_FAILED) - result = m().mk_app(get_fid(), OP_MOD, arg1, arg2); + result = m.mk_app(get_fid(), OP_MOD, arg1, arg2); } void mk_rem(expr * arg1, expr * arg2, expr_ref & result) { if (mk_rem_core(arg1, arg2, result) == BR_FAILED) - result = m().mk_app(get_fid(), OP_REM, arg1, arg2); + result = m.mk_app(get_fid(), OP_REM, arg1, arg2); } br_status mk_to_int_core(expr * arg, expr_ref & result); br_status mk_to_real_core(expr * arg, expr_ref & result); void mk_to_int(expr * arg, expr_ref & result) { if (mk_to_int_core(arg, result) == BR_FAILED) - result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg); + result = m.mk_app(get_fid(), OP_TO_INT, 1, &arg); } void mk_to_real(expr * arg, expr_ref & result) { if (mk_to_real_core(arg, result) == BR_FAILED) - result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg); + result = m.mk_app(get_fid(), OP_TO_REAL, 1, &arg); } br_status mk_is_int(expr * arg, expr_ref & result); diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 972259bd724..1557c9b3cd8 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -217,7 +217,7 @@ br_status bv_rewriter::mk_uge(expr * a, expr * b, expr_ref & result) { } br_status bv_rewriter::mk_ult(expr * a, expr * b, expr_ref & result) { - result = m().mk_not(m_util.mk_ule(b, a)); + result = m.mk_not(m_util.mk_ule(b, a)); return BR_REWRITE2; } @@ -234,7 +234,7 @@ br_status bv_rewriter::mk_sge(expr * a, expr * b, expr_ref & result) { } br_status bv_rewriter::mk_slt(expr * a, expr * b, expr_ref & result) { - result = m().mk_not(m_util.mk_sle(b, a)); + result = m.mk_not(m_util.mk_sle(b, a)); return BR_REWRITE2; } @@ -300,7 +300,7 @@ bool bv_rewriter::are_eq_upto_num(expr * _a, expr * _b, if (has_num_b) is_numeral(b->get_arg(0), b0_val, b0_sz); SASSERT(a0_sz == m_util.get_bv_size(a) && b0_sz == m_util.get_bv_size(a)); if (has_num_a && numa > 2) { - common = m().mk_app(m_util.get_fid(), add_decl_kind(), numa - 1, a->get_args() + 1); + common = m.mk_app(m_util.get_fid(), add_decl_kind(), numa - 1, a->get_args() + 1); } else { common = has_num_a ? a->get_arg(1) : a; @@ -311,13 +311,13 @@ bool bv_rewriter::are_eq_upto_num(expr * _a, expr * _b, // simplifies expressions as (bvuleq (X + c1) (X + c2)) for some common expression X and numerals c1, c2 br_status bv_rewriter::rw_leq_overflow(bool is_signed, expr * a, expr * b, expr_ref & result) { if (is_signed) return BR_FAILED; - expr_ref common(m()); + expr_ref common(m); numeral a0_val, b0_val; if (!are_eq_upto_num(a, b, common, a0_val, b0_val)) return BR_FAILED; SASSERT(a0_val.is_nonneg() && b0_val.is_nonneg()); const unsigned sz = m_util.get_bv_size(a); if (a0_val == b0_val) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } if (a0_val < b0_val) { @@ -329,14 +329,14 @@ br_status bv_rewriter::rw_leq_overflow(bool is_signed, expr * a, expr * b, expr_ const numeral lower = rational::power_of_two(sz) - a0_val; const numeral upper = rational::power_of_two(sz) - b0_val - numeral::one(); if (lower == upper) { - result = m().mk_eq(common, mk_numeral(lower, sz)); + result = m.mk_eq(common, mk_numeral(lower, sz)); } else if (b0_val.is_zero()) { result = m_util.mk_ule(mk_numeral(lower, sz), common); } else { SASSERT(lower.is_pos()); - result = m().mk_and(m_util.mk_ule(mk_numeral(lower, sz), common), + result = m.mk_and(m_util.mk_ule(mk_numeral(lower, sz), common), m_util.mk_ule(common, mk_numeral(upper, sz))); } return BR_REWRITE2; @@ -363,11 +363,11 @@ br_status bv_rewriter::rw_leq_concats(bool is_signed, expr * _a, expr * _b, expr const numeral hi_bf = m_util.norm(bf_sz > sz_min ? div(bf, rational::power_of_two(bf_sz - sz_min)) : bf, sz_min, is_signed); if (hi_af != hi_bf) { - result = hi_af < hi_bf ? m().mk_true() : m().mk_false(); + result = hi_af < hi_bf ? m.mk_true() : m.mk_false(); return BR_DONE; } - expr_ref new_a(m()); - expr_ref new_b(m()); + expr_ref new_a(m); + expr_ref new_b(m); if (af_sz > sz_min) { ptr_buffer new_args; new_args.push_back(mk_numeral(af, af_sz - sz_min)); @@ -391,11 +391,11 @@ br_status bv_rewriter::rw_leq_concats(bool is_signed, expr * _a, expr * _b, expr { // common prefix unsigned common = 0; - while (common < num_min && m().are_equal(a->get_arg(common), b->get_arg(common))) ++common; + while (common < num_min && m.are_equal(a->get_arg(common), b->get_arg(common))) ++common; SASSERT((common == numa) == (common == numb)); if (common == numa) { SASSERT(0); // shouldn't get here as both sides are equal - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } if (common > 0) { @@ -411,13 +411,13 @@ br_status bv_rewriter::rw_leq_concats(bool is_signed, expr * _a, expr * _b, expr while (new_numa && new_numb) { expr * const last_a = a->get_arg(new_numa - 1); expr * const last_b = b->get_arg(new_numb - 1); - if (!m().are_equal(last_a, last_b)) break; + if (!m.are_equal(last_a, last_b)) break; new_numa--; new_numb--; } if (new_numa == 0) { SASSERT(0); // shouldn't get here as both sides are equal - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } if (new_numa != numa) { @@ -438,7 +438,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref bool is_num2 = is_numeral(b, r2, sz); if (a == b) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } @@ -448,7 +448,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref r2 = m_util.norm(r2, sz, is_signed); if (is_num1 && is_num2) { - result = m().mk_bool_val(r1 <= r2); + result = m.mk_bool_val(r1 <= r2); return BR_DONE; } @@ -467,11 +467,11 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref if (is_num2) { if (r2 == lower) { - result = m().mk_eq(a, b); + result = m.mk_eq(a, b); return BR_REWRITE1; } if (r2 == upper) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } } @@ -479,13 +479,13 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref if (is_num1) { // 0 <= b is true if (r1 == lower) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } // 2^n-1 <= b is a = b if (r1 == upper) { - result = m().mk_eq(a, b); + result = m.mk_eq(a, b); return BR_REWRITE1; } } @@ -512,12 +512,10 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref // other cases r1 > r2, r1 < r2 are TBD if (!is_signed && is_num1 && m_util.is_bv_add(b, a1, a2) && is_numeral(a1, r2, sz)) { result = m_util.mk_ule(a2, m_util.mk_numeral(-r2 - 1, sz)); - if (r1 > r2) { - result = m().mk_and(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2)); - } - else if (r1 < r2) { - result = m().mk_or(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2)); - } + if (r1 > r2) + result = m.mk_and(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2)); + else if (r1 < r2) + result = m.mk_or(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2)); return BR_REWRITE2; } @@ -525,7 +523,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref const br_status cst = rw_leq_concats(is_signed, a, b, result); if (cst != BR_FAILED) { TRACE("le_extra", tout << (is_signed ? "bv_sle\n" : "bv_ule\n") - << mk_ismt2_pp(a, m(), 2) << "\n" << mk_ismt2_pp(b, m(), 2) << "\n--->\n"<< mk_ismt2_pp(result, m(), 2) << "\n";); + << mk_ismt2_pp(a, m, 2) << "\n" << mk_ismt2_pp(b, m, 2) << "\n--->\n"<< mk_ismt2_pp(result, m, 2) << "\n";); return cst; } } @@ -534,7 +532,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref const br_status cst = rw_leq_overflow(is_signed, a, b, result); if (cst != BR_FAILED) { TRACE("le_extra", tout << (is_signed ? "bv_sle\n" : "bv_ule\n") - << mk_ismt2_pp(a, m(), 2) << "\n" << mk_ismt2_pp(b, m(), 2) << "\n--->\n"<< mk_ismt2_pp(result, m(), 2) << "\n";); + << mk_ismt2_pp(a, m, 2) << "\n" << mk_ismt2_pp(b, m, 2) << "\n--->\n"<< mk_ismt2_pp(result, m, 2) << "\n";); return cst; } } @@ -548,7 +546,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref expr * b_2 = to_app(b)->get_arg(1); unsigned sz1 = get_bv_size(b_1); unsigned sz2 = get_bv_size(b_2); - result = m().mk_and(m().mk_eq(m_mk_extract(sz2+sz1-1, sz2, a), b_1), + result = m.mk_and(m.mk_eq(m_mk_extract(sz2+sz1-1, sz2, a), b_1), m_util.mk_ule(m_mk_extract(sz2-1, 0, a), b_2)); return BR_REWRITE3; } @@ -572,11 +570,11 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref if (first_non_zero == UINT_MAX) { // all bits are zero - result = m().mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz)); + result = m.mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz)); return BR_REWRITE1; } else if (first_non_zero < bv_sz - 1 && m_le2extract) { - result = m().mk_and(m().mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), m_util.mk_numeral(numeral(0), bv_sz - first_non_zero - 1)), + result = m.mk_and(m.mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), m_util.mk_numeral(numeral(0), bv_sz - first_non_zero - 1)), m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b))); return BR_REWRITE3; } @@ -673,7 +671,7 @@ unsigned bv_rewriter::propagate_extract(unsigned high, expr * arg, expr_ref & re } if (new_arg) new_args.push_back(new_arg); } - result = m().mk_app(get_fid(), a->get_decl()->get_decl_kind(), new_args.size(), new_args.data()); + result = m.mk_app(get_fid(), a->get_decl()->get_decl_kind(), new_args.size(), new_args.data()); SASSERT(m_util.is_bv(result)); return removable; } @@ -777,17 +775,17 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ expr * curr = to_app(arg)->get_arg(i); new_args.push_back(m_mk_extract(high, low, curr)); } - result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), new_args.size(), new_args.data()); + result = m.mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), new_args.size(), new_args.data()); return BR_REWRITE2; } if (m_extract_prop && (high >= low)) { - expr_ref ep_res(m()); + expr_ref ep_res(m); const unsigned ep_rm = propagate_extract(high, arg, ep_res); if (ep_rm != 0) { result = m_mk_extract(high, low, ep_res); - TRACE("extract_prop", tout << mk_ismt2_pp(arg, m()) << "\n[" << high <<"," << low << "]\n" << ep_rm << "---->\n" - << mk_ismt2_pp(result.get(), m()) << "\n";); + TRACE("extract_prop", tout << mk_ismt2_pp(arg, m) << "\n[" << high <<"," << low << "]\n" << ep_rm << "---->\n" + << mk_ismt2_pp(result.get(), m) << "\n";); return BR_REWRITE2; } } @@ -797,9 +795,9 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ // branch of ite to be expanded or if one of the expanded ite branches have a single // reference count. expr* c = nullptr, *t = nullptr, *e = nullptr; - if (m().is_ite(arg, c, t, e) && - (t->get_ref_count() == 1 || e->get_ref_count() == 1 || !m().is_ite(t) || !m().is_ite(e))) { - result = m().mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e)); + if (m.is_ite(arg, c, t, e) && + (t->get_ref_count() == 1 || e->get_ref_count() == 1 || !m.is_ite(t) || !m.is_ite(e))) { + result = m.mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e)); return BR_REWRITE2; } @@ -855,9 +853,9 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { expr* x = nullptr, *y = nullptr; if (m_util.is_bv_shl(arg1, x, y)) { - expr_ref sum(m_util.mk_bv_add(y, arg2), m()); - expr_ref cond(m_util.mk_ule(y, sum), m()); - result = m().mk_ite(cond, + expr_ref sum(m_util.mk_bv_add(y, arg2), m); + expr_ref cond(m_util.mk_ule(y, sum), m); + result = m.mk_ite(cond, m_util.mk_bv_shl(x, sum), mk_numeral(0, bv_size)); return BR_REWRITE3; @@ -989,7 +987,7 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) { r1 += r2; if (r1 > numeral(bv_size)) r1 = numeral(bv_size); - result = m().mk_app(get_fid(), OP_BASHR, + result = m.mk_app(get_fid(), OP_BASHR, to_app(arg1)->get_arg(0), mk_numeral(r1, bv_size)); return BR_REWRITE1; // not really needed at this time. @@ -1029,7 +1027,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e } else { // The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff) - result = m().mk_ite(m().mk_app(get_fid(), OP_SLT, arg1, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_app(get_fid(), OP_SLT, arg1, mk_numeral(0, bv_size)), mk_numeral(1, bv_size), mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size)); return BR_REWRITE2; @@ -1057,7 +1055,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m().mk_ite(m().mk_eq(arg2, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), m_util.mk_bv_sdiv0(arg1), m_util.mk_bv_sdiv_i(arg1, arg2)); return BR_REWRITE2; @@ -1097,7 +1095,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e unsigned shift; if (r2.is_power_of_two(shift)) { - result = m().mk_app(get_fid(), OP_BLSHR, arg1, mk_numeral(shift, bv_size)); + result = m.mk_app(get_fid(), OP_BLSHR, arg1, mk_numeral(shift, bv_size)); return BR_REWRITE1; } @@ -1112,11 +1110,11 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m().mk_ite(m().mk_eq(arg2, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), m_util.mk_bv_udiv0(arg1), m_util.mk_bv_udiv_i(arg1, arg2)); - TRACE("bv_udiv", tout << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n---->\n" << mk_ismt2_pp(result, m()) << "\n";); + TRACE("bv_udiv", tout << mk_ismt2_pp(arg1, m) << "\n" << mk_ismt2_pp(arg2, m) << "\n---->\n" << mk_ismt2_pp(result, m) << "\n";); return BR_REWRITE2; } @@ -1128,7 +1126,7 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e r2 = m_util.norm(r2, bv_size, true); if (r2.is_zero()) { if (!hi_div0) { - result = m().mk_app(get_fid(), OP_BSREM0, arg1); + result = m.mk_app(get_fid(), OP_BSREM0, arg1); return BR_REWRITE1; } else { @@ -1149,19 +1147,19 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e return BR_DONE; } - result = m().mk_app(get_fid(), OP_BSREM_I, arg1, arg2); + result = m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2); return BR_DONE; } if (hi_div0) { - result = m().mk_app(get_fid(), OP_BSREM_I, arg1, arg2); + result = m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2); return BR_DONE; } bv_size = get_bv_size(arg2); - result = m().mk_ite(m().mk_eq(arg2, mk_numeral(0, bv_size)), - m().mk_app(get_fid(), OP_BSREM0, arg1), - m().mk_app(get_fid(), OP_BSREM_I, arg1, arg2)); + result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), + m.mk_app(get_fid(), OP_BSREM0, arg1), + m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2)); return BR_REWRITE2; } @@ -1253,7 +1251,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e // urem(0, x) ==> ite(x = 0, urem0(x), 0) if (is_num1 && r1.is_zero()) { expr * zero = arg1; - result = m().mk_ite(m().mk_eq(arg2, zero), + result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_bv_urem0(zero), zero); return BR_REWRITE2; @@ -1265,7 +1263,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e bv_size = get_bv_size(arg1); expr * x_minus_1 = arg1; expr * minus_one = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size); - result = m().mk_ite(m().mk_eq(x, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(x, mk_numeral(0, bv_size)), m_util.mk_bv_urem0(minus_one), x_minus_1); return BR_REWRITE2; @@ -1295,7 +1293,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m().mk_ite(m().mk_eq(arg2, mk_numeral(0, bv_size)), + result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), m_util.mk_bv_urem0(arg1), m_util.mk_bv_urem_i(arg1, arg2)); return BR_REWRITE2; @@ -1357,8 +1355,8 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e !m_util.is_concat(a) && !m_util.is_concat(b)) { unsigned nb = r2.get_num_bits(); - expr_ref a1(m_util.mk_bv_smod(a, arg2), m()); - expr_ref a2(m_util.mk_bv_smod(b, arg2), m()); + expr_ref a1(m_util.mk_bv_smod(a, arg2), m); + expr_ref a2(m_util.mk_bv_smod(b, arg2), m); a1 = m_util.mk_concat( mk_numeral(0, bv_size - nb), m_mk_extract(nb-1,0,a1)); a2 = m_util.mk_concat( mk_numeral(0, bv_size - nb), m_mk_extract(nb-1,0,a2)); result = m_util.mk_bv_mul(a1, a2); @@ -1371,14 +1369,14 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e } if (hi_div0) { - result = m().mk_app(get_fid(), OP_BSMOD_I, arg1, arg2); + result = m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2); return BR_DONE; } bv_size = get_bv_size(arg2); - result = m().mk_ite(m().mk_eq(arg2, mk_numeral(0, bv_size)), - m().mk_app(get_fid(), OP_BSMOD0, arg1), - m().mk_app(get_fid(), OP_BSMOD_I, arg1, arg2)); + result = m.mk_ite(m.mk_eq(arg2, mk_numeral(0, bv_size)), + m.mk_app(get_fid(), OP_BSMOD0, arg1), + m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2)); return BR_REWRITE2; } @@ -1413,7 +1411,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) { result = m_autil.mk_int(0); return BR_DONE; } - expr_ref_vector args(m()); + expr_ref_vector args(m); unsigned num_args = to_app(arg)->get_num_args(); for (expr* x : *to_app(arg)) { @@ -1421,7 +1419,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) { } unsigned sz = get_bv_size(to_app(arg)->get_arg(num_args-1)); for (unsigned i = num_args - 1; i > 0; ) { - expr_ref tmp(m()); + expr_ref tmp(m); --i; tmp = args[i].get(); tmp = m_autil.mk_mul(m_autil.mk_numeral(power(numeral(2), sz), true), tmp); @@ -1432,13 +1430,13 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) { return BR_REWRITE2; } if (is_mul_no_overflow(arg)) { - expr_ref_vector args(m()); + expr_ref_vector args(m); for (expr* x : *to_app(arg)) args.push_back(m_util.mk_bv2int(x)); result = m_autil.mk_mul(args.size(), args.data()); return BR_REWRITE2; } if (is_add_no_overflow(arg)) { - expr_ref_vector args(m()); + expr_ref_vector args(m); for (expr* x : *to_app(arg)) args.push_back(m_util.mk_bv2int(x)); result = m_autil.mk_add(args.size(), args.data()); return BR_REWRITE2; @@ -1507,7 +1505,7 @@ unsigned bv_rewriter::num_leading_zero_bits(expr* e) { br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_ref & result) { - expr_ref_buffer new_args(m()); + expr_ref_buffer new_args(m); numeral v1; numeral v2; unsigned sz1, sz2; @@ -1554,11 +1552,11 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re if (!fused_numeral && !expanded && !fused_extract) { expr* x, *y, *z; if (eq_args) { - if (m().is_ite(new_args.back(), x, y, z)) { + if (m.is_ite(new_args.back(), x, y, z)) { ptr_buffer args1, args2; for (expr* arg : new_args) args1.push_back(y), args2.push_back(z); - result = m().mk_ite(x, m_util.mk_concat(args1), m_util.mk_concat(args2)); + result = m.mk_ite(x, m_util.mk_concat(args1), m_util.mk_concat(args2)); return BR_REWRITE2; } } @@ -1776,8 +1774,8 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re std::reverse(exs.begin(), exs.end()); result = m_util.mk_concat(exs.size(), exs.data()); TRACE("mask_bug", - tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m()) << ")\n"; - tout << mk_ismt2_pp(result, m()) << "))\n";); + tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m) << ")\n"; + tout << mk_ismt2_pp(result, m) << "))\n";); return BR_REWRITE2; } @@ -1896,8 +1894,8 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r } SASSERT(t != 0); numeral two(2); - expr_ref_buffer exs(m()); - expr_ref not_t(m()); + expr_ref_buffer exs(m); + expr_ref not_t(m); not_t = m_util.mk_bv_not(t); unsigned low = 0; unsigned i = 0; @@ -1936,7 +1934,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r } ptr_buffer new_args; - expr_ref c(m()); // may not be used + expr_ref c(m); // may not be used if (!v1.is_zero()) { c = mk_numeral(v1, sz); new_args.push_back(c); @@ -1990,13 +1988,13 @@ bool bv_rewriter::distribute_concat(decl_kind k, unsigned n, expr* const* args, expr* e = to_app(arg)->get_arg(0); unsigned sz1 = get_bv_size(e); unsigned sz2 = get_bv_size(arg); - expr_ref_vector args1(m()), args2(m()); + expr_ref_vector args1(m), args2(m); for (unsigned j = 0; j < n; ++j) { args1.push_back(m_mk_extract(sz2 - 1, sz2 - sz1, args[j])); args2.push_back(m_mk_extract(sz2 - sz1 - 1, 0, args[j])); } - expr* arg1 = m().mk_app(get_fid(), k, args1.size(), args1.data()); - expr* arg2 = m().mk_app(get_fid(), k, args2.size(), args2.data()); + expr* arg1 = m.mk_app(get_fid(), k, args1.size(), args1.data()); + expr* arg2 = m.mk_app(get_fid(), k, args2.size(), args2.data()); result = m_util.mk_concat(arg1, arg2); return true; } @@ -2028,15 +2026,15 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) { } expr* x, *y, *z; - if (m().is_ite(arg, x, y, z) && m_util.is_numeral(y, val, bv_size)) { + if (m.is_ite(arg, x, y, z) && m_util.is_numeral(y, val, bv_size)) { val = bitwise_not(bv_size, val); - result = m().mk_ite(x, m_util.mk_numeral(val, bv_size), m_util.mk_bv_not(z)); + result = m.mk_ite(x, m_util.mk_numeral(val, bv_size), m_util.mk_bv_not(z)); return BR_REWRITE2; } - if (m().is_ite(arg, x, y, z) && m_util.is_numeral(z, val, bv_size)) { + if (m.is_ite(arg, x, y, z) && m_util.is_numeral(z, val, bv_size)) { val = bitwise_not(bv_size, val); - result = m().mk_ite(x, m_util.mk_bv_not(y), m_util.mk_numeral(val, bv_size)); + result = m.mk_ite(x, m_util.mk_bv_not(y), m_util.mk_numeral(val, bv_size)); return BR_REWRITE2; } @@ -2051,13 +2049,13 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) { } } if (m_util.is_bv_add(arg, s, t)) { - expr_ref ns(m()); - expr_ref nt(m()); + expr_ref ns(m); + expr_ref nt(m); // ~(x + y) --> (~x + ~y + 1) when x and y are easy to negate if (is_negatable(t, nt) && is_negatable(s, ns)) { bv_size = m_util.get_bv_size(s); expr * nargs[3] = { m_util.mk_numeral(rational::one(), bv_size), ns.get(), nt.get() }; - result = m().mk_app(m_util.get_fid(), OP_BADD, 3, nargs); + result = m.mk_app(m_util.get_fid(), OP_BADD, 3, nargs); return BR_REWRITE1; } } @@ -2092,7 +2090,7 @@ br_status bv_rewriter::mk_bv_nor(unsigned num_args, expr * const * args, expr_re br_status bv_rewriter::mk_bv_xnor(unsigned num_args, expr * const * args, expr_ref & result) { switch (num_args) { - case 0: result = m().mk_true(); break; + case 0: result = m.mk_true(); break; case 1: result = m_util.mk_bv_not(args[0]); break; case 2: result = m_util.mk_bv_not(m_util.mk_bv_xor(num_args, args)); break; default: @@ -2176,7 +2174,7 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } - result = m().mk_ite(m().mk_eq(arg1, arg2), + result = m.mk_ite(m.mk_eq(arg1, arg2), mk_numeral(1, 1), mk_numeral(0, 1)); return BR_REWRITE2; @@ -2214,7 +2212,7 @@ br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_re return st; } - result = m().mk_app(get_fid(), OP_BOR, x, y); + result = m.mk_app(get_fid(), OP_BOR, x, y); return BR_REWRITE1; #else unsigned _num_args; @@ -2244,7 +2242,7 @@ br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_re } } } - result = m().mk_app(get_fid(), OP_BOR, _num_args, _args); + result = m.mk_app(get_fid(), OP_BOR, _num_args, _args); return BR_REWRITE1; #endif } @@ -2253,21 +2251,17 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) { numeral val; unsigned bv_size; loop: - if (is_numeral(x, val, bv_size)) { - if (val.is_zero()) - return true; - div(val, rational::power_of_two(idx), val); - return (val % numeral(2)).is_zero(); - } + if (is_numeral(x, val, bv_size)) + return val.is_zero() || !val.get_bit(idx); + if (m_util.is_concat(x)) { unsigned i = to_app(x)->get_num_args(); while (i > 0) { --i; expr * y = to_app(x)->get_arg(i); bv_size = get_bv_size(y); - if (bv_size <= idx) { + if (bv_size <= idx) idx -= bv_size; - } else { x = y; goto loop; @@ -2363,7 +2357,7 @@ br_status bv_rewriter::mk_bit2bool(expr * n, int idx, expr_ref & result) { return BR_FAILED; div(v, rational::power_of_two(idx), bit); mod(bit, rational(2), bit); - result = m().mk_bool_val(bit.is_one()); + result = m.mk_bool_val(bit.is_one()); return BR_DONE; } @@ -2381,61 +2375,62 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { if (is_numeral(lhs)) { SASSERT(is_numeral(rhs)); - result = m().mk_bool_val(lhs == rhs); + result = m.mk_bool_val(lhs == rhs); return BR_DONE; } expr* a = nullptr, *b = nullptr, *c = nullptr; - if (m().is_ite(lhs, a, b, c)) { - bool_rewriter rw(m()); - expr_ref e1(rw.mk_eq(b, rhs), m()); - expr_ref e2(rw.mk_eq(c, rhs), m()); + if (m.is_ite(lhs, a, b, c)) { + bool_rewriter rw(m); + expr_ref e1(rw.mk_eq(b, rhs), m); + expr_ref e2(rw.mk_eq(c, rhs), m); result = rw.mk_ite(a, e1, e2); return BR_REWRITE2; } if (m_util.is_bv_not(lhs, a)) { SASSERT(v.is_one() || v.is_zero()); - result = m().mk_eq(a, mk_numeral(numeral(1) - v, 1)); + result = m.mk_eq(a, mk_numeral(numeral(1) - v, 1)); return BR_REWRITE1; } bool is_one = v.is_one(); - expr_ref bit1(m()); - bit1 = is_one ? rhs : mk_numeral(numeral(1), 1); - + if (m_util.is_bv_or(lhs)) { + if (!m_bit1) + m_bit1 = is_one ? rhs : mk_numeral(numeral(1), 1); ptr_buffer new_args; for (expr* arg : *to_app(lhs)) - new_args.push_back(m().mk_eq(arg, bit1)); - result = m().mk_or(new_args); + new_args.push_back(m.mk_eq(arg, m_bit1)); + result = m.mk_or(new_args); if (is_one) { return BR_REWRITE2; } else { - result = m().mk_not(result); + result = m.mk_not(result); return BR_REWRITE3; } } if (m_util.is_bv_xor(lhs)) { + if (!m_bit1) + m_bit1 = is_one ? rhs : mk_numeral(numeral(1), 1); ptr_buffer new_args; for (expr* arg : *to_app(lhs)) - new_args.push_back(m().mk_eq(arg, bit1)); + new_args.push_back(m.mk_eq(arg, m_bit1)); // TODO: bool xor is not flat_assoc... must fix that. - result = m().mk_xor(new_args); + result = m.mk_xor(new_args); if (is_one) { return BR_REWRITE2; } else { - result = m().mk_not(result); + result = m.mk_not(result); return BR_REWRITE3; } } - return BR_FAILED; } @@ -2443,7 +2438,7 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu unsigned sz = get_bv_size(lhs); if (sz == 1) return BR_FAILED; - TRACE("blast_eq_value", tout << "sz: " << sz << "\n" << mk_ismt2_pp(lhs, m()) << "\n";); + TRACE("blast_eq_value", tout << "sz: " << sz << "\n" << mk_ismt2_pp(lhs, m) << "\n";); if (is_numeral(lhs)) std::swap(lhs, rhs); @@ -2458,11 +2453,11 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu ptr_buffer new_args; for (unsigned i = 0; i < sz; i++) { bool bit0 = (v % two).is_zero(); - new_args.push_back(m().mk_eq(m_mk_extract(i,i, lhs), + new_args.push_back(m.mk_eq(m_mk_extract(i,i, lhs), mk_numeral(bit0 ? 0 : 1, 1))); div(v, two, v); } - result = m().mk_and(new_args); + result = m.mk_and(new_args); return BR_REWRITE3; } @@ -2503,7 +2498,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { unsigned rsz1 = sz1 - low1; unsigned rsz2 = sz2 - low2; if (rsz1 == rsz2) { - new_eqs.push_back(m().mk_eq(m_mk_extract(sz1 - 1, low1, arg1), + new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1), m_mk_extract(sz2 - 1, low2, arg2))); low1 = 0; low2 = 0; @@ -2512,14 +2507,14 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { continue; } else if (rsz1 < rsz2) { - new_eqs.push_back(m().mk_eq(m_mk_extract(sz1 - 1, low1, arg1), + new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1), m_mk_extract(rsz1 + low2 - 1, low2, arg2))); low1 = 0; low2 += rsz1; --i1; } else { - new_eqs.push_back(m().mk_eq(m_mk_extract(rsz2 + low1 - 1, low1, arg1), + new_eqs.push_back(m.mk_eq(m_mk_extract(rsz2 + low1 - 1, low1, arg1), m_mk_extract(sz2 - 1, low2, arg2))); low1 += rsz2; low2 = 0; @@ -2528,7 +2523,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { } SASSERT(i1 == 0 && i2 == 0); SASSERT(new_eqs.size() >= 1); - result = m().mk_and(new_eqs); + result = m.mk_and(new_eqs); return BR_REWRITE3; } @@ -2548,9 +2543,9 @@ bool bv_rewriter::is_minus_one_times_t(expr * arg) { void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & result) { SASSERT(is_numeral(c)); if (is_minus_one_times_t(t1)) - result = m().mk_eq(t2, m_util.mk_bv_sub(c, t1)); + result = m.mk_eq(t2, m_util.mk_bv_sub(c, t1)); else - result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2)); + result = m.mk_eq(t1, m_util.mk_bv_sub(c, t2)); } #include "ast/ast_pp.h" @@ -2564,9 +2559,9 @@ bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) { } unsigned sz = to_app(rhs)->get_num_args(); expr * t1 = to_app(rhs)->get_arg(0); - expr_ref t2(m()); + expr_ref t2(m); if (sz > 2) { - t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1); + t2 = m.mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1); } else { SASSERT(sz == 2); @@ -2623,7 +2618,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { // c * x = a if (m_util.is_numeral(rhs, rhs_val, sz)) { // x = c_inv * a - result = m().mk_eq(x, m_util.mk_numeral(c_inv_val * rhs_val, sz)); + result = m.mk_eq(x, m_util.mk_numeral(c_inv_val * rhs_val, sz)); return BR_REWRITE1; } @@ -2634,9 +2629,9 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { // x = c_inv * c2 * x2 numeral new_c2 = m_util.norm(c_inv_val * c2_val, sz); if (new_c2.is_one()) - result = m().mk_eq(x, x2); + result = m.mk_eq(x, x2); else - result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val * c2_val, sz), x2)); + result = m.mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val * c2_val, sz), x2)); return BR_REWRITE1; } @@ -2644,7 +2639,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { // and t_i's have non-unary coefficients (this condition is used to make sure we are actually reducing the number of multipliers). if (is_add_mul_const(rhs)) { // Potential problem: this simplification may increase the number of adders by reducing the amount of sharing. - result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs)); + result = m.mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs)); return BR_REWRITE2; } } @@ -2662,7 +2657,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) { } } if (found) { - result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz), + result = m.mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz), m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs)); return BR_REWRITE3; } @@ -2682,12 +2677,12 @@ bool bv_rewriter::is_urem_any(expr * e, expr * & dividend, expr * & divisor) { br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (lhs == rhs) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } if (is_numeral(lhs) && is_numeral(rhs)) { - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } @@ -2699,7 +2694,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { #if 0 if (!gcd_test(lhs, rhs)) { - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } #endif @@ -2713,13 +2708,13 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { st = mk_mul_eq(lhs, rhs, result); if (st != BR_FAILED) { - TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";); + TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m) << "\n=\n" << mk_ismt2_pp(rhs, m) << "\n----->\n" << mk_ismt2_pp(result,m) << "\n";); return st; } st = mk_mul_eq(rhs, lhs, result); if (st != BR_FAILED) { - TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";); + TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m) << "\n=\n" << mk_ismt2_pp(rhs, m) << "\n----->\n" << mk_ismt2_pp(result,m) << "\n";); return st; } @@ -2738,24 +2733,24 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { && is_numeral(rhs, rhs_val, rhs_sz) && is_numeral(divisor, divisor_val, divisor_sz)) { if (!divisor_val.is_zero() && rhs_val >= divisor_val) {//(= (bvurem x c1) c2) where c2 >= c1 - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } if ((divisor_val + rhs_val) >= rational::power_of_two(divisor_sz)) {//(= (bvurem x c1) c2) where c1+c2 >= 2^width - result = m().mk_eq(dividend, rhs); + result = m.mk_eq(dividend, rhs); return BR_REWRITE2; } } } - expr_ref new_lhs(m()); - expr_ref new_rhs(m()); + expr_ref new_lhs(m); + expr_ref new_rhs(m); if (m_util.is_bv_add(lhs) || m_util.is_bv_mul(lhs) || m_util.is_bv_add(rhs) || m_util.is_bv_mul(rhs)) { st = cancel_monomials(lhs, rhs, false, new_lhs, new_rhs); if (st != BR_FAILED) { if (is_numeral(new_lhs) && is_numeral(new_rhs)) { - result = m().mk_bool_val(new_lhs == new_rhs); + result = m.mk_bool_val(new_lhs == new_rhs); return BR_DONE; } lhs = new_lhs; @@ -2772,7 +2767,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { } if (st != BR_FAILED) { - result = m().mk_eq(lhs, rhs); + result = m.mk_eq(lhs, rhs); return BR_DONE; } } @@ -2782,7 +2777,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { } if (swapped) { - result = m().mk_eq(lhs, rhs); + result = m.mk_eq(lhs, rhs); return BR_DONE; } @@ -2794,7 +2789,7 @@ br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & res if (m_mkbv2num) { unsigned i; for (i = 0; i < num; i++) - if (!m().is_true(args[i]) && !m().is_false(args[i])) + if (!m.is_true(args[i]) && !m.is_false(args[i])) return BR_FAILED; numeral val; numeral two(2); @@ -2802,7 +2797,7 @@ br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & res while (i > 0) { --i; val *= two; - if (m().is_true(args[i])) + if (m.is_true(args[i])) val++; } result = mk_numeral(val, num); @@ -2812,18 +2807,18 @@ br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & res } br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) { - TRACE("bv_ite", tout << "mk_ite_core:\n" << mk_ismt2_pp(c, m()) << "?\n" - << mk_ismt2_pp(t, m()) << "\n:" << mk_ismt2_pp(e, m()) << "\n";); - if (m().are_equal(t, e)) { + TRACE("bv_ite", tout << "mk_ite_core:\n" << mk_ismt2_pp(c, m) << "?\n" + << mk_ismt2_pp(t, m) << "\n:" << mk_ismt2_pp(e, m) << "\n";); + if (m.are_equal(t, e)) { result = e; return BR_REWRITE1; } - if (m().is_not(c)) { - result = m().mk_ite(to_app(c)->get_arg(0), e, t); + if (m.is_not(c)) { + result = m.mk_ite(to_app(c)->get_arg(0), e, t); return BR_REWRITE1; } - if (m_ite2id && m().is_eq(c) && is_bv(t) && is_bv(e)) { + if (m_ite2id && m.is_eq(c) && is_bv(t) && is_bv(e)) { // detect when ite is actually some simple function based on the pattern (lhs=rhs) ? t : e expr * lhs = to_app(c)->get_arg(0); expr * rhs = to_app(c)->get_arg(1); @@ -2832,8 +2827,8 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu if (is_numeral(lhs)) std::swap(lhs, rhs); - if ( (m().are_equal(lhs, t) && m().are_equal(rhs, e)) - || (m().are_equal(lhs, e) && m().are_equal(rhs, t))) { + if ( (m.are_equal(lhs, t) && m.are_equal(rhs, e)) + || (m.are_equal(lhs, e) && m.are_equal(rhs, t))) { // (a = b ? a : b) is b. (a = b ? b : a) is a result = e; return BR_REWRITE1; @@ -2846,8 +2841,8 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu && is_numeral(t, t_n, t_sz) && is_numeral(e, e_n, e_sz)) { if (t_sz == 1) { SASSERT(rhs_sz == sz && e_sz == sz && t_sz == sz); - SASSERT(!m().are_equal(t, e)); - result = m().are_equal(rhs, t) ? lhs : m_util.mk_bv_not(lhs); + SASSERT(!m.are_equal(t, e)); + result = m.are_equal(rhs, t) ? lhs : m_util.mk_bv_not(lhs); return BR_REWRITE1; } if (rhs_n.is_one() && t_n.is_one() && e_n.is_zero()) { @@ -2873,7 +2868,7 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) { if (num_args <= 1) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } unsigned sz = get_bv_size(args[0]); @@ -2882,7 +2877,7 @@ br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ return BR_FAILED; if (num_args <= 1u << sz) return BR_FAILED; - result = m().mk_false(); + result = m.mk_false(); return BR_DONE; } @@ -2895,11 +2890,11 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_num2 = is_numeral(args[1], a1_val, bv_sz); if (is_num1 && (a0_val.is_zero() || (bv_sz != 1 && a0_val.is_one()))) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } if (is_num2 && (a1_val.is_zero() || (bv_sz != 1 && a1_val.is_one()))) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } @@ -2913,9 +2908,9 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, rational lim = rational::power_of_two(bv_sz-1); rational r = a0_val * a1_val; if (is_overflow) - result = m().mk_bool_val(sign0 != sign1 || r < lim); + result = m.mk_bool_val(sign0 != sign1 || r < lim); else - result = m().mk_bool_val(sign0 == sign1 || r <= lim); + result = m.mk_bool_val(sign0 == sign1 || r <= lim); return BR_DONE; } @@ -2927,18 +2922,18 @@ br_status bv_rewriter::mk_bvumul_no_overflow(unsigned num, expr * const * args, bool is_num1 = is_numeral(args[0], a0_val, bv_sz); bool is_num2 = is_numeral(args[1], a1_val, bv_sz); if (is_num1 && (a0_val.is_zero() || a0_val.is_one())) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } if (is_num2 && (a1_val.is_zero() || a1_val.is_one())) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } if (is_num1 && is_num2) { rational mr = a0_val * a1_val; rational lim = rational::power_of_two(bv_sz); - result = m().mk_bool_val(mr < lim); + result = m.mk_bool_val(mr < lim); return BR_DONE; } diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 703e668b679..b22a119474a 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -25,10 +25,11 @@ Module Name: class bv_rewriter_core { protected: + ast_manager& m; typedef rational numeral; bv_util m_util; - ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } + expr_ref m_bit1; bool is_numeral(expr * n) const { return m_util.is_numeral(n); } bool is_numeral(expr * n, numeral & r) const { unsigned sz; return m_util.is_numeral(n, r, sz); } @@ -44,7 +45,7 @@ class bv_rewriter_core { decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast(UINT_MAX); } public: - bv_rewriter_core(ast_manager & m):m_util(m) {} + bv_rewriter_core(ast_manager & m):m(m), m_util(m), m_bit1(m) {} }; class bv_rewriter : public poly_rewriter { @@ -176,7 +177,7 @@ class bv_rewriter : public poly_rewriter { br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { if (mk_app_core(f, num_args, args, result) == BR_FAILED) - result = m().mk_app(f, num_args, args); + result = m.mk_app(f, num_args, args); } bool is_urem_any(expr * e, expr * & dividend, expr * & divisor); @@ -190,14 +191,14 @@ class bv_rewriter : public poly_rewriter { #define MK_BV_BINARY(OP) \ expr_ref OP(expr* a, expr* b) { \ - expr_ref result(m()); \ + expr_ref result(m); \ if (BR_FAILED == OP(a, b, result)) \ result = m_util.OP(a, b); \ return result; \ } \ expr_ref mk_zero_extend(unsigned n, expr * arg) { - expr_ref result(m()); + expr_ref result(m); if (BR_FAILED == mk_zero_extend(n, arg, result)) result = m_util.mk_zero_extend(n, arg); return result; @@ -211,7 +212,7 @@ class bv_rewriter : public poly_rewriter { expr_ref mk_bv2int(expr* a) { - expr_ref result(m()); + expr_ref result(m); if (BR_FAILED == mk_bv2int(a, result)) result = m_util.mk_bv2int(a); return result; diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index c505103bb20..c9253b0e403 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -106,7 +106,6 @@ class poly_rewriter : public Config { SASSERT(!m_som || !m_hoist_mul); // som is mutually exclusive with hoisting multiplication. } - ast_manager & m() const { return Config::m(); } family_id get_fid() const { return Config::get_fid(); } void updt_params(params_ref const & p); diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 0a17fc37537..f9ae333b414 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -51,7 +51,7 @@ expr * poly_rewriter::mk_add_app(unsigned num_args, expr * const * args) switch (num_args) { case 0: return mk_numeral(numeral(0)); case 1: return args[0]; - default: return m().mk_app(get_fid(), add_decl_kind(), num_args, args); + default: return m.mk_app(get_fid(), add_decl_kind(), num_args, args); } } @@ -119,7 +119,7 @@ expr * poly_rewriter::mk_mul_app(unsigned num_args, expr * const * args) if (new_args.size() > 2 && is_numeral(new_args.get(0), a)) { return mk_mul_app(a, mk_mul_app(new_args.size() - 1, new_args.data() + 1)); } - return m().mk_app(get_fid(), mul_decl_kind(), new_args.size(), new_args.data()); + return m.mk_app(get_fid(), mul_decl_kind(), new_args.size(), new_args.data()); } } else { @@ -127,7 +127,7 @@ expr * poly_rewriter::mk_mul_app(unsigned num_args, expr * const * args) if (num_args > 2 && is_numeral(args[0], a)) { return mk_mul_app(a, mk_mul_app(num_args - 1, args + 1)); } - return m().mk_app(get_fid(), mul_decl_kind(), num_args, args); + return m.mk_app(get_fid(), mul_decl_kind(), num_args, args); } } } @@ -189,9 +189,9 @@ br_status poly_rewriter::mk_flat_mul_core(unsigned num_args, expr * cons br_status st = mk_nflat_mul_core(flat_args.size(), flat_args.data(), result); TRACE("poly_rewriter", tout << "flat mul:\n"; - for (unsigned i = 0; i < num_args; i++) tout << mk_bounded_pp(args[i], m()) << "\n"; + for (unsigned i = 0; i < num_args; i++) tout << mk_bounded_pp(args[i], m) << "\n"; tout << "---->\n"; - for (unsigned i = 0; i < flat_args.size(); i++) tout << mk_bounded_pp(flat_args[i], m()) << "\n"; + for (unsigned i = 0; i < flat_args.size(); i++) tout << mk_bounded_pp(flat_args[i], m) << "\n"; tout << st << "\n"; ); if (st == BR_FAILED) { @@ -292,7 +292,7 @@ br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * con new_add_args.push_back(mk_mul_app(c, to_app(var)->get_arg(i))); } result = mk_add_app(new_add_args.size(), new_add_args.data()); - TRACE("mul_bug", tout << "result: " << mk_bounded_pp(result, m(),5) << "\n";); + TRACE("mul_bug", tout << "result: " << mk_bounded_pp(result, m,5) << "\n";); return BR_REWRITE2; } } @@ -328,7 +328,7 @@ br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * con for (unsigned i = 0; i < new_args.size(); i++) { if (i > 0) tout << (lt(new_args[i-1], new_args[i]) ? " < " : " !< "); - tout << mk_ismt2_pp(new_args[i], m()); + tout << mk_ismt2_pp(new_args[i], m); } tout << "\nordered: " << ordered << "\n";); if (ordered && num_coeffs == 0 && !use_power()) @@ -340,7 +340,7 @@ br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * con for (unsigned i = 0; i < new_args.size(); i++) { if (i > 0) tout << (lt(new_args[i-1], new_args[i]) ? " < " : " !< "); - tout << mk_ismt2_pp(new_args[i], m()); + tout << mk_ismt2_pp(new_args[i], m); } tout << "\n";); } @@ -349,8 +349,8 @@ br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * con result = mk_mul_app(c, result); TRACE("poly_rewriter", for (unsigned i = 0; i < num_args; ++i) - tout << mk_ismt2_pp(args[i], m()) << " "; - tout << "\nmk_nflat_mul_core result:\n" << mk_ismt2_pp(result, m()) << "\n";); + tout << mk_ismt2_pp(args[i], m) << " "; + tout << "\nmk_nflat_mul_core result:\n" << mk_ismt2_pp(result, m) << "\n";); return BR_DONE; } @@ -373,7 +373,7 @@ br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * con } } unsigned orig_size = sums.size(); - expr_ref_buffer sum(m()); // must be ref_buffer because we may throw an exception + expr_ref_buffer sum(m); // must be ref_buffer because we may throw an exception ptr_buffer m_args; TRACE("som", tout << "starting som...\n";); do { @@ -566,7 +566,7 @@ br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * con SASSERT(m_sort_sums || ordered); TRACE("rewriter", tout << "ordered: " << ordered << " sort sums: " << m_sort_sums << "\n"; - for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";); + for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m) << "\n";); if (has_multiple) { // expensive case @@ -589,7 +589,7 @@ br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * con coeffs.push_back(a); } } - expr_ref_buffer new_args(m()); + expr_ref_buffer new_args(m); if (!c.is_zero()) { new_args.push_back(mk_numeral(c)); } @@ -639,7 +639,7 @@ br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * con if (num_coeffs == 1 && is_numeral(args[0], a) && !a.is_zero()) return BR_FAILED; } - expr_ref_buffer new_args(m()); + expr_ref_buffer new_args(m); if (!c.is_zero()) new_args.push_back(mk_numeral(c)); for (unsigned i = 0; i < num_args; i++) { @@ -690,8 +690,8 @@ br_status poly_rewriter::mk_sub(unsigned num_args, expr * const * args, return BR_DONE; } set_curr_sort(args[0]->get_sort()); - expr_ref minus_one(mk_numeral(numeral(-1)), m()); - expr_ref_buffer new_args(m()); + expr_ref minus_one(mk_numeral(numeral(-1)), m); + expr_ref_buffer new_args(m); new_args.push_back(args[0]); for (unsigned i = 1; i < num_args; i++) { if (is_zero(args[i])) continue; @@ -984,11 +984,11 @@ bool poly_rewriter::hoist_ite(expr_ref& e) { return false; obj_hashtable shared; ptr_buffer adds; - expr_ref_vector bs(m()), pinned(m()); + expr_ref_vector bs(m), pinned(m); TO_BUFFER(is_add, adds, e); unsigned i = 0; for (expr* a : adds) { - if (m().is_ite(a)) { + if (m.is_ite(a)) { shared.reset(); numeral g(0); if (hoist_ite(a, shared, g) && (is_nontrivial_gcd(g) || !shared.empty())) { @@ -1026,7 +1026,7 @@ bool poly_rewriter::hoist_ite(expr_ref& e) { template bool poly_rewriter::hoist_ite(expr* a, obj_hashtable& shared, numeral& g) { expr* c = nullptr, *t = nullptr, *e = nullptr; - if (m().is_ite(a, c, t, e)) { + if (m.is_ite(a, c, t, e)) { return hoist_ite(t, shared, g) && hoist_ite(e, shared, g); } rational k, g1; @@ -1064,8 +1064,8 @@ bool poly_rewriter::hoist_ite(expr* a, obj_hashtable& shared, nume template expr* poly_rewriter::apply_hoist(expr* a, numeral const& g, obj_hashtable const& shared) { expr* c = nullptr, *t = nullptr, *e = nullptr; - if (m().is_ite(a, c, t, e)) { - return m().mk_ite(c, apply_hoist(t, g, shared), apply_hoist(e, g, shared)); + if (m.is_ite(a, c, t, e)) { + return m.mk_ite(c, apply_hoist(t, g, shared), apply_hoist(e, g, shared)); } rational k; if (is_nontrivial_gcd(g) && is_int_numeral(a, k)) {