1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 bv2real_rewriter.cpp
7
8 Abstract:
9
10 Basic rewriting rules for bv2real propagation.
11
12 Author:
13
14 Nikolaj (nbjorner) 2011-08-05
15
16 Notes:
17
18 --*/
19 #include "tactic/arith/bv2real_rewriter.h"
20 #include "ast/rewriter/rewriter_def.h"
21 #include "ast/ast_pp.h"
22 #include "ast/for_each_expr.h"
23
24
bv2real_util(ast_manager & m,rational const & default_root,rational const & default_divisor,unsigned max_num_bits)25 bv2real_util::bv2real_util(ast_manager& m, rational const& default_root, rational const& default_divisor, unsigned max_num_bits) :
26 m_manager(m),
27 m_arith(m),
28 m_bv(m),
29 m_decls(m),
30 m_pos_le(m),
31 m_pos_lt(m),
32 m_side_conditions(m),
33 m_default_root(default_root),
34 m_default_divisor(default_divisor),
35 m_max_divisor(rational(2)*default_divisor),
36 m_max_num_bits(max_num_bits) {
37 sort* real = m_arith.mk_real();
38 sort* domain[2] = { real, real };
39 m_pos_lt = m.mk_fresh_func_decl("<","",2,domain,m.mk_bool_sort());
40 m_pos_le = m.mk_fresh_func_decl("<=","",2,domain,m.mk_bool_sort());
41 m_decls.push_back(m_pos_lt);
42 m_decls.push_back(m_pos_le);
43 }
44
is_bv2real(func_decl * f) const45 bool bv2real_util::is_bv2real(func_decl* f) const {
46 return m_decl2sig.contains(f);
47 }
48
is_bv2real(func_decl * f,unsigned num_args,expr * const * args,expr * & m,expr * & n,rational & d,rational & r) const49 bool bv2real_util::is_bv2real(func_decl* f, unsigned num_args, expr* const* args,
50 expr*& m, expr*& n, rational& d, rational& r) const {
51 bvr_sig sig;
52 if (!m_decl2sig.find(f, sig)) {
53 return false;
54 }
55 SASSERT(num_args == 2);
56 m = args[0];
57 n = args[1];
58 d = sig.m_d;
59 r = sig.m_r;
60 SASSERT(sig.m_d.is_int() && sig.m_d.is_pos());
61 SASSERT(sig.m_r.is_int() && sig.m_r.is_pos());
62 SASSERT(m_bv.get_bv_size(m) == sig.m_msz);
63 SASSERT(m_bv.get_bv_size(n) == sig.m_nsz);
64 return true;
65 }
66
is_bv2real(expr * e,expr * & m,expr * & n,rational & d,rational & r) const67 bool bv2real_util::is_bv2real(expr* e, expr*& m, expr*& n, rational& d, rational& r) const {
68 if (!is_app(e)) return false;
69 func_decl* f = to_app(e)->get_decl();
70 return is_bv2real(f, to_app(e)->get_num_args(), to_app(e)->get_args(), m, n, d, r);
71 }
72
73 class bv2real_util::contains_bv2real_proc {
74 bv2real_util const& m_util;
75 public:
76 class found {};
contains_bv2real_proc(bv2real_util const & u)77 contains_bv2real_proc(bv2real_util const& u): m_util(u) {}
operator ()(app * a)78 void operator()(app* a) {
79 if (m_util.is_bv2real(a->get_decl())) {
80 throw found();
81 }
82 }
operator ()(var *)83 void operator()(var*) {}
operator ()(quantifier *)84 void operator()(quantifier*) {}
85 };
86
contains_bv2real(expr * e) const87 bool bv2real_util::contains_bv2real(expr* e) const {
88 contains_bv2real_proc p(*this);
89 try {
90 for_each_expr(p, e);
91 }
92 catch (const contains_bv2real_proc::found &) {
93 return true;
94 }
95 return false;
96 }
97
mk_bv2real(expr * _s,expr * _t,rational & d,rational & r,expr_ref & result)98 bool bv2real_util::mk_bv2real(expr* _s, expr* _t, rational& d, rational& r, expr_ref& result) {
99 expr_ref s(_s,m()), t(_t,m());
100 if (align_divisor(s, t, d)) {
101 result = mk_bv2real_c(s, t, d, r);
102 return true;
103 }
104 else {
105 return false;
106 }
107 }
108
mk_bv2real_c(expr * s,expr * t,rational const & d,rational const & r)109 expr* bv2real_util::mk_bv2real_c(expr* s, expr* t, rational const& d, rational const& r) {
110 bvr_sig sig;
111 sig.m_msz = m_bv.get_bv_size(s);
112 sig.m_nsz = m_bv.get_bv_size(t);
113 sig.m_d = d;
114 sig.m_r = r;
115 func_decl* f;
116 if (!m_sig2decl.find(sig, f)) {
117 sort* domain[2] = { s->get_sort(), t->get_sort() };
118 sort* real = m_arith.mk_real();
119 f = m_manager.mk_fresh_func_decl("bv2real", "", 2, domain, real);
120 m_decls.push_back(f);
121 m_sig2decl.insert(sig, f);
122 m_decl2sig.insert(f, sig);
123 }
124 return m_manager.mk_app(f, s, t);
125 }
126
mk_bv2real_reduced(expr * s,expr * t,rational const & d,rational const & r,expr_ref & result)127 void bv2real_util::mk_bv2real_reduced(expr* s, expr* t, rational const& d, rational const& r, expr_ref & result) {
128 expr_ref s1(m()), t1(m()), r1(m());
129 rational num;
130 mk_sbv2real(s, s1);
131 mk_sbv2real(t, t1);
132 mk_div(s1, d, s1);
133 mk_div(t1, d, t1);
134 r1 = a().mk_power(a().mk_numeral(r, false), a().mk_numeral(rational(1,2),false));
135 t1 = a().mk_mul(t1, r1);
136 result = a().mk_add(s1, t1);
137 }
138
mk_div(expr * e,rational const & d,expr_ref & result)139 void bv2real_util::mk_div(expr* e, rational const& d, expr_ref& result) {
140 result = a().mk_div(e, a().mk_numeral(rational(d), false));
141 }
142
mk_sbv2real(expr * e,expr_ref & result)143 void bv2real_util::mk_sbv2real(expr* e, expr_ref& result) {
144 rational r;
145 unsigned bv_size = m_bv.get_bv_size(e);
146 rational bsize = power(rational(2), bv_size);
147 expr_ref bvr(a().mk_to_real(m_bv.mk_bv2int(e)), m());
148 expr_ref c(m_bv.mk_sle(m_bv.mk_numeral(rational(0), bv_size), e), m());
149 result = m().mk_ite(c, bvr, a().mk_sub(bvr, a().mk_numeral(bsize, false)));
150 }
151
152
mk_bv_mul(rational const & n,expr * t)153 expr* bv2real_util::mk_bv_mul(rational const& n, expr* t) {
154 if (n.is_one()) return t;
155 expr_ref s(mk_sbv(n), m());
156 return mk_bv_mul(s, t);
157 }
158
align_divisors(expr_ref & s1,expr_ref & s2,expr_ref & t1,expr_ref & t2,rational & d1,rational & d2)159 void bv2real_util::align_divisors(expr_ref& s1, expr_ref& s2, expr_ref& t1, expr_ref& t2, rational& d1, rational& d2) {
160 if (d1 == d2) {
161 return;
162 }
163 // s/d1 ~ t/d2 <=> lcm*s/d1 ~ lcm*t/d2 <=> (lcm/d1)*s ~ (lcm/d2)*t
164 // s/d1 ~ t/d2 <=> s/gcd*d1' ~ t/gcd*d2' <=> d2'*s/lcm ~ d1'*t/lcm
165
166 rational g = gcd(d1,d2);
167 rational l = lcm(d1,d2);
168 rational d1g = d1/g;
169 rational d2g = d2/g;
170 s1 = mk_bv_mul(d2g, s1);
171 s2 = mk_bv_mul(d2g, s2);
172 t1 = mk_bv_mul(d1g, t1);
173 t2 = mk_bv_mul(d1g, t2);
174 d1 = l;
175 d2 = l;
176 }
177
mk_bv_mul(expr * s,expr * t)178 expr* bv2real_util::mk_bv_mul(expr* s, expr* t) {
179 SASSERT(m_bv.is_bv(s));
180 SASSERT(m_bv.is_bv(t));
181 if (is_zero(s)) {
182 return s;
183 }
184 if (is_zero(t)) {
185 return t;
186 }
187 expr_ref s1(s, m()), t1(t, m());
188 align_sizes(s1, t1);
189 unsigned n = m_bv.get_bv_size(t1);
190 unsigned max_bits = get_max_num_bits();
191 bool add_side_conds = 2*n > max_bits;
192 if (n >= max_bits) {
193 // nothing
194 }
195 else if (2*n > max_bits) {
196 s1 = mk_extend(max_bits-n, s1);
197 t1 = mk_extend(max_bits-n, t1);
198 }
199 else {
200 s1 = mk_extend(n, s1);
201 t1 = mk_extend(n, t1);
202 }
203 if (add_side_conds) {
204 add_side_condition(m_bv.mk_bvsmul_no_ovfl(s1, t1));
205 add_side_condition(m_bv.mk_bvsmul_no_udfl(s1, t1));
206 }
207 return m_bv.mk_bv_mul(s1, t1);
208 }
209
is_zero(expr * n)210 bool bv2real_util::is_zero(expr* n) {
211 rational r;
212 unsigned sz;
213 return m_bv.is_numeral(n, r, sz) && r.is_zero();
214 }
215
mk_bv_add(expr * s,expr * t)216 expr* bv2real_util::mk_bv_add(expr* s, expr* t) {
217 SASSERT(m_bv.is_bv(s));
218 SASSERT(m_bv.is_bv(t));
219
220 if (is_zero(s)) {
221 return t;
222 }
223 if (is_zero(t)) {
224 return s;
225 }
226 expr_ref s1(s, m()), t1(t, m());
227 align_sizes(s1, t1);
228 s1 = mk_extend(1, s1);
229 t1 = mk_extend(1, t1);
230 return m_bv.mk_bv_add(s1, t1);
231 }
232
align_sizes(expr_ref & s,expr_ref & t)233 void bv2real_util::align_sizes(expr_ref& s, expr_ref& t) {
234 unsigned sz1 = m_bv.get_bv_size(s);
235 unsigned sz2 = m_bv.get_bv_size(t);
236 if (sz1 > sz2) {
237 t = mk_extend(sz1-sz2, t);
238 }
239 else if (sz1 < sz2) {
240 s = mk_extend(sz2-sz1, s);
241 }
242 }
243
mk_sbv(rational const & n)244 expr* bv2real_util::mk_sbv(rational const& n) {
245 SASSERT(n.is_int());
246 if (n.is_neg()) {
247 rational m = abs(n);
248 unsigned nb = m.get_num_bits();
249 return m_bv.mk_bv_neg(m_bv.mk_numeral(m, nb+1));
250 }
251 else {
252 unsigned nb = n.get_num_bits();
253 return m_bv.mk_numeral(n, nb+1);
254 }
255 }
256
mk_bv_sub(expr * s,expr * t)257 expr* bv2real_util::mk_bv_sub(expr* s, expr* t) {
258 expr_ref s1(s, m()), t1(t, m());
259 align_sizes(s1, t1);
260 s1 = mk_extend(1, s1);
261 t1 = mk_extend(1, t1);
262 return m_bv.mk_bv_sub(s1, t1);
263 }
264
mk_extend(unsigned sz,expr * b)265 expr* bv2real_util::mk_extend(unsigned sz, expr* b) {
266 if (sz == 0) {
267 return b;
268 }
269 rational r;
270 unsigned bv_sz;
271 if (m_bv.is_numeral(b, r, bv_sz) &&
272 power(rational(2),bv_sz-1) > r) {
273 return m_bv.mk_numeral(r, bv_sz + sz);
274 }
275 return m_bv.mk_sign_extend(sz, b);
276 }
277
278
is_bv2real(expr * n,expr_ref & s,expr_ref & t,rational & d,rational & r)279 bool bv2real_util::is_bv2real(expr* n, expr_ref& s, expr_ref& t, rational& d, rational& r) {
280 expr* _s, *_t;
281 if (is_bv2real(n, _s, _t, d, r)) {
282 s = _s;
283 t = _t;
284 return true;
285 }
286 rational k;
287 bool is_int;
288 if (m_arith.is_numeral(n, k, is_int) && !is_int) {
289 d = denominator(k);
290 r = default_root();
291 s = mk_sbv(numerator(k));
292 t = mk_sbv(rational(0));
293 return true;
294 }
295 return false;
296 }
297
align_divisor(expr_ref & s,expr_ref & t,rational & d)298 bool bv2real_util::align_divisor(expr_ref& s, expr_ref& t, rational& d) {
299 if (d > max_divisor()) {
300 //
301 // if divisor is over threshold, then divide s and t
302 // add side condition that s, t are divisible.
303 //
304 rational overflow = d / max_divisor();
305 if (!overflow.is_int()) return false;
306 if (!mk_is_divisible_by(s, overflow)) return false;
307 if (!mk_is_divisible_by(t, overflow)) return false;
308 d = max_divisor();
309 }
310 return true;
311 }
312
mk_is_divisible_by(expr_ref & s,rational const & _overflow)313 bool bv2real_util::mk_is_divisible_by(expr_ref& s, rational const& _overflow) {
314 rational overflow(_overflow);
315 SASSERT(overflow.is_int());
316 SASSERT(overflow.is_pos());
317 SASSERT(!overflow.is_one());
318 TRACE("bv2real_rewriter",
319 tout << mk_pp(s, m()) << " " << overflow << "\n";);
320 unsigned power2 = 0;
321 while ((overflow % rational(2)) == rational(0)) {
322 power2++;
323 overflow = div(overflow, rational(2));
324 }
325
326 if (power2 > 0) {
327 unsigned sz = m_bv.get_bv_size(s);
328 if (sz <= power2) {
329 add_side_condition(m().mk_eq(s, m_bv.mk_numeral(rational(0), sz)));
330 s = m_bv.mk_numeral(rational(0), 1);
331 }
332 else {
333 expr* s1 = m_bv.mk_extract(power2-1, 0, s);
334 add_side_condition(m().mk_eq(s1, m_bv.mk_numeral(rational(0), power2)));
335 s = m_bv.mk_extract(sz-1, power2, s);
336 }
337 }
338
339 TRACE("bv2real_rewriter",
340 tout << mk_pp(s, m()) << " " << overflow << "\n";);
341
342 return overflow.is_one();
343 }
344
345
346
347 // ---------------------------------------------------------------------
348 // bv2real_rewriter
349
bv2real_rewriter(ast_manager & m,bv2real_util & util)350 bv2real_rewriter::bv2real_rewriter(ast_manager& m, bv2real_util& util):
351 m_manager(m),
352 m_util(util),
353 m_bv(m),
354 m_arith(m)
355 {}
356
357
mk_app_core(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)358 br_status bv2real_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
359 TRACE("bv2real_rewriter",
360 tout << mk_pp(f, m()) << " ";
361 for (unsigned i = 0; i < num_args; ++i) {
362 tout << mk_pp(args[i], m()) << " ";
363 }
364 tout << "\n";);
365 if(f->get_family_id() == m_arith.get_family_id()) {
366 switch (f->get_decl_kind()) {
367 case OP_NUM: return BR_FAILED;
368 case OP_LE: SASSERT(num_args == 2); return mk_le(args[0], args[1], result);
369 case OP_GE: SASSERT(num_args == 2); return mk_ge(args[0], args[1], result);
370 case OP_LT: SASSERT(num_args == 2); return mk_lt(args[0], args[1], result);
371 case OP_GT: SASSERT(num_args == 2); return mk_gt(args[0], args[1], result);
372 case OP_ADD: return mk_add(num_args, args, result);
373 case OP_MUL: return mk_mul(num_args, args, result);
374 case OP_SUB: return mk_sub(num_args, args, result);
375 case OP_DIV: SASSERT(num_args == 2); return mk_div(args[0], args[1], result);
376 case OP_IDIV: return BR_FAILED;
377 case OP_MOD: return BR_FAILED;
378 case OP_REM: return BR_FAILED;
379 case OP_UMINUS: SASSERT(num_args == 1); return mk_uminus(args[0], result);
380 case OP_TO_REAL: return BR_FAILED; // TBD
381 case OP_TO_INT: return BR_FAILED; // TBD
382 case OP_IS_INT: return BR_FAILED; // TBD
383 default: return BR_FAILED;
384 }
385 }
386 if (f->get_family_id() == m().get_basic_family_id()) {
387 switch (f->get_decl_kind()) {
388 case OP_EQ: SASSERT(num_args == 2); return mk_eq(args[0], args[1], result);
389 case OP_ITE: SASSERT(num_args == 3); return mk_ite(args[0], args[1], args[2], result);
390 default: return BR_FAILED;
391 }
392 }
393 if (u().is_pos_ltf(f)) {
394 SASSERT(num_args == 2);
395 return mk_lt_pos(args[0], args[1], result);
396 }
397 if (u().is_pos_lef(f)) {
398 SASSERT(num_args == 2);
399 return mk_le_pos(args[0], args[1], result);
400 }
401
402 return BR_FAILED;
403 }
404
mk_le(expr * s,expr * t,bool is_pos,bool is_neg,expr_ref & result)405 bool bv2real_rewriter::mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_ref& result) {
406 expr_ref s1(m()), s2(m()), t1(m()), t2(m());
407 rational d1, d2, r1, r2;
408 SASSERT(is_pos || is_neg);
409 if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) &&
410 r1 == r2 && r1 == rational(2)) {
411 //
412 // (s1 + s2*sqrt(2))/d1 <= (t1 + t2*sqrt(2))/d2
413 // <=>
414 //
415 // let s1 = s1*d2-t1*d1, t2 = s2*d2-t2*d1
416 //
417 //
418 // s1 + s2*sqrt(2) <= 0
419 // <=
420 // s1 + s2*approx(sign(s2),sqrt(2)) <= 0
421 // or (s1 = 0 & s2 = 0)
422 //
423 // If s2 is negative use an under-approximation for sqrt(r).
424 // If s2 is positive use an over-approximation for sqrt(r).
425 // e.g., r = 2, then 5/4 and 3/2 are under/over approximations.
426 // Then s1 + s2*approx(sign(s2), r) <= 0 => s1 + s2*sqrt(r) <= 0
427
428
429 u().align_divisors(s1, s2, t1, t2, d1, d2);
430 s1 = u().mk_bv_sub(s1, t1);
431 s2 = u().mk_bv_sub(s2, t2);
432 unsigned s2_size = m_bv.get_bv_size(s2);
433 expr_ref le_proxy(m().mk_fresh_const("le_proxy",m().mk_bool_sort()), m());
434 u().add_aux_decl(to_app(le_proxy)->get_decl());
435 expr_ref gt_proxy(m().mk_not(le_proxy), m());
436 expr_ref s2_is_nonpos(m_bv.mk_sle(s2, m_bv.mk_numeral(rational(0), s2_size)), m());
437
438 expr_ref under(u().mk_bv_add(u().mk_bv_mul(rational(4), s1), u().mk_bv_mul(rational(5), s2)), m());
439 expr_ref z1(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(under)), m());
440 expr_ref le_under(m_bv.mk_sle(under, z1), m());
441 expr_ref over(u().mk_bv_add(u().mk_bv_mul(rational(2), s1), u().mk_bv_mul(rational(3), s2)), m());
442 expr_ref z2(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(over)), m());
443 expr_ref le_over(m_bv.mk_sle(over, z2), m());
444
445 // predicate may occur in positive polarity.
446 if (is_pos) {
447 // s1 + s2*sqrt(2) <= 0 <== s2 <= 0 & s1 + s2*(5/4) <= 0; 4*s1 + 5*s2 <= 0
448 expr* e1 = m().mk_implies(m().mk_and(le_proxy, s2_is_nonpos), le_under);
449 // s1 + s2*sqrt(2) <= 0 <== s2 > 0 & s1 + s2*(3/2); 0 <=> 2*s1 + 3*s2 <= 0
450 expr* e2 = m().mk_implies(m().mk_and(le_proxy, m().mk_not(s2_is_nonpos)), le_over);
451 u().add_side_condition(e1);
452 u().add_side_condition(e2);
453 }
454 // predicate may occur in negative polarity.
455 if (is_neg) {
456 // s1 + s2*sqrt(2) > 0 <== s2 > 0 & s1 + s2*(5/4) > 0; 4*s1 + 5*s2 > 0
457 expr* e3 = m().mk_implies(m().mk_and(gt_proxy, m().mk_not(s2_is_nonpos)), m().mk_not(le_under));
458 // s1 + s2*sqrt(2) > 0 <== s2 <= 0 & s1 + s2*(3/2) > 0 <=> 2*s1 + 3*s2 > 0
459 expr* e4 = m().mk_implies(m().mk_and(gt_proxy, s2_is_nonpos), m().mk_not(le_over));
460 u().add_side_condition(e3);
461 u().add_side_condition(e4);
462 }
463
464 TRACE("bv2real_rewriter", tout << "mk_le\n";);
465
466 if (is_pos) {
467 result = le_proxy;
468 }
469 else {
470 result = gt_proxy;
471 }
472 return true;
473 }
474 return false;
475 }
476
mk_le_pos(expr * s,expr * t,expr_ref & result)477 br_status bv2real_rewriter::mk_le_pos(expr * s, expr * t, expr_ref & result) {
478 if (mk_le(s, t, true, false, result)) {
479 return BR_DONE;
480 }
481 return BR_FAILED;
482 }
483
mk_lt_pos(expr * s,expr * t,expr_ref & result)484 br_status bv2real_rewriter::mk_lt_pos(expr * s, expr * t, expr_ref & result) {
485 if (mk_le(t, s, false, true, result)) {
486 return BR_DONE;
487 }
488 return BR_FAILED;
489 }
490
491
mk_le(expr * s,expr * t,expr_ref & result)492 br_status bv2real_rewriter::mk_le(expr * s, expr * t, expr_ref & result) {
493 expr_ref s1(m()), s2(m()), t1(m()), t2(m());
494 rational d1, d2, r1, r2;
495
496 if (mk_le(s, t, true, true, result)) {
497 return BR_DONE;
498 }
499
500 if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
501 //
502 // somewhat expensive approach without having
503 // polarity information for sound approximation.
504 //
505
506 // Convert to:
507 // t1 + t2*sqrt(r) >= 0
508 // then to:
509 //
510 // (t1 >= 0 && t2 <= 0 => t1^2 >= t2^2*r)
511 // (t1 <= 0 && t2 >= 0 => t1^2 <= t2^2*r)
512 // (t1 >= 0 || t2 >= 0)
513 //
514 // A cheaper approach is to approximate > under the assumption
515 // that > occurs in positive polarity.
516 // then if t2 is negative use an over-approximation for sqrt(r)
517 // if t2 is positive use an under-approximation for sqrt(r).
518 // e.g., r = 2, then 5/4 and 3/2 are under/over approximations.
519 // Then t1 + t2*approx(sign(t2), r) > 0 => t1 + t2*sqrt(r) > 0
520 //
521 u().align_divisors(s1, s2, t1, t2, d1, d2);
522 t1 = u().mk_bv_sub(t1, s1);
523 t2 = u().mk_bv_sub(t2, s2);
524 expr_ref z1(m()), z2(m());
525 z1 = m_bv.mk_numeral(rational(0), m_bv.get_bv_size(t1));
526 z2 = m_bv.mk_numeral(rational(0), m_bv.get_bv_size(t2));
527
528 expr* gz1 = m_bv.mk_sle(z1, t1);
529 expr* lz1 = m_bv.mk_sle(t1, z1);
530 expr* gz2 = m_bv.mk_sle(z2, t2);
531 expr* lz2 = m_bv.mk_sle(t2, z2);
532 expr_ref t12(u().mk_bv_mul(t1, t1), m());
533 expr_ref t22(u().mk_bv_mul(r1, u().mk_bv_mul(t2, t2)), m());
534 u().align_sizes(t12, t22);
535 expr* ge = m_bv.mk_sle(t22, t12);
536 expr* le = m_bv.mk_sle(t12, t22);
537 expr* e1 = m().mk_or(gz1, gz2);
538 expr* e2 = m().mk_or(m().mk_not(gz1), m().mk_not(lz2), ge);
539 expr* e3 = m().mk_or(m().mk_not(gz2), m().mk_not(lz1), le);
540 result = m().mk_and(e1, e2, e3);
541 TRACE("bv2real_rewriter", tout << "\n";);
542 return BR_DONE;
543 }
544 return BR_FAILED;
545 }
546
mk_lt(expr * arg1,expr * arg2,expr_ref & result)547 br_status bv2real_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
548 result = m().mk_not(m_arith.mk_le(arg2, arg1));
549 return BR_REWRITE2;
550 }
551
mk_ge(expr * arg1,expr * arg2,expr_ref & result)552 br_status bv2real_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
553 return mk_le(arg2, arg1, result);
554 }
555
mk_gt(expr * arg1,expr * arg2,expr_ref & result)556 br_status bv2real_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
557 result = m().mk_not(m_arith.mk_le(arg1, arg2));
558 return BR_REWRITE2;
559 }
560
mk_ite(expr * c,expr * s,expr * t,expr_ref & result)561 br_status bv2real_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result) {
562 expr_ref s1(m()), s2(m()), t1(m()), t2(m());
563 rational d1, d2, r1, r2;
564 if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
565 u().align_divisors(s1, s2, t1, t2, d1, d2);
566 u().align_sizes(s1, t1);
567 u().align_sizes(s2, t2);
568 if (u().mk_bv2real(m().mk_ite(c, s1, t1), m().mk_ite(c, s2, t2), d1, r1, result)) {
569 return BR_DONE;
570 }
571 }
572 return BR_FAILED;
573 }
574
mk_eq(expr * s,expr * t,expr_ref & result)575 br_status bv2real_rewriter::mk_eq(expr * s, expr * t, expr_ref & result) {
576 expr_ref s1(m()), s2(m()), t1(m()), t2(m());
577 rational d1, d2, r1, r2;
578 if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
579 u().align_divisors(s1, s2, t1, t2, d1, d2);
580 u().align_sizes(s1, t1);
581 u().align_sizes(s2, t2);
582 result = m().mk_and(m().mk_eq(s1, t1), m().mk_eq(s2, t2));
583 return BR_DONE;
584 }
585 return BR_FAILED;
586 }
587
mk_uminus(expr * s,expr_ref & result)588 br_status bv2real_rewriter::mk_uminus(expr * s, expr_ref & result) {
589 expr_ref s1(m()), s2(m());
590 rational d1, r1;
591 if (u().is_bv2real(s, s1, s2, d1, r1)) {
592 s1 = u().mk_extend(1, s1);
593 s2 = u().mk_extend(1, s2);
594 if (u().mk_bv2real(m_bv.mk_bv_neg(s1), m_bv.mk_bv_neg(s2), d1, r1, result)) {
595 return BR_DONE;
596 }
597 }
598 return BR_FAILED;
599 }
600
mk_add(unsigned num_args,expr * const * args,expr_ref & result)601 br_status bv2real_rewriter::mk_add(unsigned num_args, expr * const* args, expr_ref& result) {
602 br_status r = BR_DONE;
603 SASSERT(num_args > 0);
604 result = args[0];
605 for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
606 r = mk_add(result, args[i], result);
607 }
608 return r;
609 }
610
mk_add(expr * s,expr * t,expr_ref & result)611 br_status bv2real_rewriter::mk_add(expr* s, expr* t, expr_ref& result) {
612 expr_ref s1(m()), s2(m()), t1(m()), t2(m());
613 rational d1, d2, r1, r2;
614 if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
615 u().align_divisors(s1, s2, t1, t2, d1, d2);
616 if (u().mk_bv2real(u().mk_bv_add(s1, t1), u().mk_bv_add(t2, s2), d1, r1, result)) {
617 return BR_DONE;
618 }
619 }
620 return BR_FAILED;
621 }
622
mk_mul(unsigned num_args,expr * const * args,expr_ref & result)623 br_status bv2real_rewriter::mk_mul(unsigned num_args, expr * const* args, expr_ref& result) {
624 br_status r = BR_DONE;
625 SASSERT(num_args > 0);
626 result = args[0];
627 for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
628 r = mk_mul(result, args[i], result);
629 }
630 return r;
631 }
632
mk_div(expr * s,expr * t,expr_ref & result)633 br_status bv2real_rewriter::mk_div(expr* s, expr* t, expr_ref& result) {
634 return BR_FAILED;
635 }
636
mk_mul(expr * s,expr * t,expr_ref & result)637 br_status bv2real_rewriter::mk_mul(expr* s, expr* t, expr_ref& result) {
638 // TBD: optimize
639 expr_ref s1(m()), t1(m()), s2(m()), t2(m());
640 rational d1, d2, r1, r2;
641
642 if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
643 // s1*t1 + r1*(s2*t2) + (s1*t2 + s2*t2)*r1
644 expr_ref u1(m()), u2(m());
645 u1 = u().mk_bv_add(u().mk_bv_mul(s1, t1), u().mk_bv_mul(r1, u().mk_bv_mul(t2, s2)));
646 u2 = u().mk_bv_add(u().mk_bv_mul(s1, t2), u().mk_bv_mul(s2, t1));
647 rational tmp = d1*d2;
648 if (u().mk_bv2real(u1, u2, tmp, r1, result)) {
649 return BR_DONE;
650 }
651 }
652 return BR_FAILED;
653 }
654
mk_sub(unsigned num_args,expr * const * args,expr_ref & result)655 br_status bv2real_rewriter::mk_sub(unsigned num_args, expr * const* args, expr_ref& result) {
656 br_status r = BR_DONE;
657 SASSERT(num_args > 0);
658 result = args[0];
659 for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
660 r = mk_sub(result, args[i], result);
661 }
662 return r;
663 }
664
665
mk_sub(expr * s,expr * t,expr_ref & result)666 br_status bv2real_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) {
667 expr_ref s1(m()), s2(m()), t1(m()), t2(m());
668 rational d1, d2, r1, r2;
669 if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
670 u().align_divisors(s1, s2, t1, t2, d1, d2);
671 if (u().mk_bv2real(u().mk_bv_sub(s1, t1), u().mk_bv_sub(s2, t2), d1, r1, result)) {
672 return BR_DONE;
673 }
674 }
675 return BR_FAILED;
676 }
677
678
679
680
681 template class rewriter_tpl<bv2real_rewriter_cfg>;
682
683
mk_app_core(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)684 br_status bv2real_elim_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
685 expr* m, *n;
686 rational d, r;
687 if (m_util.is_bv2real(f, num_args, args, m, n, d, r)) {
688 m_util.mk_bv2real_reduced(m, n, d, r, result);
689 return BR_REWRITE_FULL;
690 }
691 return BR_FAILED;
692 }
693
694 template class rewriter_tpl<bv2real_elim_rewriter_cfg>;
695
696