1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 arith_rewriter.h 7 8 Abstract: 9 10 Basic rewriting rules for arithmetic 11 12 Author: 13 14 Leonardo (leonardo) 2011-04-10 15 16 Notes: 17 18 --*/ 19 #pragma once 20 21 #include "ast/rewriter/poly_rewriter.h" 22 #include "ast/arith_decl_plugin.h" 23 #include "ast/seq_decl_plugin.h" 24 25 class arith_rewriter_core { 26 protected: 27 typedef rational numeral; 28 arith_util m_util; 29 scoped_ptr<seq_util> m_seq; 30 bool m_expand_power{ false }; 31 bool m_mul2power{ false }; 32 bool m_expand_tan{ false }; 33 m()34 ast_manager & m() const { return m_util.get_manager(); } get_fid()35 family_id get_fid() const { return m_util.get_family_id(); } 36 seq_util& seq(); 37 is_numeral(expr * n)38 bool is_numeral(expr * n) const { return m_util.is_numeral(n); } is_numeral(expr * n,numeral & r)39 bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); } is_minus_one(expr * n)40 bool is_minus_one(expr * n) const { return m_util.is_minus_one(n); } normalize(numeral & c,sort * s)41 void normalize(numeral & c, sort * s) {} mk_numeral(numeral const & r,sort * s)42 app * mk_numeral(numeral const & r, sort * s) { return m_util.mk_numeral(r, s); } add_decl_kind()43 decl_kind add_decl_kind() const { return OP_ADD; } mul_decl_kind()44 decl_kind mul_decl_kind() const { return OP_MUL; } use_power()45 bool use_power() const { return m_mul2power && !m_expand_power; } power_decl_kind()46 decl_kind power_decl_kind() const { return OP_POWER; } 47 app* mk_power(expr* x, rational const& r, sort* s); 48 expr* coerce(expr* x, sort* s); 49 public: arith_rewriter_core(ast_manager & m)50 arith_rewriter_core(ast_manager & m):m_util(m) {} is_zero(expr * n)51 bool is_zero(expr * n) const { return m_util.is_zero(n); } 52 }; 53 54 class arith_rewriter : public poly_rewriter<arith_rewriter_core> { 55 bool m_arith_lhs; 56 bool m_arith_ineq_lhs; 57 bool m_gcd_rounding; 58 bool m_elim_to_real; 59 bool m_push_to_real; 60 bool m_anum_simp; 61 bool m_elim_rem; 62 bool m_eq2ineq; 63 unsigned m_max_degree; 64 65 void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts); 66 enum const_treatment { CT_FLOOR, CT_CEIL, CT_FALSE }; 67 bool div_polynomial(expr * t, numeral const & g, const_treatment ct, expr_ref & result); 68 enum op_kind { LE, GE, EQ }; inv(op_kind k)69 static op_kind inv(op_kind k) { return k == LE ? GE : (k == GE ? LE : EQ); } 70 bool is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); 71 br_status is_separated(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); 72 bool is_non_negative(expr* e); 73 br_status mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); 74 75 bool elim_to_real_var(expr * var, expr_ref & new_var); 76 bool elim_to_real_mon(expr * monomial, expr_ref & new_monomial); 77 bool elim_to_real_pol(expr * p, expr_ref & new_p); 78 bool elim_to_real(expr * arg1, expr * arg2, expr_ref & new_arg1, expr_ref & new_arg2); 79 80 void updt_local_params(params_ref const & p); 81 82 bool is_anum_simp_target(unsigned num_args, expr * const * args); 83 84 br_status mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result); 85 br_status mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result); 86 br_status mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result); 87 88 bool is_reduce_power_target(expr * arg, bool is_eq); 89 expr * reduce_power(expr * arg, bool is_eq); 90 br_status reduce_power(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); 91 92 bool is_arith_term(expr * n) const; 93 94 bool is_pi_multiple(expr * t, rational & k); 95 bool is_pi_offset(expr * t, rational & k, expr * & m); 96 bool is_2_pi_integer(expr * t); 97 bool is_2_pi_integer_offset(expr * t, expr * & m); 98 bool is_pi_integer(expr * t); 99 bool is_pi_integer_offset(expr * t, expr * & m); 100 bool is_neg_poly(expr* e, expr_ref& neg) const; 101 expr_ref neg_monomial(expr * e) const; 102 expr * mk_sin_value(rational const & k); 103 app * mk_sqrt(rational const & k); 104 bool divides(expr* d, expr* n, expr_ref& result); 105 expr_ref remove_divisor(expr* arg, expr* num, expr* den); 106 void flat_mul(expr* e, ptr_buffer<expr>& args); 107 void remove_divisor(expr* d, ptr_buffer<expr>& args); 108 public: 109 arith_rewriter(ast_manager & m, params_ref const & p = params_ref()): 110 poly_rewriter<arith_rewriter_core>(m, p) { 111 updt_local_params(p); 112 } 113 114 void updt_params(params_ref const & p); 115 116 static void get_param_descrs(param_descrs & r); 117 118 br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); mk_app(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)119 void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { 120 if (mk_app_core(f, num_args, args, result) == BR_FAILED) 121 result = m().mk_app(f, num_args, args); 122 } 123 124 br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result); 125 br_status mk_le_core(expr * arg1, expr * arg2, expr_ref & result); 126 br_status mk_lt_core(expr * arg1, expr * arg2, expr_ref & result); 127 br_status mk_ge_core(expr * arg1, expr * arg2, expr_ref & result); 128 br_status mk_gt_core(expr * arg1, expr * arg2, expr_ref & result); 129 130 br_status mk_add_core(unsigned num_args, expr * const * args, expr_ref & result); 131 br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result); 132 mk_eq(expr * arg1,expr * arg2,expr_ref & result)133 void mk_eq(expr * arg1, expr * arg2, expr_ref & result) { 134 if (mk_eq_core(arg1, arg2, result) == BR_FAILED) 135 result = m_util.mk_eq(arg1, arg2); 136 } mk_le(expr * arg1,expr * arg2,expr_ref & result)137 void mk_le(expr * arg1, expr * arg2, expr_ref & result) { 138 if (mk_le_core(arg1, arg2, result) == BR_FAILED) 139 result = m_util.mk_le(arg1, arg2); 140 } mk_lt(expr * arg1,expr * arg2,expr_ref & result)141 void mk_lt(expr * arg1, expr * arg2, expr_ref & result) { mk_lt_core(arg1, arg2, result); } mk_ge(expr * arg1,expr * arg2,expr_ref & result)142 void mk_ge(expr * arg1, expr * arg2, expr_ref & result) { 143 if (mk_ge_core(arg1, arg2, result) == BR_FAILED) 144 result = m_util.mk_ge(arg1, arg2); 145 } mk_gt(expr * arg1,expr * arg2,expr_ref & result)146 void mk_gt(expr * arg1, expr * arg2, expr_ref & result) { mk_gt_core(arg1, arg2, result); } 147 148 br_status mk_abs_core(expr * arg, expr_ref & result); 149 150 br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result); 151 br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result); 152 br_status mk_idivides(unsigned k, expr * arg, expr_ref & result); 153 br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result); 154 br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result); 155 br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result); mk_div(expr * arg1,expr * arg2,expr_ref & result)156 void mk_div(expr * arg1, expr * arg2, expr_ref & result) { 157 if (mk_div_core(arg1, arg2, result) == BR_FAILED) 158 result = m().mk_app(get_fid(), OP_DIV, arg1, arg2); 159 } mk_idiv(expr * arg1,expr * arg2,expr_ref & result)160 void mk_idiv(expr * arg1, expr * arg2, expr_ref & result) { 161 if (mk_idiv_core(arg1, arg2, result) == BR_FAILED) 162 result = m().mk_app(get_fid(), OP_IDIV, arg1, arg2); 163 } mk_mod(expr * arg1,expr * arg2,expr_ref & result)164 void mk_mod(expr * arg1, expr * arg2, expr_ref & result) { 165 if (mk_mod_core(arg1, arg2, result) == BR_FAILED) 166 result = m().mk_app(get_fid(), OP_MOD, arg1, arg2); 167 } mk_rem(expr * arg1,expr * arg2,expr_ref & result)168 void mk_rem(expr * arg1, expr * arg2, expr_ref & result) { 169 if (mk_rem_core(arg1, arg2, result) == BR_FAILED) 170 result = m().mk_app(get_fid(), OP_REM, arg1, arg2); 171 } 172 173 br_status mk_to_int_core(expr * arg, expr_ref & result); 174 br_status mk_to_real_core(expr * arg, expr_ref & result); mk_to_int(expr * arg,expr_ref & result)175 void mk_to_int(expr * arg, expr_ref & result) { 176 if (mk_to_int_core(arg, result) == BR_FAILED) 177 result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg); 178 } mk_to_real(expr * arg,expr_ref & result)179 void mk_to_real(expr * arg, expr_ref & result) { 180 if (mk_to_real_core(arg, result) == BR_FAILED) 181 result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg); 182 } 183 br_status mk_is_int(expr * arg, expr_ref & result); 184 185 br_status mk_sin_core(expr * arg, expr_ref & result); 186 br_status mk_cos_core(expr * arg, expr_ref & result); 187 br_status mk_tan_core(expr * arg, expr_ref & result); 188 189 br_status mk_asin_core(expr * arg, expr_ref & result); 190 br_status mk_acos_core(expr * arg, expr_ref & result); 191 br_status mk_atan_core(expr * arg, expr_ref & result); 192 193 br_status mk_sinh_core(expr * arg, expr_ref & result); 194 br_status mk_cosh_core(expr * arg, expr_ref & result); 195 br_status mk_tanh_core(expr * arg, expr_ref & result); 196 }; 197 198