1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 fpa_rewriter.cpp
7
8 Abstract:
9
10 Basic rewriting rules for floating point numbers.
11
12 Author:
13
14 Leonardo (leonardo) 2012-02-02
15
16 Notes:
17
18 --*/
19 #include "ast/rewriter/fpa_rewriter.h"
20 #include "params/fpa_rewriter_params.hpp"
21 #include "ast/ast_smt2_pp.h"
22
fpa_rewriter(ast_manager & m,params_ref const & p)23 fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) :
24 m_util(m),
25 m_fm(m_util.fm()),
26 m_hi_fp_unspecified(false) {
27 updt_params(p);
28 }
29
~fpa_rewriter()30 fpa_rewriter::~fpa_rewriter() {
31 }
32
updt_params(params_ref const & _p)33 void fpa_rewriter::updt_params(params_ref const & _p) {
34 fpa_rewriter_params p(_p);
35 m_hi_fp_unspecified = p.hi_fp_unspecified();
36 }
37
get_param_descrs(param_descrs & r)38 void fpa_rewriter::get_param_descrs(param_descrs & r) {
39 }
40
mk_app_core(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)41 br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
42 br_status st = BR_FAILED;
43 SASSERT(f->get_family_id() == get_fid());
44 fpa_op_kind k = (fpa_op_kind)f->get_decl_kind();
45 switch (k) {
46 case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
47 case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
48 case OP_FPA_RM_TOWARD_POSITIVE:
49 case OP_FPA_RM_TOWARD_NEGATIVE:
50 case OP_FPA_RM_TOWARD_ZERO:
51 SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
52
53 case OP_FPA_PLUS_INF:
54 case OP_FPA_MINUS_INF:
55 case OP_FPA_NAN:
56 case OP_FPA_PLUS_ZERO:
57 case OP_FPA_MINUS_ZERO:
58 SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
59
60 case OP_FPA_NUM:
61 SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
62
63 case OP_FPA_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break;
64 case OP_FPA_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break;
65 case OP_FPA_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break;
66 case OP_FPA_MUL: SASSERT(num_args == 3); st = mk_mul(args[0], args[1], args[2], result); break;
67 case OP_FPA_DIV: SASSERT(num_args == 3); st = mk_div(args[0], args[1], args[2], result); break;
68 case OP_FPA_REM: SASSERT(num_args == 2); st = mk_rem(args[0], args[1], result); break;
69 case OP_FPA_ABS: SASSERT(num_args == 1); st = mk_abs(args[0], result); break;
70 case OP_FPA_MIN: SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break;
71 case OP_FPA_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
72 case OP_FPA_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break;
73 case OP_FPA_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
74 case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break;
75
76 case OP_FPA_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break;
77 case OP_FPA_LT: SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break;
78 case OP_FPA_GT: SASSERT(num_args == 2); st = mk_gt(args[0], args[1], result); break;
79 case OP_FPA_LE: SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break;
80 case OP_FPA_GE: SASSERT(num_args == 2); st = mk_ge(args[0], args[1], result); break;
81 case OP_FPA_IS_ZERO: SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break;
82 case OP_FPA_IS_NAN: SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break;
83 case OP_FPA_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
84 case OP_FPA_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
85 case OP_FPA_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
86 case OP_FPA_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break;
87 case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break;
88
89 case OP_FPA_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
90 case OP_FPA_TO_FP: st = mk_to_fp(f, num_args, args, result); break;
91 case OP_FPA_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(f, args[0], args[1], result); break;
92 case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break;
93 case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break;
94 case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break;
95 case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
96
97 case OP_FPA_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
98 case OP_FPA_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;
99
100 default:
101 NOT_IMPLEMENTED_YET();
102 }
103 return st;
104 }
105
mk_to_fp(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)106 br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
107 SASSERT(f->get_num_parameters() == 2);
108 SASSERT(f->get_parameter(0).is_int());
109 SASSERT(f->get_parameter(1).is_int());
110 scoped_mpf v(m_fm);
111 mpf_rounding_mode rmv;
112 rational r1, r2, r3;
113 unsigned bvs1, bvs2, bvs3;
114 unsigned ebits = f->get_parameter(0).get_int();
115 unsigned sbits = f->get_parameter(1).get_int();
116
117 if (num_args == 1) {
118 if (m_util.bu().is_numeral(args[0], r1, bvs1)) {
119 // BV -> float
120 SASSERT(bvs1 == sbits + ebits);
121 unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
122 scoped_mpz sig(mpzm), exp(mpzm);
123
124 const mpz & sm1 = m_fm.m_powers2(sbits - 1);
125 const mpz & em1 = m_fm.m_powers2(ebits);
126
127 const mpq & q = r1.to_mpq();
128 SASSERT(mpzm.is_one(q.denominator()));
129 scoped_mpz z(mpzm);
130 z = q.numerator();
131
132 mpzm.rem(z, sm1, sig);
133 mpzm.div(z, sm1, z);
134
135 mpzm.rem(z, em1, exp);
136 mpzm.div(z, em1, z);
137
138 SASSERT(mpzm.is_int64(exp));
139 mpf_exp_t mpf_exp = mpzm.get_int64(exp);
140 mpf_exp = m_fm.unbias_exp(ebits, mpf_exp);
141
142 m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), mpf_exp, sig);
143 TRACE("fp_rewriter",
144 tout << "sgn: " << !mpzm.is_zero(z) << std::endl;
145 tout << "sig: " << mpzm.to_string(sig) << std::endl;
146 tout << "exp: " << mpf_exp << std::endl;
147 tout << "v: " << m_fm.to_string(v) << std::endl;);
148
149 result = m_util.mk_value(v);
150 return BR_DONE;
151 }
152 }
153 else if (num_args == 2) {
154 if (!m_util.is_rm_numeral(args[0], rmv))
155 return BR_FAILED;
156
157 if (m_util.au().is_numeral(args[1], r1)) {
158 // rm + real -> float
159 TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;);
160 scoped_mpf v(m_fm);
161 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq());
162 result = m_util.mk_value(v);
163 // TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
164 return BR_DONE;
165 }
166 else if (m_util.is_numeral(args[1], v)) {
167 // rm + float -> float
168 TRACE("fp_rewriter", tout << "v: " << m_fm.to_string(v) << std::endl; );
169 scoped_mpf vf(m_fm);
170 m_fm.set(vf, ebits, sbits, rmv, v);
171 result = m_util.mk_value(vf);
172 // TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
173 return BR_DONE;
174 }
175 else if (m_util.bu().is_numeral(args[1], r1, bvs1)) {
176 // rm + signed bv -> float
177 TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;);
178 r1 = m_util.bu().norm(r1, bvs1, true);
179 TRACE("fp_rewriter", tout << "r1 norm: " << r1 << std::endl;);
180 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq());
181 result = m_util.mk_value(v);
182 return BR_DONE;
183 }
184 }
185 else if (num_args == 3) {
186 if (m_util.is_rm_numeral(args[0], rmv) &&
187 m_util.au().is_real(args[1]) &&
188 m_util.au().is_int(args[2])) {
189 // rm + real + int -> float
190 if (!m_util.is_rm_numeral(args[0], rmv) ||
191 !m_util.au().is_numeral(args[1], r1) ||
192 !m_util.au().is_numeral(args[2], r2))
193 return BR_FAILED;
194
195 TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
196 m_fm.set(v, ebits, sbits, rmv, r2.to_mpq().numerator(), r1.to_mpq());
197 result = m_util.mk_value(v);
198 return BR_DONE;
199 }
200 else if (m_util.is_rm_numeral(args[0], rmv) &&
201 m_util.au().is_int(args[1]) &&
202 m_util.au().is_real(args[2])) {
203 // rm + int + real -> float
204 if (!m_util.is_rm_numeral(args[0], rmv) ||
205 !m_util.au().is_numeral(args[1], r1) ||
206 !m_util.au().is_numeral(args[2], r2))
207 return BR_FAILED;
208
209 TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
210 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq().numerator(), r2.to_mpq());
211 result = m_util.mk_value(v);
212 return BR_DONE;
213 }
214 else if (m_util.bu().is_numeral(args[0], r1, bvs1) &&
215 m_util.bu().is_numeral(args[1], r2, bvs2) &&
216 m_util.bu().is_numeral(args[2], r3, bvs3)) {
217 // 3 BV -> float
218 SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator()));
219 SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator()));
220 SASSERT(m_fm.mpz_manager().is_int64(r3.to_mpq().numerator()));
221 mpf_exp_t biased_exp = m_fm.mpz_manager().get_int64(r2.to_mpq().numerator());
222 m_fm.set(v, bvs2, bvs3 + 1,
223 r1.is_one(),
224 m_fm.unbias_exp(bvs2, biased_exp),
225 r3.to_mpq().numerator());
226 TRACE("fp_rewriter", tout << "v = " << m_fm.to_string(v) << std::endl;);
227 result = m_util.mk_value(v);
228 return BR_DONE;
229 }
230 }
231
232 return BR_FAILED;
233 }
234
mk_to_fp_unsigned(func_decl * f,expr * arg1,expr * arg2,expr_ref & result)235 br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
236 SASSERT(f->get_num_parameters() == 2);
237 SASSERT(f->get_parameter(0).is_int());
238 SASSERT(f->get_parameter(1).is_int());
239 unsigned ebits = f->get_parameter(0).get_int();
240 unsigned sbits = f->get_parameter(1).get_int();
241 mpf_rounding_mode rmv;
242 rational r;
243 unsigned bvs;
244
245 if (m_util.is_rm_numeral(arg1, rmv) &&
246 m_util.bu().is_numeral(arg2, r, bvs)) {
247 scoped_mpf v(m_fm);
248 m_fm.set(v, ebits, sbits, rmv, r.to_mpq());
249 result = m_util.mk_value(v);
250 return BR_DONE;
251 }
252
253 return BR_FAILED;
254 }
255
mk_add(expr * arg1,expr * arg2,expr * arg3,expr_ref & result)256 br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
257 mpf_rounding_mode rm;
258 if (m_util.is_rm_numeral(arg1, rm)) {
259 scoped_mpf v2(m_fm), v3(m_fm);
260 if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) {
261 scoped_mpf t(m_fm);
262 m_fm.add(rm, v2, v3, t);
263 result = m_util.mk_value(t);
264 return BR_DONE;
265 }
266 }
267
268 return BR_FAILED;
269 }
270
mk_sub(expr * arg1,expr * arg2,expr * arg3,expr_ref & result)271 br_status fpa_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
272 // a - b = a + (-b)
273 result = m_util.mk_add(arg1, arg2, m_util.mk_neg(arg3));
274 return BR_REWRITE2;
275 }
276
mk_mul(expr * arg1,expr * arg2,expr * arg3,expr_ref & result)277 br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
278 mpf_rounding_mode rm;
279
280 if (m_util.is_rm_numeral(arg1, rm)) {
281 scoped_mpf v2(m_fm), v3(m_fm);
282 if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) {
283 scoped_mpf t(m_fm);
284 m_fm.mul(rm, v2, v3, t);
285 result = m_util.mk_value(t);
286 return BR_DONE;
287 }
288 }
289
290 return BR_FAILED;
291 }
292
mk_div(expr * arg1,expr * arg2,expr * arg3,expr_ref & result)293 br_status fpa_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
294 mpf_rounding_mode rm;
295
296 if (m_util.is_rm_numeral(arg1, rm)) {
297 scoped_mpf v2(m_fm), v3(m_fm);
298 if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) {
299 scoped_mpf t(m_fm);
300 m_fm.div(rm, v2, v3, t);
301 result = m_util.mk_value(t);
302 return BR_DONE;
303 }
304 }
305 return BR_FAILED;
306 }
307
mk_neg(expr * arg1,expr_ref & result)308 br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) {
309 if (m_util.is_nan(arg1)) {
310 // -nan --> nan
311 result = arg1;
312 return BR_DONE;
313 }
314 if (m_util.is_pinf(arg1)) {
315 // - +oo --> -oo
316 result = m_util.mk_ninf(m().get_sort(arg1));
317 return BR_DONE;
318 }
319 if (m_util.is_ninf(arg1)) {
320 // - -oo -> +oo
321 result = m_util.mk_pinf(m().get_sort(arg1));
322 return BR_DONE;
323 }
324 if (m_util.is_neg(arg1)) {
325 // - - a --> a
326 result = to_app(arg1)->get_arg(0);
327 return BR_DONE;
328 }
329
330 scoped_mpf v1(m_fm);
331 if (m_util.is_numeral(arg1, v1)) {
332 m_fm.neg(v1);
333 result = m_util.mk_value(v1);
334 return BR_DONE;
335 }
336
337 return BR_FAILED;
338 }
339
mk_rem(expr * arg1,expr * arg2,expr_ref & result)340 br_status fpa_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
341 scoped_mpf v1(m_fm), v2(m_fm);
342
343 if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
344 scoped_mpf t(m_fm);
345 m_fm.rem(v1, v2, t);
346 result = m_util.mk_value(t);
347 return BR_DONE;
348 }
349
350 return BR_FAILED;
351 }
352
mk_abs(expr * arg1,expr_ref & result)353 br_status fpa_rewriter::mk_abs(expr * arg1, expr_ref & result) {
354 if (m_util.is_nan(arg1)) {
355 result = arg1;
356 return BR_DONE;
357 }
358
359 scoped_mpf v(m_fm);
360 if (m_util.is_numeral(arg1, v)) {
361 if (m_fm.is_neg(v)) m_fm.neg(v);
362 result = m_util.mk_value(v);
363 return BR_DONE;
364 }
365
366 return BR_FAILED;
367 }
368
mk_min(expr * arg1,expr * arg2,expr_ref & result)369 br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
370 if (m_util.is_nan(arg1)) {
371 result = arg2;
372 return BR_DONE;
373 }
374 else if (m_util.is_nan(arg2)) {
375 result = arg1;
376 return BR_DONE;
377 }
378
379 scoped_mpf v1(m_fm), v2(m_fm);
380 if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
381 if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))
382 return BR_FAILED;
383
384 scoped_mpf r(m_fm);
385 m_fm.minimum(v1, v2, r);
386 result = m_util.mk_value(r);
387 return BR_DONE;
388 }
389
390 return BR_FAILED;
391 }
392
mk_max(expr * arg1,expr * arg2,expr_ref & result)393 br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
394 if (m_util.is_nan(arg1)) {
395 result = arg2;
396 return BR_DONE;
397 }
398 else if (m_util.is_nan(arg2)) {
399 result = arg1;
400 return BR_DONE;
401 }
402
403 scoped_mpf v1(m_fm), v2(m_fm);
404 if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
405 if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))
406 return BR_FAILED;
407
408 scoped_mpf r(m_fm);
409 m_fm.maximum(v1, v2, r);
410 result = m_util.mk_value(r);
411 return BR_DONE;
412 }
413
414 return BR_FAILED;
415 }
416
mk_fma(expr * arg1,expr * arg2,expr * arg3,expr * arg4,expr_ref & result)417 br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
418 mpf_rounding_mode rm;
419
420 if (m_util.is_rm_numeral(arg1, rm)) {
421 scoped_mpf v2(m_fm), v3(m_fm), v4(m_fm);
422 if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3) && m_util.is_numeral(arg4, v4)) {
423 scoped_mpf t(m_fm);
424 m_fm.fma(rm, v2, v3, v4, t);
425 result = m_util.mk_value(t);
426 return BR_DONE;
427 }
428 }
429
430 return BR_FAILED;
431 }
432
mk_sqrt(expr * arg1,expr * arg2,expr_ref & result)433 br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
434 mpf_rounding_mode rm;
435
436 if (m_util.is_rm_numeral(arg1, rm)) {
437 scoped_mpf v2(m_fm);
438 if (m_util.is_numeral(arg2, v2)) {
439 scoped_mpf t(m_fm);
440 m_fm.sqrt(rm, v2, t);
441 result = m_util.mk_value(t);
442 return BR_DONE;
443 }
444 }
445
446 return BR_FAILED;
447 }
448
mk_round_to_integral(expr * arg1,expr * arg2,expr_ref & result)449 br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result) {
450 mpf_rounding_mode rm;
451
452 if (m_util.is_rm_numeral(arg1, rm)) {
453 scoped_mpf v2(m_fm);
454 if (m_util.is_numeral(arg2, v2)) {
455 scoped_mpf t(m_fm);
456 m_fm.round_to_integral(rm, v2, t);
457 result = m_util.mk_value(t);
458 return BR_DONE;
459 }
460 }
461
462 return BR_FAILED;
463 }
464
465 // This the floating point theory ==
mk_float_eq(expr * arg1,expr * arg2,expr_ref & result)466 br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) {
467 scoped_mpf v1(m_fm), v2(m_fm);
468
469 if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
470 result = (m_fm.eq(v1, v2)) ? m().mk_true() : m().mk_false();
471 return BR_DONE;
472 }
473
474 return BR_FAILED;
475 }
476
477 // Return (= arg NaN)
mk_eq_nan(expr * arg)478 app * fpa_rewriter::mk_eq_nan(expr * arg) {
479 return m().mk_eq(arg, m_util.mk_nan(m().get_sort(arg)));
480 }
481
482 // Return (not (= arg NaN))
mk_neq_nan(expr * arg)483 app * fpa_rewriter::mk_neq_nan(expr * arg) {
484 return m().mk_not(mk_eq_nan(arg));
485 }
486
mk_lt(expr * arg1,expr * arg2,expr_ref & result)487 br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
488 if (m_util.is_nan(arg1) || m_util.is_nan(arg2)) {
489 result = m().mk_false();
490 return BR_DONE;
491 }
492 if (m_util.is_ninf(arg1)) {
493 // -oo < arg2 --> not(arg2 = -oo) and not(arg2 = NaN)
494 result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2));
495 return BR_REWRITE3;
496 }
497 if (m_util.is_ninf(arg2)) {
498 // arg1 < -oo --> false
499 result = m().mk_false();
500 return BR_DONE;
501 }
502 if (m_util.is_pinf(arg1)) {
503 // +oo < arg2 --> false
504 result = m().mk_false();
505 return BR_DONE;
506 }
507 if (m_util.is_pinf(arg2)) {
508 // arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN)
509 result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1));
510 return BR_REWRITE3;
511 }
512
513 scoped_mpf v1(m_fm), v2(m_fm);
514 if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
515 result = (m_fm.lt(v1, v2)) ? m().mk_true() : m().mk_false();
516 return BR_DONE;
517 }
518
519 return BR_FAILED;
520 }
521
mk_gt(expr * arg1,expr * arg2,expr_ref & result)522 br_status fpa_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
523 result = m_util.mk_lt(arg2, arg1);
524 return BR_REWRITE1;
525 }
526
mk_le(expr * arg1,expr * arg2,expr_ref & result)527 br_status fpa_rewriter::mk_le(expr * arg1, expr * arg2, expr_ref & result) {
528 if (m_util.is_nan(arg1) || m_util.is_nan(arg2)) {
529 result = m().mk_false();
530 return BR_DONE;
531 }
532
533 scoped_mpf v1(m_fm), v2(m_fm);
534 if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
535 result = (m_fm.le(v1, v2)) ? m().mk_true() : m().mk_false();
536 return BR_DONE;
537 }
538
539 return BR_FAILED;
540 }
541
mk_ge(expr * arg1,expr * arg2,expr_ref & result)542 br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
543 result = m_util.mk_le(arg2, arg1);
544 return BR_REWRITE1;
545 }
546
mk_is_zero(expr * arg1,expr_ref & result)547 br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
548 scoped_mpf v(m_fm);
549
550 if (m_util.is_numeral(arg1, v)) {
551 result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false();
552 return BR_DONE;
553 }
554
555 return BR_FAILED;
556 }
557
mk_is_nzero(expr * arg1,expr_ref & result)558 br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
559 scoped_mpf v(m_fm);
560
561 if (m_util.is_numeral(arg1, v)) {
562 result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false();
563 return BR_DONE;
564 }
565
566 return BR_FAILED;
567 }
568
mk_is_pzero(expr * arg1,expr_ref & result)569 br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
570 scoped_mpf v(m_fm);
571
572 if (m_util.is_numeral(arg1, v)) {
573 result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false();
574 return BR_DONE;
575 }
576
577 return BR_FAILED;
578 }
579
mk_is_nan(expr * arg1,expr_ref & result)580 br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) {
581 scoped_mpf v(m_fm);
582
583 if (m_util.is_numeral(arg1, v)) {
584 result = (m_fm.is_nan(v)) ? m().mk_true() : m().mk_false();
585 return BR_DONE;
586 }
587
588 return BR_FAILED;
589 }
590
mk_is_inf(expr * arg1,expr_ref & result)591 br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) {
592 scoped_mpf v(m_fm);
593
594 if (m_util.is_numeral(arg1, v)) {
595 result = (m_fm.is_inf(v)) ? m().mk_true() : m().mk_false();
596 return BR_DONE;
597 }
598
599 return BR_FAILED;
600 }
601
mk_is_normal(expr * arg1,expr_ref & result)602 br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) {
603 scoped_mpf v(m_fm);
604
605 if (m_util.is_numeral(arg1, v)) {
606 result = (m_fm.is_normal(v)) ? m().mk_true() : m().mk_false();
607 return BR_DONE;
608 }
609
610 return BR_FAILED;
611 }
612
mk_is_subnormal(expr * arg1,expr_ref & result)613 br_status fpa_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) {
614 scoped_mpf v(m_fm);
615
616 if (m_util.is_numeral(arg1, v)) {
617 result = (m_fm.is_denormal(v)) ? m().mk_true() : m().mk_false();
618 return BR_DONE;
619 }
620
621 return BR_FAILED;
622 }
623
mk_is_negative(expr * arg1,expr_ref & result)624 br_status fpa_rewriter::mk_is_negative(expr * arg1, expr_ref & result) {
625 scoped_mpf v(m_fm);
626
627 if (m_util.is_numeral(arg1, v)) {
628 result = (m_fm.is_neg(v)) ? m().mk_true() : m().mk_false();
629 return BR_DONE;
630 }
631
632 return BR_FAILED;
633 }
634
mk_is_positive(expr * arg1,expr_ref & result)635 br_status fpa_rewriter::mk_is_positive(expr * arg1, expr_ref & result) {
636 scoped_mpf v(m_fm);
637
638 if (m_util.is_numeral(arg1, v)) {
639 result = (m_fm.is_neg(v) || m_fm.is_nan(v)) ? m().mk_false() : m().mk_true();
640 return BR_DONE;
641 }
642
643 return BR_FAILED;
644 }
645
646
647 // This the SMT =
mk_eq_core(expr * arg1,expr * arg2,expr_ref & result)648 br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
649 scoped_mpf v1(m_fm), v2(m_fm);
650
651 if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
652 // Note: == is the floats-equality, here we need normal equality.
653 result = (m_fm.is_nan(v1) && m_fm.is_nan(v2)) ? m().mk_true() :
654 (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1)!=m_fm.sgn(v2)) ? m().mk_false() :
655 (v1 == v2) ? m().mk_true() :
656 m().mk_false();
657 return BR_DONE;
658 }
659
660 return BR_FAILED;
661 }
662
mk_bv2rm(expr * arg,expr_ref & result)663 br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) {
664 rational bv_val;
665 unsigned sz = 0;
666
667 if (m_util.bu().is_numeral(arg, bv_val, sz)) {
668 SASSERT(bv_val.is_uint64());
669 switch (bv_val.get_uint64()) {
670 case BV_RM_TIES_TO_AWAY: result = m_util.mk_round_nearest_ties_to_away(); break;
671 case BV_RM_TIES_TO_EVEN: result = m_util.mk_round_nearest_ties_to_even(); break;
672 case BV_RM_TO_NEGATIVE: result = m_util.mk_round_toward_negative(); break;
673 case BV_RM_TO_POSITIVE: result = m_util.mk_round_toward_positive(); break;
674 case BV_RM_TO_ZERO:
675 default: result = m_util.mk_round_toward_zero();
676 }
677
678 return BR_DONE;
679 }
680
681 return BR_FAILED;
682 }
683
mk_fp(expr * sgn,expr * exp,expr * sig,expr_ref & result)684 br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result) {
685 unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
686 rational rsgn, rexp, rsig;
687 unsigned bvsz_sgn, bvsz_exp, bvsz_sig;
688
689 if (m_util.bu().is_numeral(sgn, rsgn, bvsz_sgn) &&
690 m_util.bu().is_numeral(sig, rsig, bvsz_sig) &&
691 m_util.bu().is_numeral(exp, rexp, bvsz_exp)) {
692 SASSERT(mpzm.is_one(rexp.to_mpq().denominator()));
693 SASSERT(mpzm.is_one(rsig.to_mpq().denominator()));
694 scoped_mpf v(m_fm);
695 mpf_exp_t biased_exp = mpzm.get_int64(rexp.to_mpq().numerator());
696 m_fm.set(v, bvsz_exp, bvsz_sig + 1,
697 rsgn.is_one(),
698 m_fm.unbias_exp(bvsz_exp, biased_exp),
699 rsig.to_mpq().numerator());
700 TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_fm.to_string(v) << std::endl;);
701 result = m_util.mk_value(v);
702 return BR_DONE;
703 }
704
705 return BR_FAILED;
706 }
707
mk_to_bv(func_decl * f,expr * arg1,expr * arg2,bool is_signed,expr_ref & result)708 br_status fpa_rewriter::mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool is_signed, expr_ref & result) {
709 SASSERT(f->get_num_parameters() == 1);
710 SASSERT(f->get_parameter(0).is_int());
711 int bv_sz = f->get_parameter(0).get_int();
712 mpf_rounding_mode rmv;
713 scoped_mpf v(m_fm);
714
715 if (m_util.is_rm_numeral(arg1, rmv) &&
716 m_util.is_numeral(arg2, v)) {
717
718 if (m_fm.is_nan(v) || m_fm.is_inf(v))
719 return mk_to_bv_unspecified(f, result);
720
721 bv_util bu(m());
722 scoped_mpq q(m_fm.mpq_manager());
723 m_fm.to_sbv_mpq(rmv, v, q);
724
725 rational r(q);
726 rational ul, ll;
727 if (!is_signed) {
728 ul = m_fm.m_powers2.m1(bv_sz);
729 ll = rational(0);
730 }
731 else {
732 ul = m_fm.m_powers2.m1(bv_sz - 1);
733 ll = -m_fm.m_powers2(bv_sz - 1);
734 }
735 if (r >= ll && r <= ul) {
736 result = bu.mk_numeral(r, bv_sz);
737 return BR_DONE;
738 }
739 else
740 return mk_to_bv_unspecified(f, result);
741 }
742
743 return BR_FAILED;
744 }
745
mk_to_bv_unspecified(func_decl * f,expr_ref & result)746 br_status fpa_rewriter::mk_to_bv_unspecified(func_decl * f, expr_ref & result) {
747 if (m_hi_fp_unspecified) {
748 unsigned bv_sz = m_util.bu().get_bv_size(f->get_range());
749 result = m_util.bu().mk_numeral(0, bv_sz);
750 return BR_DONE;
751 }
752 else
753 return BR_FAILED;
754 }
755
mk_to_ubv(func_decl * f,expr * arg1,expr * arg2,expr_ref & result)756 br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
757 return mk_to_bv(f, arg1, arg2, false, result);
758 }
759
mk_to_sbv(func_decl * f,expr * arg1,expr * arg2,expr_ref & result)760 br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
761 return mk_to_bv(f, arg1, arg2, true, result);
762 }
763
mk_to_ieee_bv(func_decl * f,expr * arg,expr_ref & result)764 br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) {
765 TRACE("fp_rewriter", tout << "to_ieee_bv of " << mk_ismt2_pp(arg, m()) << std::endl;);
766 scoped_mpf v(m_fm);
767
768 if (m_util.is_numeral(arg, v)) {
769 TRACE("fp_rewriter", tout << "to_ieee_bv numeral: " << m_fm.to_string(v) << std::endl;);
770 bv_util bu(m());
771 const mpf & x = v.get();
772
773 if (m_fm.is_nan(v)) {
774 if (m_hi_fp_unspecified) {
775 expr * args[4] = { bu.mk_numeral(0, 1),
776 bu.mk_numeral(rational::minus_one(), x.get_ebits()),
777 bu.mk_numeral(0, x.get_sbits() - 2),
778 bu.mk_numeral(1, 1) };
779 result = bu.mk_concat(4, args);
780 return BR_REWRITE1;
781 }
782 }
783 else {
784 scoped_mpz rz(m_fm.mpq_manager());
785 m_fm.to_ieee_bv_mpz(v, rz);
786 result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits());
787 return BR_DONE;
788 }
789 }
790
791 return BR_FAILED;
792 }
793
mk_to_real(expr * arg,expr_ref & result)794 br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
795 scoped_mpf v(m_fm);
796
797 if (m_util.is_numeral(arg, v)) {
798 if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
799 if (m_hi_fp_unspecified) {
800 result = m_util.au().mk_numeral(rational(0), false);
801 return BR_DONE;
802 }
803 }
804 else {
805 scoped_mpq r(m_fm.mpq_manager());
806 m_fm.to_rational(v, r);
807 result = m_util.au().mk_numeral(r.get(), false);
808 return BR_DONE;
809 }
810 }
811
812 return BR_FAILED;
813 }
814
mk_bvwrap(expr * arg,expr_ref & result)815 br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
816 if (is_app_of(arg, m_util.get_family_id(), OP_FPA_FP)) {
817 bv_util bu(m());
818 SASSERT(to_app(arg)->get_num_args() == 3);
819 sort_ref fpsrt(m());
820 fpsrt = to_app(arg)->get_decl()->get_range();
821 expr_ref a0(m()), a1(m()), a2(m());
822 a0 = to_app(arg)->get_arg(0);
823 a1 = to_app(arg)->get_arg(1);
824 a2 = to_app(arg)->get_arg(2);
825 if (bu.is_extract(a0) && bu.is_extract(a1) && bu.is_extract(a2)) {
826 unsigned w0 = bu.get_extract_high(a0) - bu.get_extract_low(a0) + 1;
827 unsigned w1 = bu.get_extract_high(a1) - bu.get_extract_low(a1) + 1;
828 unsigned w2 = bu.get_extract_high(a2) - bu.get_extract_low(a2) + 1;
829 unsigned cw = w0 + w1 + w2;
830 if (cw == m_util.get_ebits(fpsrt) + m_util.get_sbits(fpsrt)) {
831 expr_ref aa0(m()), aa1(m()), aa2(m());
832 aa0 = to_app(a0)->get_arg(0);
833 aa1 = to_app(a1)->get_arg(0);
834 aa2 = to_app(a2)->get_arg(0);
835 if (aa0 == aa1 && aa1 == aa2 && bu.get_bv_size(aa0) == cw) {
836 result = aa0;
837 return BR_DONE;
838 }
839 }
840 }
841 }
842
843 return BR_FAILED;
844 }
845