1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 arith_rewriter.cpp
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 #include "params/arith_rewriter_params.hpp"
20 #include "ast/rewriter/arith_rewriter.h"
21 #include "ast/rewriter/poly_rewriter_def.h"
22 #include "math/polynomial/algebraic_numbers.h"
23 #include "ast/ast_pp.h"
24
seq()25 seq_util& arith_rewriter_core::seq() {
26 if (!m_seq) {
27 m_seq = alloc(seq_util, m());
28 }
29 return *m_seq;
30 }
31
updt_local_params(params_ref const & _p)32 void arith_rewriter::updt_local_params(params_ref const & _p) {
33 arith_rewriter_params p(_p);
34 m_arith_lhs = p.arith_lhs();
35 m_arith_ineq_lhs = p.arith_ineq_lhs();
36 m_gcd_rounding = p.gcd_rounding();
37 m_elim_to_real = p.elim_to_real();
38 m_push_to_real = p.push_to_real();
39 m_anum_simp = p.algebraic_number_evaluator();
40 m_max_degree = p.max_degree();
41 m_expand_power = p.expand_power();
42 m_mul2power = p.mul_to_power();
43 m_elim_rem = p.elim_rem();
44 m_expand_tan = p.expand_tan();
45 m_eq2ineq = p.eq2ineq();
46 set_sort_sums(p.sort_sums());
47 }
48
updt_params(params_ref const & p)49 void arith_rewriter::updt_params(params_ref const & p) {
50 poly_rewriter<arith_rewriter_core>::updt_params(p);
51 updt_local_params(p);
52 }
53
get_param_descrs(param_descrs & r)54 void arith_rewriter::get_param_descrs(param_descrs & r) {
55 poly_rewriter<arith_rewriter_core>::get_param_descrs(r);
56 arith_rewriter_params::collect_param_descrs(r);
57 }
58
mk_app_core(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)59 br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
60 br_status st = BR_FAILED;
61 SASSERT(f->get_family_id() == get_fid());
62 switch (f->get_decl_kind()) {
63 case OP_NUM: st = BR_FAILED; break;
64 case OP_IRRATIONAL_ALGEBRAIC_NUM: st = BR_FAILED; break;
65 case OP_LE: SASSERT(num_args == 2); st = mk_le_core(args[0], args[1], result); break;
66 case OP_GE: SASSERT(num_args == 2); st = mk_ge_core(args[0], args[1], result); break;
67 case OP_LT: SASSERT(num_args == 2); st = mk_lt_core(args[0], args[1], result); break;
68 case OP_GT: SASSERT(num_args == 2); st = mk_gt_core(args[0], args[1], result); break;
69 case OP_ADD: st = mk_add_core(num_args, args, result); break;
70 case OP_MUL: st = mk_mul_core(num_args, args, result); break;
71 case OP_SUB: st = mk_sub(num_args, args, result); break;
72 case OP_DIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
73 SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break;
74 case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
75 SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break;
76 case OP_IDIVIDES: SASSERT(num_args == 1); st = mk_idivides(f->get_parameter(0).get_int(), args[0], result); break;
77 case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break;
78 case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break;
79 case OP_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break;
80 case OP_TO_REAL: SASSERT(num_args == 1); st = mk_to_real_core(args[0], result); break;
81 case OP_TO_INT: SASSERT(num_args == 1); st = mk_to_int_core(args[0], result); break;
82 case OP_IS_INT: SASSERT(num_args == 1); st = mk_is_int(args[0], result); break;
83 case OP_POWER: SASSERT(num_args == 2); st = mk_power_core(args[0], args[1], result); break;
84 case OP_ABS: SASSERT(num_args == 1); st = mk_abs_core(args[0], result); break;
85 case OP_SIN: SASSERT(num_args == 1); st = mk_sin_core(args[0], result); break;
86 case OP_COS: SASSERT(num_args == 1); st = mk_cos_core(args[0], result); break;
87 case OP_TAN: SASSERT(num_args == 1); st = mk_tan_core(args[0], result); break;
88 case OP_ASIN: SASSERT(num_args == 1); st = mk_asin_core(args[0], result); break;
89 case OP_ACOS: SASSERT(num_args == 1); st = mk_acos_core(args[0], result); break;
90 case OP_ATAN: SASSERT(num_args == 1); st = mk_atan_core(args[0], result); break;
91 case OP_SINH: SASSERT(num_args == 1); st = mk_sinh_core(args[0], result); break;
92 case OP_COSH: SASSERT(num_args == 1); st = mk_cosh_core(args[0], result); break;
93 case OP_TANH: SASSERT(num_args == 1); st = mk_tanh_core(args[0], result); break;
94 default: st = BR_FAILED; break;
95 }
96 CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m());
97 for (unsigned i = 0; i < num_args; ++i) tout << mk_pp(args[i], m()) << " ";
98 tout << "\n==>\n" << mk_pp(result.get(), m()) << "\n";
99 if (is_app(result)) tout << "args: " << to_app(result)->get_num_args() << "\n";
100 );
101 return st;
102 }
103
get_coeffs_gcd(expr * t,numeral & g,bool & first,unsigned & num_consts)104 void arith_rewriter::get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts) {
105 unsigned sz;
106 expr * const * ms = get_monomials(t, sz);
107 SASSERT(sz >= 1);
108 numeral a;
109 for (unsigned i = 0; i < sz; i++) {
110 expr * arg = ms[i];
111 if (is_numeral(arg, a)) {
112 if (!a.is_zero())
113 num_consts++;
114 continue;
115 }
116 if (first) {
117 get_power_product(arg, g);
118 SASSERT(g.is_int());
119 first = false;
120 }
121 else {
122 get_power_product(arg, a);
123 SASSERT(a.is_int());
124 g = gcd(abs(a), g);
125 }
126 if (g.is_one())
127 return;
128 }
129 }
130
div_polynomial(expr * t,numeral const & g,const_treatment ct,expr_ref & result)131 bool arith_rewriter::div_polynomial(expr * t, numeral const & g, const_treatment ct, expr_ref & result) {
132 SASSERT(m_util.is_int(t));
133 SASSERT(!g.is_one());
134 unsigned sz;
135 expr * const * ms = get_monomials(t, sz);
136 expr_ref_buffer new_args(m());
137 numeral a;
138 for (unsigned i = 0; i < sz; i++) {
139 expr * arg = ms[i];
140 if (is_numeral(arg, a)) {
141 a /= g;
142 if (!a.is_int()) {
143 switch (ct) {
144 case CT_FLOOR:
145 a = floor(a);
146 break;
147 case CT_CEIL:
148 a = ceil(a);
149 break;
150 case CT_FALSE:
151 return false;
152 }
153 }
154 if (!a.is_zero())
155 new_args.push_back(m_util.mk_numeral(a, true));
156 continue;
157 }
158 expr * pp = get_power_product(arg, a);
159 a /= g;
160 SASSERT(a.is_int());
161 if (!a.is_zero()) {
162 if (a.is_one())
163 new_args.push_back(pp);
164 else
165 new_args.push_back(m_util.mk_mul(m_util.mk_numeral(a, true), pp));
166 }
167 }
168 switch (new_args.size()) {
169 case 0: result = m_util.mk_numeral(numeral(0), true); return true;
170 case 1: result = new_args[0]; return true;
171 default: result = m_util.mk_add(new_args.size(), new_args.c_ptr()); return true;
172 }
173 }
174
is_bound(expr * arg1,expr * arg2,op_kind kind,expr_ref & result)175 bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) {
176 numeral b, c;
177 if (!is_add(arg1) && !m_util.is_mod(arg1) && is_numeral(arg2, c)) {
178 numeral a;
179 bool r = false;
180 expr * pp = get_power_product(arg1, a);
181 if (a.is_neg()) {
182 a.neg();
183 c.neg();
184 kind = inv(kind);
185 r = true;
186 }
187 if (!a.is_one())
188 r = true;
189 if (!r)
190 return false;
191 c /= a;
192 bool is_int = m_util.is_int(arg1);
193 if (is_int && !c.is_int()) {
194 switch (kind) {
195 case LE: c = floor(c); break;
196 case GE: c = ceil(c); break;
197 case EQ: result = m().mk_false(); return true;
198 }
199 }
200 expr_ref k(m_util.mk_numeral(c, is_int), m());
201 switch (kind) {
202 case LE: result = m_util.mk_le(pp, k); return true;
203 case GE: result = m_util.mk_ge(pp, k); return true;
204 case EQ: result = m_util.mk_eq(pp, k); return true;
205 }
206 }
207 expr* t1, *t2;
208 bool is_int = false;
209 if (m_util.is_mod(arg2)) {
210 std::swap(arg1, arg2);
211 switch (kind) {
212 case LE: kind = GE; break;
213 case GE: kind = LE; break;
214 case EQ: break;
215 }
216 }
217
218 if (m_util.is_numeral(arg2, c, is_int) && is_int &&
219 m_util.is_mod(arg1, t1, t2) && m_util.is_numeral(t2, b, is_int) && !b.is_zero()) {
220 // mod x b <= c = false if c < 0, b != 0, true if c >= b, b != 0
221 if (c.is_neg()) {
222 switch (kind) {
223 case EQ:
224 case LE: result = m().mk_false(); return true;
225 case GE: result = m().mk_true(); return true;
226 }
227 }
228 if (c.is_zero() && kind == GE) {
229 result = m().mk_true();
230 return true;
231 }
232 if (c.is_pos() && c >= abs(b)) {
233 switch (kind) {
234 case LE: result = m().mk_true(); return true;
235 case EQ:
236 case GE: result = m().mk_false(); return true;
237 }
238 }
239 // mod x b <= b - 1
240 if (c + rational::one() == abs(b) && kind == LE) {
241 result = m().mk_true();
242 return true;
243 }
244 }
245
246 return false;
247 }
248
249
is_non_negative(expr * e)250 bool arith_rewriter::is_non_negative(expr* e) {
251 rational r;
252 auto is_even_power = [&](expr* e) {
253 expr* n = nullptr, *p = nullptr;
254 unsigned pu;
255 return m_util.is_power(e, n, p) && m_util.is_unsigned(p, pu) && (pu % 2 == 0);
256 };
257 auto is_power_of_positive = [&](expr* e) {
258 expr* n = nullptr, * p = nullptr;
259 return m_util.is_power(e, n, p) && m_util.is_numeral(n, r) && r.is_pos();
260 };
261 if (is_even_power(e))
262 return true;
263 if (is_power_of_positive(e))
264 return true;
265 if (seq().str.is_length(e))
266 return true;
267 if (!m_util.is_mul(e))
268 return false;
269 expr_mark mark;
270 ptr_buffer<expr> args;
271 flat_mul(e, args);
272 bool sign = false;
273 for (expr* arg : args) {
274 if (is_even_power(arg))
275 continue;
276 if (is_power_of_positive(arg))
277 continue;
278 if (seq().str.is_length(e))
279 continue;
280 if (m_util.is_numeral(arg, r)) {
281 if (r.is_neg())
282 sign = !sign;
283 continue;
284 }
285 mark.mark(arg, !mark.is_marked(arg));
286 }
287 if (sign)
288 return false;
289 for (expr* arg : args)
290 if (mark.is_marked(arg))
291 return false;
292 return true;
293 }
294
295 /**
296 * perform static analysis on arg1 to determine a non-negative lower bound.
297 * a + b + r1 <= r2 -> false if r1 > r2 and a >= 0, b >= 0
298 * a + b + r1 >= r2 -> false if r1 < r2 and a <= 0, b <= 0
299 * a + b + r1 >= r1 -> a = 0 and b = 0 if a >= 0, b >= 0 where a, b are multipliers
300 */
is_separated(expr * arg1,expr * arg2,op_kind kind,expr_ref & result)301 br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) {
302 if (kind != LE && kind != GE)
303 return BR_FAILED;
304 rational bound(0), r1, r2;
305 expr_ref narg(m());
306 bool has_bound = true;
307 if (!m_util.is_numeral(arg2, r2))
308 return BR_FAILED;
309 auto update_bound = [&](expr* arg) {
310 if (m_util.is_numeral(arg, r1)) {
311 bound += r1;
312 return;
313 }
314 if (kind == LE && is_non_negative(arg))
315 return;
316 if (kind == GE && is_neg_poly(arg, narg) && is_non_negative(narg))
317 return;
318 has_bound = false;
319 };
320 if (m_util.is_add(arg1)) {
321 for (expr* arg : *to_app(arg1)) {
322 update_bound(arg);
323 }
324 }
325 else {
326 update_bound(arg1);
327 }
328 if (!has_bound)
329 return BR_FAILED;
330
331 if (kind == LE && r1 < r2)
332 return BR_FAILED;
333 if (kind == GE && r1 > r2)
334 return BR_FAILED;
335 if (kind == LE && r1 > r2) {
336 result = m().mk_false();
337 return BR_DONE;
338 }
339 if (kind == GE && r1 < r2) {
340 result = m().mk_false();
341 return BR_DONE;
342 }
343
344 SASSERT(r1 == r2);
345 expr_ref zero(m_util.mk_numeral(rational(0), m().get_sort(arg1)), m());
346
347 if (r1.is_zero() && m_util.is_mul(arg1)) {
348 expr_ref_buffer eqs(m());
349 ptr_buffer<expr> args;
350 flat_mul(arg1, args);
351 for (expr* arg : args) {
352 if (m_util.is_numeral(arg))
353 continue;
354 eqs.push_back(m().mk_eq(arg, zero));
355 }
356 result = m().mk_or(eqs);
357 return BR_REWRITE2;
358 }
359
360 if (kind == LE && m_util.is_add(arg1)) {
361 expr_ref_buffer leqs(m());
362 for (expr* arg : *to_app(arg1)) {
363 if (!m_util.is_numeral(arg))
364 leqs.push_back(m_util.mk_le(arg, zero));
365 }
366 result = m().mk_and(leqs);
367 return BR_REWRITE2;
368 }
369
370 if (kind == GE && m_util.is_add(arg1)) {
371 expr_ref_buffer geqs(m());
372 for (expr* arg : *to_app(arg1)) {
373 if (!m_util.is_numeral(arg))
374 geqs.push_back(m_util.mk_ge(arg, zero));
375 }
376 result = m().mk_and(geqs);
377 return BR_REWRITE2;
378 }
379
380 return BR_FAILED;
381 }
382
elim_to_real_var(expr * var,expr_ref & new_var)383 bool arith_rewriter::elim_to_real_var(expr * var, expr_ref & new_var) {
384 numeral val;
385 if (m_util.is_numeral(var, val)) {
386 if (!val.is_int())
387 return false;
388 new_var = m_util.mk_numeral(val, true);
389 return true;
390 }
391 else if (m_util.is_to_real(var)) {
392 new_var = to_app(var)->get_arg(0);
393 return true;
394 }
395 return false;
396 }
397
elim_to_real_mon(expr * monomial,expr_ref & new_monomial)398 bool arith_rewriter::elim_to_real_mon(expr * monomial, expr_ref & new_monomial) {
399 if (m_util.is_mul(monomial)) {
400 expr_ref_buffer new_vars(m());
401 expr_ref new_var(m());
402 unsigned num = to_app(monomial)->get_num_args();
403 for (unsigned i = 0; i < num; i++) {
404 if (!elim_to_real_var(to_app(monomial)->get_arg(i), new_var))
405 return false;
406 new_vars.push_back(new_var);
407 }
408 new_monomial = m_util.mk_mul(new_vars.size(), new_vars.c_ptr());
409 return true;
410 }
411 else {
412 return elim_to_real_var(monomial, new_monomial);
413 }
414 }
415
elim_to_real_pol(expr * p,expr_ref & new_p)416 bool arith_rewriter::elim_to_real_pol(expr * p, expr_ref & new_p) {
417 if (m_util.is_add(p)) {
418 expr_ref_buffer new_monomials(m());
419 expr_ref new_monomial(m());
420 for (expr* arg : *to_app(p)) {
421 if (!elim_to_real_mon(arg, new_monomial))
422 return false;
423 new_monomials.push_back(new_monomial);
424 }
425 new_p = m_util.mk_add(new_monomials.size(), new_monomials.c_ptr());
426 return true;
427 }
428 else {
429 return elim_to_real_mon(p, new_p);
430 }
431 }
432
elim_to_real(expr * arg1,expr * arg2,expr_ref & new_arg1,expr_ref & new_arg2)433 bool arith_rewriter::elim_to_real(expr * arg1, expr * arg2, expr_ref & new_arg1, expr_ref & new_arg2) {
434 if (!m_util.is_real(arg1))
435 return false;
436 return elim_to_real_pol(arg1, new_arg1) && elim_to_real_pol(arg2, new_arg2);
437 }
438
is_reduce_power_target(expr * arg,bool is_eq)439 bool arith_rewriter::is_reduce_power_target(expr * arg, bool is_eq) {
440 unsigned sz;
441 expr * const * args;
442 if (m_util.is_mul(arg)) {
443 sz = to_app(arg)->get_num_args();
444 args = to_app(arg)->get_args();
445 }
446 else {
447 sz = 1;
448 args = &arg;
449 }
450 for (unsigned i = 0; i < sz; i++) {
451 expr * arg = args[i];
452 expr* arg0, *arg1;
453 if (m_util.is_power(arg, arg0, arg1)) {
454 rational k;
455 if (m_util.is_numeral(arg1, k) && k.is_int() && ((is_eq && k > rational(1)) || (!is_eq && k > rational(2))))
456 return true;
457 }
458 }
459 return false;
460 }
461
reduce_power(expr * arg,bool is_eq)462 expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) {
463 if (is_zero(arg))
464 return arg;
465 unsigned sz;
466 expr * const * args;
467 if (m_util.is_mul(arg)) {
468 sz = to_app(arg)->get_num_args();
469 args = to_app(arg)->get_args();
470 }
471 else {
472 sz = 1;
473 args = &arg;
474 }
475 ptr_buffer<expr> new_args;
476 rational k;
477 for (unsigned i = 0; i < sz; i++) {
478 expr * arg = args[i];
479 expr * arg0, *arg1;
480 if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() &&
481 ((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) {
482 if (is_eq || !k.is_even()) {
483 if (m_util.is_int(arg0))
484 arg0 = m_util.mk_to_real(arg0);
485 new_args.push_back(arg0);
486 }
487 else {
488 new_args.push_back(m_util.mk_power(arg0, m_util.mk_real(2)));
489 }
490 }
491 else {
492 new_args.push_back(arg);
493 }
494 }
495 SASSERT(new_args.size() >= 1);
496 if (new_args.size() == 1)
497 return new_args[0];
498 else
499 return m_util.mk_mul(new_args.size(), new_args.c_ptr());
500 }
501
reduce_power(expr * arg1,expr * arg2,op_kind kind,expr_ref & result)502 br_status arith_rewriter::reduce_power(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) {
503 expr * new_arg1 = reduce_power(arg1, kind == EQ);
504 expr * new_arg2 = reduce_power(arg2, kind == EQ);
505 switch (kind) {
506 case LE: result = m_util.mk_le(new_arg1, new_arg2); return BR_REWRITE1;
507 case GE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_REWRITE1;
508 default: result = m().mk_eq(new_arg1, new_arg2); return BR_REWRITE1;
509 }
510 }
511
mk_le_ge_eq_core(expr * arg1,expr * arg2,op_kind kind,expr_ref & result)512 br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) {
513 expr *orig_arg1 = arg1, *orig_arg2 = arg2;
514 expr_ref new_arg1(m());
515 expr_ref new_arg2(m());
516 if ((is_zero(arg1) && is_reduce_power_target(arg2, kind == EQ)) ||
517 (is_zero(arg2) && is_reduce_power_target(arg1, kind == EQ)))
518 return reduce_power(arg1, arg2, kind, result);
519 br_status st = cancel_monomials(arg1, arg2, m_arith_ineq_lhs || m_arith_lhs, new_arg1, new_arg2);
520 TRACE("mk_le_bug", tout << "st: " << st << " " << new_arg1 << " " << new_arg2 << "\n";);
521 if (st != BR_FAILED) {
522 arg1 = new_arg1;
523 arg2 = new_arg2;
524 }
525 expr_ref new_new_arg1(m());
526 expr_ref new_new_arg2(m());
527 if (m_elim_to_real && elim_to_real(arg1, arg2, new_new_arg1, new_new_arg2)) {
528 arg1 = new_new_arg1;
529 arg2 = new_new_arg2;
530 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";);
531 if (st == BR_FAILED)
532 st = BR_DONE;
533 }
534 numeral a1, a2;
535 if (is_numeral(arg1, a1) && is_numeral(arg2, a2)) {
536 switch (kind) {
537 case LE: result = a1 <= a2 ? m().mk_true() : m().mk_false(); return BR_DONE;
538 case GE: result = a1 >= a2 ? m().mk_true() : m().mk_false(); return BR_DONE;
539 default: result = a1 == a2 ? m().mk_true() : m().mk_false(); return BR_DONE;
540 }
541 }
542
543 #define ANUM_LE_GE_EQ() { \
544 switch (kind) { \
545 case LE: result = am.le(v1, v2) ? m().mk_true() : m().mk_false(); return BR_DONE; \
546 case GE: result = am.ge(v1, v2) ? m().mk_true() : m().mk_false(); return BR_DONE; \
547 default: result = am.eq(v1, v2) ? m().mk_true() : m().mk_false(); return BR_DONE; \
548 } \
549 }
550
551 if (m_anum_simp) {
552 if (is_numeral(arg1, a1) && m_util.is_irrational_algebraic_numeral(arg2)) {
553 anum_manager & am = m_util.am();
554 scoped_anum v1(am);
555 am.set(v1, a1.to_mpq());
556 anum const & v2 = m_util.to_irrational_algebraic_numeral(arg2);
557 ANUM_LE_GE_EQ();
558 }
559 if (m_util.is_irrational_algebraic_numeral(arg1) && is_numeral(arg2, a2)) {
560 anum_manager & am = m_util.am();
561 anum const & v1 = m_util.to_irrational_algebraic_numeral(arg1);
562 scoped_anum v2(am);
563 am.set(v2, a2.to_mpq());
564 ANUM_LE_GE_EQ();
565 }
566 if (m_util.is_irrational_algebraic_numeral(arg1) && m_util.is_irrational_algebraic_numeral(arg2)) {
567 anum_manager & am = m_util.am();
568 anum const & v1 = m_util.to_irrational_algebraic_numeral(arg1);
569 anum const & v2 = m_util.to_irrational_algebraic_numeral(arg2);
570 ANUM_LE_GE_EQ();
571 }
572 }
573 br_status st1 = is_separated(arg1, arg2, kind, result);
574 if (st1 != BR_FAILED)
575 return st1;
576 if (is_bound(arg1, arg2, kind, result))
577 return BR_DONE;
578 if (is_bound(arg2, arg1, inv(kind), result))
579 return BR_DONE;
580 bool is_int = m_util.is_int(arg1);
581 if (is_int && m_gcd_rounding) {
582 bool first = true;
583 numeral g;
584 unsigned num_consts = 0;
585 get_coeffs_gcd(arg1, g, first, num_consts);
586 TRACE("arith_rewriter_gcd", tout << "[step1] g: " << g << ", num_consts: " << num_consts << "\n";);
587 if ((first || !g.is_one()) && num_consts <= 1)
588 get_coeffs_gcd(arg2, g, first, num_consts);
589 TRACE("arith_rewriter_gcd", tout << "[step2] g: " << g << ", num_consts: " << num_consts << "\n";);
590 g = abs(g);
591 if (!first && !g.is_one() && num_consts <= 1) {
592 bool is_sat = div_polynomial(arg1, g, (kind == LE ? CT_CEIL : (kind == GE ? CT_FLOOR : CT_FALSE)), new_arg1);
593 if (!is_sat) {
594 result = m().mk_false();
595 return BR_DONE;
596 }
597 is_sat = div_polynomial(arg2, g, (kind == LE ? CT_FLOOR : (kind == GE ? CT_CEIL : CT_FALSE)), new_arg2);
598 if (!is_sat) {
599 result = m().mk_false();
600 return BR_DONE;
601 }
602 arg1 = new_arg1.get();
603 arg2 = new_arg2.get();
604 st = BR_DONE;
605 }
606 }
607 expr* c = nullptr, *t = nullptr, *e = nullptr;
608 if (m().is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) {
609 switch (kind) {
610 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;
611 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;
612 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;
613 }
614 }
615 if (m().is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) {
616 switch (kind) {
617 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;
618 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;
619 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;
620 }
621 }
622 if (m().is_ite(arg1, c, t, e) && arg1->get_ref_count() == 1) {
623 switch (kind) {
624 case LE: result = m().mk_ite(c, m_util.mk_le(t, arg2), m_util.mk_le(e, arg2)); return BR_REWRITE2;
625 case GE: result = m().mk_ite(c, m_util.mk_ge(t, arg2), m_util.mk_ge(e, arg2)); return BR_REWRITE2;
626 case EQ: result = m().mk_ite(c, m().mk_eq(t, arg2), m().mk_eq(e, arg2)); return BR_REWRITE2;
627 }
628 }
629 if (m_util.is_to_int(arg2) && is_numeral(arg1)) {
630 kind = inv(kind);
631 std::swap(arg1, arg2);
632 }
633 if (m_util.is_to_int(arg1, t) && is_numeral(arg2, a2)) {
634 switch (kind) {
635 case LE:
636 result = m_util.mk_lt(t, m_util.mk_numeral(a2+1, false));
637 return BR_REWRITE1;
638 case GE:
639 result = m_util.mk_ge(t, m_util.mk_numeral(a2, false));
640 return BR_REWRITE1;
641 case EQ:
642 result = m_util.mk_ge(t, m_util.mk_numeral(a2, false));
643 result = m().mk_and(m_util.mk_lt(t, m_util.mk_numeral(a2+1, false)), result);
644 return BR_REWRITE3;
645 }
646 }
647 if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
648 a2.neg();
649 new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));
650 switch (kind) {
651 case LE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_DONE;
652 case GE: result = m_util.mk_le(new_arg1, new_arg2); return BR_DONE;
653 case EQ: result = m_util.mk_eq(new_arg1, new_arg2); return BR_DONE;
654 }
655 }
656 else if (st == BR_DONE && arg1 == orig_arg1 && arg2 == orig_arg2) {
657 // Nothing new; return BR_FAILED to avoid rewriting loops.
658 return BR_FAILED;
659 }
660 else if (st != BR_FAILED) {
661 switch (kind) {
662 case LE: result = m_util.mk_le(arg1, arg2); return BR_DONE;
663 case GE: result = m_util.mk_ge(arg1, arg2); return BR_DONE;
664 default: result = m().mk_eq(arg1, arg2); return BR_DONE;
665 }
666 }
667 return BR_FAILED;
668 }
669
mk_le_core(expr * arg1,expr * arg2,expr_ref & result)670 br_status arith_rewriter::mk_le_core(expr * arg1, expr * arg2, expr_ref & result) {
671 return mk_le_ge_eq_core(arg1, arg2, LE, result);
672 }
673
mk_lt_core(expr * arg1,expr * arg2,expr_ref & result)674 br_status arith_rewriter::mk_lt_core(expr * arg1, expr * arg2, expr_ref & result) {
675 result = m().mk_not(m_util.mk_le(arg2, arg1));
676 return BR_REWRITE2;
677 }
678
mk_ge_core(expr * arg1,expr * arg2,expr_ref & result)679 br_status arith_rewriter::mk_ge_core(expr * arg1, expr * arg2, expr_ref & result) {
680 return mk_le_ge_eq_core(arg1, arg2, GE, result);
681 }
682
mk_gt_core(expr * arg1,expr * arg2,expr_ref & result)683 br_status arith_rewriter::mk_gt_core(expr * arg1, expr * arg2, expr_ref & result) {
684 result = m().mk_not(m_util.mk_le(arg1, arg2));
685 return BR_REWRITE2;
686 }
687
is_arith_term(expr * n) const688 bool arith_rewriter::is_arith_term(expr * n) const {
689 return n->get_kind() == AST_APP && to_app(n)->get_family_id() == get_fid();
690 }
691
mk_eq_core(expr * arg1,expr * arg2,expr_ref & result)692 br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
693 br_status st = BR_FAILED;
694 if (m_eq2ineq) {
695 result = m().mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2));
696 st = BR_REWRITE2;
697 }
698 else if (m_arith_lhs || is_arith_term(arg1) || is_arith_term(arg2)) {
699 st = mk_le_ge_eq_core(arg1, arg2, EQ, result);
700 }
701 return st;
702 }
703
neg_monomial(expr * e) const704 expr_ref arith_rewriter::neg_monomial(expr* e) const {
705 expr_ref_vector args(m());
706 rational a1;
707 if (is_app(e) && m_util.is_mul(e)) {
708 if (is_numeral(to_app(e)->get_arg(0), a1)) {
709 if (!a1.is_minus_one()) {
710 args.push_back(m_util.mk_numeral(-a1, m_util.is_int(e)));
711 }
712 args.append(to_app(e)->get_num_args() - 1, to_app(e)->get_args() + 1);
713 }
714 else {
715 args.push_back(m_util.mk_numeral(rational(-1), m_util.is_int(e)));
716 args.push_back(e);
717 }
718 }
719 else {
720 args.push_back(m_util.mk_numeral(rational(-1), m_util.is_int(e)));
721 args.push_back(e);
722 }
723 if (args.size() == 1) {
724 return expr_ref(args.back(), m());
725 }
726 else {
727 return expr_ref(m_util.mk_mul(args.size(), args.c_ptr()), m());
728 }
729 }
730
is_neg_poly(expr * t,expr_ref & neg) const731 bool arith_rewriter::is_neg_poly(expr* t, expr_ref& neg) const {
732 rational r;
733 if (m_util.is_mul(t) && is_numeral(to_app(t)->get_arg(0), r) && r.is_neg()) {
734 neg = neg_monomial(t);
735 return true;
736 }
737
738 if (!m_util.is_add(t)) {
739 return false;
740 }
741 expr * t2 = to_app(t)->get_arg(0);
742
743 if (m_util.is_mul(t2) && is_numeral(to_app(t2)->get_arg(0), r) && r.is_neg()) {
744 expr_ref_vector args1(m());
745 for (expr* e1 : *to_app(t)) {
746 args1.push_back(neg_monomial(e1));
747 }
748 neg = m_util.mk_add(args1.size(), args1.c_ptr());
749 return true;
750 }
751 return false;
752 }
753
is_anum_simp_target(unsigned num_args,expr * const * args)754 bool arith_rewriter::is_anum_simp_target(unsigned num_args, expr * const * args) {
755 if (!m_anum_simp)
756 return false;
757 unsigned num_irrat = 0;
758 unsigned num_rat = 0;
759 for (unsigned i = 0; i < num_args; i++) {
760 if (m_util.is_numeral(args[i])) {
761 num_rat++;
762 if (num_irrat > 0)
763 return true;
764 }
765 if (m_util.is_irrational_algebraic_numeral(args[i]) &&
766 m_util.am().degree(m_util.to_irrational_algebraic_numeral(args[i])) <= m_max_degree) {
767 num_irrat++;
768 if (num_irrat > 1 || num_rat > 0)
769 return true;
770 }
771 }
772 return false;
773 }
774
mk_add_core(unsigned num_args,expr * const * args,expr_ref & result)775 br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, expr_ref & result) {
776 if (is_anum_simp_target(num_args, args)) {
777 expr_ref_buffer new_args(m());
778 anum_manager & am = m_util.am();
779 scoped_anum r(am);
780 scoped_anum arg(am);
781 rational rarg;
782 am.set(r, 0);
783 for (unsigned i = 0; i < num_args; i ++) {
784 unsigned d = am.degree(r);
785 if (d > 1 && d > m_max_degree) {
786 new_args.push_back(m_util.mk_numeral(am, r, false));
787 am.set(r, 0);
788 }
789
790 if (m_util.is_numeral(args[i], rarg)) {
791 am.set(arg, rarg.to_mpq());
792 am.add(r, arg, r);
793 continue;
794 }
795
796 if (m_util.is_irrational_algebraic_numeral(args[i])) {
797 anum const & irarg = m_util.to_irrational_algebraic_numeral(args[i]);
798 if (am.degree(irarg) <= m_max_degree) {
799 am.add(r, irarg, r);
800 continue;
801 }
802 }
803
804 new_args.push_back(args[i]);
805 }
806
807 if (new_args.empty()) {
808 result = m_util.mk_numeral(am, r, false);
809 return BR_DONE;
810 }
811
812 new_args.push_back(m_util.mk_numeral(am, r, false));
813 br_status st = poly_rewriter<arith_rewriter_core>::mk_add_core(new_args.size(), new_args.c_ptr(), result);
814 if (st == BR_FAILED) {
815 result = m().mk_app(get_fid(), OP_ADD, new_args.size(), new_args.c_ptr());
816 return BR_DONE;
817 }
818 return st;
819 }
820 else {
821 return poly_rewriter<arith_rewriter_core>::mk_add_core(num_args, args, result);
822 }
823 }
824
mk_mul_core(unsigned num_args,expr * const * args,expr_ref & result)825 br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
826 if (is_anum_simp_target(num_args, args)) {
827 expr_ref_buffer new_args(m());
828 anum_manager & am = m_util.am();
829 scoped_anum r(am);
830 scoped_anum arg(am);
831 rational rarg;
832 am.set(r, 1);
833 for (unsigned i = 0; i < num_args; i ++) {
834 unsigned d = am.degree(r);
835 if (d > 1 && d > m_max_degree) {
836 new_args.push_back(m_util.mk_numeral(am, r, false));
837 am.set(r, 1);
838 }
839
840 if (m_util.is_numeral(args[i], rarg)) {
841 am.set(arg, rarg.to_mpq());
842 am.mul(r, arg, r);
843 continue;
844 }
845 if (m_util.is_irrational_algebraic_numeral(args[i])) {
846 anum const & irarg = m_util.to_irrational_algebraic_numeral(args[i]);
847 if (am.degree(irarg) <= m_max_degree) {
848 am.mul(r, irarg, r);
849 continue;
850 }
851 }
852
853 new_args.push_back(args[i]);
854 }
855
856 if (new_args.empty()) {
857 result = m_util.mk_numeral(am, r, false);
858 return BR_DONE;
859 }
860 new_args.push_back(m_util.mk_numeral(am, r, false));
861
862 br_status st = poly_rewriter<arith_rewriter_core>::mk_mul_core(new_args.size(), new_args.c_ptr(), result);
863 if (st == BR_FAILED) {
864 result = m().mk_app(get_fid(), OP_MUL, new_args.size(), new_args.c_ptr());
865 return BR_DONE;
866 }
867 return st;
868 }
869 else {
870 return poly_rewriter<arith_rewriter_core>::mk_mul_core(num_args, args, result);
871 }
872 }
873
mk_div_irrat_rat(expr * arg1,expr * arg2,expr_ref & result)874 br_status arith_rewriter::mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result) {
875 SASSERT(m_util.is_real(arg1));
876 SASSERT(m_util.is_irrational_algebraic_numeral(arg1));
877 SASSERT(m_util.is_numeral(arg2));
878 anum_manager & am = m_util.am();
879 anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1);
880 rational rval2;
881 VERIFY(m_util.is_numeral(arg2, rval2));
882 if (rval2.is_zero())
883 return BR_FAILED;
884 scoped_anum val2(am);
885 am.set(val2, rval2.to_mpq());
886 scoped_anum r(am);
887 am.div(val1, val2, r);
888 result = m_util.mk_numeral(am, r, false);
889 return BR_DONE;
890 }
891
mk_div_rat_irrat(expr * arg1,expr * arg2,expr_ref & result)892 br_status arith_rewriter::mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result) {
893 SASSERT(m_util.is_real(arg1));
894 SASSERT(m_util.is_numeral(arg1));
895 SASSERT(m_util.is_irrational_algebraic_numeral(arg2));
896 anum_manager & am = m_util.am();
897 rational rval1;
898 VERIFY(m_util.is_numeral(arg1, rval1));
899 scoped_anum val1(am);
900 am.set(val1, rval1.to_mpq());
901 anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2);
902 scoped_anum r(am);
903 am.div(val1, val2, r);
904 result = m_util.mk_numeral(am, r, false);
905 return BR_DONE;
906 }
907
mk_div_irrat_irrat(expr * arg1,expr * arg2,expr_ref & result)908 br_status arith_rewriter::mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result) {
909 SASSERT(m_util.is_real(arg1));
910 SASSERT(m_util.is_irrational_algebraic_numeral(arg1));
911 SASSERT(m_util.is_irrational_algebraic_numeral(arg2));
912 anum_manager & am = m_util.am();
913 anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1);
914 if (am.degree(val1) > m_max_degree)
915 return BR_FAILED;
916 anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2);
917 if (am.degree(val2) > m_max_degree)
918 return BR_FAILED;
919 scoped_anum r(am);
920 am.div(val1, val2, r);
921 result = m_util.mk_numeral(am, r.get(), false);
922 return BR_DONE;
923 }
924
mk_div_core(expr * arg1,expr * arg2,expr_ref & result)925 br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & result) {
926 if (m_anum_simp) {
927 if (m_util.is_irrational_algebraic_numeral(arg1) && m_util.is_numeral(arg2))
928 return mk_div_irrat_rat(arg1, arg2, result);
929 if (m_util.is_irrational_algebraic_numeral(arg1) && m_util.is_irrational_algebraic_numeral(arg2))
930 return mk_div_irrat_irrat(arg1, arg2, result);
931 if (m_util.is_irrational_algebraic_numeral(arg2) && m_util.is_numeral(arg1))
932 return mk_div_rat_irrat(arg1, arg2, result);
933 }
934 set_curr_sort(m().get_sort(arg1));
935 numeral v1, v2;
936 bool is_int;
937 if (m_util.is_numeral(arg2, v2, is_int)) {
938 SASSERT(!is_int);
939 if (v2.is_zero()) {
940 return BR_FAILED;
941 }
942 else if (m_util.is_numeral(arg1, v1, is_int)) {
943 result = m_util.mk_numeral(v1/v2, false);
944 return BR_DONE;
945 }
946 else {
947 numeral k(1);
948 k /= v2;
949 result = m().mk_app(get_fid(), OP_MUL,
950 m_util.mk_numeral(k, false),
951 arg1);
952 return BR_REWRITE1;
953 }
954 }
955
956 #if 0
957 if (!m_util.is_int(arg1)) {
958 // (/ (* v1 b) (* v2 d)) --> (* v1/v2 (/ b d))
959 expr * a, * b, * c, * d;
960 if (m_util.is_mul(arg1, a, b) && m_util.is_numeral(a, v1)) {
961 // do nothing arg1 is of the form v1 * b
962 }
963 else {
964 v1 = rational(1);
965 b = arg1;
966 }
967 if (m_util.is_mul(arg2, c, d) && m_util.is_numeral(c, v2)) {
968 // do nothing arg2 is of the form v2 * d
969 }
970 else {
971 v2 = rational(1);
972 d = arg2;
973 }
974 TRACE("div_bug", tout << "v1: " << v1 << ", v2: " << v2 << "\n";);
975 if (!v1.is_one() || !v2.is_one()) {
976 v1 /= v2;
977 result = m_util.mk_mul(m_util.mk_numeral(v1, false),
978 m_util.mk_div(b, d));
979 expr_ref z(m_util.mk_real(0), m());
980 result = m().mk_ite(m().mk_eq(d, z), m_util.mk_div(arg1, z), result);
981 return BR_REWRITE2;
982 }
983 }
984 #endif
985
986 return BR_FAILED;
987 }
988
mk_idivides(unsigned k,expr * arg,expr_ref & result)989 br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) {
990 result = m().mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0));
991 return BR_REWRITE2;
992 }
993
mk_idiv_core(expr * arg1,expr * arg2,expr_ref & result)994 br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result) {
995 set_curr_sort(m().get_sort(arg1));
996 numeral v1, v2;
997 bool is_int;
998 if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
999 result = m_util.mk_numeral(div(v1, v2), is_int);
1000 return BR_DONE;
1001 }
1002 if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) {
1003 result = arg1;
1004 return BR_DONE;
1005 }
1006 if (m_util.is_numeral(arg2, v2, is_int) && v2.is_minus_one()) {
1007 result = m_util.mk_mul(m_util.mk_int(-1), arg1);
1008 return BR_REWRITE1;
1009 }
1010 if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
1011 return BR_FAILED;
1012 }
1013 if (arg1 == arg2) {
1014 expr_ref zero(m_util.mk_int(0), m());
1015 result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1));
1016 return BR_REWRITE3;
1017 }
1018 if (m_util.is_numeral(arg2, v2, is_int) && v2.is_pos() && m_util.is_add(arg1)) {
1019 expr_ref_buffer args(m());
1020 bool change = false;
1021 rational add(0);
1022 for (expr* arg : *to_app(arg1)) {
1023 rational arg_v;
1024 if (m_util.is_numeral(arg, arg_v) && arg_v.is_pos() && mod(arg_v, v2) != arg_v) {
1025 change = true;
1026 args.push_back(m_util.mk_numeral(mod(arg_v, v2), true));
1027 add += div(arg_v, v2);
1028 }
1029 else {
1030 args.push_back(arg);
1031 }
1032 }
1033 if (change) {
1034 result = m_util.mk_idiv(m().mk_app(to_app(arg1)->get_decl(), args.size(), args.c_ptr()), arg2);
1035 result = m_util.mk_add(m_util.mk_numeral(add, true), result);
1036 TRACE("div_bug", tout << "mk_div result: " << result << "\n";);
1037 return BR_REWRITE3;
1038 }
1039 }
1040 if (divides(arg1, arg2, result)) {
1041 expr_ref zero(m_util.mk_int(0), m());
1042 result = m().mk_ite(m().mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result);
1043 return BR_REWRITE_FULL;
1044 }
1045 return BR_FAILED;
1046 }
1047
1048 //
1049 // implement div ab ac = floor( ab / ac) = floor (b / c) = div b c
1050 //
divides(expr * num,expr * den,expr_ref & result)1051 bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) {
1052 expr_fast_mark1 mark;
1053 rational num_r(1), den_r(1);
1054 expr* num_e = nullptr, *den_e = nullptr;
1055 ptr_buffer<expr> args1, args2;
1056 flat_mul(num, args1);
1057 flat_mul(den, args2);
1058 for (expr * arg : args1) {
1059 mark.mark(arg);
1060 if (m_util.is_numeral(arg, num_r)) num_e = arg;
1061 }
1062 for (expr* arg : args2) {
1063 // dont remove divisor on (div (* -1 x) (* -1 y)) because rewriting would diverge.
1064 if (mark.is_marked(arg) && (!m_util.is_numeral(arg, num_r) || !num_r.is_minus_one())) {
1065 result = remove_divisor(arg, num, den);
1066 return true;
1067 }
1068 if (m_util.is_numeral(arg, den_r)) den_e = arg;
1069 }
1070 rational g = gcd(num_r, den_r);
1071 if (!g.is_one()) {
1072 SASSERT(g.is_pos());
1073 // replace num_e, den_e by their gcd reduction.
1074 for (unsigned i = 0; i < args1.size(); ++i) {
1075 if (args1[i] == num_e) {
1076 args1[i] = m_util.mk_numeral(num_r / g, true);
1077 break;
1078 }
1079 }
1080 for (unsigned i = 0; i < args2.size(); ++i) {
1081 if (args2[i] == den_e) {
1082 args2[i] = m_util.mk_numeral(den_r / g, true);
1083 break;
1084 }
1085 }
1086 num = m_util.mk_mul(args1.size(), args1.c_ptr());
1087 den = m_util.mk_mul(args2.size(), args2.c_ptr());
1088 result = m_util.mk_idiv(num, den);
1089 return true;
1090 }
1091 return false;
1092 }
1093
1094
remove_divisor(expr * arg,expr * num,expr * den)1095 expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
1096 ptr_buffer<expr> args1, args2;
1097 flat_mul(num, args1);
1098 flat_mul(den, args2);
1099 remove_divisor(arg, args1);
1100 remove_divisor(arg, args2);
1101 expr_ref zero(m_util.mk_int(0), m());
1102 num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.c_ptr());
1103 den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.c_ptr());
1104 expr_ref d(m_util.mk_idiv(num, den), m());
1105 expr_ref nd(m_util.mk_idiv(m_util.mk_uminus(num), m_util.mk_uminus(den)), m());
1106 return expr_ref(m().mk_ite(m().mk_eq(zero, arg),
1107 m_util.mk_idiv(zero, zero),
1108 m().mk_ite(m_util.mk_ge(arg, zero),
1109 d,
1110 nd)),
1111 m());
1112 }
1113
flat_mul(expr * e,ptr_buffer<expr> & args)1114 void arith_rewriter::flat_mul(expr* e, ptr_buffer<expr>& args) {
1115 args.push_back(e);
1116 for (unsigned i = 0; i < args.size(); ++i) {
1117 e = args[i];
1118 if (m_util.is_mul(e)) {
1119 args.append(to_app(e)->get_num_args(), to_app(e)->get_args());
1120 args[i] = args.back();
1121 args.shrink(args.size()-1);
1122 --i;
1123 }
1124 }
1125 }
1126
remove_divisor(expr * d,ptr_buffer<expr> & args)1127 void arith_rewriter::remove_divisor(expr* d, ptr_buffer<expr>& args) {
1128 for (unsigned i = 0; i < args.size(); ++i) {
1129 if (args[i] == d) {
1130 args[i] = args.back();
1131 args.shrink(args.size()-1);
1132 return;
1133 }
1134 }
1135 UNREACHABLE();
1136 }
1137
symmod(rational const & a,rational const & b)1138 static rational symmod(rational const& a, rational const& b) {
1139 rational r = mod(a, b);
1140 if (2*r > b) r -= b;
1141 return r;
1142 }
1143
mk_mod_core(expr * arg1,expr * arg2,expr_ref & result)1144 br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
1145 set_curr_sort(m().get_sort(arg1));
1146 numeral v1, v2;
1147 bool is_int;
1148 if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
1149 result = m_util.mk_numeral(mod(v1, v2), is_int);
1150 return BR_DONE;
1151 }
1152
1153 if (m_util.is_numeral(arg2, v2, is_int) && is_int && (v2.is_one() || v2.is_minus_one())) {
1154 result = m_util.mk_numeral(numeral(0), true);
1155 return BR_DONE;
1156 }
1157
1158 if (arg1 == arg2 && !m_util.is_numeral(arg2)) {
1159 expr_ref zero(m_util.mk_int(0), m());
1160 result = m().mk_ite(m().mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero);
1161 return BR_DONE;
1162 }
1163
1164 // mod is idempotent on non-zero modulus.
1165 expr* t1, *t2;
1166 if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
1167 result = arg1;
1168 return BR_DONE;
1169 }
1170
1171 // propagate mod inside only if there is something to reduce.
1172 if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) {
1173 TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";);
1174 expr_ref_buffer args(m());
1175 bool change = false;
1176 for (expr* arg : *to_app(arg1)) {
1177 rational arg_v;
1178 if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) != arg_v) {
1179 change = true;
1180 args.push_back(m_util.mk_numeral(mod(arg_v, v2), true));
1181 }
1182 else if (m_util.is_mod(arg, t1, t2) && t2 == arg2) {
1183 change = true;
1184 args.push_back(t1);
1185 }
1186 else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, v2) != arg_v) {
1187 change = true;
1188 args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, v2), true), t2));
1189 }
1190 else {
1191 args.push_back(arg);
1192 }
1193 }
1194 if (!change) {
1195 return BR_FAILED; // did not find any target for applying simplification
1196 }
1197 result = m_util.mk_mod(m().mk_app(to_app(arg1)->get_decl(), args.size(), args.c_ptr()), arg2);
1198 TRACE("mod_bug", tout << "mk_mod result: " << mk_ismt2_pp(result, m()) << "\n";);
1199 return BR_REWRITE3;
1200 }
1201
1202 return BR_FAILED;
1203 }
1204
mk_rem_core(expr * arg1,expr * arg2,expr_ref & result)1205 br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & result) {
1206 set_curr_sort(m().get_sort(arg1));
1207 numeral v1, v2;
1208 bool is_int;
1209 if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
1210 numeral m = mod(v1, v2);
1211 //
1212 // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2)
1213 //
1214 if (v2.is_neg()) {
1215 m.neg();
1216 }
1217 result = m_util.mk_numeral(m, is_int);
1218 return BR_DONE;
1219 }
1220 else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) {
1221 result = m_util.mk_numeral(numeral(0), true);
1222 return BR_DONE;
1223 }
1224 else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
1225 if (is_add(arg1) || is_mul(arg1)) {
1226 return BR_FAILED;
1227 }
1228 else {
1229 if (v2.is_neg()) {
1230 result = m_util.mk_uminus(m_util.mk_mod(arg1, arg2));
1231 return BR_REWRITE2;
1232 }
1233 else {
1234 result = m_util.mk_mod(arg1, arg2);
1235 return BR_REWRITE1;
1236 }
1237 }
1238 }
1239 else if (m_elim_rem) {
1240 expr * mod = m_util.mk_mod(arg1, arg2);
1241 result = m().mk_ite(m_util.mk_ge(arg2, m_util.mk_numeral(rational(0), true)),
1242 mod,
1243 m_util.mk_uminus(mod));
1244 TRACE("elim_rem", tout << "result: " << mk_ismt2_pp(result, m()) << "\n";);
1245 return BR_REWRITE3;
1246 }
1247 return BR_FAILED;
1248 }
1249
coerce(expr * x,sort * s)1250 expr* arith_rewriter_core::coerce(expr* x, sort* s) {
1251 if (m_util.is_int(x) && m_util.is_real(s))
1252 return m_util.mk_to_real(x);
1253 if (m_util.is_real(x) && m_util.is_int(s))
1254 return m_util.mk_to_int(x);
1255 return x;
1256 }
1257
mk_power(expr * x,rational const & r,sort * s)1258 app* arith_rewriter_core::mk_power(expr* x, rational const& r, sort* s) {
1259 SASSERT(r.is_unsigned() && r.is_pos());
1260 bool is_int = m_util.is_int(x);
1261 app* y = m_util.mk_power(x, m_util.mk_numeral(r, is_int));
1262 if (m_util.is_int(s))
1263 y = m_util.mk_to_int(y);
1264 return y;
1265 }
1266
mk_power_core(expr * arg1,expr * arg2,expr_ref & result)1267 br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & result) {
1268 numeral x, y;
1269 bool is_num_x = m_util.is_numeral(arg1, x);
1270 bool is_num_y = m_util.is_numeral(arg2, y);
1271 auto ensure_real = [&](expr* e) { return m_util.is_int(e) ? m_util.mk_to_real(e) : e; };
1272
1273 TRACE("arith", tout << mk_pp(arg1, m()) << " " << mk_pp(arg2, m()) << "\n";);
1274 if (is_num_x && x.is_one()) {
1275 result = m_util.mk_numeral(x, false);
1276 return BR_DONE;
1277 }
1278
1279 if (is_num_y && y.is_one()) {
1280 result = ensure_real(arg1);
1281 return BR_REWRITE1;
1282 }
1283
1284 if (is_num_x && is_num_y) {
1285 if (x.is_zero() && y.is_zero())
1286 return BR_FAILED;
1287
1288 if (y.is_zero()) {
1289 result = m_util.mk_numeral(rational(1), false);
1290 return BR_DONE;
1291 }
1292
1293 if (x.is_zero()) {
1294 result = m_util.mk_numeral(x, false);
1295 return BR_DONE;
1296 }
1297
1298 if (y.is_unsigned() && y.get_unsigned() <= m_max_degree) {
1299 x = power(x, y.get_unsigned());
1300 result = m_util.mk_numeral(x, false);
1301 return BR_DONE;
1302 }
1303
1304 if ((-y).is_unsigned() && (-y).get_unsigned() <= m_max_degree) {
1305 x = power(rational(1)/x, (-y).get_unsigned());
1306 result = m_util.mk_numeral(x, false);
1307 return BR_DONE;
1308 }
1309
1310 if (y.is_minus_one()) {
1311 result = m_util.mk_numeral(rational(1) / x, false);
1312 return BR_DONE;
1313 }
1314 }
1315
1316 expr* arg10, *arg11;
1317 if (m_util.is_power(arg1, arg10, arg11) && is_num_y && y.is_int() && !y.is_zero()) {
1318 // (^ (^ t y2) y) --> (^ t (* y2 y)) If y2 > 0 && y != 0 && y and y2 are integers
1319 rational y2;
1320 if (m_util.is_numeral(arg11, y2) && y2.is_int() && y2.is_pos()) {
1321 result = m_util.mk_power(ensure_real(arg10), m_util.mk_numeral(y*y2, false));
1322 return BR_REWRITE2;
1323 }
1324 }
1325
1326 if (is_num_y && y.is_minus_one()) {
1327 result = m_util.mk_div(m_util.mk_real(1), ensure_real(arg1));
1328 result = m().mk_ite(m().mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))),
1329 m_util.mk_real(0),
1330 result);
1331 return BR_REWRITE2;
1332 }
1333
1334 if (is_num_y && y.is_neg()) {
1335 // (^ t -k) --> (^ (/ 1 t) k)
1336 result = m_util.mk_power(m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1),
1337 m_util.mk_numeral(-y, false));
1338 result = m().mk_ite(m().mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))),
1339 m_util.mk_real(0),
1340 result);
1341 return BR_REWRITE3;
1342 }
1343
1344 if (is_num_y && !y.is_int() && !numerator(y).is_one()) {
1345 // (^ t (/ p q)) --> (^ (^ t (/ 1 q)) p)
1346 result = m_util.mk_power(m_util.mk_power(ensure_real(arg1), m_util.mk_numeral(rational(1)/denominator(y), false)),
1347 m_util.mk_numeral(numerator(y), false));
1348 return BR_REWRITE3;
1349 }
1350
1351 if ((m_expand_power || (m_som && is_app(arg1) && to_app(arg1)->get_family_id() == get_fid())) &&
1352 is_num_y && y.is_unsigned() && 1 < y.get_unsigned() && y.get_unsigned() <= m_max_degree) {
1353 ptr_buffer<expr> args;
1354 unsigned k = y.get_unsigned();
1355 for (unsigned i = 0; i < k; i++) {
1356 args.push_back(arg1);
1357 }
1358 result = ensure_real(m_util.mk_mul(args.size(), args.c_ptr()));
1359 return BR_REWRITE2;
1360 }
1361
1362 if (!is_num_y)
1363 return BR_FAILED;
1364
1365 bool is_irrat_x = m_util.is_irrational_algebraic_numeral(arg1);
1366
1367 if (!is_num_x && !is_irrat_x)
1368 return BR_FAILED;
1369
1370 if (y.is_zero()) {
1371 return BR_FAILED;
1372 }
1373
1374 rational num_y = numerator(y);
1375 rational den_y = denominator(y);
1376 bool is_neg_y = false;
1377 if (num_y.is_neg()) {
1378 num_y.neg();
1379 is_neg_y = true;
1380 }
1381 SASSERT(num_y.is_pos());
1382 SASSERT(den_y.is_pos());
1383
1384 if (!num_y.is_unsigned() || !den_y.is_unsigned())
1385 return BR_FAILED;
1386
1387 unsigned u_num_y = num_y.get_unsigned();
1388 unsigned u_den_y = den_y.get_unsigned();
1389
1390 if (u_num_y > m_max_degree || u_den_y > m_max_degree)
1391 return BR_FAILED;
1392
1393 if (is_num_x) {
1394 rational xk, r;
1395 xk = power(x, u_num_y);
1396 if (xk.is_neg() && u_den_y % 2 == 0) {
1397 return BR_FAILED;
1398 }
1399 if (xk.root(u_den_y, r)) {
1400 if (is_neg_y)
1401 r = rational(1)/r;
1402 result = m_util.mk_numeral(r, false);
1403 return BR_DONE;
1404 }
1405 if (m_anum_simp) {
1406 anum_manager & am = m_util.am();
1407 scoped_anum r(am);
1408 am.set(r, xk.to_mpq());
1409 am.root(r, u_den_y, r);
1410 if (is_neg_y)
1411 am.inv(r);
1412 result = m_util.mk_numeral(am, r, false);
1413 return BR_DONE;
1414 }
1415 return BR_FAILED;
1416 }
1417
1418 SASSERT(is_irrat_x);
1419 if (!m_anum_simp)
1420 return BR_FAILED;
1421
1422 anum const & val = m_util.to_irrational_algebraic_numeral(arg1);
1423 anum_manager & am = m_util.am();
1424 if (am.degree(val) > m_max_degree)
1425 return BR_FAILED;
1426 scoped_anum r(am);
1427 am.power(val, u_num_y, r);
1428 am.root(r, u_den_y, r);
1429 if (is_neg_y)
1430 am.inv(r);
1431 result = m_util.mk_numeral(am, r, false);
1432 return BR_DONE;
1433 }
1434
mk_to_int_core(expr * arg,expr_ref & result)1435 br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
1436 numeral a;
1437 expr* x = nullptr;
1438 if (m_util.convert_int_numerals_to_real())
1439 return BR_FAILED;
1440
1441 if (m_util.is_numeral(arg, a)) {
1442 result = m_util.mk_numeral(floor(a), true);
1443 return BR_DONE;
1444 }
1445
1446 if (m_util.is_to_real(arg, x)) {
1447 result = x;
1448 return BR_DONE;
1449 }
1450
1451 if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) {
1452 // Try to apply simplifications such as:
1453 // (to_int (+ 1.0 (to_real x)) y) --> (+ 1 x (to_int y))
1454
1455 expr_ref_buffer int_args(m()), real_args(m());
1456 for (expr* c : *to_app(arg)) {
1457 if (m_util.is_numeral(c, a) && a.is_int()) {
1458 int_args.push_back(m_util.mk_numeral(a, true));
1459 }
1460 else if (m_util.is_to_real(c, x)) {
1461 int_args.push_back(x);
1462 }
1463 else {
1464 real_args.push_back(c);
1465 }
1466 }
1467 if (real_args.empty() && m_util.is_power(arg))
1468 return BR_FAILED;
1469
1470 if (real_args.empty()) {
1471 result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.c_ptr());
1472 return BR_REWRITE1;
1473 }
1474 if (!int_args.empty() && m_util.is_add(arg)) {
1475 decl_kind k = to_app(arg)->get_decl()->get_decl_kind();
1476 expr_ref t1(m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr()), m());
1477 expr_ref t2(m().mk_app(get_fid(), k, real_args.size(), real_args.c_ptr()), m());
1478 int_args.reset();
1479 int_args.push_back(t1);
1480 int_args.push_back(m_util.mk_to_int(t2));
1481 result = m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr());
1482 return BR_REWRITE3;
1483 }
1484 }
1485 return BR_FAILED;
1486 }
1487
mk_to_real_core(expr * arg,expr_ref & result)1488 br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) {
1489 numeral a;
1490 if (m_util.is_numeral(arg, a)) {
1491 result = m_util.mk_numeral(a, false);
1492 return BR_DONE;
1493 }
1494 // push to_real over OP_ADD, OP_MUL
1495 if (m_push_to_real) {
1496 if (m_util.is_add(arg) || m_util.is_mul(arg)) {
1497 ptr_buffer<expr> new_args;
1498 for (expr* e : *to_app(arg))
1499 new_args.push_back(m_util.mk_to_real(e));
1500 if (m_util.is_add(arg))
1501 result = m().mk_app(get_fid(), OP_ADD, new_args.size(), new_args.c_ptr());
1502 else
1503 result = m().mk_app(get_fid(), OP_MUL, new_args.size(), new_args.c_ptr());
1504 return BR_REWRITE2;
1505 }
1506 }
1507 return BR_FAILED;
1508 }
1509
mk_is_int(expr * arg,expr_ref & result)1510 br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) {
1511 numeral a;
1512 if (m_util.is_numeral(arg, a)) {
1513 result = a.is_int() ? m().mk_true() : m().mk_false();
1514 return BR_DONE;
1515 }
1516 else if (m_util.is_to_real(arg)) {
1517 result = m().mk_true();
1518 return BR_DONE;
1519 }
1520 else {
1521 result = m().mk_eq(m().mk_app(get_fid(), OP_TO_REAL,
1522 m().mk_app(get_fid(), OP_TO_INT, arg)),
1523 arg);
1524 return BR_REWRITE3;
1525 }
1526 }
1527
mk_abs_core(expr * arg,expr_ref & result)1528 br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) {
1529 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));
1530 return BR_REWRITE2;
1531 }
1532
1533
1534 // Return true if t is of the form c*Pi where c is a numeral.
1535 // Store c into k
is_pi_multiple(expr * t,rational & k)1536 bool arith_rewriter::is_pi_multiple(expr * t, rational & k) {
1537 if (m_util.is_pi(t)) {
1538 k = rational(1);
1539 return true;
1540 }
1541 expr * a, * b;
1542 return m_util.is_mul(t, a, b) && m_util.is_pi(b) && m_util.is_numeral(a, k);
1543 }
1544
1545 // Return true if t is of the form (+ s c*Pi) where c is a numeral.
1546 // Store c into k, and c*Pi into m.
is_pi_offset(expr * t,rational & k,expr * & m)1547 bool arith_rewriter::is_pi_offset(expr * t, rational & k, expr * & m) {
1548 if (m_util.is_add(t)) {
1549 for (expr* arg : *to_app(t))
1550 if (is_pi_multiple(arg, k)) {
1551 m = arg;
1552 return true;
1553 }
1554 }
1555 return false;
1556 }
1557
1558 // Return true if t is of the form 2*pi*to_real(s).
is_2_pi_integer(expr * t)1559 bool arith_rewriter::is_2_pi_integer(expr * t) {
1560 expr * a, * m, * b, * c;
1561 rational k;
1562 return
1563 m_util.is_mul(t, a, m) &&
1564 m_util.is_numeral(a, k) &&
1565 k.is_int() &&
1566 mod(k, rational(2)).is_zero() &&
1567 m_util.is_mul(m, b, c) &&
1568 ((m_util.is_pi(b) && m_util.is_to_real(c)) || (m_util.is_to_real(b) && m_util.is_pi(c)));
1569 }
1570
1571 // Return true if t is of the form s + 2*pi*to_real(s).
1572 // Store 2*pi*to_real(s) into m.
is_2_pi_integer_offset(expr * t,expr * & m)1573 bool arith_rewriter::is_2_pi_integer_offset(expr * t, expr * & m) {
1574 if (m_util.is_add(t)) {
1575 for (expr* arg : *to_app(t))
1576 if (is_2_pi_integer(arg)) {
1577 m = arg;
1578 return true;
1579 }
1580 }
1581 return false;
1582 }
1583
1584 // Return true if t is of the form pi*to_real(s).
is_pi_integer(expr * t)1585 bool arith_rewriter::is_pi_integer(expr * t) {
1586 expr * a, * b;
1587 if (m_util.is_mul(t, a, b)) {
1588 rational k;
1589 if (m_util.is_numeral(a, k)) {
1590 if (!k.is_int())
1591 return false;
1592 expr * c, * d;
1593 if (!m_util.is_mul(b, c, d))
1594 return false;
1595 a = c;
1596 b = d;
1597 }
1598 TRACE("tan", tout << "is_pi_integer " << mk_ismt2_pp(t, m()) << "\n";
1599 tout << "a: " << mk_ismt2_pp(a, m()) << "\n";
1600 tout << "b: " << mk_ismt2_pp(b, m()) << "\n";);
1601 return
1602 (m_util.is_pi(a) && m_util.is_to_real(b)) ||
1603 (m_util.is_to_real(a) && m_util.is_pi(b));
1604 }
1605 return false;
1606 }
1607
1608 // Return true if t is of the form s + pi*to_real(s).
1609 // Store 2*pi*to_real(s) into m.
is_pi_integer_offset(expr * t,expr * & m)1610 bool arith_rewriter::is_pi_integer_offset(expr * t, expr * & m) {
1611 if (m_util.is_add(t)) {
1612 for (expr* arg : *to_app(t))
1613 if (is_pi_integer(arg)) {
1614 m = arg;
1615 return true;
1616 }
1617 }
1618 return false;
1619 }
1620
mk_sqrt(rational const & k)1621 app * arith_rewriter::mk_sqrt(rational const & k) {
1622 return m_util.mk_power(m_util.mk_numeral(k, false), m_util.mk_numeral(rational(1, 2), false));
1623 }
1624
1625 // Return a constant representing sin(k * pi).
1626 // Return 0 if failed.
mk_sin_value(rational const & k)1627 expr * arith_rewriter::mk_sin_value(rational const & k) {
1628 rational k_prime = mod(floor(k), rational(2)) + k - floor(k);
1629 TRACE("sine", tout << "k: " << k << ", k_prime: " << k_prime << "\n";);
1630 SASSERT(k_prime >= rational(0) && k_prime < rational(2));
1631 bool neg = false;
1632 if (k_prime >= rational(1)) {
1633 neg = true;
1634 k_prime = k_prime - rational(1);
1635 }
1636 SASSERT(k_prime >= rational(0) && k_prime < rational(1));
1637 if (k_prime.is_zero() || k_prime.is_one()) {
1638 // sin(0) == sin(pi) == 0
1639 return m_util.mk_numeral(rational(0), false);
1640 }
1641 if (k_prime == rational(1, 2)) {
1642 // sin(pi/2) == 1, sin(3/2 pi) == -1
1643 return m_util.mk_numeral(rational(neg ? -1 : 1), false);
1644 }
1645 if (k_prime == rational(1, 6) || k_prime == rational(5, 6)) {
1646 // sin(pi/6) == sin(5/6 pi) == 1/2
1647 // sin(7 pi/6) == sin(11/6 pi) == -1/2
1648 return m_util.mk_numeral(rational(neg ? -1 : 1, 2), false);
1649 }
1650 if (k_prime == rational(1, 4) || k_prime == rational(3, 4)) {
1651 // sin(pi/4) == sin(3/4 pi) == Sqrt(1/2)
1652 // sin(5/4 pi) == sin(7/4 pi) == - Sqrt(1/2)
1653 expr * result = mk_sqrt(rational(1, 2));
1654 return neg ? m_util.mk_uminus(result) : result;
1655 }
1656 if (k_prime == rational(1, 3) || k_prime == rational(2, 3)) {
1657 // sin(pi/3) == sin(2/3 pi) == Sqrt(3)/2
1658 // sin(4/3 pi) == sin(5/3 pi) == - Sqrt(3)/2
1659 expr * result = m_util.mk_div(mk_sqrt(rational(3)), m_util.mk_numeral(rational(2), false));
1660 return neg ? m_util.mk_uminus(result) : result;
1661 }
1662 if (k_prime == rational(1, 12) || k_prime == rational(11, 12)) {
1663 // sin(1/12 pi) == sin(11/12 pi) == [sqrt(6) - sqrt(2)]/4
1664 // sin(13/12 pi) == sin(23/12 pi) == -[sqrt(6) - sqrt(2)]/4
1665 expr * result = m_util.mk_div(m_util.mk_sub(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false));
1666 return neg ? m_util.mk_uminus(result) : result;
1667 }
1668 if (k_prime == rational(5, 12) || k_prime == rational(7, 12)) {
1669 // sin(5/12 pi) == sin(7/12 pi) == [sqrt(6) + sqrt(2)]/4
1670 // sin(17/12 pi) == sin(19/12 pi) == -[sqrt(6) + sqrt(2)]/4
1671 expr * result = m_util.mk_div(m_util.mk_add(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false));
1672 return neg ? m_util.mk_uminus(result) : result;
1673 }
1674 return nullptr;
1675 }
1676
mk_sin_core(expr * arg,expr_ref & result)1677 br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
1678 expr * m, *x;
1679 if (m_util.is_asin(arg, x)) {
1680 // sin(asin(x)) == x
1681 result = x;
1682 return BR_DONE;
1683 }
1684 if (m_util.is_acos(arg, x)) {
1685 // sin(acos(x)) == sqrt(1 - x^2)
1686 result = m_util.mk_power(m_util.mk_sub(m_util.mk_real(1), m_util.mk_mul(x,x)), m_util.mk_numeral(rational(1,2), false));
1687 return BR_REWRITE_FULL;
1688 }
1689 rational k;
1690 if (is_numeral(arg, k) && k.is_zero()) {
1691 // sin(0) == 0
1692 result = arg;
1693 return BR_DONE;
1694 }
1695
1696 if (is_pi_multiple(arg, k)) {
1697 result = mk_sin_value(k);
1698 if (result.get() != nullptr)
1699 return BR_REWRITE_FULL;
1700 }
1701
1702 if (is_pi_offset(arg, k, m)) {
1703 rational k_prime = mod(floor(k), rational(2)) + k - floor(k);
1704 SASSERT(k_prime >= rational(0) && k_prime < rational(2));
1705 if (k_prime.is_zero()) {
1706 // sin(x + 2*n*pi) == sin(x)
1707 result = m_util.mk_sin(m_util.mk_sub(arg, m));
1708 return BR_REWRITE2;
1709 }
1710 if (k_prime == rational(1, 2)) {
1711 // sin(x + pi/2 + 2*n*pi) == cos(x)
1712 result = m_util.mk_cos(m_util.mk_sub(arg, m));
1713 return BR_REWRITE2;
1714 }
1715 if (k_prime.is_one()) {
1716 // sin(x + pi + 2*n*pi) == -sin(x)
1717 result = m_util.mk_uminus(m_util.mk_sin(m_util.mk_sub(arg, m)));
1718 return BR_REWRITE3;
1719 }
1720 if (k_prime == rational(3, 2)) {
1721 // sin(x + 3/2*pi + 2*n*pi) == -cos(x)
1722 result = m_util.mk_uminus(m_util.mk_cos(m_util.mk_sub(arg, m)));
1723 return BR_REWRITE3;
1724 }
1725 }
1726
1727 if (is_2_pi_integer_offset(arg, m)) {
1728 // sin(x + 2*pi*to_real(a)) == sin(x)
1729 result = m_util.mk_sin(m_util.mk_sub(arg, m));
1730 return BR_REWRITE2;
1731 }
1732
1733 return BR_FAILED;
1734 }
1735
mk_cos_core(expr * arg,expr_ref & result)1736 br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) {
1737 expr* x;
1738 if (m_util.is_acos(arg, x)) {
1739 // cos(acos(x)) == x
1740 result = x;
1741 return BR_DONE;
1742 }
1743 if (m_util.is_asin(arg, x)) {
1744 // cos(asin(x)) == ...
1745 }
1746
1747 rational k;
1748 if (is_numeral(arg, k) && k.is_zero()) {
1749 // cos(0) == 1
1750 result = m_util.mk_numeral(rational(1), false);
1751 return BR_DONE;
1752 }
1753
1754 if (is_pi_multiple(arg, k)) {
1755 k = k + rational(1, 2);
1756 result = mk_sin_value(k);
1757 if (result.get() != nullptr)
1758 return BR_REWRITE_FULL;
1759 }
1760
1761 expr * m;
1762 if (is_pi_offset(arg, k, m)) {
1763 rational k_prime = mod(floor(k), rational(2)) + k - floor(k);
1764 SASSERT(k_prime >= rational(0) && k_prime < rational(2));
1765 if (k_prime.is_zero()) {
1766 // cos(x + 2*n*pi) == cos(x)
1767 result = m_util.mk_cos(m_util.mk_sub(arg, m));
1768 return BR_REWRITE2;
1769 }
1770 if (k_prime == rational(1, 2)) {
1771 // cos(x + pi/2 + 2*n*pi) == -sin(x)
1772 result = m_util.mk_uminus(m_util.mk_sin(m_util.mk_sub(arg, m)));
1773 return BR_REWRITE3;
1774 }
1775 if (k_prime.is_one()) {
1776 // cos(x + pi + 2*n*pi) == -cos(x)
1777 result = m_util.mk_uminus(m_util.mk_cos(m_util.mk_sub(arg, m)));
1778 return BR_REWRITE3;
1779 }
1780 if (k_prime == rational(3, 2)) {
1781 // cos(x + 3/2*pi + 2*n*pi) == sin(x)
1782 result = m_util.mk_sin(m_util.mk_sub(arg, m));
1783 return BR_REWRITE2;
1784 }
1785 }
1786
1787 if (is_2_pi_integer_offset(arg, m)) {
1788 // cos(x + 2*pi*to_real(a)) == cos(x)
1789 result = m_util.mk_cos(m_util.mk_sub(arg, m));
1790 return BR_REWRITE2;
1791 }
1792
1793 return BR_FAILED;
1794 }
1795
mk_tan_core(expr * arg,expr_ref & result)1796 br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) {
1797 expr* x;
1798 if (m_util.is_atan(arg, x)) {
1799 // tan(atan(x)) == x
1800 result = x;
1801 return BR_DONE;
1802 }
1803
1804 rational k;
1805 if (is_numeral(arg, k) && k.is_zero()) {
1806 // tan(0) == 0
1807 result = arg;
1808 return BR_DONE;
1809 }
1810
1811 if (is_pi_multiple(arg, k)) {
1812 expr_ref n(m()), d(m());
1813 n = mk_sin_value(k);
1814 if (n.get() == nullptr)
1815 goto end;
1816 if (is_zero(n)) {
1817 result = n;
1818 return BR_DONE;
1819 }
1820 k = k + rational(1, 2);
1821 d = mk_sin_value(k);
1822 SASSERT(d.get() != 0);
1823 if (is_zero(d)) {
1824 goto end;
1825 }
1826 result = m_util.mk_div(n, d);
1827 return BR_REWRITE_FULL;
1828 }
1829
1830 expr * m;
1831 if (is_pi_offset(arg, k, m)) {
1832 rational k_prime = k - floor(k);
1833 SASSERT(k_prime >= rational(0) && k_prime < rational(1));
1834 if (k_prime.is_zero()) {
1835 // tan(x + n*pi) == tan(x)
1836 result = m_util.mk_tan(m_util.mk_sub(arg, m));
1837 return BR_REWRITE2;
1838 }
1839 }
1840
1841 if (is_pi_integer_offset(arg, m)) {
1842 // tan(x + pi*to_real(a)) == tan(x)
1843 result = m_util.mk_tan(m_util.mk_sub(arg, m));
1844 return BR_REWRITE2;
1845 }
1846
1847 end:
1848 if (m_expand_tan) {
1849 result = m_util.mk_div(m_util.mk_sin(arg), m_util.mk_cos(arg));
1850 return BR_REWRITE2;
1851 }
1852 return BR_FAILED;
1853 }
1854
mk_asin_core(expr * arg,expr_ref & result)1855 br_status arith_rewriter::mk_asin_core(expr * arg, expr_ref & result) {
1856 // Remark: we assume that ForAll x : asin(-x) == asin(x).
1857 // Mathematica uses this as an axiom. Although asin is an underspecified function for x < -1 or x > 1.
1858 // Actually, in Mathematica, asin(x) is a total function that returns a complex number fo x < -1 or x > 1.
1859 rational k;
1860 if (is_numeral(arg, k)) {
1861 if (k.is_zero()) {
1862 result = arg;
1863 return BR_DONE;
1864 }
1865 if (k < rational(-1)) {
1866 // asin(-2) == -asin(2)
1867 // asin(-3) == -asin(3)
1868 k.neg();
1869 result = m_util.mk_uminus(m_util.mk_asin(m_util.mk_numeral(k, false)));
1870 return BR_REWRITE2;
1871 }
1872
1873 if (k > rational(1))
1874 return BR_FAILED;
1875
1876 bool neg = false;
1877 if (k.is_neg()) {
1878 neg = true;
1879 k.neg();
1880 }
1881
1882 if (k.is_one()) {
1883 // asin(1) == pi/2
1884 // asin(-1) == -pi/2
1885 result = m_util.mk_mul(m_util.mk_numeral(rational(neg ? -1 : 1, 2), false), m_util.mk_pi());
1886 return BR_REWRITE2;
1887 }
1888
1889 if (k == rational(1, 2)) {
1890 // asin(1/2) == pi/6
1891 // asin(-1/2) == -pi/6
1892 result = m_util.mk_mul(m_util.mk_numeral(rational(neg ? -1 : 1, 6), false), m_util.mk_pi());
1893 return BR_REWRITE2;
1894 }
1895 }
1896
1897 expr * t;
1898 if (m_util.is_times_minus_one(arg, t)) {
1899 // See comment above
1900 // asin(-x) ==> -asin(x)
1901 result = m_util.mk_uminus(m_util.mk_asin(t));
1902 return BR_REWRITE2;
1903 }
1904
1905 return BR_FAILED;
1906 }
1907
mk_acos_core(expr * arg,expr_ref & result)1908 br_status arith_rewriter::mk_acos_core(expr * arg, expr_ref & result) {
1909 rational k;
1910 if (is_numeral(arg, k)) {
1911 if (k.is_zero()) {
1912 // acos(0) = pi/2
1913 result = m_util.mk_mul(m_util.mk_numeral(rational(1, 2), false), m_util.mk_pi());
1914 return BR_REWRITE2;
1915 }
1916 if (k.is_one()) {
1917 // acos(1) = 0
1918 result = m_util.mk_numeral(rational(0), false);
1919 return BR_DONE;
1920 }
1921 if (k.is_minus_one()) {
1922 // acos(-1) = pi
1923 result = m_util.mk_pi();
1924 return BR_DONE;
1925 }
1926 if (k == rational(1, 2)) {
1927 // acos(1/2) = pi/3
1928 result = m_util.mk_mul(m_util.mk_numeral(rational(1, 3), false), m_util.mk_pi());
1929 return BR_REWRITE2;
1930 }
1931 if (k == rational(-1, 2)) {
1932 // acos(-1/2) = 2/3 pi
1933 result = m_util.mk_mul(m_util.mk_numeral(rational(2, 3), false), m_util.mk_pi());
1934 return BR_REWRITE2;
1935 }
1936 }
1937 return BR_FAILED;
1938 }
1939
mk_atan_core(expr * arg,expr_ref & result)1940 br_status arith_rewriter::mk_atan_core(expr * arg, expr_ref & result) {
1941 rational k;
1942 if (is_numeral(arg, k)) {
1943 if (k.is_zero()) {
1944 result = arg;
1945 return BR_DONE;
1946 }
1947
1948 if (k.is_one()) {
1949 // atan(1) == pi/4
1950 result = m_util.mk_mul(m_util.mk_numeral(rational(1, 4), false), m_util.mk_pi());
1951 return BR_REWRITE2;
1952 }
1953
1954 if (k.is_minus_one()) {
1955 // atan(-1) == -pi/4
1956 result = m_util.mk_mul(m_util.mk_numeral(rational(-1, 4), false), m_util.mk_pi());
1957 return BR_REWRITE2;
1958 }
1959
1960 if (k < rational(-1)) {
1961 // atan(-2) == -tan(2)
1962 // atan(-3) == -tan(3)
1963 k.neg();
1964 result = m_util.mk_uminus(m_util.mk_atan(m_util.mk_numeral(k, false)));
1965 return BR_REWRITE2;
1966 }
1967 return BR_FAILED;
1968 }
1969
1970 expr * t;
1971 if (m_util.is_times_minus_one(arg, t)) {
1972 // atan(-x) ==> -atan(x)
1973 result = m_util.mk_uminus(m_util.mk_atan(t));
1974 return BR_REWRITE2;
1975 }
1976 return BR_FAILED;
1977 }
1978
mk_sinh_core(expr * arg,expr_ref & result)1979 br_status arith_rewriter::mk_sinh_core(expr * arg, expr_ref & result) {
1980 expr* x;
1981 if (m_util.is_asinh(arg, x)) {
1982 // sinh(asinh(x)) == x
1983 result = x;
1984 return BR_DONE;
1985 }
1986 expr * t;
1987 if (m_util.is_times_minus_one(arg, t)) {
1988 // sinh(-t) == -sinh(t)
1989 result = m_util.mk_uminus(m_util.mk_sinh(t));
1990 return BR_REWRITE2;
1991 }
1992 return BR_FAILED;
1993 }
1994
mk_cosh_core(expr * arg,expr_ref & result)1995 br_status arith_rewriter::mk_cosh_core(expr * arg, expr_ref & result) {
1996 expr* t;
1997 if (m_util.is_acosh(arg, t)) {
1998 // cosh(acosh(t)) == t
1999 result = t;
2000 return BR_DONE;
2001 }
2002 if (m_util.is_times_minus_one(arg, t)) {
2003 // cosh(-t) == cosh
2004 result = m_util.mk_cosh(t);
2005 return BR_DONE;
2006 }
2007 return BR_FAILED;
2008 }
2009
mk_tanh_core(expr * arg,expr_ref & result)2010 br_status arith_rewriter::mk_tanh_core(expr * arg, expr_ref & result) {
2011 expr * t;
2012 if (m_util.is_atanh(arg, t)) {
2013 // tanh(atanh(t)) == t
2014 result = t;
2015 return BR_DONE;
2016 }
2017 if (m_util.is_times_minus_one(arg, t)) {
2018 // tanh(-t) == -tanh(t)
2019 result = m_util.mk_uminus(m_util.mk_tanh(t));
2020 return BR_REWRITE2;
2021 }
2022 return BR_FAILED;
2023 }
2024
2025 template class poly_rewriter<arith_rewriter_core>;
2026