diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index bea672265..d8a6f7e08 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -120,7 +120,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]; @@ -357,21 +357,21 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin if (m_anum_simp) { if (is_numeral(arg1, a1) && m_util.is_irrational_algebraic_numeral(arg2)) { - anum_manager & am = m_util.am(); + anum_manager & am = m_util.am(); scoped_anum v1(am); am.set(v1, a1.to_mpq()); anum const & v2 = m_util.to_irrational_algebraic_numeral(arg2); ANUM_LE_GE_EQ(); } if (m_util.is_irrational_algebraic_numeral(arg1) && is_numeral(arg2, a2)) { - anum_manager & am = m_util.am(); + anum_manager & am = m_util.am(); anum const & v1 = m_util.to_irrational_algebraic_numeral(arg1); scoped_anum v2(am); am.set(v2, a2.to_mpq()); ANUM_LE_GE_EQ(); } if (m_util.is_irrational_algebraic_numeral(arg1) && m_util.is_irrational_algebraic_numeral(arg2)) { - anum_manager & am = m_util.am(); + anum_manager & am = m_util.am(); anum const & v1 = m_util.to_irrational_algebraic_numeral(arg1); anum const & v2 = m_util.to_irrational_algebraic_numeral(arg2); ANUM_LE_GE_EQ(); @@ -384,7 +384,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin bool is_int = m_util.is_int(arg1); if (is_int && m_gcd_rounding) { bool first = true; - numeral g; + numeral g; unsigned num_consts = 0; get_coeffs_gcd(arg1, g, first, num_consts); TRACE("arith_rewriter_gcd", tout << "[step1] g: " << g << ", num_consts: " << num_consts << "\n";); @@ -454,7 +454,7 @@ bool arith_rewriter::is_anum_simp_target(unsigned num_args, expr * const * args) if (num_irrat > 0) return true; } - if (m_util.is_irrational_algebraic_numeral(args[i]) && + if (m_util.is_irrational_algebraic_numeral(args[i]) && m_util.am().degree(m_util.to_irrational_algebraic_numeral(args[i])) <= m_max_degree) { num_irrat++; if (num_irrat > 1 || num_rat > 0) @@ -466,9 +466,9 @@ 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()); - anum_manager & am = m_util.am(); - scoped_anum r(am); + expr_ref_buffer new_args(m()); + anum_manager & am = m_util.am(); + scoped_anum r(am); scoped_anum arg(am); rational rarg; am.set(r, 0); @@ -478,13 +478,13 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex new_args.push_back(m_util.mk_numeral(r, false)); am.set(r, 0); } - + if (m_util.is_numeral(args[i], rarg)) { am.set(arg, rarg.to_mpq()); am.add(r, arg, r); continue; } - + if (m_util.is_irrational_algebraic_numeral(args[i])) { anum const & irarg = m_util.to_irrational_algebraic_numeral(args[i]); if (am.degree(irarg) <= m_max_degree) { @@ -516,9 +516,9 @@ 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()); - anum_manager & am = m_util.am(); - scoped_anum r(am); + expr_ref_buffer new_args(m()); + anum_manager & am = m_util.am(); + scoped_anum r(am); scoped_anum arg(am); rational rarg; am.set(r, 1); @@ -537,7 +537,7 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex if (m_util.is_irrational_algebraic_numeral(args[i])) { anum const & irarg = m_util.to_irrational_algebraic_numeral(args[i]); if (am.degree(irarg) <= m_max_degree) { - am.mul(r, irarg, r); + am.mul(r, irarg, r); continue; } } @@ -550,7 +550,7 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex return BR_DONE; } new_args.push_back(m_util.mk_numeral(r, false)); - + br_status st = poly_rewriter::mk_mul_core(new_args.size(), new_args.c_ptr(), result); if (st == BR_FAILED) { result = m().mk_app(get_fid(), OP_MUL, new_args.size(), new_args.c_ptr()); @@ -563,55 +563,55 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex } } -br_status arith_rewriter::mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result) { - SASSERT(m_util.is_real(arg1)); - SASSERT(m_util.is_irrational_algebraic_numeral(arg1)); - SASSERT(m_util.is_numeral(arg2)); - anum_manager & am = m_util.am(); - anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1); - rational rval2; +br_status arith_rewriter::mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result) { + SASSERT(m_util.is_real(arg1)); + SASSERT(m_util.is_irrational_algebraic_numeral(arg1)); + SASSERT(m_util.is_numeral(arg2)); + anum_manager & am = m_util.am(); + anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1); + rational rval2; VERIFY(m_util.is_numeral(arg2, rval2)); if (rval2.is_zero()) return BR_FAILED; - scoped_anum val2(am); - am.set(val2, rval2.to_mpq()); - scoped_anum r(am); - am.div(val1, val2, r); - result = m_util.mk_numeral(r, false); - return BR_DONE; -} - -br_status arith_rewriter::mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result) { - SASSERT(m_util.is_real(arg1)); - SASSERT(m_util.is_numeral(arg1)); - SASSERT(m_util.is_irrational_algebraic_numeral(arg2)); - anum_manager & am = m_util.am(); - rational rval1; - VERIFY(m_util.is_numeral(arg1, rval1)); - scoped_anum val1(am); - am.set(val1, rval1.to_mpq()); - anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2); - scoped_anum r(am); - am.div(val1, val2, r); - result = m_util.mk_numeral(r, false); - return BR_DONE; -} - -br_status arith_rewriter::mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result) { - SASSERT(m_util.is_real(arg1)); - SASSERT(m_util.is_irrational_algebraic_numeral(arg1)); - SASSERT(m_util.is_irrational_algebraic_numeral(arg2)); - anum_manager & am = m_util.am(); - anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1); - if (am.degree(val1) > m_max_degree) - return BR_FAILED; - anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2); - if (am.degree(val2) > m_max_degree) - return BR_FAILED; + scoped_anum val2(am); + am.set(val2, rval2.to_mpq()); scoped_anum r(am); am.div(val1, val2, r); result = m_util.mk_numeral(r, false); - return BR_DONE; + return BR_DONE; +} + +br_status arith_rewriter::mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result) { + SASSERT(m_util.is_real(arg1)); + SASSERT(m_util.is_numeral(arg1)); + SASSERT(m_util.is_irrational_algebraic_numeral(arg2)); + anum_manager & am = m_util.am(); + rational rval1; + VERIFY(m_util.is_numeral(arg1, rval1)); + scoped_anum val1(am); + am.set(val1, rval1.to_mpq()); + anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2); + scoped_anum r(am); + am.div(val1, val2, r); + result = m_util.mk_numeral(r, false); + return BR_DONE; +} + +br_status arith_rewriter::mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result) { + SASSERT(m_util.is_real(arg1)); + SASSERT(m_util.is_irrational_algebraic_numeral(arg1)); + SASSERT(m_util.is_irrational_algebraic_numeral(arg2)); + anum_manager & am = m_util.am(); + anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1); + if (am.degree(val1) > m_max_degree) + return BR_FAILED; + anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2); + if (am.degree(val2) > m_max_degree) + return BR_FAILED; + scoped_anum r(am); + am.div(val1, val2, r); + result = m_util.mk_numeral(r, false); + return BR_DONE; } br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & result) { @@ -681,7 +681,7 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu } return BR_FAILED; } - + br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(m().get_sort(arg1)); numeral v1, v2; @@ -690,7 +690,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul result = m_util.mk_numeral(mod(v1, v2), is_int); return BR_DONE; } - + if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) { result = m_util.mk_numeral(numeral(0), true); return BR_DONE; @@ -728,7 +728,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul TRACE("mod_bug", tout << "mk_mod result: " << mk_ismt2_pp(result, m()) << "\n";); return BR_REWRITE3; } - + return BR_FAILED; } @@ -782,8 +782,8 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res bool is_num_x = m_util.is_numeral(arg1, x); bool is_num_y = m_util.is_numeral(arg2, y); bool is_int_sort = m_util.is_int(arg1); - - if ((is_num_x && x.is_one()) || + + if ((is_num_x && x.is_one()) || (is_num_y && y.is_one())) { result = arg1; return BR_DONE; @@ -792,8 +792,8 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res if (is_num_x && is_num_y) { if (x.is_zero() && y.is_zero()) return BR_FAILED; - - if (y.is_zero()) { + + if (y.is_zero()) { result = m_util.mk_numeral(rational(1), m().get_sort(arg1)); return BR_DONE; } @@ -803,12 +803,12 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res return BR_DONE; } - if (y.is_unsigned() && y.get_unsigned() <= m_max_degree) { + if (y.is_unsigned() && y.get_unsigned() <= m_max_degree) { x = power(x, y.get_unsigned()); result = m_util.mk_numeral(x, m().get_sort(arg1)); return BR_DONE; } - + if (!is_int_sort && (-y).is_unsigned() && (-y).get_unsigned() <= m_max_degree) { x = power(rational(1)/x, (-y).get_unsigned()); result = m_util.mk_numeral(x, m().get_sort(arg1)); @@ -854,10 +854,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res return BR_FAILED; bool is_irrat_x = m_util.is_irrational_algebraic_numeral(arg1); - - if (!is_num_x && !is_irrat_x) + + if (!is_num_x && !is_irrat_x) return BR_FAILED; - + rational num_y = numerator(y); rational den_y = denominator(y); bool is_neg_y = false; @@ -867,7 +867,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res } SASSERT(num_y.is_pos()); SASSERT(den_y.is_pos()); - + if (is_neg_y && is_int_sort) return BR_FAILED; @@ -876,10 +876,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res unsigned u_num_y = num_y.get_unsigned(); unsigned u_den_y = den_y.get_unsigned(); - + if (u_num_y > m_max_degree || u_den_y > m_max_degree) return BR_FAILED; - + if (is_num_x) { rational xk, r; xk = power(x, u_num_y); @@ -984,7 +984,7 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) { for (unsigned i = 0; i < num; i++) { new_args.push_back(m_util.mk_to_real(to_app(arg)->get_arg(i))); } - if (m_util.is_add(arg)) + if (m_util.is_add(arg)) result = m().mk_app(get_fid(), OP_ADD, new_args.size(), new_args.c_ptr()); else result = m().mk_app(get_fid(), OP_MUL, new_args.size(), new_args.c_ptr()); @@ -1052,9 +1052,9 @@ bool arith_rewriter::is_pi_offset(expr * t, rational & k, expr * & m) { bool arith_rewriter::is_2_pi_integer(expr * t) { expr * a, * m, * b, * c; rational k; - return - m_util.is_mul(t, a, m) && - m_util.is_numeral(a, k) && + return + m_util.is_mul(t, a, m) && + m_util.is_numeral(a, k) && k.is_int() && mod(k, rational(2)).is_zero() && m_util.is_mul(m, b, c) && @@ -1094,7 +1094,7 @@ bool arith_rewriter::is_pi_integer(expr * t) { 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 + return (m_util.is_pi(a) && m_util.is_to_real(b)) || (m_util.is_to_real(a) && m_util.is_pi(b)); } @@ -1130,7 +1130,7 @@ expr * arith_rewriter::mk_sin_value(rational const & k) { bool neg = false; if (k_prime >= rational(1)) { neg = true; - k_prime = k_prime - rational(1); + k_prime = k_prime - rational(1); } SASSERT(k_prime >= rational(0) && k_prime < rational(1)); if (k_prime.is_zero() || k_prime.is_one()) { @@ -1342,7 +1342,7 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) { } br_status arith_rewriter::mk_asin_core(expr * arg, expr_ref & result) { - // Remark: we assume that ForAll x : asin(-x) == asin(x). + // Remark: we assume that ForAll x : asin(-x) == asin(x). // Mathematica uses this as an axiom. Although asin is an underspecified function for x < -1 or x > 1. // Actually, in Mathematica, asin(x) is a total function that returns a complex number fo x < -1 or x > 1. rational k; @@ -1355,13 +1355,13 @@ br_status arith_rewriter::mk_asin_core(expr * arg, expr_ref & result) { // asin(-2) == -asin(2) // asin(-3) == -asin(3) k.neg(); - result = m_util.mk_uminus(m_util.mk_asin(m_util.mk_numeral(k, false))); + result = m_util.mk_uminus(m_util.mk_asin(m_util.mk_numeral(k, false))); return BR_REWRITE2; } if (k > rational(1)) return BR_FAILED; - + bool neg = false; if (k.is_neg()) { neg = true; @@ -1450,7 +1450,7 @@ br_status arith_rewriter::mk_atan_core(expr * arg, expr_ref & result) { // atan(-2) == -tan(2) // atan(-3) == -tan(3) k.neg(); - result = m_util.mk_uminus(m_util.mk_atan(m_util.mk_numeral(k, false))); + result = m_util.mk_uminus(m_util.mk_atan(m_util.mk_numeral(k, false))); return BR_REWRITE2; } return BR_FAILED; diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index 90a807874..ea0b9e85a 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -27,7 +27,7 @@ Notes: template class poly_rewriter : public Config { protected: - typedef typename Config::numeral numeral; + typedef typename Config::numeral numeral; sort * m_curr_sort; obj_map m_expr2pos; bool m_flat; @@ -36,7 +36,7 @@ protected: bool m_sort_sums; bool m_hoist_mul; bool m_hoist_cmul; - + bool is_numeral(expr * n) const { return Config::is_numeral(n); } bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); } bool is_zero(expr * n) const { return Config::is_zero(n); } @@ -85,10 +85,10 @@ protected: struct hoist_cmul_lt; bool is_mul(expr * t, numeral & c, expr * & pp); void hoist_cmul(expr_ref_buffer & args); - + public: poly_rewriter(ast_manager & m, params_ref const & p = params_ref()): - Config(m), + Config(m), m_curr_sort(0), m_sort_sums(false) { updt_params(p); @@ -154,7 +154,7 @@ public: // The result of the following functions is never BR_FAILED br_status mk_uminus(expr * arg, expr_ref & result); br_status mk_sub(unsigned num_args, expr * const * args, expr_ref & result); - + void mk_sub(expr* a1, expr* a2, expr_ref& result) { expr* args[2] = { a1, a2 }; mk_sub(2, args, result);