1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 fpa2bv_converter.cpp
7
8 Abstract:
9
10 Conversion routines for Floating Point -> Bit-Vector
11
12 Author:
13
14 Christoph (cwinter) 2012-02-09
15
16 Notes:
17
18 --*/
19 #include<math.h>
20
21 #include "ast/ast_smt2_pp.h"
22 #include "ast/ast_pp.h"
23 #include "ast/well_sorted.h"
24 #include "ast/rewriter/th_rewriter.h"
25 #include "ast/used_vars.h"
26 #include "ast/rewriter/var_subst.h"
27
28 #include "ast/fpa/fpa2bv_converter.h"
29 #include "ast/rewriter/fpa_rewriter.h"
30
31 #define BVULT(X,Y,R) { expr_ref t(m); t = m_bv_util.mk_ule(Y,X); m_simp.mk_not(t, R); }
32
fpa2bv_converter(ast_manager & m)33 fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
34 m(m),
35 m_simp(m),
36 m_bv_util(m),
37 m_arith_util(m),
38 m_dt_util(m),
39 m_seq_util(m),
40 m_util(m),
41 m_mpf_manager(m_util.fm()),
42 m_mpz_manager(m_mpf_manager.mpz_manager()),
43 m_hi_fp_unspecified(true),
44 m_extra_assertions(m) {
45 m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m.mk_family_id("fpa")));
46 }
47
~fpa2bv_converter()48 fpa2bv_converter::~fpa2bv_converter() {
49 reset();
50 }
51
mk_eq(expr * a,expr * b,expr_ref & result)52 void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
53 if (is_float(a) && is_float(b)) {
54
55
56 TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl;
57 tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
58
59 SASSERT(m_util.is_fp(a) && m_util.is_fp(b));
60
61 expr_ref eq_sgn(m), eq_exp(m), eq_sig(m);
62 m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn);
63 m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), eq_exp);
64 m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), eq_sig);
65
66 dbg_decouple("fpa2bv_eq_sgn", eq_sgn);
67 dbg_decouple("fpa2bv_eq_exp", eq_exp);
68 dbg_decouple("fpa2bv_eq_sig", eq_sig);
69
70 expr_ref both_the_same(m);
71 m_simp.mk_and(eq_sgn, eq_exp, eq_sig, both_the_same);
72 dbg_decouple("fpa2bv_eq_both_the_same", both_the_same);
73
74 // The SMT FPA theory asks for _one_ NaN value, but the bit-blasting
75 // has many, like IEEE754. This encoding of equality makes it look like
76 // a single NaN again.
77 expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m);
78 mk_is_nan(a, a_is_nan);
79 mk_is_nan(b, b_is_nan);
80 m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan);
81 dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan);
82
83 m_simp.mk_or(both_are_nan, both_the_same, result);
84 }
85 else if (is_rm(a) && is_rm(b)) {
86 SASSERT(m_util.is_bv2rm(b) && m_util.is_bv2rm(a));
87
88 TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl;
89 tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
90
91 m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result);
92 }
93 else
94 UNREACHABLE();
95 }
96
mk_ite(expr * c,expr * t,expr * f,expr_ref & result)97 void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
98 if (m_util.is_fp(t) && m_util.is_fp(f)) {
99 expr_ref t_sgn(m), t_sig(m), t_exp(m);
100 expr_ref f_sgn(m), f_sig(m), f_exp(m);
101 split_fp(t, t_sgn, t_exp, t_sig);
102 split_fp(f, f_sgn, f_exp, f_sig);
103
104 expr_ref sgn(m), s(m), e(m);
105 m_simp.mk_ite(c, t_sgn, f_sgn, sgn);
106 m_simp.mk_ite(c, t_sig, f_sig, s);
107 m_simp.mk_ite(c, t_exp, f_exp, e);
108
109 result = m_util.mk_fp(sgn, e, s);
110 }
111 else if (m_util.is_rm(t) && m_util.is_rm(f))
112 {
113 SASSERT(m_util.is_bv2rm(t) && m_util.is_bv2rm(f));
114 TRACE("fpa2bv", tout << "ite rm: t=" << mk_ismt2_pp(t, m) << " f=" << mk_ismt2_pp(f, m) << std::endl; );
115 m_simp.mk_ite(c, to_app(t)->get_arg(0), to_app(f)->get_arg(0), result);
116 result = m_util.mk_bv2rm(result);
117 }
118 else
119 UNREACHABLE();
120 }
121
mk_distinct(func_decl * f,unsigned num,expr * const * args,expr_ref & result)122 void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
123 // Note: in SMT there is only one NaN, so multiple of them are considered
124 // equal, thus (distinct NaN NaN) is false, even if the two NaNs have
125 // different bitwise representations (see also mk_eq).
126 result = m.mk_true();
127 for (unsigned i = 0; i < num; i++) {
128 for (unsigned j = i+1; j < num; j++) {
129 expr_ref eq(m), neq(m);
130 mk_eq(args[i], args[j], eq);
131 neq = m.mk_not(eq);
132 m_simp.mk_and(result, neq, result);
133 }
134 }
135 }
136
mk_numeral(func_decl * f,unsigned num,expr * const * args,expr_ref & result)137 void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
138 SASSERT(num == 0);
139 SASSERT(f->get_num_parameters() == 1);
140 SASSERT(f->get_parameter(0).is_external());
141 unsigned p_id = f->get_parameter(0).get_ext_id();
142 mpf const & v = m_plugin->get_value(p_id);
143 mk_numeral(f->get_range(), v, result);
144 }
145
mk_numeral(sort * s,mpf const & v,expr_ref & result)146 void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) {
147 unsigned sbits = v.get_sbits();
148 unsigned ebits = v.get_ebits();
149
150 bool sign = m_util.fm().sgn(v);
151 mpz const & sig = m_util.fm().sig(v);
152 mpf_exp_t const & exp = m_util.fm().exp(v);
153
154 if (m_util.fm().is_nan(v))
155 mk_nan(s, result);
156 else if (m_util.fm().is_inf(v)) {
157 if (m_util.fm().sgn(v))
158 mk_ninf(s, result);
159 else
160 mk_pinf(s, result);
161 }
162 else {
163 expr_ref bv_sgn(m), bv_sig(m), e(m), biased_exp(m);
164 bv_sgn = m_bv_util.mk_numeral((sign) ? 1 : 0, 1);
165 bv_sig = m_bv_util.mk_numeral(rational(sig), sbits-1);
166 e = m_bv_util.mk_numeral(exp, ebits);
167
168 mk_bias(e, biased_exp);
169
170 result = m_util.mk_fp(bv_sgn, biased_exp, bv_sig);
171 TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is "
172 << mk_ismt2_pp(result, m) << std::endl;);
173 }
174 }
175
mk_fresh_const(char const * prefix,unsigned sz)176 app * fpa2bv_converter::mk_fresh_const(char const * prefix, unsigned sz) {
177 return m.mk_fresh_const(prefix, m_bv_util.mk_sort(sz));
178 }
179
mk_const(func_decl * f,expr_ref & result)180 void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
181 SASSERT(f->get_family_id() == null_family_id);
182 SASSERT(f->get_arity() == 0);
183 expr * r;
184 if (m_const2bv.find(f, r)) {
185 result = r;
186 }
187 else {
188 sort * srt = f->get_range();
189 SASSERT(is_float(srt));
190 unsigned ebits = m_util.get_ebits(srt);
191 unsigned sbits = m_util.get_sbits(srt);
192
193 app_ref sgn(m), s(m), e(m);
194
195 #ifdef Z3DEBUG_FPA2BV_NAMES
196 std::string p("fpa2bv");
197 std::string name = f->get_name().str();
198
199 sgn = mk_fresh_const((p + "_sgn_" + name).c_str(), 1);
200 e = mk_fresh_const((p + "_exp_" + name).c_str(), ebits);
201 s = mk_fresh_const((p + "_sig_" + name).c_str(), sbits-1);
202 #else
203 app_ref bv(m);
204 unsigned bv_sz = 1 + ebits + (sbits - 1);
205 bv = mk_fresh_const(nullptr, bv_sz);
206
207 sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
208 e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
209 s = m_bv_util.mk_extract(sbits - 2, 0, bv);
210
211 SASSERT(m_bv_util.get_bv_size(sgn) == 1);
212 SASSERT(m_bv_util.get_bv_size(s) == sbits-1);
213 SASSERT(m_bv_util.get_bv_size(e) == ebits);
214 #endif
215
216 result = m_util.mk_fp(sgn, e, s);
217
218 m_const2bv.insert(f, result);
219 m.inc_ref(f);
220 m.inc_ref(result);
221 }
222 }
223
mk_var(unsigned base_inx,sort * srt,expr_ref & result)224 void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result) {
225 SASSERT(is_float(srt));
226 unsigned ebits = m_util.get_ebits(srt);
227 unsigned sbits = m_util.get_sbits(srt);
228
229 expr_ref sgn(m), s(m), e(m);
230
231 sgn = m.mk_var(base_inx, m_bv_util.mk_sort(1));
232 s = m.mk_var(base_inx+1, m_bv_util.mk_sort(sbits-1));
233 e = m.mk_var(base_inx+2, m_bv_util.mk_sort(ebits));
234
235 result = m_util.mk_fp(sgn, e, s);
236 }
237
extra_quantify(expr * e)238 expr_ref fpa2bv_converter::extra_quantify(expr * e)
239 {
240 used_vars uv;
241 unsigned nv;
242
243 ptr_buffer<sort> new_decl_sorts;
244 sbuffer<symbol> new_decl_names;
245 expr_ref_buffer subst_map(m);
246
247 uv(e);
248 nv = uv.get_num_vars();
249 subst_map.resize(uv.get_max_found_var_idx_plus_1());
250
251 if (nv == 0)
252 return expr_ref(e, m);
253
254 for (unsigned i = 0; i < nv; i++)
255 {
256 if (uv.contains(i)) {
257 TRACE("fpa2bv", tout << "uv[" << i << "] = " << mk_ismt2_pp(uv.get(i), m) << std::endl; );
258 sort * s = uv.get(i);
259 var * v = m.mk_var(i, s);
260 new_decl_sorts.push_back(s);
261 new_decl_names.push_back(symbol(i));
262 subst_map.set(i, v);
263 }
264 }
265
266 expr_ref res(m);
267 var_subst vsubst(m);
268 res = vsubst.operator()(e, nv, subst_map.data());
269 TRACE("fpa2bv", tout << "subst'd = " << mk_ismt2_pp(res, m) << std::endl; );
270 res = m.mk_forall(nv, new_decl_sorts.data(), new_decl_names.data(), res);
271 return res;
272 }
273
mk_uf(func_decl * f,unsigned num,expr * const * args,expr_ref & result)274 void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
275 {
276 TRACE("fpa2bv", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
277
278 expr_ref fapp(m);
279 sort_ref rng(m);
280 app_ref bv_app(m), flt_app(m);
281 rng = f->get_range();
282 fapp = m.mk_app(f, num, args);
283 if (m_util.is_float(rng)) {
284 sort_ref bv_rng(m);
285 expr_ref new_eq(m);
286 unsigned ebits = m_util.get_ebits(rng);
287 unsigned sbits = m_util.get_sbits(rng);
288 unsigned bv_sz = ebits+sbits;
289 bv_rng = m_bv_util.mk_sort(bv_sz);
290 func_decl * bv_f = mk_bv_uf(f, f->get_domain(), bv_rng);
291 bv_app = m.mk_app(bv_f, num, args);
292 flt_app = m_util.mk_fp(m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv_app),
293 m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app),
294 m_bv_util.mk_extract(sbits-2, 0, bv_app));
295 new_eq = m.mk_eq(fapp, flt_app);
296 m_extra_assertions.push_back(extra_quantify(new_eq));
297 result = flt_app;
298 }
299 else if (m_util.is_rm(rng)) {
300 sort_ref bv_rng(m);
301 expr_ref new_eq(m);
302 bv_rng = m_bv_util.mk_sort(3);
303 func_decl * bv_f = mk_bv_uf(f, f->get_domain(), bv_rng);
304 bv_app = m.mk_app(bv_f, num, args);
305 flt_app = m_util.mk_bv2rm(bv_app);
306 new_eq = m.mk_eq(fapp, flt_app);
307 m_extra_assertions.push_back(extra_quantify(new_eq));
308 result = flt_app;
309 }
310 else
311 result = fapp;
312
313 TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
314 SASSERT(is_well_sorted(m, result));
315 }
316
mk_rm_const(func_decl * f,expr_ref & result)317 void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
318 SASSERT(f->get_family_id() == null_family_id);
319 SASSERT(f->get_arity() == 0);
320 expr * r;
321 if (m_rm_const2bv.find(f, r)) {
322 result = r;
323 }
324 else {
325 SASSERT(is_rm(f->get_range()));
326
327 expr_ref bv3(m);
328 bv3 = m.mk_fresh_const(
329 #ifdef Z3DEBUG_FPA2BV_NAMES
330 "fpa2bv_rm"
331 #else
332 nullptr
333 #endif
334 , m_bv_util.mk_sort(3));
335
336 result = m_util.mk_bv2rm(bv3);
337 m_rm_const2bv.insert(f, result);
338 m.inc_ref(f);
339 m.inc_ref(result);
340
341 expr_ref rcc(m);
342 rcc = bu().mk_ule(bv3, bu().mk_numeral(4, 3));
343 m_extra_assertions.push_back(rcc);
344 }
345 }
346
mk_pinf(func_decl * f,expr_ref & result)347 void fpa2bv_converter::mk_pinf(func_decl * f, expr_ref & result) {
348 mk_pinf(f->get_range(), result);
349 }
350
mk_pinf(sort * s,expr_ref & result)351 void fpa2bv_converter::mk_pinf(sort * s, expr_ref & result) {
352 SASSERT(is_float(s));
353 unsigned sbits = m_util.get_sbits(s);
354 unsigned ebits = m_util.get_ebits(s);
355 expr_ref top_exp(m);
356 mk_top_exp(ebits, top_exp);
357 result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), top_exp, m_bv_util.mk_numeral(0, sbits-1));
358 }
359
mk_ninf(func_decl * f,expr_ref & result)360 void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) {
361 mk_ninf(f->get_range(), result);
362 }
363
mk_ninf(sort * s,expr_ref & result)364 void fpa2bv_converter::mk_ninf(sort * s, expr_ref & result) {
365 SASSERT(is_float(s));
366 unsigned sbits = m_util.get_sbits(s);
367 unsigned ebits = m_util.get_ebits(s);
368 expr_ref top_exp(m);
369 mk_top_exp(ebits, top_exp);
370 result = m_util.mk_fp(m_bv_util.mk_numeral(1, 1), top_exp, m_bv_util.mk_numeral(0, sbits-1));
371 }
372
mk_nan(func_decl * f,expr_ref & result)373 void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) {
374 mk_nan(f->get_range(), result);
375 }
376
mk_nan(sort * s,expr_ref & result)377 void fpa2bv_converter::mk_nan(sort * s, expr_ref & result) {
378 SASSERT(is_float(s));
379 unsigned sbits = m_util.get_sbits(s);
380 unsigned ebits = m_util.get_ebits(s);
381 expr_ref top_exp(m);
382 mk_top_exp(ebits, top_exp);
383 result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), top_exp, m_bv_util.mk_numeral(1, sbits - 1));
384 }
385
mk_nzero(func_decl * f,expr_ref & result)386 void fpa2bv_converter::mk_nzero(func_decl * f, expr_ref & result) {
387 mk_nzero(f->get_range(), result);
388 }
389
mk_nzero(sort * s,expr_ref & result)390 void fpa2bv_converter::mk_nzero(sort * s, expr_ref & result) {
391 SASSERT(is_float(s));
392 unsigned sbits = m_util.get_sbits(s);
393 unsigned ebits = m_util.get_ebits(s);
394 expr_ref bot_exp(m);
395 mk_bot_exp(ebits, bot_exp);
396 result = m_util.mk_fp(m_bv_util.mk_numeral(1, 1), bot_exp, m_bv_util.mk_numeral(0, sbits - 1));
397 }
398
mk_pzero(func_decl * f,expr_ref & result)399 void fpa2bv_converter::mk_pzero(func_decl * f, expr_ref & result) {
400 mk_pzero(f->get_range(), result);
401 }
402
mk_pzero(sort * s,expr_ref & result)403 void fpa2bv_converter::mk_pzero(sort * s, expr_ref & result) {
404 SASSERT(is_float(s));
405 unsigned sbits = m_util.get_sbits(s);
406 unsigned ebits = m_util.get_ebits(s);
407 expr_ref bot_exp(m);
408 mk_bot_exp(ebits, bot_exp);
409 result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), bot_exp, m_bv_util.mk_numeral(0, sbits-1));
410 }
411
mk_zero(sort * s,expr_ref & sgn,expr_ref & result)412 void fpa2bv_converter::mk_zero(sort * s, expr_ref & sgn, expr_ref & result) {
413 expr_ref is_pos(m), pzero(m), nzero(m);
414 is_pos = m.mk_eq(sgn, m_bv_util.mk_numeral(0, 1));
415 mk_pzero(s, pzero);
416 mk_nzero(s, nzero);
417 mk_ite(is_pos, pzero, nzero, result);
418 }
419
mk_one(func_decl * f,expr_ref & sign,expr_ref & result)420 void fpa2bv_converter::mk_one(func_decl * f, expr_ref & sign, expr_ref & result) {
421 mk_one(f->get_range(), sign, result);
422 }
423
mk_one(sort * s,expr_ref & sign,expr_ref & result)424 void fpa2bv_converter::mk_one(sort * s, expr_ref & sign, expr_ref & result) {
425 SASSERT(is_float(s));
426 unsigned sbits = m_util.get_sbits(s);
427 unsigned ebits = m_util.get_ebits(s);
428 result = m_util.mk_fp(sign, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits), m_bv_util.mk_numeral(0, sbits-1));
429 }
430
add_core(unsigned sbits,unsigned ebits,expr_ref & c_sgn,expr_ref & c_sig,expr_ref & c_exp,expr_ref & d_sgn,expr_ref & d_sig,expr_ref & d_exp,expr_ref & res_sgn,expr_ref & res_sig,expr_ref & res_exp)431 void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
432 expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp,
433 expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp)
434 {
435 // c/d are now such that c_exp >= d_exp.
436 expr_ref exp_delta(m);
437 exp_delta = m_bv_util.mk_bv_sub(c_exp, d_exp);
438
439 dbg_decouple("fpa2bv_add_exp_delta", exp_delta);
440
441 if (log2(sbits + 2) < ebits + 2)
442 {
443 // cap the delta
444 expr_ref cap(m), cap_le_delta(m), exp_delta_ext(m);
445 cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2);
446 cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta));
447 exp_delta_ext = m_bv_util.mk_zero_extend(2, exp_delta);
448 m_simp.mk_ite(cap_le_delta, cap, exp_delta_ext, exp_delta);
449 exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta);
450 dbg_decouple("fpa2bv_add_exp_cap", cap);
451 }
452
453 dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta);
454
455 // Three extra bits for c/d
456 c_sig = m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, 3));
457 d_sig = m_bv_util.mk_concat(d_sig, m_bv_util.mk_numeral(0, 3));
458
459 SASSERT(is_well_sorted(m, c_sig));
460 SASSERT(is_well_sorted(m, d_sig));
461
462 // Alignment shift with sticky bit computation.
463 expr_ref big_d_sig(m);
464 big_d_sig = m_bv_util.mk_concat(d_sig, m_bv_util.mk_numeral(0, sbits+3));
465
466 SASSERT(is_well_sorted(m, big_d_sig));
467 if (ebits > sbits)
468 throw default_exception("addition/subtract with ebits > sbits not supported");
469
470
471 expr_ref shifted_big(m), shifted_d_sig(m), sticky_raw(m), sticky(m);
472 shifted_big = m_bv_util.mk_bv_lshr(big_d_sig, m_bv_util.mk_concat(m_bv_util.mk_numeral(0, (2*(sbits+3))-ebits), exp_delta));
473 shifted_d_sig = m_bv_util.mk_extract((2*(sbits+3)-1), (sbits+3), shifted_big);
474 SASSERT(is_well_sorted(m, shifted_d_sig));
475
476 sticky_raw = m_bv_util.mk_extract(sbits+2, 0, shifted_big);
477 expr_ref sticky_eq(m), nil_sbit3(m), one_sbit3(m);
478 nil_sbit3 = m_bv_util.mk_numeral(0, sbits+3);
479 one_sbit3 = m_bv_util.mk_numeral(1, sbits+3);
480 m_simp.mk_eq(sticky_raw, nil_sbit3, sticky_eq);
481 m_simp.mk_ite(sticky_eq, nil_sbit3, one_sbit3, sticky);
482 SASSERT(is_well_sorted(m, sticky));
483
484 expr * or_args[2] = { shifted_d_sig, sticky };
485 shifted_d_sig = m_bv_util.mk_bv_or(2, or_args);
486 SASSERT(is_well_sorted(m, shifted_d_sig));
487
488 expr_ref eq_sgn(m);
489 m_simp.mk_eq(c_sgn, d_sgn, eq_sgn);
490
491 dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn);
492 TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; );
493
494 // two extra bits for catching the overflow.
495 c_sig = m_bv_util.mk_zero_extend(2, c_sig);
496 shifted_d_sig = m_bv_util.mk_zero_extend(2, shifted_d_sig);
497
498 SASSERT(m_bv_util.get_bv_size(c_sig) == sbits+5);
499 SASSERT(m_bv_util.get_bv_size(shifted_d_sig) == sbits+5);
500
501 dbg_decouple("fpa2bv_add_c_sig", c_sig);
502 dbg_decouple("fpa2bv_add_shifted_d_sig", shifted_d_sig);
503
504 expr_ref sum(m), c_plus_d(m), c_minus_d(m);
505 c_plus_d = m_bv_util.mk_bv_add(c_sig, shifted_d_sig);
506 c_minus_d = m_bv_util.mk_bv_sub(c_sig, shifted_d_sig);
507 m_simp.mk_ite(eq_sgn, c_plus_d, c_minus_d, sum);
508
509 SASSERT(is_well_sorted(m, sum));
510
511 dbg_decouple("fpa2bv_add_sum", sum);
512
513 expr_ref sign_bv(m), n_sum(m);
514 sign_bv = m_bv_util.mk_extract(sbits+4, sbits+4, sum);
515 n_sum = m_bv_util.mk_bv_neg(sum);
516
517 dbg_decouple("fpa2bv_add_sign_bv", sign_bv);
518 dbg_decouple("fpa2bv_add_n_sum", n_sum);
519
520 family_id bvfid = m_bv_util.get_fid();
521
522 expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
523 expr_ref not_c_sgn(m), not_d_sgn(m), not_sign_bv(m);
524 not_c_sgn = m_bv_util.mk_bv_not(c_sgn);
525 not_d_sgn = m_bv_util.mk_bv_not(d_sgn);
526 not_sign_bv = m_bv_util.mk_bv_not(sign_bv);
527 res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_c_sgn, d_sgn, sign_bv);
528 res_sgn_c2 = m.mk_app(bvfid, OP_BAND, c_sgn, not_d_sgn, not_sign_bv);
529 res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn);
530 expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
531 res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
532
533 expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
534 one_1 = m_bv_util.mk_numeral(1, 1);
535 m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
536 m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
537
538 dbg_decouple("fpa2bv_add_sig_abs", sig_abs);
539
540 res_sig = m_bv_util.mk_extract(sbits+3, 0, sig_abs);
541 res_exp = m_bv_util.mk_sign_extend(2, c_exp); // rounder requires 2 extra bits!
542 }
543
mk_add(func_decl * f,unsigned num,expr * const * args,expr_ref & result)544 void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
545 SASSERT(num == 3);
546 SASSERT(m_util.is_bv2rm(args[0]));
547
548 expr_ref rm(m), x(m), y(m);
549 rm = to_app(args[0])->get_arg(0);
550 x = args[1];
551 y = args[2];
552 mk_add(f->get_range(), rm, x, y, result);
553 }
554
mk_add(sort * s,expr_ref & rm,expr_ref & x,expr_ref & y,expr_ref & result)555 void fpa2bv_converter::mk_add(sort * s, expr_ref & rm, expr_ref & x, expr_ref & y, expr_ref & result) {
556 expr_ref nan(m), nzero(m), pzero(m);
557 mk_nan(s, nan);
558 mk_nzero(s, nzero);
559 mk_pzero(s, pzero);
560
561 expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m);
562 expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m);
563 mk_is_nan(x, x_is_nan);
564 mk_is_zero(x, x_is_zero);
565 mk_is_pos(x, x_is_pos);
566 mk_is_neg(x, x_is_neg);
567 mk_is_inf(x, x_is_inf);
568 mk_is_nan(y, y_is_nan);
569 mk_is_zero(y, y_is_zero);
570 mk_is_pos(y, y_is_pos);
571 mk_is_neg(y, y_is_neg);
572 mk_is_inf(y, y_is_inf);
573
574 dbg_decouple("fpa2bv_add_x_is_nan", x_is_nan);
575 dbg_decouple("fpa2bv_add_x_is_zero", x_is_zero);
576 dbg_decouple("fpa2bv_add_x_is_pos", x_is_pos);
577 dbg_decouple("fpa2bv_add_x_is_neg", x_is_neg);
578 dbg_decouple("fpa2bv_add_x_is_inf", x_is_inf);
579 dbg_decouple("fpa2bv_add_y_is_nan", y_is_nan);
580 dbg_decouple("fpa2bv_add_y_is_zero", y_is_zero);
581 dbg_decouple("fpa2bv_add_y_is_pos", y_is_pos);
582 dbg_decouple("fpa2bv_add_y_is_neg", y_is_neg);
583 dbg_decouple("fpa2bv_add_y_is_inf", y_is_inf);
584
585 expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m);
586 expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m);
587
588 m_simp.mk_or(x_is_nan, y_is_nan, c1);
589 v1 = nan;
590
591 mk_is_inf(x, c2);
592 expr_ref nx(m), ny(m), nx_xor_ny(m), inf_xor(m);
593 mk_is_neg(x, nx);
594 mk_is_neg(y, ny);
595 m_simp.mk_xor(nx, ny, nx_xor_ny);
596 m_simp.mk_and(y_is_inf, nx_xor_ny, inf_xor);
597 mk_ite(inf_xor, nan, x, v2);
598
599 mk_is_inf(y, c3);
600 expr_ref xy_is_neg(m), v3_and(m);
601 m_simp.mk_xor(x_is_neg, y_is_neg, xy_is_neg);
602 m_simp.mk_and(x_is_inf, xy_is_neg, v3_and);
603 mk_ite(v3_and, nan, y, v3);
604
605 expr_ref rm_is_to_neg(m), signs_and(m), signs_xor(m), v4_and(m), rm_and_xor(m), neg_cond(m);
606 m_simp.mk_and(x_is_zero, y_is_zero, c4);
607 m_simp.mk_and(x_is_neg, y_is_neg, signs_and);
608 m_simp.mk_xor(x_is_neg, y_is_neg, signs_xor);
609 mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
610 m_simp.mk_and(rm_is_to_neg, signs_xor, rm_and_xor);
611 m_simp.mk_or(signs_and, rm_and_xor, neg_cond);
612 mk_ite(neg_cond, nzero, pzero, v4);
613 m_simp.mk_and(x_is_neg, y_is_neg, v4_and);
614 mk_ite(v4_and, x, v4, v4);
615
616 c5 = x_is_zero;
617 v5 = y;
618
619 c6 = y_is_zero;
620 v6 = x;
621
622 // Actual addition.
623 unsigned ebits = m_util.get_ebits(s);
624 unsigned sbits = m_util.get_sbits(s);
625
626 expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
627 unpack(x, a_sgn, a_sig, a_exp, a_lz, false);
628 unpack(y, b_sgn, b_sig, b_exp, b_lz, false);
629
630 dbg_decouple("fpa2bv_add_unpack_a_sgn", a_sgn);
631 dbg_decouple("fpa2bv_add_unpack_a_sig", a_sig);
632 dbg_decouple("fpa2bv_add_unpack_a_exp", a_exp);
633 dbg_decouple("fpa2bv_add_unpack_b_sgn", b_sgn);
634 dbg_decouple("fpa2bv_add_unpack_b_sig", b_sig);
635 dbg_decouple("fpa2bv_add_unpack_b_exp", b_exp);
636
637 expr_ref swap_cond(m);
638 swap_cond = m_bv_util.mk_sle(a_exp, b_exp);
639
640 expr_ref c_sgn(m), c_sig(m), c_exp(m), d_sgn(m), d_sig(m), d_exp(m);
641 m_simp.mk_ite(swap_cond, b_sgn, a_sgn, c_sgn);
642 m_simp.mk_ite(swap_cond, b_sig, a_sig, c_sig); // has sbits
643 m_simp.mk_ite(swap_cond, b_exp, a_exp, c_exp); // has ebits
644 m_simp.mk_ite(swap_cond, a_sgn, b_sgn, d_sgn);
645 m_simp.mk_ite(swap_cond, a_sig, b_sig, d_sig); // has sbits
646 m_simp.mk_ite(swap_cond, a_exp, b_exp, d_exp); // has ebits
647
648 expr_ref res_sgn(m), res_sig(m), res_exp(m);
649 add_core(sbits, ebits,
650 c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp,
651 res_sgn, res_sig, res_exp);
652
653 expr_ref is_zero_sig(m), nil_sbit4(m);
654 nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4);
655 m_simp.mk_eq(res_sig, nil_sbit4, is_zero_sig);
656
657 SASSERT(is_well_sorted(m, is_zero_sig));
658
659 dbg_decouple("fpa2bv_add_is_zero_sig", is_zero_sig);
660
661 expr_ref zero_case(m);
662 mk_ite(rm_is_to_neg, nzero, pzero, zero_case);
663
664 expr_ref rounded(m);
665 round(s, rm, res_sgn, res_sig, res_exp, rounded);
666
667 mk_ite(is_zero_sig, zero_case, rounded, v7);
668
669 dbg_decouple("fpa2bv_add_c1", c1);
670 dbg_decouple("fpa2bv_add_c2", c2);
671 dbg_decouple("fpa2bv_add_c3", c3);
672 dbg_decouple("fpa2bv_add_c4", c4);
673 dbg_decouple("fpa2bv_add_c5", c5);
674 dbg_decouple("fpa2bv_add_c6", c6);
675
676 mk_ite(c6, v6, v7, result);
677 mk_ite(c5, v5, result, result);
678 mk_ite(c4, v4, result, result);
679 mk_ite(c3, v3, result, result);
680 mk_ite(c2, v2, result, result);
681 mk_ite(c1, v1, result, result);
682
683 SASSERT(is_well_sorted(m, result));
684
685 TRACE("fpa2bv_add", tout << "ADD = " << mk_ismt2_pp(result, m) << std::endl; );
686 }
687
mk_sub(func_decl * f,unsigned num,expr * const * args,expr_ref & result)688 void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
689 SASSERT(num == 3);
690 expr_ref rm(m), x(m), y(m);
691 rm = args[0];
692 x = args[1];
693 y = args[2];
694 mk_sub(f->get_range(), rm, x, y, result);
695 }
696
mk_sub(sort * s,expr_ref & rm,expr_ref & x,expr_ref & y,expr_ref & result)697 void fpa2bv_converter::mk_sub(sort * s, expr_ref & rm, expr_ref & x, expr_ref & y, expr_ref & result) {
698 expr_ref t(m);
699 mk_neg(s, y, t);
700 mk_add(s, rm, x, t, result);
701 }
702
mk_neg(func_decl * f,unsigned num,expr * const * args,expr_ref & result)703 void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
704 SASSERT(num == 1);
705 expr_ref x(m);
706 x = args[0];
707 mk_neg(f->get_range(), x, result);
708 }
709
mk_neg(sort * srt,expr_ref & x,expr_ref & result)710 void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) {
711 expr_ref sgn(m), sig(m), exp(m);
712 split_fp(x, sgn, exp, sig);
713 expr_ref x_is_nan(m), nsgn(m), nx(m);
714 mk_is_nan(x, x_is_nan);
715 nsgn = m_bv_util.mk_bv_not(sgn);
716 nx = m_util.mk_fp(nsgn, exp, sig);
717 mk_ite(x_is_nan, x, nx, result);
718 }
719
mk_mul(func_decl * f,unsigned num,expr * const * args,expr_ref & result)720 void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
721 SASSERT(num == 3);
722 SASSERT(m_util.is_bv2rm(args[0]));
723
724 expr_ref rm(m), x(m), y(m);
725 rm = to_app(args[0])->get_arg(0);
726 x = args[1];
727 y = args[2];
728 mk_mul(f->get_range(), rm, x, y, result);
729 }
730
mk_mul(sort * s,expr_ref & rm,expr_ref & x,expr_ref & y,expr_ref & result)731 void fpa2bv_converter::mk_mul(sort * s, expr_ref & rm, expr_ref & x, expr_ref & y, expr_ref & result) {
732 expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
733 mk_nan(s, nan);
734 mk_nzero(s, nzero);
735 mk_pzero(s, pzero);
736 mk_ninf(s, ninf);
737 mk_pinf(s, pinf);
738
739 expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
740 expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
741 mk_is_nan(x, x_is_nan);
742 mk_is_zero(x, x_is_zero);
743 mk_is_pos(x, x_is_pos);
744 mk_is_inf(x, x_is_inf);
745 mk_is_nan(y, y_is_nan);
746 mk_is_zero(y, y_is_zero);
747 mk_is_pos(y, y_is_pos);
748 mk_is_inf(y, y_is_inf);
749
750 dbg_decouple("fpa2bv_mul_x_is_nan", x_is_nan);
751 dbg_decouple("fpa2bv_mul_x_is_zero", x_is_zero);
752 dbg_decouple("fpa2bv_mul_x_is_pos", x_is_pos);
753 dbg_decouple("fpa2bv_mul_x_is_inf", x_is_inf);
754 dbg_decouple("fpa2bv_mul_y_is_nan", y_is_nan);
755 dbg_decouple("fpa2bv_mul_y_is_zero", y_is_zero);
756 dbg_decouple("fpa2bv_mul_y_is_pos", y_is_pos);
757 dbg_decouple("fpa2bv_mul_y_is_inf", y_is_inf);
758
759 expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m);
760 expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m);
761
762 // (x is NaN) || (y is NaN) -> NaN
763 m_simp.mk_or(x_is_nan, y_is_nan, c1);
764 v1 = nan;
765
766 // (x is +oo) -> if (y is 0) then NaN else inf with y's sign.
767 mk_is_pinf(x, c2);
768 expr_ref y_sgn_inf(m);
769 mk_ite(y_is_pos, pinf, ninf, y_sgn_inf);
770 mk_ite(y_is_zero, nan, y_sgn_inf, v2);
771
772 // (y is +oo) -> if (x is 0) then NaN else inf with x's sign.
773 mk_is_pinf(y, c3);
774 expr_ref x_sgn_inf(m);
775 mk_ite(x_is_pos, pinf, ninf, x_sgn_inf);
776 mk_ite(x_is_zero, nan, x_sgn_inf, v3);
777
778 // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign.
779 mk_is_ninf(x, c4);
780 expr_ref neg_y_sgn_inf(m);
781 mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf);
782 mk_ite(y_is_zero, nan, neg_y_sgn_inf, v4);
783
784 // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign.
785 mk_is_ninf(y, c5);
786 expr_ref neg_x_sgn_inf(m);
787 mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf);
788 mk_ite(x_is_zero, nan, neg_x_sgn_inf, v5);
789
790 // (x is 0) || (y is 0) -> x but with sign = x.sign ^ y.sign
791 m_simp.mk_or(x_is_zero, y_is_zero, c6);
792 expr_ref sign_xor(m);
793 m_simp.mk_xor(x_is_pos, y_is_pos, sign_xor);
794 mk_ite(sign_xor, nzero, pzero, v6);
795
796 // else comes the actual multiplication.
797 unsigned sbits = m_util.get_sbits(s);
798
799 expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
800 unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
801 unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
802
803 dbg_decouple("fpa2bv_mul_a_sig", a_sig);
804 dbg_decouple("fpa2bv_mul_a_exp", a_exp);
805 dbg_decouple("fpa2bv_mul_b_sig", b_sig);
806 dbg_decouple("fpa2bv_mul_b_exp", b_exp);
807
808 expr_ref a_lz_ext(m), b_lz_ext(m);
809 a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz);
810 b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz);
811
812 dbg_decouple("fpa2bv_mul_lz_a", a_lz);
813 dbg_decouple("fpa2bv_mul_lz_b", b_lz);
814
815 expr_ref a_sig_ext(m), b_sig_ext(m);
816 a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig);
817 b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig);
818
819 expr_ref a_exp_ext(m), b_exp_ext(m);
820 a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
821 b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
822
823 expr_ref res_sgn(m), res_sig(m), res_exp(m);
824 expr * signs[2] = { a_sgn, b_sgn };
825 res_sgn = m_bv_util.mk_bv_xor(2, signs);
826
827 dbg_decouple("fpa2bv_mul_res_sgn", res_sgn);
828
829 res_exp = m_bv_util.mk_bv_add(
830 m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
831 m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
832
833 expr_ref product(m);
834 product = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext);
835
836 dbg_decouple("fpa2bv_mul_product", product);
837
838 SASSERT(m_bv_util.get_bv_size(product) == 2*sbits);
839
840 expr_ref h_p(m), l_p(m), rbits(m);
841 h_p = m_bv_util.mk_extract(2*sbits-1, sbits, product);
842 l_p = m_bv_util.mk_extract(sbits-1, 0, product);
843
844 if (sbits >= 4) {
845 expr_ref sticky(m);
846 sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product));
847 rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, product), sticky);
848 }
849 else
850 rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - sbits));
851
852 SASSERT(m_bv_util.get_bv_size(rbits) == 4);
853 res_sig = m_bv_util.mk_concat(h_p, rbits);
854
855 round(s, rm, res_sgn, res_sig, res_exp, v7);
856
857 // And finally, we tie them together.
858 mk_ite(c6, v6, v7, result);
859 mk_ite(c5, v5, result, result);
860 mk_ite(c4, v4, result, result);
861 mk_ite(c3, v3, result, result);
862 mk_ite(c2, v2, result, result);
863 mk_ite(c1, v1, result, result);
864
865 SASSERT(is_well_sorted(m, result));
866
867 TRACE("fpa2bv_mul", tout << "MUL = " << mk_ismt2_pp(result, m) << std::endl; );
868 }
869
mk_div(func_decl * f,unsigned num,expr * const * args,expr_ref & result)870 void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
871 SASSERT(num == 3);
872 SASSERT(m_util.is_bv2rm(args[0]));
873 expr_ref rm(m), x(m), y(m);
874 rm = to_app(args[0])->get_arg(0);
875 x = args[1];
876 y = args[2];
877 mk_div(f->get_range(), rm, x, y, result);
878 }
879
mk_div(sort * s,expr_ref & rm,expr_ref & x,expr_ref & y,expr_ref & result)880 void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & y, expr_ref & result) {
881 expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
882 mk_nan(s, nan);
883 mk_nzero(s, nzero);
884 mk_pzero(s, pzero);
885 mk_ninf(s, ninf);
886 mk_pinf(s, pinf);
887
888 expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
889 expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
890 mk_is_nan(x, x_is_nan);
891 mk_is_zero(x, x_is_zero);
892 mk_is_pos(x, x_is_pos);
893 mk_is_inf(x, x_is_inf);
894 mk_is_nan(y, y_is_nan);
895 mk_is_zero(y, y_is_zero);
896 mk_is_pos(y, y_is_pos);
897 mk_is_inf(y, y_is_inf);
898
899 dbg_decouple("fpa2bv_div_x_is_nan", x_is_nan);
900 dbg_decouple("fpa2bv_div_x_is_zero", x_is_zero);
901 dbg_decouple("fpa2bv_div_x_is_pos", x_is_pos);
902 dbg_decouple("fpa2bv_div_x_is_inf", x_is_inf);
903 dbg_decouple("fpa2bv_div_y_is_nan", y_is_nan);
904 dbg_decouple("fpa2bv_div_y_is_zero", y_is_zero);
905 dbg_decouple("fpa2bv_div_y_is_pos", y_is_pos);
906 dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf);
907
908 expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m);
909 expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m);
910
911 // (x is NaN) || (y is NaN) -> NaN
912 m_simp.mk_or(x_is_nan, y_is_nan, c1);
913 v1 = nan;
914
915 // (x is +oo) -> if (y is oo) then NaN else inf with y's sign.
916 mk_is_pinf(x, c2);
917 expr_ref y_sgn_inf(m);
918 mk_ite(y_is_pos, pinf, ninf, y_sgn_inf);
919 mk_ite(y_is_inf, nan, y_sgn_inf, v2);
920
921 // (y is +oo) -> if (x is oo) then NaN else 0 with sign x.sgn ^ y.sgn
922 mk_is_pinf(y, c3);
923 expr_ref xy_zero(m), signs_xor(m);
924 m_simp.mk_xor(x_is_pos, y_is_pos, signs_xor);
925 mk_ite(signs_xor, nzero, pzero, xy_zero);
926 mk_ite(x_is_inf, nan, xy_zero, v3);
927
928 // (x is -oo) -> if (y is oo) then NaN else inf with -y's sign.
929 mk_is_ninf(x, c4);
930 expr_ref neg_y_sgn_inf(m);
931 mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf);
932 mk_ite(y_is_inf, nan, neg_y_sgn_inf, v4);
933
934 // (y is -oo) -> if (x is oo) then NaN else 0 with sign x.sgn ^ y.sgn
935 mk_is_ninf(y, c5);
936 mk_ite(x_is_inf, nan, xy_zero, v5);
937
938 // (y is 0) -> if (x is 0) then NaN else inf with xor sign.
939 c6 = y_is_zero;
940 expr_ref sgn_inf(m);
941 mk_ite(signs_xor, ninf, pinf, sgn_inf);
942 mk_ite(x_is_zero, nan, sgn_inf, v6);
943
944 // (x is 0) -> result is zero with sgn = x.sgn^y.sgn
945 // This is a special case to avoid problems with the unpacking of zero.
946 c7 = x_is_zero;
947 mk_ite(signs_xor, nzero, pzero, v7);
948
949 // else comes the actual division.
950 unsigned ebits = m_util.get_ebits(s);
951 unsigned sbits = m_util.get_sbits(s);
952 if (ebits > sbits)
953 throw default_exception("division with ebits > sbits not supported");
954 SASSERT(ebits <= sbits);
955
956 expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
957 unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
958 unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
959
960 unsigned extra_bits = sbits+2;
961 expr_ref a_sig_ext(m), b_sig_ext(m);
962 a_sig_ext = m_bv_util.mk_concat(a_sig, m_bv_util.mk_numeral(0, sbits + extra_bits));
963 b_sig_ext = m_bv_util.mk_zero_extend(sbits + extra_bits, b_sig);
964
965 expr_ref a_exp_ext(m), b_exp_ext(m);
966 a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
967 b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
968
969 expr_ref res_sgn(m), res_sig(m), res_exp(m);
970 expr * signs[2] = { a_sgn, b_sgn };
971 res_sgn = m_bv_util.mk_bv_xor(2, signs);
972
973 expr_ref a_lz_ext(m), b_lz_ext(m);
974 a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz);
975 b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz);
976
977 res_exp = m_bv_util.mk_bv_sub(
978 m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
979 m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
980
981 expr_ref quotient(m);
982 // b_sig_ext can't be 0 here, so it's safe to use OP_BUDIV_I
983 quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, a_sig_ext, b_sig_ext);
984
985 dbg_decouple("fpa2bv_div_quotient", quotient);
986
987 SASSERT(m_bv_util.get_bv_size(quotient) == (sbits + sbits + extra_bits));
988
989 expr_ref sticky(m);
990 sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(extra_bits-2, 0, quotient));
991 res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(extra_bits+sbits+1, extra_bits-1, quotient), sticky);
992
993 SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
994
995 expr_ref res_sig_lz(m);
996 mk_leading_zeros(res_sig, sbits + 4, res_sig_lz);
997 dbg_decouple("fpa2bv_div_res_sig_lz", res_sig_lz);
998 expr_ref res_sig_shift_amount(m);
999 res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4));
1000 dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount);
1001 expr_ref shift_cond(m);
1002 shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4));
1003 expr_ref res_sig_shifted(m), res_exp_shifted(m);
1004 res_sig_shifted = m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount);
1005 res_exp_shifted = m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits + 1, 0, res_sig_shift_amount));
1006 m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig);
1007 m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp);
1008
1009 round(s, rm, res_sgn, res_sig, res_exp, v8);
1010
1011 // And finally, we tie them together.
1012 mk_ite(c7, v7, v8, result);
1013 mk_ite(c6, v6, result, result);
1014 mk_ite(c5, v5, result, result);
1015 mk_ite(c4, v4, result, result);
1016 mk_ite(c3, v3, result, result);
1017 mk_ite(c2, v2, result, result);
1018 mk_ite(c1, v1, result, result);
1019
1020 SASSERT(is_well_sorted(m, result));
1021
1022 TRACE("fpa2bv_div", tout << "DIV = " << mk_ismt2_pp(result, m) << std::endl; );
1023 }
1024
mk_rem(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1025 void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1026 SASSERT(num == 2);
1027 expr_ref x(m), y(m);
1028 x = args[0];
1029 y = args[1];
1030 mk_rem(f->get_range(), x, y, result);
1031 }
1032
mk_rem(sort * s,expr_ref & x,expr_ref & y,expr_ref & result)1033 void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) {
1034 TRACE("fpa2bv_rem", tout << "X = " << mk_ismt2_pp(x, m) << std::endl;
1035 tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;);
1036
1037 expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
1038 mk_nan(s, nan);
1039 mk_nzero(s, nzero);
1040 mk_pzero(s, pzero);
1041 mk_ninf(s, ninf);
1042 mk_pinf(s, pinf);
1043
1044 expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m);
1045 expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m);
1046 mk_is_nan(x, x_is_nan);
1047 mk_is_zero(x, x_is_zero);
1048 mk_is_pos(x, x_is_pos);
1049 mk_is_neg(x, x_is_neg);
1050 mk_is_inf(x, x_is_inf);
1051 mk_is_nan(y, y_is_nan);
1052 mk_is_zero(y, y_is_zero);
1053 mk_is_pos(y, y_is_pos);
1054 mk_is_neg(y, y_is_neg);
1055 mk_is_inf(y, y_is_inf);
1056
1057 dbg_decouple("fpa2bv_rem_x_is_nan", x_is_nan);
1058 dbg_decouple("fpa2bv_rem_x_is_zero", x_is_zero);
1059 dbg_decouple("fpa2bv_rem_x_is_pos", x_is_pos);
1060 dbg_decouple("fpa2bv_rem_x_is_inf", x_is_inf);
1061 dbg_decouple("fpa2bv_rem_y_is_nan", y_is_nan);
1062 dbg_decouple("fpa2bv_rem_y_is_zero", y_is_zero);
1063 dbg_decouple("fpa2bv_rem_y_is_pos", y_is_pos);
1064 dbg_decouple("fpa2bv_rem_y_is_inf", y_is_inf);
1065
1066 expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m);
1067 expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m);
1068
1069 // (x is NaN) || (y is NaN) -> NaN
1070 m_simp.mk_or(x_is_nan, y_is_nan, c1);
1071 v1 = nan;
1072
1073 // (x is +-oo) -> NaN
1074 c2 = x_is_inf;
1075 v2 = nan;
1076
1077 // (y is +-oo) -> x
1078 c3 = y_is_inf;
1079 v3 = x;
1080
1081 // (y is 0) -> NaN.
1082 c4 = y_is_zero;
1083 v4 = nan;
1084
1085 // (x is 0) -> x
1086 c5 = x_is_zero;
1087 v5 = pzero;
1088
1089 // exp(x) < exp(y) -> x
1090 unsigned ebits = m_util.get_ebits(s);
1091 unsigned sbits = m_util.get_sbits(s);
1092 expr_ref x_sgn(m), x_sig(m), x_exp(m);
1093 expr_ref y_sgn(m), y_sig(m), y_exp(m);
1094 split_fp(x, x_sgn, x_exp, x_sig);
1095 split_fp(y, y_sgn, y_exp, y_sig);
1096 expr_ref one_ebits(m), y_exp_m1(m), xe_lt_yem1(m), ye_neq_zero(m);
1097 one_ebits = m_bv_util.mk_numeral(1, ebits);
1098 y_exp_m1 = m_bv_util.mk_bv_sub(y_exp, one_ebits);
1099 BVULT(x_exp, y_exp_m1, xe_lt_yem1);
1100 ye_neq_zero = m.mk_not(m.mk_eq(y_exp, m_bv_util.mk_numeral(0, ebits)));
1101 c6 = m.mk_and(ye_neq_zero, xe_lt_yem1);
1102 v6 = x;
1103
1104 expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
1105 expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
1106 unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
1107 unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
1108
1109 dbg_decouple("fpa2bv_rem_a_sgn", a_sgn);
1110 dbg_decouple("fpa2bv_rem_a_sig", a_sig);
1111 dbg_decouple("fpa2bv_rem_a_exp", a_exp);
1112 dbg_decouple("fpa2bv_rem_a_lz", a_lz);
1113 dbg_decouple("fpa2bv_rem_b_sgn", b_sgn);
1114 dbg_decouple("fpa2bv_rem_b_sig", b_sig);
1115 dbg_decouple("fpa2bv_rem_b_exp", b_exp);
1116 dbg_decouple("fpa2bv_rem_b_lz", b_lz);
1117
1118 // else the actual remainder.
1119 // max. exponent difference is (2^ebits) - 3
1120 const mpz & two_to_ebits = fu().fm().m_powers2(ebits);
1121 scoped_mpz max_exp_diff(m_mpz_manager);
1122 m_mpz_manager.sub(two_to_ebits, 3, max_exp_diff);
1123 if (m_mpz_manager.gt(max_exp_diff, INT32_MAX))
1124 // because zero-extend allows only int params...
1125 throw rewriter_exception("Maximum exponent difference in fp.rem does not fit into a signed int. Huge exponents in fp.rem are not supported.");
1126
1127 expr_ref a_exp_ext(m), b_exp_ext(m);
1128 a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
1129 b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
1130
1131 expr_ref a_lz_ext(m), b_lz_ext(m);
1132 a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz);
1133 b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz);
1134
1135 expr_ref exp_diff(m), neg_exp_diff(m), exp_diff_is_neg(m), exp_diff_ge_zero(m), exp_diff_is_zero(m);
1136 exp_diff = m_bv_util.mk_bv_sub(
1137 m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
1138 m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
1139 neg_exp_diff = m_bv_util.mk_bv_neg(exp_diff);
1140 exp_diff_is_neg = m_bv_util.mk_sle(exp_diff, m_bv_util.mk_numeral(0, ebits+2));
1141 exp_diff_is_zero = m.mk_eq(exp_diff, m_bv_util.mk_numeral(0, ebits+2));
1142 exp_diff_ge_zero = m_bv_util.mk_sle(m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp_diff)), exp_diff);
1143 dbg_decouple("fpa2bv_rem_exp_diff", exp_diff);
1144
1145 // CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal,
1146 // but calculating this via successive approx. of rem = x - y * nearest(x/y)
1147 // as in mpf::rem creates huge circuits, too. Lazy instantiation seems the
1148 // way to go in the long run (using the lazy bit-blaster helps on simple instances).
1149 expr_ref lshift(m), rshift(m), shifted(m), huge_rem(m), huge_div(m), huge_div_is_even(m);
1150 expr_ref a_sig_ext_l = a_sig, b_sig_ext_l = b_sig;
1151 scoped_mpz remaining(m_mpz_manager);
1152 m_mpz_manager.set(remaining, max_exp_diff);
1153 while (m_mpz_manager.gt(remaining, INT32_MAX)) {
1154 SASSERT(false); // zero-extend ast's expect int params which would overflow.
1155 a_sig_ext_l = m_bv_util.mk_zero_extend(INT32_MAX, a_sig_ext_l);
1156 b_sig_ext_l = m_bv_util.mk_zero_extend(INT32_MAX, b_sig_ext_l);
1157 m_mpz_manager.sub(remaining, INT32_MAX, remaining);
1158 }
1159 if (!m_mpz_manager.is_zero(remaining)) {
1160 unsigned rn = m_mpz_manager.get_uint(remaining);
1161 a_sig_ext_l = m_bv_util.mk_zero_extend(rn, a_sig_ext_l);
1162 b_sig_ext_l = m_bv_util.mk_zero_extend(rn, b_sig_ext_l);
1163 }
1164 expr_ref a_sig_ext(m), b_sig_ext(m);
1165 a_sig_ext = m_bv_util.mk_concat(a_sig_ext_l, m_bv_util.mk_numeral(0, 3));
1166 b_sig_ext = m_bv_util.mk_concat(b_sig_ext_l, m_bv_util.mk_numeral(0, 3));
1167
1168 scoped_mpz max_exp_diff_adj(m_mpz_manager);
1169 m_mpz_manager.add(max_exp_diff, sbits, max_exp_diff_adj);
1170 m_mpz_manager.sub(max_exp_diff_adj, ebits, max_exp_diff_adj);
1171 m_mpz_manager.add(max_exp_diff_adj, 1, max_exp_diff_adj);
1172 expr_ref edr_tmp = exp_diff, nedr_tmp = neg_exp_diff;
1173 m_mpz_manager.set(remaining, max_exp_diff_adj);
1174 if (m_mpz_manager.gt(remaining, INT32_MAX))
1175 throw default_exception("zero extension bit-vector types are too large; would exhaust memory");
1176 if (!m_mpz_manager.is_zero(remaining)) {
1177 edr_tmp = m_bv_util.mk_zero_extend(m_mpz_manager.get_uint(remaining), edr_tmp);
1178 nedr_tmp = m_bv_util.mk_zero_extend(m_mpz_manager.get_uint(remaining), nedr_tmp);
1179 }
1180 lshift = edr_tmp;
1181 rshift = nedr_tmp;
1182
1183 shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift),
1184 m_bv_util.mk_bv_shl(a_sig_ext, lshift));
1185 huge_rem = m_bv_util.mk_bv_urem(shifted, b_sig_ext);
1186 huge_div = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, shifted, b_sig_ext);
1187 huge_div_is_even = m.mk_eq(m_bv_util.mk_extract(0, 0, huge_div), m_bv_util.mk_numeral(0, 1));
1188 SASSERT(is_well_sorted(m, huge_rem));
1189 dbg_decouple("fpa2bv_rem_exp_diff_is_neg", exp_diff_is_neg);
1190 dbg_decouple("fpa2bv_rem_lshift", lshift);
1191 dbg_decouple("fpa2bv_rem_rshift", rshift);
1192 dbg_decouple("fpa2bv_rem_huge_rem", huge_rem);
1193 dbg_decouple("fpa2bv_rem_huge_div", huge_div);
1194
1195 expr_ref rndd_sgn(m), rndd_exp(m), rndd_sig(m), rne_bv(m), rndd_sig_lz(m);
1196 rndd_sgn = a_sgn;
1197 rndd_exp = m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext);
1198 rndd_sig = m_bv_util.mk_extract(sbits+3, 0, huge_rem);
1199 rne_bv = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3);
1200 mk_leading_zeros(rndd_sig, ebits+2, rndd_sig_lz);
1201 dbg_decouple("fpa2bv_rem_rndd_sgn", rndd_sgn);
1202 dbg_decouple("fpa2bv_rem_rndd_sig", rndd_sig);
1203 dbg_decouple("fpa2bv_rem_rndd_sig_lz", rndd_sig_lz);
1204 dbg_decouple("fpa2bv_rem_rndd_exp", rndd_exp);
1205
1206 SASSERT(m_bv_util.get_bv_size(rndd_exp) == ebits+2);
1207 SASSERT(m_bv_util.get_bv_size(y_exp_m1) == ebits);
1208
1209 expr_ref rndd_exp_eq_y_exp(m), rndd_exp_eq_y_exp_m1(m), y_sig_le_rndd_sig(m);
1210 rndd_exp_eq_y_exp = m.mk_eq(rndd_sig_lz, m_bv_util.mk_numeral(1, ebits+2));
1211 rndd_exp_eq_y_exp_m1 = m.mk_eq(rndd_sig_lz, m_bv_util.mk_numeral(2, ebits+2));
1212 dbg_decouple("fpa2bv_rem_rndd_exp_eq_y_exp_m1", rndd_exp_eq_y_exp_m1);
1213
1214 expr_ref y_sig_ext(m), y_sig_eq_rndd_sig(m);
1215 y_sig_ext = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(2, b_sig), m_bv_util.mk_numeral(0, 2));
1216 y_sig_le_rndd_sig = m_bv_util.mk_sle(y_sig_ext, rndd_sig);
1217 y_sig_eq_rndd_sig = m.mk_eq(y_sig_ext, rndd_sig);
1218 dbg_decouple("fpa2bv_rem_y_sig_ext", y_sig_ext);
1219 dbg_decouple("fpa2bv_rem_y_sig_le_rndd_sig", y_sig_le_rndd_sig);
1220 dbg_decouple("fpa2bv_rem_y_sig_eq_rndd_sig", y_sig_eq_rndd_sig);
1221
1222 expr_ref adj_cnd(m);
1223 adj_cnd = m.mk_or(m.mk_and(rndd_exp_eq_y_exp, y_sig_le_rndd_sig),
1224 m.mk_and(rndd_exp_eq_y_exp_m1, y_sig_le_rndd_sig, m.mk_not(y_sig_eq_rndd_sig)),
1225 m.mk_and(rndd_exp_eq_y_exp_m1, y_sig_eq_rndd_sig, m.mk_not(huge_div_is_even)));
1226 dbg_decouple("fpa2bv_rem_adj_cnd", adj_cnd);
1227
1228 expr_ref rndd(m), rounded_sub_y(m), rounded_add_y(m), add_cnd(m), adjusted(m);
1229 round(s, rne_bv, rndd_sgn, rndd_sig, rndd_exp, rndd);
1230 mk_sub(s, rne_bv, rndd, y, rounded_sub_y);
1231 mk_add(s, rne_bv, rndd, y, rounded_add_y);
1232 add_cnd = m.mk_not(m.mk_eq(rndd_sgn, b_sgn));
1233 mk_ite(add_cnd, rounded_add_y, rounded_sub_y, adjusted);
1234 mk_ite(adj_cnd, adjusted, rndd, v7);
1235 dbg_decouple("fpa2bv_rem_add_cnd", add_cnd);
1236 dbg_decouple("fpa2bv_rem_adj_cnd", adj_cnd);
1237 dbg_decouple("fpa2bv_rem_rndd", rndd);
1238
1239 // And finally, we tie them together.
1240 mk_ite(c6, v6, v7, result);
1241 mk_ite(c5, v5, result, result);
1242 mk_ite(c4, v4, result, result);
1243 mk_ite(c3, v3, result, result);
1244 mk_ite(c2, v2, result, result);
1245 mk_ite(c1, v1, result, result);
1246
1247 expr_ref result_is_zero(m), zeros(m);
1248 mk_is_zero(result, result_is_zero);
1249 mk_ite(x_is_pos, pzero, nzero, zeros);
1250 mk_ite(result_is_zero, zeros, result, result);
1251
1252 SASSERT(is_well_sorted(m, result));
1253
1254 TRACE("fpa2bv_rem", tout << "REM = " << mk_ismt2_pp(result, m) << std::endl; );
1255 }
1256
mk_abs(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1257 void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1258 SASSERT(num == 1);
1259 expr_ref x(m);
1260 x = args[0];
1261 mk_abs(f->get_range(), x, result);
1262 }
1263
mk_abs(sort * s,expr_ref & x,expr_ref & result)1264 void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) {
1265 expr_ref sgn(m), sig(m), exp(m);
1266 split_fp(x, sgn, exp, sig);
1267 result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), exp, sig);
1268 }
1269
mk_min_i(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1270 void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1271 func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_MIN, 0, nullptr, num, args), m);
1272 mk_min(fu, num, args, result);
1273 }
1274
mk_max_i(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1275 void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1276 func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_MAX, 0, nullptr, num, args), m);
1277 mk_max(fu, num, args, result);
1278 }
1279
mk_min(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1280 void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1281 SASSERT(num == 2);
1282
1283 expr * x = args[0], * y = args[1];
1284
1285 expr_ref x_sgn(m), x_sig(m), x_exp(m);
1286 expr_ref y_sgn(m), y_sig(m), y_exp(m);
1287 split_fp(x, x_sgn, x_exp, x_sig);
1288 split_fp(y, y_sgn, y_exp, y_sig);
1289
1290 expr_ref bv0(m), bv1(m);
1291 bv0 = m_bv_util.mk_numeral(0, 1);
1292 bv1 = m_bv_util.mk_numeral(1, 1);
1293
1294 expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), xy_are_zero(m);
1295 mk_is_nan(x, x_is_nan);
1296 mk_is_nan(y, y_is_nan);
1297 mk_is_zero(x, x_is_zero);
1298 mk_is_zero(y, y_is_zero);
1299 xy_are_zero = m.mk_and(x_is_zero, y_is_zero);
1300
1301 expr_ref x_is_pos(m), x_is_neg(m);
1302 expr_ref y_is_pos(m), y_is_neg(m);
1303 expr_ref pn(m), np(m), pn_or_np_zeros(m);
1304 mk_is_pos(x, x_is_pos);
1305 mk_is_pos(y, y_is_pos);
1306 mk_is_neg(x, x_is_neg);
1307 mk_is_neg(y, y_is_neg);
1308 pn_or_np_zeros = m.mk_and(xy_are_zero, m.mk_not(m.mk_eq(x_sgn, y_sgn)));
1309
1310 expr_ref unspec(m);
1311 unspec = mk_min_max_unspecified(f, x, y);
1312
1313 expr_ref x_lt_y(m);
1314 mk_float_lt(f, num, args, x_lt_y);
1315
1316 mk_ite(x_lt_y, x, y, result);
1317 mk_ite(xy_are_zero, y, result, result);
1318 mk_ite(pn_or_np_zeros, unspec, result, result);
1319 mk_ite(y_is_nan, x, result, result);
1320 mk_ite(x_is_nan, y, result, result);
1321
1322 SASSERT(is_well_sorted(m, result));
1323 }
1324
mk_max(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1325 void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1326 SASSERT(num == 2);
1327
1328 expr * x = args[0], *y = args[1];
1329
1330 expr_ref x_sgn(m), x_sig(m), x_exp(m);
1331 expr_ref y_sgn(m), y_sig(m), y_exp(m);
1332 split_fp(x, x_sgn, x_exp, x_sig);
1333 split_fp(y, y_sgn, y_exp, y_sig);
1334
1335 expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), xy_are_zero(m);
1336 mk_is_nan(x, x_is_nan);
1337 mk_is_nan(y, y_is_nan);
1338 mk_is_zero(x, x_is_zero);
1339 mk_is_zero(y, y_is_zero);
1340 xy_are_zero = m.mk_and(x_is_zero, y_is_zero);
1341
1342 expr_ref x_is_pos(m), x_is_neg(m);
1343 expr_ref y_is_pos(m), y_is_neg(m);
1344 expr_ref pn(m), np(m), pn_or_np_zeros(m);
1345 mk_is_pos(x, x_is_pos);
1346 mk_is_pos(y, y_is_pos);
1347 mk_is_neg(x, x_is_neg);
1348 mk_is_neg(y, y_is_neg);
1349 pn_or_np_zeros = m.mk_and(xy_are_zero, m.mk_not(m.mk_eq(x_sgn, y_sgn)));
1350
1351 expr_ref unspec(m);
1352 unspec = mk_min_max_unspecified(f, x, y);
1353
1354 expr_ref x_gt_y(m);
1355 mk_float_gt(f, num, args, x_gt_y);
1356
1357 mk_ite(x_gt_y, x, y, result);
1358 mk_ite(xy_are_zero, y, result, result);
1359 mk_ite(pn_or_np_zeros, unspec, result, result);
1360 mk_ite(y_is_nan, x, result, result);
1361 mk_ite(x_is_nan, y, result, result);
1362
1363 SASSERT(is_well_sorted(m, result));
1364 }
1365
mk_min_max_unspecified(func_decl * f,expr * x,expr * y)1366 expr_ref fpa2bv_converter::mk_min_max_unspecified(func_decl * f, expr * x, expr * y) {
1367 unsigned ebits = m_util.get_ebits(f->get_range());
1368 unsigned sbits = m_util.get_sbits(f->get_range());
1369 expr_ref res(m);
1370
1371 // The only cases in which min/max is unspecified for is when the arguments are +0.0 and -0.0.
1372 // There is no "hardware interpretation" for fp.min/fp.max.
1373
1374 std::pair<app*, app*> decls(0, 0);
1375 if (!m_min_max_ufs.find(f, decls)) {
1376 decls.first = m.mk_fresh_const(nullptr, m_bv_util.mk_sort(1));
1377 decls.second = m.mk_fresh_const(nullptr, m_bv_util.mk_sort(1));
1378 m_min_max_ufs.insert(f, decls);
1379 m.inc_ref(f);
1380 m.inc_ref(decls.first);
1381 m.inc_ref(decls.second);
1382 }
1383
1384 expr_ref pn(m), np(m);
1385 pn = m_util.mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
1386 np = m_util.mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
1387
1388 expr_ref x_is_pzero(m), y_is_nzero(m), xyzero(m);
1389 mk_is_pzero(x, x_is_pzero);
1390 mk_is_nzero(y, y_is_nzero);
1391 m_simp.mk_and(x_is_pzero, y_is_nzero, xyzero);
1392 mk_ite(xyzero, pn, np, res);
1393
1394 return res;
1395 }
1396
mk_fma(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1397 void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1398 SASSERT(num == 4);
1399 SASSERT(m_util.is_bv2rm(args[0]));
1400
1401 // fusedma means (x * y) + z
1402 expr_ref rm(m), x(m), y(m), z(m);
1403 rm = to_app(args[0])->get_arg(0);
1404 x = args[1];
1405 y = args[2];
1406 z = args[3];
1407
1408 expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
1409 mk_nan(f, nan);
1410 mk_nzero(f, nzero);
1411 mk_pzero(f, pzero);
1412 mk_ninf(f, ninf);
1413 mk_pinf(f, pinf);
1414
1415 expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m);
1416 expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m);
1417 expr_ref z_is_nan(m), z_is_zero(m), z_is_pos(m), z_is_neg(m), z_is_inf(m);
1418 mk_is_nan(x, x_is_nan);
1419 mk_is_zero(x, x_is_zero);
1420 mk_is_pos(x, x_is_pos);
1421 mk_is_neg(x, x_is_neg);
1422 mk_is_inf(x, x_is_inf);
1423 mk_is_nan(y, y_is_nan);
1424 mk_is_zero(y, y_is_zero);
1425 mk_is_pos(y, y_is_pos);
1426 mk_is_neg(y, y_is_neg);
1427 mk_is_inf(y, y_is_inf);
1428 mk_is_nan(z, z_is_nan);
1429 mk_is_zero(z, z_is_zero);
1430 mk_is_pos(z, z_is_pos);
1431 mk_is_neg(z, z_is_neg);
1432 mk_is_inf(z, z_is_inf);
1433
1434 expr_ref rm_is_to_neg(m);
1435 mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
1436
1437 dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan);
1438 dbg_decouple("fpa2bv_fma_x_is_zero", x_is_zero);
1439 dbg_decouple("fpa2bv_fma_x_is_pos", x_is_pos);
1440 dbg_decouple("fpa2bv_fma_x_is_inf", x_is_inf);
1441 dbg_decouple("fpa2bv_fma_y_is_nan", y_is_nan);
1442 dbg_decouple("fpa2bv_fma_y_is_zero", y_is_zero);
1443 dbg_decouple("fpa2bv_fma_y_is_pos", y_is_pos);
1444 dbg_decouple("fpa2bv_fma_y_is_inf", y_is_inf);
1445 dbg_decouple("fpa2bv_fma_z_is_nan", z_is_nan);
1446 dbg_decouple("fpa2bv_fma_z_is_zero", z_is_zero);
1447 dbg_decouple("fpa2bv_fma_z_is_pos", z_is_pos);
1448 dbg_decouple("fpa2bv_fma_z_is_inf", z_is_inf);
1449
1450 expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m);
1451 expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m);
1452
1453 expr_ref inf_xor(m), inf_cond(m);
1454 m_simp.mk_xor(x_is_neg, y_is_neg, inf_xor);
1455 m_simp.mk_xor(inf_xor, z_is_neg, inf_xor);
1456 m_simp.mk_and(z_is_inf, inf_xor, inf_cond);
1457
1458 // (x is NaN) || (y is NaN) || (z is Nan) -> NaN
1459 m_simp.mk_or(x_is_nan, y_is_nan, z_is_nan, c1);
1460 v1 = nan;
1461
1462 // (x is +oo) -> if (y is 0) then NaN else inf with y's sign.
1463 mk_is_pinf(x, c2);
1464 expr_ref y_sgn_inf(m), inf_or(m);
1465 mk_ite(y_is_pos, pinf, ninf, y_sgn_inf);
1466 m_simp.mk_or(y_is_zero, inf_cond, inf_or);
1467 mk_ite(inf_or, nan, y_sgn_inf, v2);
1468
1469 // (y is +oo) -> if (x is 0) then NaN else inf with x's sign.
1470 mk_is_pinf(y, c3);
1471 expr_ref x_sgn_inf(m);
1472 mk_ite(x_is_pos, pinf, ninf, x_sgn_inf);
1473 m_simp.mk_or(x_is_zero, inf_cond, inf_or);
1474 mk_ite(inf_or, nan, x_sgn_inf, v3);
1475
1476 // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign.
1477 mk_is_ninf(x, c4);
1478 expr_ref neg_y_sgn_inf(m);
1479 mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf);
1480 m_simp.mk_or(y_is_zero, inf_cond, inf_or);
1481 mk_ite(inf_or, nan, neg_y_sgn_inf, v4);
1482
1483 // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign.
1484 mk_is_ninf(y, c5);
1485 expr_ref neg_x_sgn_inf(m);
1486 mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf);
1487 m_simp.mk_or(x_is_zero, inf_cond, inf_or);
1488 mk_ite(inf_or, nan, neg_x_sgn_inf, v5);
1489
1490 // z is +-INF -> z.
1491 mk_is_inf(z, c6);
1492 v6 = z;
1493
1494 // (x is 0) || (y is 0) -> z
1495 expr_ref c71(m), xy_sgn(m), xyz_sgn(m);
1496 m_simp.mk_or(x_is_zero, y_is_zero, c7);
1497 m_simp.mk_xor(x_is_neg, y_is_neg, xy_sgn);
1498
1499 m_simp.mk_xor(xy_sgn, z_is_neg, xyz_sgn);
1500 m_simp.mk_and(z_is_zero, xyz_sgn, c71);
1501
1502 expr_ref zero_cond(m), rm_is_not_to_neg(m);
1503 rm_is_not_to_neg = m.mk_not(rm_is_to_neg);
1504 m_simp.mk_ite(rm_is_to_neg, nzero, pzero, zero_cond);
1505 mk_ite(c71, zero_cond, z, v7);
1506
1507 // else comes the fused multiplication.
1508 expr_ref one_1(m), zero_1(m);
1509 one_1 = m_bv_util.mk_numeral(1, 1);
1510 zero_1 = m_bv_util.mk_numeral(0, 1);
1511
1512 unsigned ebits = m_util.get_ebits(f->get_range());
1513 unsigned sbits = m_util.get_sbits(f->get_range());
1514
1515 expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
1516 expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
1517 expr_ref c_sgn(m), c_sig(m), c_exp(m), c_lz(m);
1518 unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
1519 unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
1520 unpack(z, c_sgn, c_sig, c_exp, c_lz, true);
1521
1522 expr_ref a_lz_ext(m), b_lz_ext(m), c_lz_ext(m);
1523 a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz);
1524 b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz);
1525 c_lz_ext = m_bv_util.mk_zero_extend(2, c_lz);
1526
1527 expr_ref a_sig_ext(m), b_sig_ext(m);
1528 a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig);
1529 b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig);
1530
1531 expr_ref a_exp_ext(m), b_exp_ext(m), c_exp_ext(m);
1532 a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
1533 b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
1534 c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp);
1535
1536 dbg_decouple("fpa2bv_fma_a_sig", a_sig_ext);
1537 dbg_decouple("fpa2bv_fma_b_sig", b_sig_ext);
1538 dbg_decouple("fpa2bv_fma_c_sig", c_sig);
1539 dbg_decouple("fpa2bv_fma_a_exp", a_exp_ext);
1540 dbg_decouple("fpa2bv_fma_b_exp", b_exp_ext);
1541 dbg_decouple("fpa2bv_fma_c_exp", c_exp_ext);
1542 dbg_decouple("fpa2bv_fma_a_lz", a_lz_ext);
1543 dbg_decouple("fpa2bv_fma_b_lz", b_lz_ext);
1544 dbg_decouple("fpa2bv_fma_c_lz", c_lz_ext);
1545
1546 expr_ref mul_sgn(m), mul_sig(m), mul_exp(m);
1547 expr * signs[2] = { a_sgn, b_sgn };
1548
1549 mul_sgn = m_bv_util.mk_bv_xor(2, signs);
1550 dbg_decouple("fpa2bv_fma_mul_sgn", mul_sgn);
1551
1552 mul_exp = m_bv_util.mk_bv_add(
1553 m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
1554 m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
1555 dbg_decouple("fpa2bv_fma_mul_exp", mul_exp);
1556
1557 mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext);
1558 dbg_decouple("fpa2bv_fma_mul_sig", mul_sig);
1559
1560 SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits);
1561 SASSERT(m_bv_util.get_bv_size(mul_exp) == ebits + 2);
1562
1563 // The product has the form [-1][0].[2*sbits - 2].
1564
1565 // Extend c
1566 expr_ref c_sig_ext(m);
1567 c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits+2)));
1568 c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext);
1569 mul_sig = m_bv_util.mk_concat(mul_sig, m_bv_util.mk_numeral(0, 3));
1570
1571 SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits+3);
1572 SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2*sbits+3);
1573 dbg_decouple("fpa2bv_fma_c_sig_ext", c_sig_ext);
1574 dbg_decouple("fpa2bv_fma_c_exp_ext", c_exp_ext);
1575
1576 expr_ref swap_cond(m);
1577 swap_cond = m_bv_util.mk_sle(mul_exp, c_exp_ext);
1578 SASSERT(is_well_sorted(m, swap_cond));
1579 dbg_decouple("fpa2bv_fma_swap_cond", swap_cond);
1580
1581 expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m);
1582 m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn);
1583 m_simp.mk_ite(swap_cond, c_sig_ext, mul_sig, e_sig); // has 2 * sbits + 3
1584 m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2
1585 m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn);
1586 m_simp.mk_ite(swap_cond, mul_sig, c_sig_ext, f_sig); // has 2 * sbits + 3
1587 m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2
1588
1589 SASSERT(is_well_sorted(m, e_sgn));
1590 SASSERT(is_well_sorted(m, e_sig));
1591 SASSERT(is_well_sorted(m, e_exp));
1592 SASSERT(is_well_sorted(m, f_sgn));
1593 SASSERT(is_well_sorted(m, f_sig));
1594 SASSERT(is_well_sorted(m, f_exp));
1595
1596 SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+3);
1597 SASSERT(m_bv_util.get_bv_size(f_sig) == 2*sbits+3);
1598 SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2);
1599 SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2);
1600
1601 dbg_decouple("fpa2bv_fma_e_sig", e_sig);
1602 dbg_decouple("fpa2bv_fma_e_exp", e_exp);
1603 dbg_decouple("fpa2bv_fma_f_sig", f_sig);
1604 dbg_decouple("fpa2bv_fma_f_exp", f_exp);
1605
1606 expr_ref res_sgn(m), res_sig(m), res_exp(m);
1607
1608 expr_ref exp_delta(m);
1609 exp_delta = m_bv_util.mk_bv_sub(e_exp, f_exp);
1610 dbg_decouple("fpa2bv_fma_add_exp_delta", exp_delta);
1611
1612 // cap the delta
1613 expr_ref cap(m), cap_le_delta(m);
1614 cap = m_bv_util.mk_numeral(2*sbits+3, ebits+2);
1615 cap_le_delta = m_bv_util.mk_ule(cap, exp_delta);
1616 m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
1617 SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2);
1618 SASSERT(is_well_sorted(m, exp_delta));
1619 dbg_decouple("fpa2bv_fma_add_exp_delta_capped", exp_delta);
1620
1621 // Alignment shift with sticky bit computation.
1622 expr_ref shifted_big(m), shifted_f_sig(m);
1623 expr_ref alignment_sticky_raw(m), alignment_sticky(m);
1624 shifted_big = m_bv_util.mk_bv_lshr(
1625 m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)),
1626 m_bv_util.mk_zero_extend((3*sbits+3)-(ebits+2), exp_delta));
1627 shifted_f_sig = m_bv_util.mk_extract(3*sbits+2, sbits, shifted_big);
1628 alignment_sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big);
1629 alignment_sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, alignment_sticky_raw.get());
1630 dbg_decouple("fpa2bv_fma_shifted_f_sig", shifted_f_sig);
1631 dbg_decouple("fpa2bv_fma_f_sig_alignment_sticky", alignment_sticky);
1632 SASSERT(is_well_sorted(m, alignment_sticky));
1633 SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+3);
1634 SASSERT(is_well_sorted(m, shifted_f_sig));
1635
1636 // Significant addition.
1637 // Two extra bits for the sign and for catching overflows.
1638 e_sig = m_bv_util.mk_zero_extend(2, e_sig);
1639 shifted_f_sig = m_bv_util.mk_zero_extend(2, shifted_f_sig);
1640
1641 expr_ref eq_sgn(m);
1642 m_simp.mk_eq(e_sgn, f_sgn, eq_sgn);
1643 dbg_decouple("fpa2bv_fma_eq_sgn", eq_sgn);
1644
1645 SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+5);
1646 SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+5);
1647
1648 dbg_decouple("fpa2bv_fma_add_e_sig", e_sig);
1649 dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig);
1650
1651 expr_ref sum(m), e_plus_f(m), e_minus_f(m), sticky_wide(m);
1652 sticky_wide = m_bv_util.mk_zero_extend(2*sbits+4, alignment_sticky);
1653 e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig);
1654 e_plus_f = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(0, 0, e_plus_f), zero_1),
1655 m_bv_util.mk_bv_add(e_plus_f, sticky_wide),
1656 e_plus_f);
1657 e_minus_f = m_bv_util.mk_bv_sub(e_sig, shifted_f_sig);
1658 e_minus_f = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(0, 0, e_minus_f), zero_1),
1659 m_bv_util.mk_bv_sub(e_minus_f, sticky_wide),
1660 e_minus_f);
1661 SASSERT(is_well_sorted(m, shifted_f_sig));
1662 dbg_decouple("fpa2bv_fma_f_sig_or_sticky", shifted_f_sig);
1663
1664 m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum);
1665 SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits+5);
1666 SASSERT(is_well_sorted(m, sum));
1667 dbg_decouple("fpa2bv_fma_add_sum", sum);
1668
1669 expr_ref sign_bv(m), n_sum(m);
1670 sign_bv = m_bv_util.mk_extract(2*sbits+4, 2*sbits+4, sum);
1671 n_sum = m_bv_util.mk_bv_neg(sum);
1672 dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv);
1673 dbg_decouple("fpa2bv_fma_add_n_sum", n_sum);
1674
1675 expr_ref res_sig_eq(m), sig_abs(m);
1676 m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
1677 m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
1678 dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs);
1679
1680 family_id bvfid = m_bv_util.get_fid();
1681 expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
1682 expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m);
1683 not_e_sgn = m_bv_util.mk_bv_not(e_sgn);
1684 not_f_sgn = m_bv_util.mk_bv_not(f_sgn);
1685 not_sign_bv = m_bv_util.mk_bv_not(sign_bv);
1686 res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, f_sgn, sign_bv);
1687 res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv);
1688 res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn);
1689 expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
1690 res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
1691 dbg_decouple("fpa2bv_fma_res_sgn", res_sgn);
1692
1693 expr_ref is_sig_neg(m);
1694 is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2*sbits+4, 2*sbits+4, sig_abs));
1695 sig_abs = m.mk_ite(is_sig_neg, m_bv_util.mk_bv_neg(sig_abs), sig_abs);
1696 dbg_decouple("fpa2bv_fma_is_sig_neg", is_sig_neg);
1697
1698 // Result could have overflown into 4.xxx.
1699 SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+5);
1700 expr_ref extra(m), extra_is_zero(m);
1701 extra = m_bv_util.mk_extract(2*sbits+4, 2*sbits+3, sig_abs);
1702 extra_is_zero = m.mk_eq(extra, m_bv_util.mk_numeral(0, 2));
1703 dbg_decouple("fpa2bv_fma_extra", extra);
1704
1705 res_exp = m.mk_ite(extra_is_zero, e_exp, m_bv_util.mk_bv_add(e_exp, m_bv_util.mk_numeral(1, ebits + 2)));
1706
1707 // Renormalize
1708 expr_ref zero_e2(m), min_exp(m), sig_lz(m), max_exp_delta(m), sig_lz_capped(m), renorm_delta(m);
1709 zero_e2 = m_bv_util.mk_numeral(0, ebits + 2);
1710 mk_min_exp(ebits, min_exp);
1711 min_exp = m_bv_util.mk_sign_extend(2, min_exp);
1712 mk_leading_zeros(sig_abs, ebits+2, sig_lz);
1713 sig_lz = m_bv_util.mk_bv_sub(sig_lz, m_bv_util.mk_numeral(2, ebits+2));
1714 max_exp_delta = m_bv_util.mk_bv_sub(res_exp, min_exp);
1715 sig_lz_capped = m.mk_ite(m_bv_util.mk_sle(sig_lz, max_exp_delta), sig_lz, max_exp_delta);
1716 renorm_delta = m.mk_ite(m_bv_util.mk_sle(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2);
1717 res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta);
1718 sig_abs = m_bv_util.mk_bv_shl(sig_abs, m_bv_util.mk_zero_extend(2*sbits+3-ebits, renorm_delta));
1719 dbg_decouple("fpa2bv_fma_min_exp", min_exp);
1720 dbg_decouple("fpa2bv_fma_max_exp_delta", max_exp_delta);
1721 dbg_decouple("fpa2bv_fma_sig_lz", sig_lz);
1722 dbg_decouple("fpa2bv_fma_sig_lz_capped", sig_lz_capped);
1723 dbg_decouple("fpa2bv_fma_renorm_delta", renorm_delta);
1724
1725 unsigned too_short = 0;
1726 if (sbits < 5) {
1727 too_short = 6 - sbits + 1;
1728 sig_abs = m_bv_util.mk_concat(sig_abs, m_bv_util.mk_numeral(0, too_short));
1729 }
1730
1731 expr_ref sig_abs_h1(m), sticky_h1(m), sticky_h1_red(m), sig_abs_h1_f(m), res_sig_1(m);
1732 sticky_h1 = m_bv_util.mk_extract(sbits+too_short-2, 0, sig_abs);
1733 sig_abs_h1 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits-1+too_short, sig_abs);
1734 sticky_h1_red = m_bv_util.mk_zero_extend(sbits+5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get()));
1735 expr * sticky_h1_red_args[2] = { sig_abs_h1, sticky_h1_red };
1736 sig_abs_h1_f = m_bv_util.mk_bv_or(2, sticky_h1_red_args);
1737 res_sig_1 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h1_f);
1738 SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits+too_short-1);
1739 SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits+6);
1740 SASSERT(m_bv_util.get_bv_size(sticky_h1_red) == sbits+6);
1741 SASSERT(m_bv_util.get_bv_size(sig_abs_h1_f) == sbits+6);
1742 SASSERT(m_bv_util.get_bv_size(res_sig_1) == sbits+4);
1743
1744 expr_ref sig_abs_h2(m), sticky_h2(m), sticky_h2_red(m), sig_abs_h2_f(m), res_sig_2(m);
1745 sticky_h2 = m_bv_util.mk_extract(sbits+too_short-1, 0, sig_abs);
1746 sig_abs_h2 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits+too_short, sig_abs);
1747 sticky_h2_red = m_bv_util.mk_zero_extend(sbits+4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get()));
1748 expr * sticky_h2_red_args[2] = { sig_abs_h2, sticky_h2_red };
1749 sig_abs_h2_f = m_bv_util.mk_zero_extend(1, m_bv_util.mk_bv_or(2, sticky_h2_red_args));
1750 res_sig_2 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h2_f);
1751 SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits+too_short);
1752 SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits+5);
1753 SASSERT(m_bv_util.get_bv_size(sticky_h2_red) == sbits+5);
1754 SASSERT(m_bv_util.get_bv_size(sig_abs_h2_f) == sbits+6);
1755 SASSERT(m_bv_util.get_bv_size(res_sig_2) == sbits+4);
1756
1757 res_sig = m.mk_ite(extra_is_zero, res_sig_1, res_sig_2);
1758
1759 dbg_decouple("fpa2bv_fma_res_sig", res_sig);
1760 dbg_decouple("fpa2bv_fma_res_exp", res_exp);
1761 SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
1762
1763 expr_ref is_zero_sig(m), nil_sbits4(m);
1764 nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4);
1765 m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig);
1766 SASSERT(is_well_sorted(m, is_zero_sig));
1767
1768 dbg_decouple("fpa2bv_fma_is_zero_sig", is_zero_sig);
1769
1770 expr_ref zero_case(m);
1771 mk_ite(rm_is_to_neg, nzero, pzero, zero_case);
1772
1773 expr_ref rounded(m);
1774 round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded);
1775
1776 mk_ite(is_zero_sig, zero_case, rounded, v8);
1777
1778 // And finally, we tie them together.
1779 mk_ite(c7, v7, v8, result);
1780 mk_ite(c6, v6, result, result);
1781 mk_ite(c5, v5, result, result);
1782 mk_ite(c4, v4, result, result);
1783 mk_ite(c3, v3, result, result);
1784 mk_ite(c2, v2, result, result);
1785 mk_ite(c1, v1, result, result);
1786
1787 SASSERT(is_well_sorted(m, result));
1788
1789 TRACE("fpa2bv_fma_", tout << "FMA = " << mk_ismt2_pp(result, m) << std::endl; );
1790 }
1791
mk_sqrt(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1792 void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1793 SASSERT(num == 2);
1794 SASSERT(m_util.is_bv2rm(args[0]));
1795
1796 expr_ref rm(m), x(m);
1797 rm = to_app(args[0])->get_arg(0);
1798 x = args[1];
1799
1800 expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
1801 mk_nan(f, nan);
1802 mk_nzero(f, nzero);
1803 mk_pzero(f, pzero);
1804 mk_ninf(f, ninf);
1805 mk_pinf(f, pinf);
1806
1807 expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
1808 mk_is_nan(x, x_is_nan);
1809 mk_is_zero(x, x_is_zero);
1810 mk_is_pos(x, x_is_pos);
1811 mk_is_inf(x, x_is_inf);
1812
1813 expr_ref zero1(m), one1(m);
1814 zero1 = m_bv_util.mk_numeral(0, 1);
1815 one1 = m_bv_util.mk_numeral(1, 1);
1816
1817 expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m);
1818 expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m);
1819
1820 // (x is NaN) -> NaN
1821 c1 = x_is_nan;
1822 v1 = x;
1823
1824 // (x is +oo) -> +oo
1825 mk_is_pinf(x, c2);
1826 v2 = x;
1827
1828 // (x is +-0) -> +-0
1829 mk_is_zero(x, c3);
1830 v3 = x;
1831
1832 // (x < 0) -> NaN
1833 mk_is_neg(x, c4);
1834 v4 = nan;
1835
1836 // else comes the actual square root.
1837 unsigned ebits = m_util.get_ebits(f->get_range());
1838 unsigned sbits = m_util.get_sbits(f->get_range());
1839
1840 expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
1841 unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
1842
1843 dbg_decouple("fpa2bv_sqrt_sig", a_sig);
1844 dbg_decouple("fpa2bv_sqrt_exp", a_exp);
1845
1846 SASSERT(m_bv_util.get_bv_size(a_sig) == sbits);
1847 SASSERT(m_bv_util.get_bv_size(a_exp) == ebits);
1848
1849 expr_ref res_sgn(m), res_sig(m), res_exp(m);
1850
1851 res_sgn = zero1;
1852
1853 expr_ref real_exp(m);
1854 real_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(1, a_exp), m_bv_util.mk_zero_extend(1, a_lz));
1855 res_exp = m_bv_util.mk_sign_extend(2, m_bv_util.mk_extract(ebits, 1, real_exp));
1856
1857 expr_ref e_is_odd(m);
1858 e_is_odd = m.mk_eq(m_bv_util.mk_extract(0, 0, real_exp), one1);
1859
1860 dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd);
1861 dbg_decouple("fpa2bv_sqrt_real_exp", real_exp);
1862
1863 expr_ref sig_prime(m), a_z(m), z_a(m);
1864 a_z = m_bv_util.mk_concat(a_sig, zero1);
1865 z_a = m_bv_util.mk_concat(zero1, a_sig);
1866 m_simp.mk_ite(e_is_odd, a_z, z_a, sig_prime);
1867 SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1);
1868 dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime);
1869
1870 // This is algorithm 10.2 in the Handbook of Floating-Point Arithmetic
1871 expr_ref Q(m), R(m), S(m), T(m);
1872
1873 const mpz & p2 = fu().fm().m_powers2(sbits+3);
1874 Q = m_bv_util.mk_numeral(p2, sbits+5);
1875 R = m_bv_util.mk_bv_sub(m_bv_util.mk_concat(sig_prime, m_bv_util.mk_numeral(0, 4)), Q);
1876 S = Q;
1877
1878 for (unsigned i = 0; i < sbits + 3; i++) {
1879 dbg_decouple("fpa2bv_sqrt_Q", Q);
1880 dbg_decouple("fpa2bv_sqrt_R", R);
1881
1882 S = m_bv_util.mk_concat(zero1, m_bv_util.mk_extract(sbits+4, 1, S));
1883
1884 expr_ref twoQ_plus_S(m);
1885 twoQ_plus_S = m_bv_util.mk_bv_add(m_bv_util.mk_concat(Q, zero1), m_bv_util.mk_concat(zero1, S));
1886 T = m_bv_util.mk_bv_sub(m_bv_util.mk_concat(R, zero1), twoQ_plus_S);
1887
1888 dbg_decouple("fpa2bv_sqrt_T", T);
1889
1890 SASSERT(m_bv_util.get_bv_size(Q) == sbits + 5);
1891 SASSERT(m_bv_util.get_bv_size(R) == sbits + 5);
1892 SASSERT(m_bv_util.get_bv_size(S) == sbits + 5);
1893 SASSERT(m_bv_util.get_bv_size(T) == sbits + 6);
1894
1895 expr_ref t_lt_0(m), T_lsds5(m);
1896 T_lsds5 = m_bv_util.mk_extract(sbits + 5, sbits + 5, T);
1897 m_simp.mk_eq(T_lsds5, one1, t_lt_0);
1898
1899 expr * or_args[2] = { Q, S };
1900 expr_ref Q_or_S(m), R_shftd(m), T_lsds4(m);
1901 Q_or_S = m_bv_util.mk_bv_or(2, or_args);
1902 m_simp.mk_ite(t_lt_0, Q, Q_or_S, Q);
1903 R_shftd = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits + 3, 0, R), zero1);
1904 T_lsds4 = m_bv_util.mk_extract(sbits + 4, 0, T);
1905 m_simp.mk_ite(t_lt_0, R_shftd, T_lsds4, R);
1906 }
1907
1908 expr_ref is_exact(m), zero_sbits5(m);
1909 zero_sbits5 = m_bv_util.mk_numeral(0, sbits + 5);
1910 m_simp.mk_eq(R, zero_sbits5, is_exact);
1911 dbg_decouple("fpa2bv_sqrt_is_exact", is_exact);
1912
1913 expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m);
1914 last = m_bv_util.mk_extract(0, 0, Q);
1915 rest = m_bv_util.mk_extract(sbits+3, 1, Q);
1916 dbg_decouple("fpa2bv_sqrt_last", last);
1917 dbg_decouple("fpa2bv_sqrt_rest", rest);
1918 rest_ext = m_bv_util.mk_zero_extend(1, rest);
1919 expr_ref sticky(m), last_ext(m), one_sbits4(m);
1920 last_ext = m_bv_util.mk_zero_extend(sbits + 3, last);
1921 one_sbits4 = m_bv_util.mk_numeral(1, sbits + 4);
1922 m_simp.mk_ite(is_exact, last_ext, one_sbits4, sticky);
1923 expr * or_args[2] = { rest_ext, sticky };
1924 res_sig = m_bv_util.mk_bv_or(2, or_args);
1925
1926 SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
1927
1928 expr_ref rounded(m);
1929 round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded);
1930 v5 = rounded;
1931
1932 // And finally, we tie them together.
1933 mk_ite(c4, v4, v5, result);
1934 mk_ite(c3, v3, result, result);
1935 mk_ite(c2, v2, result, result);
1936 mk_ite(c1, v1, result, result);
1937
1938 SASSERT(is_well_sorted(m, result));
1939 }
1940
mk_round_to_integral(func_decl * f,unsigned num,expr * const * args,expr_ref & result)1941 void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
1942 SASSERT(num == 2);
1943 SASSERT(m_util.is_bv2rm(args[0]));
1944
1945 expr_ref rm(m), x(m);
1946 rm = to_app(args[0])->get_arg(0);
1947 x = args[1];
1948 mk_round_to_integral(f->get_range(), rm, x, result);
1949 }
1950
mk_round_to_integral(sort * s,expr_ref & rm,expr_ref & x,expr_ref & result)1951 void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result) {
1952 expr_ref rm_is_rta(m), rm_is_rte(m), rm_is_rtp(m), rm_is_rtn(m), rm_is_rtz(m);
1953 mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_rta);
1954 mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_rte);
1955 mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_rtp);
1956 mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_rtn);
1957 mk_is_rm(rm, BV_RM_TO_ZERO, rm_is_rtz);
1958
1959 expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
1960 mk_nan(s, nan);
1961 mk_nzero(s, nzero);
1962 mk_pzero(s, pzero);
1963
1964 expr_ref x_is_zero(m), x_is_pos(m), x_is_neg(m);
1965 mk_is_zero(x, x_is_zero);
1966 mk_is_pos(x, x_is_pos);
1967 mk_is_neg(x, x_is_neg);
1968
1969 dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero);
1970 dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos);
1971
1972 expr_ref c1(m), c2(m), c3(m), c4(m), c5(m);
1973 expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m);
1974
1975 // (x is NaN) -> NaN
1976 mk_is_nan(x, c1);
1977 v1 = nan;
1978
1979 // (x is +-oo) -> x
1980 mk_is_inf(x, c2);
1981 v2 = x;
1982
1983 // (x is +-0) -> x ; -0.0 -> -0.0, says IEEE754, Sec 5.9.
1984 mk_is_zero(x, c3);
1985 v3 = x;
1986
1987
1988 expr_ref one_1(m), zero_1(m);
1989 one_1 = m_bv_util.mk_numeral(1, 1);
1990 zero_1 = m_bv_util.mk_numeral(0, 1);
1991
1992 unsigned ebits = m_util.get_ebits(s);
1993 unsigned sbits = m_util.get_sbits(s);
1994
1995 expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
1996 unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
1997
1998 dbg_decouple("fpa2bv_r2i_unpacked_sgn", a_sgn);
1999 dbg_decouple("fpa2bv_r2i_unpacked_exp", a_exp);
2000 dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig);
2001 dbg_decouple("fpa2bv_r2i_unpacked_lz", a_lz);
2002
2003 expr_ref xzero(m), sgn_eq_1(m);
2004 sgn_eq_1 = m.mk_eq(a_sgn, one_1);
2005 mk_ite(sgn_eq_1, nzero, pzero, xzero);
2006
2007 // exponent < 0 -> 0/1
2008 expr_ref exp_lt_zero(m), exp_h(m), x_is_denormal(m);
2009 mk_is_denormal(x, x_is_denormal);
2010 exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp);
2011 m_simp.mk_eq(exp_h, one_1, exp_lt_zero);
2012 dbg_decouple("fpa2bv_r2i_exp_lt_zero", exp_lt_zero);
2013 c4 = m.mk_or(exp_lt_zero, x_is_denormal);
2014
2015 expr_ref pone(m), none(m), xone(m), c421(m), c422(m), c423(m), t1(m), t2(m), tie(m), v42(m), exp_lt_m1(m);
2016 mk_one(s, zero_1, pone);
2017 mk_one(s, one_1, none);
2018 mk_ite(sgn_eq_1, none, pone, xone);
2019
2020 expr_ref pow_2_sbitsm1(m), m1(m);
2021 pow_2_sbitsm1 = m_bv_util.mk_numeral(fu().fm().m_powers2(sbits - 1), sbits);
2022 m1 = m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits));
2023 m_simp.mk_eq(a_sig, pow_2_sbitsm1, t1);
2024 m_simp.mk_eq(a_exp, m1, t2);
2025 m_simp.mk_and(t1, t2, tie);
2026 dbg_decouple("fpa2bv_r2i_c42_tie", tie);
2027
2028 m_simp.mk_and(tie, rm_is_rte, c421);
2029 m_simp.mk_and(tie, rm_is_rta, c422);
2030 c423 = m_bv_util.mk_sle(a_exp, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(2, ebits)));
2031
2032 dbg_decouple("fpa2bv_r2i_c421", c421);
2033 dbg_decouple("fpa2bv_r2i_c422", c422);
2034 dbg_decouple("fpa2bv_r2i_c423", c423);
2035
2036 v42 = xone;
2037 mk_ite(c423, xzero, v42, v42);
2038 mk_ite(c422, xone, v42, v42);
2039 mk_ite(c421, xzero, v42, v42);
2040
2041 expr_ref v4_rtn(m), v4_rtp(m);
2042 mk_ite(x_is_neg, nzero, pone, v4_rtp);
2043 mk_ite(x_is_neg, none, pzero, v4_rtn);
2044
2045 mk_ite(rm_is_rtp, v4_rtp, v42, v4);
2046 mk_ite(rm_is_rtn, v4_rtn, v4, v4);
2047 mk_ite(rm_is_rtz, xzero, v4, v4);
2048
2049 SASSERT(is_well_sorted(m, v4));
2050
2051 // exponent >= sbits-1 -> x
2052 expr_ref exp_is_large(m);
2053 exp_is_large = log2(sbits-1)+1 <= ebits-1 ?
2054 m_bv_util.mk_sle(m_bv_util.mk_numeral(sbits-1, ebits), a_exp) :
2055 m.mk_false();
2056 dbg_decouple("fpa2bv_r2i_exp_is_large", exp_is_large);
2057 c5 = exp_is_large;
2058 v5 = x;
2059
2060 // Actual conversion with rounding.
2061 // exponent >= 0 && exponent < sbits - 1
2062
2063 expr_ref res_sgn(m), res_sig(m), res_exp(m);
2064 res_sgn = a_sgn;
2065 res_exp = a_exp;
2066
2067 SASSERT(m_bv_util.get_bv_size(a_sig) == sbits);
2068 SASSERT(m_bv_util.get_bv_size(a_exp) == ebits);
2069
2070 expr_ref zero_s(m);
2071 zero_s = m_bv_util.mk_numeral(0, sbits);
2072
2073 expr_ref shift(m), shifted_sig(m), div(m), rem(m);
2074 shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits - 1, sbits),
2075 m_bv_util.mk_sign_extend(sbits-ebits, a_exp));
2076 shifted_sig = m_bv_util.mk_bv_lshr(m_bv_util.mk_concat(a_sig, zero_s),
2077 m_bv_util.mk_concat(zero_s, shift));
2078 div = m_bv_util.mk_extract(2*sbits-1, sbits, shifted_sig);
2079 rem = m_bv_util.mk_extract(sbits-1, 0, shifted_sig);
2080
2081 SASSERT(is_well_sorted(m, div));
2082 SASSERT(is_well_sorted(m, rem));
2083 SASSERT(m_bv_util.get_bv_size(shift) == sbits);
2084 SASSERT(m_bv_util.get_bv_size(div) == sbits);
2085 SASSERT(m_bv_util.get_bv_size(rem) == sbits);
2086
2087 dbg_decouple("fpa2bv_r2i_shifted_sig", shifted_sig);
2088 dbg_decouple("fpa2bv_r2i_shift", shift);
2089 dbg_decouple("fpa2bv_r2i_div", div);
2090 dbg_decouple("fpa2bv_r2i_rem", rem);
2091
2092 expr_ref div_p1(m);
2093 div_p1 = m_bv_util.mk_bv_add(div, m_bv_util.mk_numeral(1, sbits));
2094
2095 expr_ref tie_pttrn(m), tie2(m), tie2_c(m), div_last(m), v51(m);
2096 tie_pttrn = m_bv_util.mk_concat(one_1, m_bv_util.mk_numeral(0, sbits-1));
2097 m_simp.mk_eq(rem, tie_pttrn, tie2);
2098 div_last = m_bv_util.mk_extract(0, 0, div);
2099 expr_ref div_last_eq_1(m), rte_and_dl_eq_1(m), rte_and_dl_eq_1_or_rta(m), tie_pttrn_ule_rem(m);
2100 div_last_eq_1 = m.mk_eq(div_last, one_1);
2101 rte_and_dl_eq_1 = m.mk_and(rm_is_rte, div_last_eq_1);
2102 rte_and_dl_eq_1_or_rta = m.mk_or(rte_and_dl_eq_1, rm_is_rta);
2103 tie_pttrn_ule_rem = m_bv_util.mk_ule(tie_pttrn, rem);
2104 tie2_c = m.mk_ite(tie2, rte_and_dl_eq_1_or_rta, tie_pttrn_ule_rem);
2105 m_simp.mk_ite(tie2_c, div_p1, div, v51);
2106
2107 dbg_decouple("fpa2bv_r2i_v51", v51);
2108 dbg_decouple("fpa2bv_r2i_tie2", tie2);
2109 dbg_decouple("fpa2bv_r2i_tie2_c", tie2_c);
2110
2111 SASSERT(is_well_sorted(m, tie2));
2112 SASSERT(is_well_sorted(m, tie2_c));
2113 SASSERT(is_well_sorted(m, v51));
2114
2115 expr_ref c521(m), v52(m), rem_eq_0(m), sgn_eq_zero(m);
2116 rem_eq_0 = m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits));
2117 sgn_eq_zero = m.mk_eq(res_sgn, zero_1);
2118 m_simp.mk_not(rem_eq_0, c521);
2119 m_simp.mk_and(c521, sgn_eq_zero, c521);
2120 m_simp.mk_ite(c521, div_p1, div, v52);
2121
2122 expr_ref c531(m), v53(m), sgn_eq_one(m);
2123 sgn_eq_one = m.mk_eq(res_sgn, one_1);
2124 m_simp.mk_not(rem_eq_0, c531);
2125 m_simp.mk_and(c531, sgn_eq_one, c531);
2126 m_simp.mk_ite(c531, div_p1, div, v53);
2127
2128 expr_ref c51(m), c52(m), c53(m);
2129 c51 = m.mk_or(rm_is_rte, rm_is_rta);
2130 c52 = rm_is_rtp;
2131 c53 = rm_is_rtn;
2132
2133 dbg_decouple("fpa2bv_r2i_c51", c51);
2134 dbg_decouple("fpa2bv_r2i_c52", c52);
2135 dbg_decouple("fpa2bv_r2i_c53", c53);
2136 dbg_decouple("fpa2bv_r2i_c531", c531);
2137
2138 res_sig = div;
2139 m_simp.mk_ite(c53, v53, res_sig, res_sig);
2140 m_simp.mk_ite(c52, v52, res_sig, res_sig);
2141 m_simp.mk_ite(c51, v51, res_sig, res_sig);
2142
2143 SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
2144 SASSERT(m_bv_util.get_bv_size(shift) == sbits);
2145
2146 expr_ref e_shift(m);
2147 e_shift = (ebits + 2 <= sbits + 1) ? m_bv_util.mk_extract(ebits + 1, 0, shift) :
2148 m_bv_util.mk_sign_extend((ebits + 2) - (sbits), shift);
2149 SASSERT(m_bv_util.get_bv_size(e_shift) == ebits + 2);
2150 res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), e_shift);
2151
2152 SASSERT(m_bv_util.get_bv_size(res_sgn) == 1);
2153 SASSERT(m_bv_util.get_bv_size(res_sig) == sbits);
2154 SASSERT(m_bv_util.get_bv_size(res_exp) == ebits + 2);
2155
2156 // Renormalize
2157 expr_ref zero_e2(m), min_exp(m), sig_lz(m), max_exp_delta(m), sig_lz_capped(m), renorm_delta(m);
2158 zero_e2 = m_bv_util.mk_numeral(0, ebits+2);
2159 mk_min_exp(ebits, min_exp);
2160 min_exp = m_bv_util.mk_sign_extend(2, min_exp);
2161 mk_leading_zeros(res_sig, ebits+2, sig_lz);
2162 max_exp_delta = m_bv_util.mk_bv_sub(res_exp, min_exp);
2163 sig_lz_capped = m.mk_ite(m_bv_util.mk_ule(sig_lz, max_exp_delta), sig_lz, max_exp_delta);
2164 renorm_delta = m.mk_ite(m_bv_util.mk_ule(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2);
2165 SASSERT(m_bv_util.get_bv_size(renorm_delta) == ebits + 2);
2166 res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta);
2167 res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta));
2168 dbg_decouple("fpa2bv_r2i_renorm_delta", renorm_delta);
2169 dbg_decouple("fpa2bv_r2i_sig_lz", sig_lz);
2170 dbg_decouple("fpa2bv_r2i_sig_lz_capped", sig_lz_capped);
2171 dbg_decouple("fpa2bv_r2i_max_exp_delta", max_exp_delta);
2172
2173 res_exp = m_bv_util.mk_extract(ebits-1, 0, res_exp);
2174 mk_bias(res_exp, res_exp);
2175 res_sig = m_bv_util.mk_extract(sbits-2, 0, res_sig);
2176 v6 = m_util.mk_fp(res_sgn, res_exp, res_sig);
2177
2178 dbg_decouple("fpa2bv_r2i_res_sgn", res_sgn);
2179 dbg_decouple("fpa2bv_r2i_res_sig", res_sig);
2180 dbg_decouple("fpa2bv_r2i_res_exp", res_exp);
2181
2182 dbg_decouple("fpa2bv_r2i_c1", c1);
2183 dbg_decouple("fpa2bv_r2i_c2", c2);
2184 dbg_decouple("fpa2bv_r2i_c3", c3);
2185 dbg_decouple("fpa2bv_r2i_c4", c4);
2186 dbg_decouple("fpa2bv_r2i_c5", c5);
2187
2188 // And finally, we tie them together.
2189 mk_ite(c5, v5, v6, result);
2190 mk_ite(c4, v4, result, result);
2191 mk_ite(c3, v3, result, result);
2192 mk_ite(c2, v2, result, result);
2193 mk_ite(c1, v1, result, result);
2194
2195 SASSERT(is_well_sorted(m, result));
2196
2197 TRACE("fpa2bv_round_to_integral", tout << "ROUND2INTEGRAL = " << mk_ismt2_pp(result, m) << std::endl; );
2198 }
2199
mk_float_eq(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2200 void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2201 SASSERT(num == 2);
2202 expr_ref x(m), y(m);
2203 x = args[0];
2204 y = args[1];
2205 mk_float_eq(f->get_range(), x, y, result);
2206 }
2207
mk_float_eq(sort * s,expr_ref & x,expr_ref & y,expr_ref & result)2208 void fpa2bv_converter::mk_float_eq(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) {
2209 TRACE("fpa2bv_float_eq", tout << "X = " << mk_ismt2_pp(x, m) << std::endl;
2210 tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;);
2211
2212 expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m);
2213 mk_is_nan(x, x_is_nan);
2214 mk_is_nan(y, y_is_nan);
2215 m_simp.mk_or(x_is_nan, y_is_nan, c1);
2216 mk_is_zero(x, x_is_zero);
2217 mk_is_zero(y, y_is_zero);
2218 m_simp.mk_and(x_is_zero, y_is_zero, c2);
2219
2220 expr_ref x_sgn(m), x_sig(m), x_exp(m);
2221 expr_ref y_sgn(m), y_sig(m), y_exp(m);
2222 split_fp(x, x_sgn, x_exp, x_sig);
2223 split_fp(y, y_sgn, y_exp, y_sig);
2224
2225 expr_ref x_eq_y_sgn(m), x_eq_y_exp(m), x_eq_y_sig(m);
2226 m_simp.mk_eq(x_sgn, y_sgn, x_eq_y_sgn);
2227 m_simp.mk_eq(x_exp, y_exp, x_eq_y_exp);
2228 m_simp.mk_eq(x_sig, y_sig, x_eq_y_sig);
2229
2230 expr_ref c3(m), t4(m);
2231 m_simp.mk_not(x_eq_y_sgn, c3);
2232 m_simp.mk_and(x_eq_y_exp, x_eq_y_sig, t4);
2233
2234 expr_ref c3t4(m), c2else(m);
2235 m_simp.mk_ite(c3, m.mk_false(), t4, c3t4);
2236 m_simp.mk_ite(c2, m.mk_true(), c3t4, c2else);
2237 m_simp.mk_ite(c1, m.mk_false(), c2else, result);
2238
2239 TRACE("fpa2bv_float_eq", tout << "FLOAT_EQ = " << mk_ismt2_pp(result, m) << std::endl; );
2240 }
2241
mk_float_lt(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2242 void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2243 SASSERT(num == 2);
2244 expr_ref x(m), y(m);
2245 x = args[0];
2246 y = args[1];
2247 mk_float_lt(f->get_range(), x, y, result);
2248 }
2249
mk_float_lt(sort * s,expr_ref & x,expr_ref & y,expr_ref & result)2250 void fpa2bv_converter::mk_float_lt(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) {
2251 expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m);
2252 mk_is_nan(x, x_is_nan);
2253 mk_is_nan(y, y_is_nan);
2254 m_simp.mk_or(x_is_nan, y_is_nan, c1);
2255 mk_is_zero(x, x_is_zero);
2256 mk_is_zero(y, y_is_zero);
2257 m_simp.mk_and(x_is_zero, y_is_zero, c2);
2258
2259 expr_ref x_sgn(m), x_sig(m), x_exp(m);
2260 expr_ref y_sgn(m), y_sig(m), y_exp(m);
2261 split_fp(x, x_sgn, x_exp, x_sig);
2262 split_fp(y, y_sgn, y_exp, y_sig);
2263
2264 expr_ref c3(m), t3(m), t4(m), one_1(m), nil_1(m);
2265 one_1 = m_bv_util.mk_numeral(1, 1);
2266 nil_1 = m_bv_util.mk_numeral(0, 1);
2267 m_simp.mk_eq(x_sgn, one_1, c3);
2268
2269 expr_ref y_sgn_eq_0(m), y_lt_x_exp(m), y_lt_x_sig(m), y_eq_x_exp(m), y_le_x_sig_exp(m), t3_or(m);
2270 m_simp.mk_eq(y_sgn, nil_1, y_sgn_eq_0);
2271 BVULT(y_exp, x_exp, y_lt_x_exp);
2272 BVULT(y_sig, x_sig, y_lt_x_sig);
2273 m_simp.mk_eq(y_exp, x_exp, y_eq_x_exp);
2274 m_simp.mk_and(y_eq_x_exp, y_lt_x_sig, y_le_x_sig_exp);
2275 m_simp.mk_or(y_lt_x_exp, y_le_x_sig_exp, t3_or);
2276 m_simp.mk_ite(y_sgn_eq_0, m.mk_true(), t3_or, t3);
2277
2278 expr_ref y_sgn_eq_1(m), x_lt_y_exp(m), x_eq_y_exp(m), x_lt_y_sig(m), x_le_y_sig_exp(m), t4_or(m);
2279 m_simp.mk_eq(y_sgn, one_1, y_sgn_eq_1);
2280 BVULT(x_exp, y_exp, x_lt_y_exp);
2281 m_simp.mk_eq(x_exp, y_exp, x_eq_y_exp);
2282 BVULT(x_sig, y_sig, x_lt_y_sig);
2283 m_simp.mk_and(x_eq_y_exp, x_lt_y_sig, x_le_y_sig_exp);
2284 m_simp.mk_or(x_lt_y_exp, x_le_y_sig_exp, t4_or);
2285 m_simp.mk_ite(y_sgn_eq_1, m.mk_false(), t4_or, t4);
2286
2287 expr_ref c3t3t4(m), c2else(m);
2288 m_simp.mk_ite(c3, t3, t4, c3t3t4);
2289 m_simp.mk_ite(c2, m.mk_false(), c3t3t4, c2else);
2290 m_simp.mk_ite(c1, m.mk_false(), c2else, result);
2291 }
2292
mk_float_gt(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2293 void fpa2bv_converter::mk_float_gt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2294 SASSERT(num == 2);
2295 expr_ref x(m), y(m);
2296 x = args[0];
2297 y = args[1];
2298 mk_float_gt(f->get_range(), x, y, result);
2299 }
2300
mk_float_gt(sort * s,expr_ref & x,expr_ref & y,expr_ref & result)2301 void fpa2bv_converter::mk_float_gt(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) {
2302 expr_ref t3(m);
2303 mk_float_le(s, x, y, t3);
2304
2305 expr_ref nan_or(m), xy_zero(m), not_t3(m), r_else(m);
2306 expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m);
2307 mk_is_nan(x, x_is_nan);
2308 mk_is_nan(y, y_is_nan);
2309 m_simp.mk_or(x_is_nan, y_is_nan, nan_or);
2310 mk_is_zero(x, x_is_zero);
2311 mk_is_zero(y, y_is_zero);
2312 m_simp.mk_and(x_is_zero, y_is_zero, xy_zero);
2313 m_simp.mk_not(t3, not_t3);
2314 m_simp.mk_ite(xy_zero, m.mk_false(), not_t3, r_else);
2315 m_simp.mk_ite(nan_or, m.mk_false(), r_else, result);
2316 }
2317
mk_float_le(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2318 void fpa2bv_converter::mk_float_le(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2319 SASSERT(num == 2);
2320 expr_ref x(m), y(m);
2321 x = args[0];
2322 y = args[1];
2323 mk_float_le(f->get_range(), x, y, result);
2324 }
2325
mk_float_le(sort * s,expr_ref & x,expr_ref & y,expr_ref & result)2326 void fpa2bv_converter::mk_float_le(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) {
2327 expr_ref a(m), b(m);
2328 mk_float_lt(s, x, y, a);
2329 mk_float_eq(s, x, y, b);
2330 m_simp.mk_or(a, b, result);
2331 }
2332
mk_float_ge(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2333 void fpa2bv_converter::mk_float_ge(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2334 SASSERT(num == 2);
2335 expr_ref x(m), y(m);
2336 x = args[0];
2337 y = args[1];
2338 mk_float_ge(f->get_range(), x, y, result);
2339 }
2340
mk_float_ge(sort * s,expr_ref & x,expr_ref & y,expr_ref & result)2341 void fpa2bv_converter::mk_float_ge(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) {
2342 expr_ref a(m), b(m);
2343 mk_float_gt(s, x, y, a);
2344 mk_float_eq(s, x, y, b);
2345 m_simp.mk_or(a, b, result);
2346 }
2347
mk_is_zero(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2348 void fpa2bv_converter::mk_is_zero(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2349 SASSERT(num == 1);
2350 mk_is_zero(args[0], result);
2351 }
2352
mk_is_nzero(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2353 void fpa2bv_converter::mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2354 SASSERT(num == 1);
2355 expr_ref a0_is_neg(m), a0_is_zero(m);
2356 mk_is_neg(args[0], a0_is_neg);
2357 mk_is_zero(args[0], a0_is_zero);
2358 m_simp.mk_and(a0_is_neg, a0_is_zero, result);
2359 }
2360
mk_is_pzero(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2361 void fpa2bv_converter::mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2362 SASSERT(num == 1);
2363 expr_ref a0_is_pos(m), a0_is_zero(m);
2364 mk_is_pos(args[0], a0_is_pos);
2365 mk_is_zero(args[0], a0_is_zero);
2366 m_simp.mk_and(a0_is_pos, a0_is_zero, result);
2367 }
2368
mk_is_nan(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2369 void fpa2bv_converter::mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2370 SASSERT(num == 1);
2371 mk_is_nan(args[0], result);
2372 }
2373
mk_is_inf(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2374 void fpa2bv_converter::mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2375 SASSERT(num == 1);
2376 mk_is_inf(args[0], result);
2377 }
2378
mk_is_normal(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2379 void fpa2bv_converter::mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2380 SASSERT(num == 1);
2381 mk_is_normal(args[0], result);
2382 }
2383
mk_is_subnormal(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2384 void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2385 SASSERT(num == 1);
2386 mk_is_denormal(args[0], result);
2387 }
2388
mk_is_negative(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2389 void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2390 SASSERT(num == 1);
2391 expr_ref t1(m), t2(m), nt1(m);
2392 mk_is_nan(args[0], t1);
2393 mk_is_neg(args[0], t2);
2394 nt1 = m.mk_not(t1);
2395 result = m.mk_and(nt1, t2);
2396 TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;);
2397 }
2398
mk_is_positive(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2399 void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2400 SASSERT(num == 1);
2401 expr_ref t1(m), t2(m), nt1(m);
2402 mk_is_nan(args[0], t1);
2403 mk_is_pos(args[0], t2);
2404 nt1 = m.mk_not(t1);
2405 result = m.mk_and(nt1, t2);
2406 }
2407
mk_to_fp(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2408 void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2409 TRACE("fpa2bv_to_fp", for (unsigned i=0; i < num; i++)
2410 tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; );
2411
2412 if (num == 1 &&
2413 m_bv_util.is_bv(args[0])) {
2414 sort * s = f->get_range();
2415 unsigned to_sbits = m_util.get_sbits(s);
2416 unsigned to_ebits = m_util.get_ebits(s);
2417
2418 expr * bv = args[0];
2419 int sz = m_bv_util.get_bv_size(bv);
2420 (void)to_sbits;
2421 SASSERT((unsigned)sz == to_sbits + to_ebits);
2422
2423 result = m_util.mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
2424 m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
2425 m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv));
2426 }
2427 else if (num == 2 &&
2428 m_util.is_rm(args[0]) &&
2429 m_util.is_float(args[1]->get_sort())) {
2430 // rm + float -> float
2431 mk_to_fp_float(f, f->get_range(), args[0], args[1], result);
2432 }
2433 else if (num == 2 &&
2434 m_util.is_rm(args[0]) &&
2435 (m_arith_util.is_int(args[1]) ||
2436 m_arith_util.is_real(args[1]))) {
2437 // rm + real -> float
2438 mk_to_fp_real(f, f->get_range(), args[0], args[1], result);
2439 }
2440 else if (num == 2 &&
2441 m_util.is_rm(args[0]) &&
2442 m_bv_util.is_bv(args[1])) {
2443 // rm + signed bv -> float
2444 mk_to_fp_signed(f, num, args, result);
2445 }
2446 else if (num == 3 &&
2447 m_bv_util.is_bv(args[0]) &&
2448 m_bv_util.is_bv(args[1]) &&
2449 m_bv_util.is_bv(args[2])) {
2450 // 3 BV -> float
2451 SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
2452 SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
2453 SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1);
2454 result = m_util.mk_fp(args[0], args[1], args[2]);
2455 }
2456 else if (num == 3 &&
2457 m_util.is_rm(args[0]) &&
2458 m_arith_util.is_numeral(args[1]) &&
2459 m_arith_util.is_numeral(args[2]))
2460 {
2461 // rm + real + int -> float
2462 mk_to_fp_real_int(f, num, args, result);
2463 }
2464 else if (num == 3 &&
2465 m_util.is_rm(args[0]) &&
2466 m_arith_util.is_int_real(args[1]) &&
2467 m_arith_util.is_int_real(args[2]))
2468 {
2469 expr_ref sig(m), exp(m), two(m), v(m);
2470 sig = args[1];
2471 exp = args[2];
2472 two = m_arith_util.mk_numeral(rational(2), true);
2473 v = m_arith_util.mk_mul(sig, m_arith_util.mk_power(two, exp));
2474 mk_to_fp_real(f, f->get_range(), args[0], v, result);
2475 }
2476 else
2477 UNREACHABLE();
2478
2479 SASSERT(is_well_sorted(m, result));
2480 }
2481
2482
mk_to_fp_float(func_decl * f,sort * s,expr * rm,expr * x,expr_ref & result)2483 void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
2484 SASSERT(m_util.is_bv2rm(rm));
2485 mk_to_fp_float(s, to_app(rm)->get_arg(0), x, result);
2486 }
2487
mk_to_fp_float(sort * to_srt,expr * rm,expr * x,expr_ref & result)2488 void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_ref & result) {
2489 unsigned from_sbits = m_util.get_sbits(x->get_sort());
2490 unsigned from_ebits = m_util.get_ebits(x->get_sort());
2491 unsigned to_sbits = m_util.get_sbits(to_srt);
2492 unsigned to_ebits = m_util.get_ebits(to_srt);
2493
2494 if (from_sbits == to_sbits && from_ebits == to_ebits)
2495 result = x;
2496 else {
2497 expr_ref c1(m), c2(m), c3(m), c4(m), c5(m);
2498 expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m);
2499 expr_ref one1(m);
2500
2501 one1 = m_bv_util.mk_numeral(1, 1);
2502 expr_ref ninf(m), pinf(m);
2503 mk_pinf(to_srt, pinf);
2504 mk_ninf(to_srt, ninf);
2505
2506 // NaN -> NaN
2507 mk_is_nan(x, c1);
2508 mk_nan(to_srt, v1);
2509
2510 // +0 -> +0
2511 mk_is_pzero(x, c2);
2512 mk_pzero(to_srt, v2);
2513
2514 // -0 -> -0
2515 mk_is_nzero(x, c3);
2516 mk_nzero(to_srt, v3);
2517
2518 // +oo -> +oo
2519 mk_is_pinf(x, c4);
2520 v4 = pinf;
2521
2522 // -oo -> -oo
2523 mk_is_ninf(x, c5);
2524 v5 = ninf;
2525
2526 // otherwise: the actual conversion with rounding.
2527 expr_ref sgn(m), sig(m), exp(m), lz(m);
2528 unpack(x, sgn, sig, exp, lz, true);
2529
2530 dbg_decouple("fpa2bv_to_float_x_sgn", sgn);
2531 dbg_decouple("fpa2bv_to_float_x_sig", sig);
2532 dbg_decouple("fpa2bv_to_float_x_exp", exp);
2533 dbg_decouple("fpa2bv_to_float_lz", lz);
2534
2535 expr_ref res_sgn(m), res_sig(m), res_exp(m);
2536
2537 res_sgn = sgn;
2538
2539 SASSERT(m_bv_util.get_bv_size(sgn) == 1);
2540 SASSERT(m_bv_util.get_bv_size(sig) == from_sbits);
2541 SASSERT(m_bv_util.get_bv_size(exp) == from_ebits);
2542 SASSERT(m_bv_util.get_bv_size(lz) == from_ebits);
2543
2544 if (from_sbits < (to_sbits + 3)) {
2545 // make sure that sig has at least to_sbits + 3
2546 res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits + 3 - from_sbits));
2547 }
2548 else if (from_sbits > (to_sbits + 3)) {
2549 // collapse the extra bits into a sticky bit.
2550 expr_ref sticky(m), low(m), high(m);
2551 high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig);
2552 SASSERT(m_bv_util.get_bv_size(high) == to_sbits + 2);
2553 low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig);
2554 sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get());
2555 SASSERT(m_bv_util.get_bv_size(sticky) == 1);
2556 dbg_decouple("fpa2bv_to_float_sticky", sticky);
2557 res_sig = m_bv_util.mk_concat(high, sticky);
2558 SASSERT(m_bv_util.get_bv_size(res_sig) == to_sbits + 3);
2559 }
2560 else
2561 res_sig = sig;
2562
2563 res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
2564 SASSERT(m_bv_util.get_bv_size(res_sig) == to_sbits + 4);
2565
2566 expr_ref exponent_overflow(m), exponent_underflow(m);
2567 exponent_overflow = m.mk_false();
2568 exponent_underflow = m.mk_false();
2569
2570 if (from_ebits < (to_ebits + 2)) {
2571 res_exp = m_bv_util.mk_sign_extend(to_ebits - from_ebits + 2, exp);
2572
2573 // subtract lz for subnormal numbers.
2574 expr_ref lz_ext(m);
2575 lz_ext = m_bv_util.mk_zero_extend(to_ebits - from_ebits + 2, lz);
2576 res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
2577 }
2578 else if (from_ebits >= (to_ebits + 2)) {
2579 unsigned ebits_diff = from_ebits - (to_ebits + 2);
2580
2581 // subtract lz for subnormal numbers.
2582 expr_ref exp_sub_lz(m);
2583 exp_sub_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), m_bv_util.mk_sign_extend(2, lz));
2584 dbg_decouple("fpa2bv_to_float_exp_sub_lz", exp_sub_lz);
2585
2586 // check whether exponent is within roundable (to_ebits+2) range.
2587 expr_ref max_exp(m), min_exp(m), exp_in_range(m);
2588 const mpz & z = m_mpf_manager.m_powers2(to_ebits + 1, true);
2589 max_exp = m_bv_util.mk_concat(
2590 m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(to_ebits, false), to_ebits + 1),
2591 m_bv_util.mk_numeral(0, 1));
2592 min_exp = m_bv_util.mk_numeral(z + mpz(2), to_ebits+2);
2593 dbg_decouple("fpa2bv_to_float_max_exp", max_exp);
2594 dbg_decouple("fpa2bv_to_float_min_exp", min_exp);
2595
2596 expr_ref first_ovf_exp(m), first_udf_exp(m);
2597 const mpz & ovft = m_mpf_manager.m_powers2.m1(to_ebits+1, false);
2598 first_ovf_exp = m_bv_util.mk_numeral(ovft, from_ebits+2);
2599 first_udf_exp = m_bv_util.mk_concat(
2600 m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits_diff + 3)),
2601 m_bv_util.mk_numeral(1, to_ebits + 1));
2602 dbg_decouple("fpa2bv_to_float_first_ovf_exp", first_ovf_exp);
2603 dbg_decouple("fpa2bv_to_float_first_udf_exp", first_udf_exp);
2604
2605 exp_in_range = m_bv_util.mk_extract(to_ebits + 1, 0, exp_sub_lz);
2606 SASSERT(m_bv_util.get_bv_size(exp_in_range) == to_ebits + 2);
2607
2608 expr_ref ovf_cond(m), udf_cond(m);
2609 ovf_cond = m_bv_util.mk_sle(first_ovf_exp, exp_sub_lz);
2610 udf_cond = m_bv_util.mk_sle(exp_sub_lz, first_udf_exp);
2611 dbg_decouple("fpa2bv_to_float_exp_ovf", ovf_cond);
2612 dbg_decouple("fpa2bv_to_float_exp_udf", udf_cond);
2613
2614 res_exp = exp_in_range;
2615 res_exp = m.mk_ite(ovf_cond, max_exp, res_exp);
2616 res_exp = m.mk_ite(udf_cond, min_exp, res_exp);
2617 }
2618
2619 SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits + 2);
2620 SASSERT(is_well_sorted(m, res_exp));
2621
2622 dbg_decouple("fpa2bv_to_float_res_sig", res_sig);
2623 dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
2624
2625 expr_ref rounded(m);
2626 expr_ref rm_e(rm, m);
2627 round(to_srt, rm_e, res_sgn, res_sig, res_exp, rounded);
2628
2629 expr_ref is_neg(m), sig_inf(m);
2630 m_simp.mk_eq(sgn, one1, is_neg);
2631 mk_ite(is_neg, ninf, pinf, sig_inf);
2632
2633 mk_ite(exponent_overflow, sig_inf, rounded, v6);
2634
2635 // And finally, we tie them together.
2636 mk_ite(c5, v5, v6, result);
2637 mk_ite(c4, v4, result, result);
2638 mk_ite(c3, v3, result, result);
2639 mk_ite(c2, v2, result, result);
2640 mk_ite(c1, v1, result, result);
2641 }
2642
2643 SASSERT(is_well_sorted(m, result));
2644 }
2645
mk_to_fp_real(func_decl * f,sort * s,expr * rm,expr * x,expr_ref & result)2646 void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
2647 TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl <<
2648 "x: " << mk_ismt2_pp(x, m) << std::endl;);
2649 SASSERT(m_util.is_float(s));
2650 SASSERT(au().is_real(x) || au().is_int(x));
2651 SASSERT(m_util.is_bv2rm(rm));
2652
2653 expr * bv_rm = to_app(rm)->get_arg(0);
2654 unsigned ebits = m_util.get_ebits(s);
2655 unsigned sbits = m_util.get_sbits(s);
2656
2657 if (m_bv_util.is_numeral(bv_rm) && m_util.au().is_numeral(x)) {
2658 rational tmp_rat; unsigned sz;
2659 m_bv_util.is_numeral(to_expr(bv_rm), tmp_rat, sz);
2660 SASSERT(tmp_rat.is_int32());
2661 SASSERT(sz == 3);
2662
2663 mpf_rounding_mode mrm;
2664 switch ((BV_RM_VAL)tmp_rat.get_unsigned()) {
2665 case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break;
2666 case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break;
2667 case BV_RM_TO_NEGATIVE: mrm = MPF_ROUND_TOWARD_NEGATIVE; break;
2668 case BV_RM_TO_POSITIVE: mrm = MPF_ROUND_TOWARD_POSITIVE; break;
2669 case BV_RM_TO_ZERO: mrm = MPF_ROUND_TOWARD_ZERO; break;
2670 default: UNREACHABLE();
2671 }
2672
2673 rational q;
2674 bool is_int;
2675 m_util.au().is_numeral(x, q, is_int);
2676
2677 if (q.is_zero())
2678 return mk_pzero(f, result);
2679 else {
2680 scoped_mpf v(m_mpf_manager);
2681 m_util.fm().set(v, ebits, sbits, mrm, q.to_mpq());
2682
2683 expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m);
2684 sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
2685 sig = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
2686 unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
2687 mk_bias(unbiased_exp, exp);
2688
2689 result = m_util.mk_fp(sgn, exp, sig);
2690 }
2691 }
2692 else if (m_util.au().is_numeral(x)) {
2693 rational q;
2694 bool is_int;
2695 m_util.au().is_numeral(x, q, is_int);
2696
2697 if (m_util.au().is_zero(x))
2698 mk_pzero(f, result);
2699 else {
2700 expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
2701 mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_nta);
2702 mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_nte);
2703 mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_tp);
2704 mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_tn);
2705 mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_tz);
2706
2707 scoped_mpf v_nta(m_mpf_manager), v_nte(m_mpf_manager), v_tp(m_mpf_manager);
2708 scoped_mpf v_tn(m_mpf_manager), v_tz(m_mpf_manager);
2709 m_util.fm().set(v_nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq());
2710 m_util.fm().set(v_nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq());
2711 m_util.fm().set(v_tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq());
2712 m_util.fm().set(v_tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq());
2713 m_util.fm().set(v_tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq());
2714
2715 expr_ref v1(m), v2(m), v3(m), v4(m);
2716
2717 expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m);
2718 sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1);
2719 sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
2720 unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
2721 mk_bias(unbiased_exp, exp);
2722 v1 = m_util.mk_fp(sgn, exp, sig);
2723
2724 sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
2725 sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
2726 unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
2727 mk_bias(unbiased_exp, exp);
2728 v2 = m_util.mk_fp(sgn, exp, sig);
2729
2730 sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
2731 sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
2732 unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
2733 mk_bias(unbiased_exp, exp);
2734 v3 = m_util.mk_fp(sgn, exp, sig);
2735
2736 sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
2737 sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
2738 unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
2739 mk_bias(unbiased_exp, exp);
2740 v4 = m_util.mk_fp(sgn, exp, sig);
2741
2742 sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
2743 sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
2744 unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
2745 mk_bias(unbiased_exp, exp);
2746
2747 result = m_util.mk_fp(sgn, exp, sig);
2748 mk_ite(rm_tn, v4, result, result);
2749 mk_ite(rm_tp, v3, result, result);
2750 mk_ite(rm_nte, v2, result, result);
2751 mk_ite(rm_nta, v1, result, result);
2752 }
2753 }
2754 else {
2755 SASSERT(!m_arith_util.is_numeral(x));
2756 bv_util & bu = m_bv_util;
2757 arith_util & au = m_arith_util;
2758
2759 expr_ref bv0(m), bv1(m), zero(m), two(m);
2760 bv0 = bu.mk_numeral(0, 1);
2761 bv1 = bu.mk_numeral(1, 1);
2762 zero = au.mk_numeral(rational(0), false);
2763 two = au.mk_numeral(rational(2), false);
2764
2765 expr_ref sgn(m), sig(m), exp(m);
2766 sgn = mk_fresh_const("fpa2bv_to_fp_real_sgn", 1);
2767 sig = mk_fresh_const("fpa2bv_to_fp_real_sig", sbits + 4);
2768 exp = mk_fresh_const("fpa2bv_to_fp_real_exp", ebits + 2);
2769
2770 expr_ref rme(bv_rm, m);
2771 round(s, rme, sgn, sig, exp, result);
2772
2773 expr * e = m.mk_eq(m_util.mk_to_real(result), x);
2774 m_extra_assertions.push_back(e);
2775 }
2776
2777 SASSERT(is_well_sorted(m, result));
2778 }
2779
mk_to_fp_real_int(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2780 void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2781 // rm + real + int -> float
2782 SASSERT(m_util.is_float(f->get_range()));
2783 unsigned ebits = m_util.get_ebits(f->get_range());
2784 unsigned sbits = m_util.get_sbits(f->get_range());
2785
2786 SASSERT(m_util.is_bv2rm(args[0]));
2787 expr * bv_rm = to_app(args[0])->get_arg(0);
2788
2789 SASSERT((m_arith_util.is_int(args[1]) && m_arith_util.is_real(args[2])) ||
2790 (m_arith_util.is_real(args[1]) && m_arith_util.is_int(args[2])));
2791
2792 rational q, e;
2793
2794 if (m_arith_util.is_int(args[1]) && m_arith_util.is_real(args[2])) {
2795 if (!m_arith_util.is_numeral(args[1], e) ||
2796 !m_arith_util.is_numeral(args[2], q))
2797 UNREACHABLE();
2798 }
2799 else {
2800 if (!m_arith_util.is_numeral(args[2], e) ||
2801 !m_arith_util.is_numeral(args[1], q))
2802 UNREACHABLE();
2803 }
2804
2805 SASSERT(e.is_int64());
2806 SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1));
2807
2808 if (q.is_zero())
2809 return mk_pzero(f, result);
2810 else {
2811 scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager);
2812 m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, e.to_mpq().numerator(), q.to_mpq());
2813 m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, e.to_mpq().numerator(), q.to_mpq());
2814 m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, e.to_mpq().numerator(), q.to_mpq());
2815 m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, e.to_mpq().numerator(), q.to_mpq());
2816 m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, e.to_mpq().numerator(), q.to_mpq());
2817
2818 app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m);
2819 a_nte = m_plugin->mk_numeral(nte);
2820 a_nta = m_plugin->mk_numeral(nta);
2821 a_tp = m_plugin->mk_numeral(tp);
2822 a_tn = m_plugin->mk_numeral(tn);
2823 a_tz = m_plugin->mk_numeral(tz);
2824
2825 expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
2826 mk_numeral(a_nte->get_decl(), 0, nullptr, bv_nte);
2827 mk_numeral(a_nta->get_decl(), 0, nullptr, bv_nta);
2828 mk_numeral(a_tp->get_decl(), 0, nullptr, bv_tp);
2829 mk_numeral(a_tn->get_decl(), 0, nullptr, bv_tn);
2830 mk_numeral(a_tz->get_decl(), 0, nullptr, bv_tz);
2831
2832 expr_ref c1(m), c2(m), c3(m), c4(m);
2833 c1 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3));
2834 c2 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3));
2835 c3 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3));
2836 c4 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3));
2837
2838 mk_ite(c1, bv_tn, bv_tz, result);
2839 mk_ite(c2, bv_tp, result, result);
2840 mk_ite(c3, bv_nta, result, result);
2841 mk_ite(c4, bv_nte, result, result);
2842 }
2843 }
2844
mk_to_real(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2845 void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2846 TRACE("fpa2bv_to_real", for (unsigned i = 0; i < num; i++)
2847 tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
2848 SASSERT(num == 1);
2849 SASSERT(f->get_num_parameters() == 0);
2850 SASSERT(is_app_of(args[0], m_plugin->get_family_id(), OP_FPA_FP));
2851
2852 expr * x = args[0];
2853 sort * s = x->get_sort();
2854 unsigned ebits = m_util.get_ebits(s);
2855 unsigned sbits = m_util.get_sbits(s);
2856
2857 sort * rs = m_arith_util.mk_real();
2858 expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m);
2859 mk_is_nan(x, x_is_nan);
2860 mk_is_inf(x, x_is_inf);
2861 mk_is_zero(x, x_is_zero);
2862
2863 expr_ref sgn(m), sig(m), exp(m), lz(m);
2864 unpack(x, sgn, sig, exp, lz, true);
2865 // sig is of the form [1].[sigbits]
2866
2867 SASSERT(m_bv_util.get_bv_size(sgn) == 1);
2868 SASSERT(m_bv_util.get_bv_size(sig) == sbits);
2869 SASSERT(m_bv_util.get_bv_size(exp) == ebits);
2870
2871 expr_ref rsig(m), bit(m), bit_eq_1(m), rsig_mul_2(m), zero(m), one(m), two(m), bv0(m), bv1(m);
2872 zero = m_arith_util.mk_numeral(rational(0), rs);
2873 one = m_arith_util.mk_numeral(rational(1), rs);
2874 two = m_arith_util.mk_numeral(rational(2), rs);
2875 bv0 = m_bv_util.mk_numeral(0, 1);
2876 bv1 = m_bv_util.mk_numeral(1, 1);
2877 rsig = one;
2878 for (unsigned i = sbits - 2; i != (unsigned)-1; i--) {
2879 bit = m_bv_util.mk_extract(i, i, sig);
2880 bit_eq_1 = m.mk_eq(bit, bv1);
2881 rsig_mul_2 = m_arith_util.mk_mul(rsig, two);
2882 rsig = m_arith_util.mk_add(rsig_mul_2,
2883 m.mk_ite(bit_eq_1, one, zero));
2884 }
2885
2886 const mpz & p2 = fu().fm().m_powers2(sbits - 1);
2887 expr_ref ep2(m);
2888 ep2 = m_arith_util.mk_numeral(rational(p2), false);
2889 rsig = m_arith_util.mk_div(rsig, ep2);
2890 dbg_decouple("fpa2bv_to_real_ep2", ep2);
2891 dbg_decouple("fpa2bv_to_real_rsig", rsig);
2892
2893 expr_ref exp_n(m), exp_p(m), exp_is_neg(m), exp_abs(m);
2894 exp_is_neg = m.mk_eq(m_bv_util.mk_extract(ebits - 1, ebits - 1, exp), bv1);
2895 dbg_decouple("fpa2bv_to_real_exp_is_neg", exp_is_neg);
2896 exp_p = m_bv_util.mk_sign_extend(1, exp);
2897 exp_n = m_bv_util.mk_bv_neg(exp_p);
2898 exp_abs = m.mk_ite(exp_is_neg, exp_n, exp_p);
2899 dbg_decouple("fpa2bv_to_real_exp_abs", exp);
2900 SASSERT(m_bv_util.get_bv_size(exp_abs) == ebits + 1);
2901
2902 expr_ref exp2(m), exp2_mul_2(m), prev_bit(m);
2903 exp2 = zero;
2904 for (unsigned i = ebits; i != (unsigned)-1; i--) {
2905 bit = m_bv_util.mk_extract(i, i, exp_abs);
2906 bit_eq_1 = m.mk_eq(bit, bv1);
2907 exp2_mul_2 = m_arith_util.mk_mul(exp2, two);
2908 exp2 = m_arith_util.mk_add(exp2_mul_2,
2909 m.mk_ite(bit_eq_1, one, zero));
2910 prev_bit = bit;
2911 }
2912
2913 expr_ref one_div_exp2(m);
2914 one_div_exp2 = m_arith_util.mk_div(one, exp2);
2915 exp2 = m.mk_ite(exp_is_neg, one_div_exp2, exp2);
2916 dbg_decouple("fpa2bv_to_real_exp2", exp2);
2917
2918 expr_ref res(m), two_exp2(m), minus_res(m), sgn_is_1(m);
2919 two_exp2 = m_arith_util.mk_power(two, exp2);
2920 res = m_arith_util.mk_mul(rsig, two_exp2);
2921 minus_res = m_arith_util.mk_uminus(res);
2922 sgn_is_1 = m.mk_eq(sgn, bv1);
2923 res = m.mk_ite(sgn_is_1, minus_res, res);
2924 dbg_decouple("fpa2bv_to_real_sig_times_exp2", res);
2925
2926 TRACE("fpa2bv_to_real", tout << "rsig = " << mk_ismt2_pp(rsig, m) << std::endl;
2927 tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;);
2928
2929 expr_ref unspec(m);
2930 mk_to_real_unspecified(f, num, args, unspec);
2931 result = m.mk_ite(x_is_zero, zero, res);
2932 result = m.mk_ite(x_is_inf, unspec, result);
2933 result = m.mk_ite(x_is_nan, unspec, result);
2934
2935 SASSERT(is_well_sorted(m, result));
2936 }
2937
mk_to_fp_signed(func_decl * f,unsigned num,expr * const * args,expr_ref & result)2938 void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
2939 TRACE("fpa2bv_to_fp_signed", for (unsigned i = 0; i < num; i++)
2940 tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
2941
2942 // This is a conversion from signed bitvector to float:
2943 // ; from signed machine integer, represented as a 2's complement bit vector
2944 // ((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))
2945 // Semantics:
2946 // Let b in[[(_ BitVec m)]] and let n be the signed integer represented by b (in 2's complement format).
2947 // [[(_ to_fp eb sb)]](r, b) = +/ -infinity if n is too large / too small to be represented as a finite
2948 // number of [[(_ FloatingPoint eb sb)]]; [[(_ to_fp eb sb)]](r, x) = y otherwise, where y is the finite
2949 // number such that [[fp.to_real]](y) is closest to n according to rounding mode r.
2950
2951 SASSERT(num == 2);
2952 SASSERT(m_util.is_float(f->get_range()));
2953 SASSERT(m_util.is_bv2rm(args[0]));
2954 SASSERT(m_bv_util.is_bv(args[1]));
2955
2956 expr_ref rm(m), x(m);
2957 rm = to_app(args[0])->get_arg(0);
2958 x = args[1];
2959
2960 dbg_decouple("fpa2bv_to_fp_signed_x", x);
2961
2962 unsigned ebits = m_util.get_ebits(f->get_range());
2963 unsigned sbits = m_util.get_sbits(f->get_range());
2964 unsigned bv_sz = m_bv_util.get_bv_size(x);
2965 SASSERT(m_bv_util.get_bv_size(rm) == 3);
2966
2967 expr_ref bv1_1(m), bv0_sz(m);
2968 bv1_1 = m_bv_util.mk_numeral(1, 1);
2969 bv0_sz = m_bv_util.mk_numeral(0, bv_sz);
2970
2971 expr_ref is_zero(m), pzero(m);
2972 is_zero = m.mk_eq(x, bv0_sz);
2973 mk_pzero(f, pzero);
2974
2975 // Special case: x == 0 -> p/n zero
2976 expr_ref c1(m), v1(m);
2977 c1 = is_zero;
2978 v1 = pzero;
2979
2980 // Special case: x != 0
2981 expr_ref is_neg_bit(m), exp_too_large(m), sig_4(m), exp_2(m);
2982 expr_ref is_neg(m), x_abs(m), neg_x(m);
2983 is_neg_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x);
2984 is_neg = m.mk_eq(is_neg_bit, bv1_1);
2985 neg_x = m_bv_util.mk_bv_neg(x); // overflow problem?
2986 x_abs = m.mk_ite(is_neg, neg_x, x);
2987 dbg_decouple("fpa2bv_to_fp_signed_is_neg", is_neg);
2988 // x_abs has an extra bit in the front.
2989 // x_abs is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2)
2990 // bv_sz-2 is the "1.0" bit for the rounder.
2991
2992 expr_ref lz(m);
2993 mk_leading_zeros(x_abs, bv_sz, lz);
2994 SASSERT(m_bv_util.get_bv_size(lz) == bv_sz);
2995 dbg_decouple("fpa2bv_to_fp_signed_lz", lz);
2996 expr_ref shifted_sig(m);
2997 shifted_sig = m_bv_util.mk_bv_shl(x_abs, lz);
2998
2999 expr_ref sticky(m);
3000 // shifted_sig is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2) * 2^(-lz)
3001 unsigned sig_sz = sbits + 4; // we want extra rounding bits.
3002 if (sig_sz <= bv_sz) {
3003 expr_ref sig_rest(m);
3004 sig_4 = m_bv_util.mk_extract(bv_sz - 1, bv_sz - sig_sz + 1, shifted_sig); // one short
3005 sig_rest = m_bv_util.mk_extract(bv_sz - sig_sz, 0, shifted_sig);
3006 sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sig_rest.get());
3007 sig_4 = m_bv_util.mk_concat(sig_4, sticky);
3008 }
3009 else {
3010 unsigned extra_bits = sig_sz - bv_sz;
3011 expr_ref extra_zeros(m);
3012 extra_zeros = m_bv_util.mk_numeral(0, extra_bits);
3013 sig_4 = m_bv_util.mk_concat(shifted_sig, extra_zeros);
3014 lz = m_bv_util.mk_bv_add(m_bv_util.mk_concat(extra_zeros, lz),
3015 m_bv_util.mk_numeral(extra_bits, sig_sz));
3016 bv_sz = bv_sz + extra_bits;
3017 SASSERT(is_well_sorted(m, lz));
3018 }
3019 SASSERT(m_bv_util.get_bv_size(sig_4) == sig_sz);
3020 dbg_decouple("fpa2bv_to_fp_signed_sig_4", sig_4);
3021
3022 expr_ref s_exp(m), exp_rest(m);
3023 s_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(bv_sz - 2, bv_sz), lz);
3024 // s_exp = (bv_sz-2) + (-lz) signed
3025 SASSERT(m_bv_util.get_bv_size(s_exp) == bv_sz);
3026 dbg_decouple("fpa2bv_to_fp_signed_s_exp", s_exp);
3027
3028 unsigned exp_sz = ebits + 2; // (+2 for rounder)
3029 exp_2 = m_bv_util.mk_extract(exp_sz - 1, 0, s_exp);
3030 // the remaining bits are 0 if ebits is large enough.
3031 exp_too_large = m.mk_false();
3032
3033 // The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
3034 // exp < bv_sz (+sign bit which is [0])
3035 unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0);
3036
3037 TRACE("fpa2bv_to_fp_signed", tout << "exp worst case sz: " << exp_worst_case_sz << std::endl;);
3038
3039 if (exp_sz < exp_worst_case_sz) {
3040 // exp_sz < exp_worst_case_sz and exp >= 0.
3041 // Take the maximum legal exponent; this
3042 // allows us to keep the most precision.
3043 expr_ref max_exp(m), max_exp_bvsz(m), zero_sig_sz(m);
3044 mk_max_exp(exp_sz, max_exp);
3045 max_exp_bvsz = m_bv_util.mk_zero_extend(bv_sz - exp_sz, max_exp);
3046
3047 exp_too_large = m_bv_util.mk_sle(
3048 m_bv_util.mk_bv_add(max_exp_bvsz, m_bv_util.mk_numeral(1, bv_sz)),
3049 s_exp);
3050 zero_sig_sz = m_bv_util.mk_numeral(0, sig_sz);
3051 sig_4 = m.mk_ite(exp_too_large, zero_sig_sz, sig_4);
3052 exp_2 = m.mk_ite(exp_too_large, max_exp, exp_2);
3053 }
3054 dbg_decouple("fpa2bv_to_fp_signed_exp_too_large", exp_too_large);
3055
3056 expr_ref sgn(m), sig(m), exp(m);
3057 sgn = is_neg_bit;
3058 sig = sig_4;
3059 exp = exp_2;
3060
3061 dbg_decouple("fpa2bv_to_fp_signed_sgn", sgn);
3062 dbg_decouple("fpa2bv_to_fp_signed_sig", sig);
3063 dbg_decouple("fpa2bv_to_fp_signed_exp", exp);
3064
3065 SASSERT(m_bv_util.get_bv_size(sig) == sbits + 4);
3066 SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
3067
3068 expr_ref v2(m);
3069 round(f->get_range(), rm, sgn, sig, exp, v2);
3070
3071 mk_ite(c1, v1, v2, result);
3072 }
3073
mk_to_fp_unsigned(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3074 void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3075 TRACE("fpa2bv_to_fp_unsigned", for (unsigned i = 0; i < num; i++)
3076 tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
3077
3078 // This is a conversion from unsigned bitvector to float:
3079 // ((_ to_fp_unsigned eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))
3080 // Semantics:
3081 // Let b in[[(_ BitVec m)]] and let n be the unsigned integer represented by b.
3082 // [[(_ to_fp_unsigned eb sb)]](r, x) = +infinity if n is too large to be
3083 // represented as a finite number of[[(_ FloatingPoint eb sb)]];
3084 // [[(_ to_fp_unsigned eb sb)]](r, x) = y otherwise, where y is the finite number
3085 // such that[[fp.to_real]](y) is closest to n according to rounding mode r.
3086
3087 SASSERT(num == 2);
3088 SASSERT(m_util.is_float(f->get_range()));
3089 SASSERT(m_util.is_bv2rm(args[0]));
3090 SASSERT(m_bv_util.is_bv(args[1]));
3091
3092 expr_ref rm(m), x(m);
3093 rm = to_app(args[0])->get_arg(0);
3094 x = args[1];
3095
3096 dbg_decouple("fpa2bv_to_fp_unsigned_x", x);
3097
3098 unsigned ebits = m_util.get_ebits(f->get_range());
3099 unsigned sbits = m_util.get_sbits(f->get_range());
3100 unsigned bv_sz = m_bv_util.get_bv_size(x);
3101 SASSERT(m_bv_util.get_bv_size(rm) == 3);
3102
3103 expr_ref bv0_1(m), bv0_sz(m);
3104 bv0_1 = m_bv_util.mk_numeral(0, 1);
3105 bv0_sz = m_bv_util.mk_numeral(0, bv_sz);
3106
3107 expr_ref is_zero(m), pzero(m);
3108 is_zero = m.mk_eq(x, bv0_sz);
3109 mk_pzero(f, pzero);
3110
3111 // Special case: x == 0 -> p/n zero
3112 expr_ref c1(m), v1(m);
3113 c1 = is_zero;
3114 v1 = pzero;
3115
3116 // Special case: x != 0
3117 expr_ref exp_too_large(m), sig_4(m), exp_2(m);
3118 // x is [bv_sz-1] . [bv_sz-2 ... 0] * 2^(bv_sz-1)
3119 // bv_sz-1 is the "1.0" bit for the rounder.
3120
3121 expr_ref lz(m);
3122 mk_leading_zeros(x, bv_sz, lz);
3123 SASSERT(m_bv_util.get_bv_size(lz) == bv_sz);
3124 dbg_decouple("fpa2bv_to_fp_unsigned_lz", lz);
3125 expr_ref shifted_sig(m);
3126 shifted_sig = m_bv_util.mk_bv_shl(x, lz);
3127
3128 expr_ref sticky(m);
3129 // shifted_sig is [bv_sz-1] . [bv_sz-2 ... 0] * 2^(bv_sz-1) * 2^(-lz)
3130 unsigned sig_sz = sbits + 4; // we want extra rounding bits.
3131 if (sig_sz <= bv_sz) {
3132 expr_ref sig_rest(m);
3133 sig_4 = m_bv_util.mk_extract(bv_sz - 1, bv_sz - sig_sz + 1, shifted_sig); // one short
3134 sig_rest = m_bv_util.mk_extract(bv_sz - sig_sz, 0, shifted_sig);
3135 sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sig_rest.get());
3136 sig_4 = m_bv_util.mk_concat(sig_4, sticky);
3137 }
3138 else {
3139 unsigned extra_bits = sig_sz - bv_sz;
3140 expr_ref extra_zeros(m);
3141 extra_zeros = m_bv_util.mk_numeral(0, extra_bits);
3142 sig_4 = m_bv_util.mk_concat(shifted_sig, extra_zeros);
3143 lz = m_bv_util.mk_bv_add(m_bv_util.mk_concat(extra_zeros, lz),
3144 m_bv_util.mk_numeral(extra_bits, sig_sz));
3145 bv_sz = bv_sz + extra_bits;
3146 SASSERT(is_well_sorted(m, lz));
3147 }
3148 SASSERT(m_bv_util.get_bv_size(sig_4) == sig_sz);
3149
3150 expr_ref s_exp(m), exp_rest(m);
3151 s_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(bv_sz - 2, bv_sz), lz);
3152 // s_exp = (bv_sz-2) + (-lz) signed
3153 SASSERT(m_bv_util.get_bv_size(s_exp) == bv_sz);
3154
3155 unsigned exp_sz = ebits + 2; // (+2 for rounder)
3156 exp_2 = m_bv_util.mk_extract(exp_sz - 1, 0, s_exp);
3157 // the remaining bits are 0 if ebits is large enough.
3158 exp_too_large = m.mk_false(); // This is always in range.
3159
3160 // The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
3161 // exp < bv_sz (+sign bit which is [0])
3162 unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0);
3163
3164 if (exp_sz < exp_worst_case_sz) {
3165 // exp_sz < exp_worst_case_sz and exp >= 0.
3166 // Take the maximum legal exponent; this
3167 // allows us to keep the most precision.
3168 expr_ref max_exp(m), max_exp_bvsz(m), zero_sig_sz(m);
3169 mk_max_exp(exp_sz, max_exp);
3170 max_exp_bvsz = m_bv_util.mk_zero_extend(bv_sz - exp_sz, max_exp);
3171
3172 exp_too_large = m_bv_util.mk_sle(m_bv_util.mk_bv_add(
3173 max_exp_bvsz,
3174 m_bv_util.mk_numeral(1, bv_sz)),
3175 s_exp);
3176 zero_sig_sz = m_bv_util.mk_numeral(0, sig_sz);
3177 sig_4 = m.mk_ite(exp_too_large, zero_sig_sz, sig_4);
3178 exp_2 = m.mk_ite(exp_too_large, max_exp, exp_2);
3179 }
3180 dbg_decouple("fpa2bv_to_fp_unsigned_exp_too_large", exp_too_large);
3181
3182 expr_ref sgn(m), sig(m), exp(m);
3183 sgn = bv0_1;
3184 sig = sig_4;
3185 exp = exp_2;
3186
3187 dbg_decouple("fpa2bv_to_fp_unsigned_sgn", sgn);
3188 dbg_decouple("fpa2bv_to_fp_unsigned_sig", sig);
3189 dbg_decouple("fpa2bv_to_fp_unsigned_exp", exp);
3190
3191 SASSERT(m_bv_util.get_bv_size(sig) == sbits + 4);
3192 SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
3193
3194 expr_ref v2(m);
3195 round(f->get_range(), rm, sgn, sig, exp, v2);
3196
3197 mk_ite(c1, v1, v2, result);
3198 }
3199
mk_to_ieee_bv(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3200 void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3201 SASSERT(num == 1);
3202 expr_ref x(m), x_is_nan(m);
3203 expr_ref sgn(m), s(m), e(m);
3204 x = args[0];
3205 split_fp(x, sgn, e, s);
3206 mk_is_nan(x, x_is_nan);
3207
3208 expr_ref unspec(m);
3209 mk_to_ieee_bv_unspecified(f, num, args, unspec);
3210
3211 expr_ref sgn_e_s(m);
3212 join_fp(x, sgn_e_s);
3213 m_simp.mk_ite(x_is_nan, unspec, sgn_e_s, result);
3214
3215 TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
3216 SASSERT(is_well_sorted(m, result));
3217 }
3218
mk_to_ieee_bv_unspecified(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3219 void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3220 SASSERT(num == 1);
3221 SASSERT(m_util.is_float(args[0]));
3222 unsigned ebits = f->get_domain()[0]->get_parameter(0).get_int();
3223 unsigned sbits = f->get_domain()[0]->get_parameter(1).get_int();
3224
3225 if (m_hi_fp_unspecified) {
3226 mk_nan(f->get_domain()[0], result);
3227 join_fp(result, result);
3228 }
3229 else {
3230 expr_ref nw = nan_wrap(args[0]);
3231
3232 sort * domain[1] = { nw->get_sort() };
3233 func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
3234 result = m.mk_app(f_bv, nw);
3235
3236 expr_ref exp_bv(m), exp_all_ones(m);
3237 exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
3238 exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits)));
3239 m_extra_assertions.push_back(std::move(exp_all_ones));
3240
3241 expr_ref sig_bv(m), sig_is_non_zero(m);
3242 sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
3243 sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
3244 m_extra_assertions.push_back(std::move(sig_is_non_zero));
3245 }
3246
3247 TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
3248 SASSERT(is_well_sorted(m, result));
3249 }
3250
mk_to_bv(func_decl * f,unsigned num,expr * const * args,bool is_signed,expr_ref & result)3251 void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {
3252 TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++)
3253 tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
3254
3255 SASSERT(num == 2);
3256 SASSERT(m_util.is_bv2rm(args[0]));
3257 SASSERT(m_util.is_float(args[1]));
3258
3259 expr * rm = to_app(args[0])->get_arg(0);
3260 expr * x = args[1];
3261 sort * xs = x->get_sort();
3262 sort * bv_srt = f->get_range();
3263
3264 expr_ref sgn(m), sig(m), exp(m), lz(m);
3265 unpack(x, sgn, sig, exp, lz, true);
3266
3267 unsigned ebits = m_util.get_ebits(xs);
3268 unsigned sbits = m_util.get_sbits(xs);
3269 unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
3270
3271 expr_ref bv0(m), bv1(m);
3272 bv0 = m_bv_util.mk_numeral(0, 1);
3273 bv1 = m_bv_util.mk_numeral(1, 1);
3274
3275 expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m);
3276 mk_is_nan(x, x_is_nan);
3277 mk_is_inf(x, x_is_inf);
3278 mk_is_zero(x, x_is_zero);
3279 mk_is_neg(x, x_is_neg);
3280 mk_is_nzero(x, x_is_nzero);
3281
3282 // NaN, Inf, or negative (except -0) -> unspecified
3283 expr_ref c1(m), v1(m), unspec_v(m);
3284 c1 = m.mk_or(x_is_nan, x_is_inf);
3285 mk_to_bv_unspecified(f, num, args, unspec_v);
3286 v1 = unspec_v;
3287 dbg_decouple("fpa2bv_to_bv_c1", c1);
3288
3289 // +-0 -> 0
3290 expr_ref c2(m), v2(m);
3291 c2 = x_is_zero;
3292 v2 = m_bv_util.mk_numeral(rational(0), bv_srt);
3293 dbg_decouple("fpa2bv_to_bv_c2", c2);
3294
3295 // Otherwise...
3296
3297 dbg_decouple("fpa2bv_to_bv_sgn", sgn);
3298 dbg_decouple("fpa2bv_to_bv_sig", sig);
3299 dbg_decouple("fpa2bv_to_bv_exp", exp);
3300 dbg_decouple("fpa2bv_to_bv_lz", lz);
3301
3302 // sig is of the form +- [1].[sig] * 2^(exp-lz)
3303 SASSERT(m_bv_util.get_bv_size(sgn) == 1);
3304 SASSERT(m_bv_util.get_bv_size(sig) == sbits);
3305 SASSERT(m_bv_util.get_bv_size(exp) == ebits);
3306 SASSERT(m_bv_util.get_bv_size(lz) == ebits);
3307
3308 unsigned sig_sz = sbits;
3309 if (sig_sz < (bv_sz + 3))
3310 sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, bv_sz-sig_sz+3));
3311 sig_sz = m_bv_util.get_bv_size(sig);
3312 SASSERT(sig_sz >= (bv_sz + 3));
3313
3314 // x is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
3315
3316 expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), is_neg_shift(m), big_sig(m);
3317 exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
3318 m_bv_util.mk_zero_extend(2, lz));
3319
3320 // big_sig is +- [... bv_sz+2 bits ...][1].[r][ ... sbits-1 ... ]
3321 big_sig = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(bv_sz + 2, sig), bv0);
3322 unsigned big_sig_sz = sig_sz+1+bv_sz+2;
3323 SASSERT(m_bv_util.get_bv_size(big_sig) == big_sig_sz);
3324
3325 is_neg_shift = m_bv_util.mk_sle(exp_m_lz, m_bv_util.mk_numeral(0, ebits+2));
3326 shift = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_neg(exp_m_lz), exp_m_lz);
3327 if (ebits+2 < big_sig_sz)
3328 shift = m_bv_util.mk_zero_extend(big_sig_sz-ebits-2, shift);
3329 else if (ebits+2 > big_sig_sz) {
3330 expr_ref upper(m);
3331 upper = m_bv_util.mk_extract(big_sig_sz, ebits+2, shift);
3332 shift = m_bv_util.mk_extract(ebits+1, 0, shift);
3333 shift = m.mk_ite(m.mk_eq(upper, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(upper))),
3334 shift,
3335 m_bv_util.mk_numeral(big_sig_sz-1, ebits+2));
3336 }
3337 dbg_decouple("fpa2bv_to_bv_shift_uncapped", shift);
3338 SASSERT(m_bv_util.get_bv_size(shift) == m_bv_util.get_bv_size(big_sig));
3339 dbg_decouple("fpa2bv_to_bv_big_sig", big_sig);
3340
3341 expr_ref shift_limit(m);
3342 shift_limit = m_bv_util.mk_numeral(bv_sz+2, m_bv_util.get_bv_size(shift));
3343 shift = m.mk_ite(m_bv_util.mk_ule(shift, shift_limit), shift, shift_limit);
3344 dbg_decouple("fpa2bv_to_bv_shift_limit", shift_limit);
3345 dbg_decouple("fpa2bv_to_bv_is_neg_shift", is_neg_shift);
3346 dbg_decouple("fpa2bv_to_bv_shift", shift);
3347
3348 expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m);
3349 big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift),
3350 m_bv_util.mk_bv_shl(big_sig, shift));
3351 int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted);
3352 SASSERT(m_bv_util.get_bv_size(int_part) == bv_sz+3);
3353 last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted);
3354 round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted);
3355 stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted);
3356 sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies.get());
3357 dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted);
3358 dbg_decouple("fpa2bv_to_bv_int_part", int_part);
3359 dbg_decouple("fpa2bv_to_bv_last", last);
3360 dbg_decouple("fpa2bv_to_bv_round", round);
3361 dbg_decouple("fpa2bv_to_bv_sticky", sticky);
3362
3363 expr_ref rounding_decision(m);
3364 rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky);
3365 SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1);
3366 dbg_decouple("fpa2bv_to_bv_rounding_decision", rounding_decision);
3367
3368 expr_ref inc(m), pre_rounded(m);
3369 inc = m_bv_util.mk_zero_extend(bv_sz+2, rounding_decision);
3370 pre_rounded = m_bv_util.mk_bv_add(int_part, inc);
3371 dbg_decouple("fpa2bv_to_bv_inc", inc);
3372 dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
3373
3374 expr_ref incd(m), pr_is_zero(m), ovfl(m);
3375 incd = m.mk_eq(rounding_decision, bv1);
3376 pr_is_zero = m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz + 3));
3377 ovfl = m.mk_and(incd, pr_is_zero);
3378 dbg_decouple("fpa2bv_to_bv_incd", incd);
3379 dbg_decouple("fpa2bv_to_bv_ovfl", ovfl);
3380
3381 expr_ref ul(m), in_range(m);
3382 if (!is_signed) {
3383 ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz)));
3384 in_range = m.mk_and(m.mk_or(m.mk_not(x_is_neg),
3385 m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz+3))),
3386 m.mk_not(ovfl),
3387 m_bv_util.mk_ule(pre_rounded, ul));
3388 }
3389 else {
3390 expr_ref ll(m);
3391 ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
3392 ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz-1)));
3393 ovfl = m.mk_or(ovfl, m_bv_util.mk_sle(pre_rounded, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz + 3))));
3394 pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded);
3395 in_range = m.mk_and(m.mk_not(ovfl),
3396 m_bv_util.mk_sle(ll, pre_rounded),
3397 m_bv_util.mk_sle(pre_rounded, ul));
3398 dbg_decouple("fpa2bv_to_bv_in_range_ll", ll);
3399 }
3400 dbg_decouple("fpa2bv_to_bv_in_range_ovfl", ovfl);
3401 dbg_decouple("fpa2bv_to_bv_in_range_ul", ul);
3402 dbg_decouple("fpa2bv_to_bv_in_range", in_range);
3403
3404 expr_ref rounded(m);
3405 rounded = m_bv_util.mk_extract(bv_sz-1, 0, pre_rounded);
3406 dbg_decouple("fpa2bv_to_bv_rounded", rounded);
3407
3408 result = m.mk_ite(m.mk_not(in_range), unspec_v, rounded);
3409 result = m.mk_ite(c2, v2, result);
3410 result = m.mk_ite(c1, v1, result);
3411
3412 SASSERT(is_well_sorted(m, result));
3413 }
3414
mk_to_ubv(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3415 void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3416 TRACE("fpa2bv_to_ubv", for (unsigned i = 0; i < num; i++)
3417 tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
3418 mk_to_bv(f, num, args, false, result);
3419 }
3420
mk_to_sbv(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3421 void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3422 TRACE("fpa2bv_to_sbv", for (unsigned i = 0; i < num; i++)
3423 tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
3424 mk_to_bv(f, num, args, true, result);
3425 }
3426
mk_to_ubv_i(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3427 void fpa2bv_converter::mk_to_ubv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3428 func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_UBV, 0, nullptr, num, args), m);
3429 mk_to_bv(f, num, args, false, result);
3430 }
3431
mk_to_sbv_i(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3432 void fpa2bv_converter::mk_to_sbv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3433 func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_SBV, 0, nullptr, num, args), m);
3434 mk_to_bv(f, num, args, true, result);
3435 }
3436
nan_wrap(expr * n)3437 expr_ref fpa2bv_converter::nan_wrap(expr * n) {
3438 expr_ref n_bv(m), arg_is_nan(m), nan(m), nan_bv(m), res(m);
3439 mk_is_nan(n, arg_is_nan);
3440 mk_nan(n->get_sort(), nan);
3441 join_fp(nan, nan_bv);
3442 join_fp(n, n_bv);
3443 res = expr_ref(m.mk_ite(arg_is_nan, nan_bv, n_bv), m);
3444 SASSERT(is_well_sorted(m, res));
3445 return res;
3446 }
3447
mk_to_bv_unspecified(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3448 void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3449 SASSERT(num == 2);
3450 SASSERT(m_util.is_bv2rm(args[0]));
3451 SASSERT(m_util.is_float(args[1]));
3452
3453 if (m_hi_fp_unspecified)
3454 result = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(f->get_range()));
3455 else {
3456 expr * rm_bv = to_app(args[0])->get_arg(0);
3457 expr_ref nw = nan_wrap(args[1]);
3458 sort * domain[2] = { rm_bv->get_sort(), nw->get_sort() };
3459 func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
3460 result = m.mk_app(f_bv, rm_bv, nw);
3461 }
3462
3463 TRACE("fpa2bv_to_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
3464 SASSERT(is_well_sorted(m, result));
3465 }
3466
mk_to_real_unspecified(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3467 void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3468 SASSERT(num == 1);
3469
3470 if (m_hi_fp_unspecified)
3471 result = m_arith_util.mk_numeral(rational(0), false);
3472 else {
3473 expr * n = args[0];
3474 expr_ref nw = nan_wrap(n);
3475 sort * domain[1] = { nw->get_sort() };
3476 func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
3477 result = m.mk_app(f_bv, nw);
3478 }
3479 }
3480
mk_fp(func_decl * f,unsigned num,expr * const * args,expr_ref & result)3481 void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
3482 SASSERT(num == 3);
3483 SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
3484 SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2]) + 1);
3485 SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
3486 result = m_util.mk_fp(args[0], args[1], args[2]);
3487 TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;);
3488 }
3489
3490
split_fp(expr * e,expr_ref & sgn,expr_ref & exp,expr_ref & sig) const3491 void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const {
3492 expr* e_sgn = nullptr, *e_exp = nullptr, *e_sig = nullptr;
3493 VERIFY(m_util.is_fp(e, e_sgn, e_exp, e_sig));
3494 sgn = e_sgn;
3495 exp = e_exp;
3496 sig = e_sig;
3497 }
3498
join_fp(expr * e,expr_ref & res)3499 void fpa2bv_converter::join_fp(expr * e, expr_ref & res) {
3500 expr_ref sgn(m), exp(m), sig(m);
3501 split_fp(e, sgn, exp, sig);
3502 res = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, exp), sig);
3503 }
3504
mk_is_nan(expr * e,expr_ref & result)3505 void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
3506 expr_ref sgn(m), sig(m), exp(m);
3507 split_fp(e, sgn, exp, sig);
3508
3509 // exp == 1^n , sig != 0
3510 expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m), zero(m);
3511 mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
3512
3513 zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
3514 m_simp.mk_eq(sig, zero, sig_is_zero);
3515 m_simp.mk_not(sig_is_zero, sig_is_not_zero);
3516 m_simp.mk_eq(exp, top_exp, exp_is_top);
3517 m_simp.mk_and(exp_is_top, sig_is_not_zero, result);
3518 }
3519
mk_is_inf(expr * e,expr_ref & result)3520 void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) {
3521 expr_ref sgn(m), sig(m), exp(m);
3522 split_fp(e, sgn, exp, sig);
3523 expr_ref eq1(m), eq2(m), top_exp(m), zero(m);
3524 mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
3525 zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
3526 m_simp.mk_eq(sig, zero, eq1);
3527 m_simp.mk_eq(exp, top_exp, eq2);
3528 m_simp.mk_and(eq1, eq2, result);
3529 }
3530
mk_is_pinf(expr * e,expr_ref & result)3531 void fpa2bv_converter::mk_is_pinf(expr * e, expr_ref & result) {
3532 expr_ref e_is_pos(m), e_is_inf(m);
3533 mk_is_pos(e, e_is_pos);
3534 mk_is_inf(e, e_is_inf);
3535 m_simp.mk_and(e_is_pos, e_is_inf, result);
3536 }
3537
mk_is_ninf(expr * e,expr_ref & result)3538 void fpa2bv_converter::mk_is_ninf(expr * e, expr_ref & result) {
3539 expr_ref e_is_neg(m), e_is_inf(m);
3540 mk_is_neg(e, e_is_neg);
3541 mk_is_inf(e, e_is_inf);
3542 m_simp.mk_and(e_is_neg, e_is_inf, result);
3543 }
3544
mk_is_pos(expr * e,expr_ref & result)3545 void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) {
3546 SASSERT(m_util.is_fp(e));
3547 SASSERT(to_app(e)->get_num_args() == 3);
3548 expr * a0 = to_app(e)->get_arg(0);
3549 expr_ref zero(m);
3550 zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(a0));
3551 m_simp.mk_eq(a0, zero, result);
3552 }
3553
mk_is_neg(expr * e,expr_ref & result)3554 void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) {
3555 SASSERT(m_util.is_fp(e));
3556 SASSERT(to_app(e)->get_num_args() == 3);
3557 expr * a0 = to_app(e)->get_arg(0);
3558 expr_ref one(m);
3559 one = m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(a0));
3560 m_simp.mk_eq(a0, one, result);
3561 }
3562
mk_is_zero(expr * e,expr_ref & result)3563 void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
3564 expr_ref sgn(m), sig(m), exp(m);
3565 split_fp(e, sgn, exp, sig);
3566 expr_ref eq1(m), eq2(m), bot_exp(m), zero(m);
3567 mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp);
3568 zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
3569 m_simp.mk_eq(sig, zero, eq1);
3570 m_simp.mk_eq(exp, bot_exp, eq2);
3571 m_simp.mk_and(eq1, eq2, result);
3572 }
3573
mk_is_nzero(expr * e,expr_ref & result)3574 void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
3575 expr_ref sgn(m), sig(m), exp(m);
3576 split_fp(e, sgn, exp, sig);
3577 expr_ref e_is_zero(m), eq(m), one_1(m);
3578 mk_is_zero(e, e_is_zero);
3579 one_1 = m_bv_util.mk_numeral(1, 1);
3580 m_simp.mk_eq(sgn, one_1, eq);
3581 m_simp.mk_and(eq, e_is_zero, result);
3582 }
3583
mk_is_pzero(expr * e,expr_ref & result)3584 void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
3585 expr_ref sgn(m), sig(m), exp(m);
3586 split_fp(e, sgn, exp, sig);
3587 expr_ref e_is_zero(m), eq(m), nil_1(m);
3588 mk_is_zero(e, e_is_zero);
3589 nil_1 = m_bv_util.mk_numeral(0, 1);
3590 m_simp.mk_eq(sgn, nil_1, eq);
3591 m_simp.mk_and(eq, e_is_zero, result);
3592 }
3593
mk_is_denormal(expr * e,expr_ref & result)3594 void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
3595 expr_ref sgn(m), sig(m), exp(m);
3596 split_fp(e, sgn, exp, sig);
3597
3598 expr_ref zero(m), zexp(m), is_zero(m), n_is_zero(m);
3599 zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp));
3600 m_simp.mk_eq(exp, zero, result);
3601 m_simp.mk_eq(exp, zero, zexp);
3602 mk_is_zero(e, is_zero);
3603 m_simp.mk_not(is_zero, n_is_zero);
3604 m_simp.mk_and(n_is_zero, zexp, result);
3605 }
3606
mk_is_normal(expr * e,expr_ref & result)3607 void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {
3608 expr_ref sgn(m), sig(m), exp(m);
3609 split_fp(e, sgn, exp, sig);
3610
3611 expr_ref is_special(m), is_denormal(m), p(m), is_zero(m);
3612 mk_is_denormal(e, is_denormal);
3613 mk_is_zero(e, is_zero);
3614 unsigned ebits = m_bv_util.get_bv_size(exp);
3615 p = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits);
3616 m_simp.mk_eq(exp, p, is_special);
3617
3618 expr_ref or_ex(m);
3619 m_simp.mk_or(is_special, is_denormal, or_ex);
3620 m_simp.mk_or(is_zero, or_ex, or_ex);
3621 m_simp.mk_not(or_ex, result);
3622 }
3623
mk_is_rm(expr * rme,BV_RM_VAL rm,expr_ref & result)3624 void fpa2bv_converter::mk_is_rm(expr * rme, BV_RM_VAL rm, expr_ref & result) {
3625 expr_ref rm_num(m);
3626 rm_num = m_bv_util.mk_numeral(rm, 3);
3627
3628 switch(rm)
3629 {
3630 case BV_RM_TIES_TO_AWAY:
3631 case BV_RM_TIES_TO_EVEN:
3632 case BV_RM_TO_NEGATIVE:
3633 case BV_RM_TO_POSITIVE:
3634 case BV_RM_TO_ZERO:
3635 return m_simp.mk_eq(rme, rm_num, result);
3636 default:
3637 UNREACHABLE();
3638 }
3639 }
3640
mk_top_exp(unsigned sz,expr_ref & result)3641 void fpa2bv_converter::mk_top_exp(unsigned sz, expr_ref & result) {
3642 result = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(sz), sz);
3643 }
3644
mk_bot_exp(unsigned sz,expr_ref & result)3645 void fpa2bv_converter::mk_bot_exp(unsigned sz, expr_ref & result) {
3646 result = m_bv_util.mk_numeral(0, sz);
3647 }
3648
mk_min_exp(unsigned ebits,expr_ref & result)3649 void fpa2bv_converter::mk_min_exp(unsigned ebits, expr_ref & result) {
3650 SASSERT(ebits >= 2);
3651 const mpz & z = m_mpf_manager.m_powers2.m1(ebits-1, true);
3652 result = m_bv_util.mk_numeral(z + mpz(1), ebits);
3653 }
3654
mk_max_exp(unsigned ebits,expr_ref & result)3655 void fpa2bv_converter::mk_max_exp(unsigned ebits, expr_ref & result) {
3656 SASSERT(ebits >= 2);
3657 result = m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(ebits-1, false), ebits);
3658 }
3659
mk_leading_zeros(expr * e,unsigned max_bits,expr_ref & result)3660 void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & result) {
3661 SASSERT(m_bv_util.is_bv(e));
3662 unsigned bv_sz = m_bv_util.get_bv_size(e);
3663
3664 if (bv_sz == 0)
3665 result = m_bv_util.mk_numeral(0, max_bits);
3666 else if (bv_sz == 1) {
3667 expr_ref eq(m), nil_1(m), one_m(m), nil_m(m);
3668 nil_1 = m_bv_util.mk_numeral(0, 1);
3669 one_m = m_bv_util.mk_numeral(1, max_bits);
3670 nil_m = m_bv_util.mk_numeral(0, max_bits);
3671 m_simp.mk_eq(e, nil_1, eq);
3672 m_simp.mk_ite(eq, one_m, nil_m, result);
3673 }
3674 else {
3675 expr_ref H(m), L(m);
3676 H = m_bv_util.mk_extract(bv_sz-1, bv_sz/2, e);
3677 L = m_bv_util.mk_extract(bv_sz/2-1, 0, e);
3678
3679 unsigned H_size = m_bv_util.get_bv_size(H);
3680 // unsigned L_size = m_bv_util.get_bv_size(L);
3681
3682 expr_ref lzH(m), lzL(m);
3683 mk_leading_zeros(H, max_bits, lzH); /* recursive! */
3684 mk_leading_zeros(L, max_bits, lzL);
3685
3686 expr_ref H_is_zero(m), nil_h(m);
3687 nil_h = m_bv_util.mk_numeral(0, H_size);
3688 m_simp.mk_eq(H, nil_h, H_is_zero);
3689
3690 expr_ref sum(m), h_m(m);
3691 h_m = m_bv_util.mk_numeral(H_size, max_bits);
3692 sum = m_bv_util.mk_bv_add(h_m, lzL);
3693 m_simp.mk_ite(H_is_zero, sum, lzH, result);
3694 }
3695
3696 SASSERT(is_well_sorted(m, result));
3697 }
3698
mk_bias(expr * e,expr_ref & result)3699 void fpa2bv_converter::mk_bias(expr * e, expr_ref & result) {
3700 unsigned ebits = m_bv_util.get_bv_size(e);
3701 SASSERT(ebits >= 2);
3702
3703 expr_ref bias(m);
3704 bias = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits);
3705 result = m_bv_util.mk_bv_add(e, bias);
3706 }
3707
mk_unbias(expr * e,expr_ref & result)3708 void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) {
3709 unsigned ebits = m_bv_util.get_bv_size(e);
3710 SASSERT(ebits >= 2);
3711
3712 expr_ref e_plus_one(m);
3713 e_plus_one = m_bv_util.mk_bv_add(e, m_bv_util.mk_numeral(1, ebits));
3714
3715 expr_ref leading(m), n_leading(m), rest(m);
3716 leading = m_bv_util.mk_extract(ebits-1, ebits-1, e_plus_one);
3717 n_leading = m_bv_util.mk_bv_not(leading);
3718 rest = m_bv_util.mk_extract(ebits-2, 0, e_plus_one);
3719
3720 result = m_bv_util.mk_concat(n_leading, rest);
3721 }
3722
unpack(expr * e,expr_ref & sgn,expr_ref & sig,expr_ref & exp,expr_ref & lz,bool normalize)3723 void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize) {
3724 SASSERT(m_util.is_fp(e));
3725 SASSERT(to_app(e)->get_num_args() == 3);
3726
3727 sort * srt = to_app(e)->get_decl()->get_range();
3728 SASSERT(is_float(srt));
3729 unsigned sbits = m_util.get_sbits(srt);
3730 unsigned ebits = m_util.get_ebits(srt);
3731
3732 split_fp(e, sgn, exp, sig);
3733
3734 SASSERT(m_bv_util.get_bv_size(sgn) == 1);
3735 SASSERT(m_bv_util.get_bv_size(exp) == ebits);
3736 SASSERT(m_bv_util.get_bv_size(sig) == sbits-1);
3737
3738 dbg_decouple("fpa2bv_unpack_sgn", sgn);
3739 dbg_decouple("fpa2bv_unpack_exp", exp);
3740 dbg_decouple("fpa2bv_unpack_sig", sig);
3741
3742 expr_ref is_normal(m);
3743 mk_is_normal(e, is_normal);
3744
3745 expr_ref normal_sig(m), normal_exp(m);
3746 normal_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(1, 1), sig);
3747 mk_unbias(exp, normal_exp);
3748 dbg_decouple("fpa2bv_unpack_normal_exp", normal_exp);
3749
3750 expr_ref denormal_sig(m), denormal_exp(m);
3751 denormal_sig = m_bv_util.mk_zero_extend(1, sig);
3752 denormal_exp = m_bv_util.mk_numeral(1, ebits);
3753 mk_unbias(denormal_exp, denormal_exp);
3754 dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp);
3755
3756 expr_ref zero_e(m);
3757 zero_e = m_bv_util.mk_numeral(0, ebits);
3758
3759 if (normalize) {
3760 expr_ref is_sig_zero(m), zero_s(m);
3761 zero_s = m_bv_util.mk_numeral(0, sbits);
3762 m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero);
3763
3764 expr_ref lz_d(m), norm_or_zero(m);
3765 mk_leading_zeros(denormal_sig, ebits, lz_d);
3766 norm_or_zero = m.mk_or(is_normal, is_sig_zero);
3767 m_simp.mk_ite(norm_or_zero, zero_e, lz_d, lz);
3768 dbg_decouple("fpa2bv_unpack_lz", lz);
3769
3770 expr_ref shift(m);
3771 m_simp.mk_ite(is_sig_zero, zero_e, lz, shift);
3772 dbg_decouple("fpa2bv_unpack_shift", shift);
3773 SASSERT(is_well_sorted(m, is_sig_zero));
3774 SASSERT(is_well_sorted(m, shift));
3775 SASSERT(m_bv_util.get_bv_size(shift) == ebits);
3776 if (ebits <= sbits) {
3777 expr_ref q(m);
3778 q = m_bv_util.mk_zero_extend(sbits-ebits, shift);
3779 denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q);
3780 }
3781 else {
3782 // the maximum shift is `sbits', because after that the mantissa
3783 // would be zero anyways. So we can safely cut the shift variable down,
3784 // as long as we check the higher bits.
3785 expr_ref zero_ems(m), sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m);
3786 zero_ems = m_bv_util.mk_numeral(0, ebits - sbits);
3787 sbits_s = m_bv_util.mk_numeral(sbits, sbits);
3788 sh = m_bv_util.mk_extract(ebits-1, sbits, shift);
3789 m_simp.mk_eq(zero_ems, sh, is_sh_zero);
3790 short_shift = m_bv_util.mk_extract(sbits-1, 0, shift);
3791 m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl);
3792 denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl);
3793 }
3794 }
3795 else
3796 lz = zero_e;
3797
3798 SASSERT(is_well_sorted(m, normal_sig));
3799 SASSERT(is_well_sorted(m, denormal_sig));
3800 SASSERT(is_well_sorted(m, normal_exp));
3801 SASSERT(is_well_sorted(m, denormal_exp));
3802
3803 dbg_decouple("fpa2bv_unpack_is_normal", is_normal);
3804
3805 m_simp.mk_ite(is_normal, normal_sig, denormal_sig, sig);
3806 m_simp.mk_ite(is_normal, normal_exp, denormal_exp, exp);
3807
3808 SASSERT(is_well_sorted(m, sgn));
3809 SASSERT(is_well_sorted(m, sig));
3810 SASSERT(is_well_sorted(m, exp));
3811
3812 SASSERT(m_bv_util.get_bv_size(sgn) == 1);
3813 SASSERT(m_bv_util.get_bv_size(sig) == sbits);
3814 SASSERT(m_bv_util.get_bv_size(exp) == ebits);
3815
3816 TRACE("fpa2bv_unpack", tout << "UNPACK SGN = " << mk_ismt2_pp(sgn, m) << std::endl; );
3817 TRACE("fpa2bv_unpack", tout << "UNPACK SIG = " << mk_ismt2_pp(sig, m) << std::endl; );
3818 TRACE("fpa2bv_unpack", tout << "UNPACK EXP = " << mk_ismt2_pp(exp, m) << std::endl; );
3819 }
3820
mk_rounding_mode(decl_kind k,expr_ref & result)3821 void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result)
3822 {
3823 switch(k)
3824 {
3825 case OP_FPA_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break;
3826 case OP_FPA_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break;
3827 case OP_FPA_RM_TOWARD_POSITIVE: result = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); break;
3828 case OP_FPA_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break;
3829 case OP_FPA_RM_TOWARD_ZERO: result = m_bv_util.mk_numeral(BV_RM_TO_ZERO, 3); break;
3830 default: UNREACHABLE();
3831 }
3832
3833 result = m_util.mk_bv2rm(result);
3834 }
3835
dbg_decouple(const char * prefix,expr_ref & e)3836 void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
3837 #ifdef Z3DEBUG_FPA2BV_NAMES
3838 return;
3839 // CMW: This works only for quantifier-free formulas.
3840 if (m_util.is_fp(e)) {
3841 expr_ref new_bv(m);
3842 expr_ref e_sgn(m), e_sig(m), e_exp(m);
3843 split_fp(e, e_sgn, e_exp, e_sig);
3844 unsigned ebits = m_bv_util.get_bv_size(e_exp);
3845 unsigned sbits = m_bv_util.get_bv_size(e_sig) + 1;
3846 unsigned bv_sz = ebits + sbits;
3847 new_bv = m.mk_fresh_const(prefix, m_bv_util.mk_sort(bv_sz));
3848 expr_ref bv_sgn(m), bv_exp(m), bv_sig(m);
3849 bv_sgn = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, new_bv);
3850 bv_exp = m_bv_util.mk_extract(bv_sz-2, bv_sz-ebits-1, new_bv);
3851 bv_sig = m_bv_util.mk_extract(sbits-2, 0, new_bv);
3852
3853 expr_ref e_sgn_eq_bv_sgn(m), e_exp_eq_bv_exp(m), e_sig_eq_bv_sig(m);
3854 e_sgn_eq_bv_sgn = m.mk_eq(e_sgn, bv_sgn);
3855 e_exp_eq_bv_exp = m.mk_eq(e_exp, bv_exp);
3856 e_sig_eq_bv_sig = m.mk_eq(e_sig, bv_sig);
3857 m_extra_assertions.push_back(e_sgn_eq_bv_sgn);
3858 m_extra_assertions.push_back(e_exp_eq_bv_exp);
3859 m_extra_assertions.push_back(e_sig_eq_bv_sig);
3860 e = m_util.mk_fp(bv_sgn, bv_exp, bv_sig);
3861 }
3862 else {
3863 expr_ref new_e(m), new_e_eq_e(m);
3864 new_e = m.mk_fresh_const(prefix, e->get_sort());
3865 new_e_eq_e = m.mk_eq(new_e, e);
3866 m_extra_assertions.push_back(new_e_eq_e);
3867 e = new_e;
3868 }
3869 #endif
3870 }
3871
mk_rounding_decision(expr * rm,expr * sgn,expr * last,expr * round,expr * sticky)3872 expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) {
3873 expr_ref rmr(rm, m);
3874 expr_ref sgnr(sgn, m);
3875 expr_ref lastr(last, m);
3876 expr_ref roundr(round, m);
3877 expr_ref stickyr(sticky, m);
3878 dbg_decouple("fpa2bv_rnd_dec_rm", rmr);
3879 dbg_decouple("fpa2bv_rnd_dec_sgn", sgnr);
3880 dbg_decouple("fpa2bv_rnd_dec_last", lastr);
3881 dbg_decouple("fpa2bv_rnd_dec_round", roundr);
3882 dbg_decouple("fpa2bv_rnd_dec_sticky", stickyr);
3883
3884 expr_ref last_or_sticky(m), round_or_sticky(m), not_last(m), not_round(m), not_sticky(m), not_lors(m), not_rors(m), not_sgn(m);
3885 expr * last_sticky[2] = { last, sticky };
3886 expr * round_sticky[2] = { round, sticky };
3887 last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky);
3888 round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky);
3889 not_last = m_bv_util.mk_bv_not(last);
3890 not_round = m_bv_util.mk_bv_not(round);
3891 not_sticky = m_bv_util.mk_bv_not(sticky);
3892 not_lors = m_bv_util.mk_bv_not(last_or_sticky);
3893 not_rors = m_bv_util.mk_bv_not(round_or_sticky);
3894 not_sgn = m_bv_util.mk_bv_not(sgn);
3895 expr * nround_lors[2] = { not_round, not_lors };
3896 expr * pos_args[2] = { sgn, not_rors };
3897 expr * neg_args[2] = { not_sgn, not_rors };
3898
3899 expr_ref inc_teven(m), inc_taway(m), inc_pos(m), inc_neg(m);
3900 inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, nround_lors));
3901 inc_taway = round;
3902 inc_pos = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, pos_args));
3903 inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args));
3904
3905 expr_ref res(m), inc_c2(m), inc_c3(m), inc_c4(m);
3906 expr_ref rm_is_to_neg(m), rm_is_to_pos(m), rm_is_away(m), rm_is_even(m), nil_1(m);
3907 nil_1 = m_bv_util.mk_numeral(0, 1);
3908 mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
3909 mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_to_pos);
3910 mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_away);
3911 mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_even);
3912 m_simp.mk_ite(rm_is_to_neg, inc_neg, nil_1, inc_c4);
3913 m_simp.mk_ite(rm_is_to_pos, inc_pos, inc_c4, inc_c3);
3914 m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2);
3915 m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, res);
3916
3917 dbg_decouple("fpa2bv_rnd_dec_res", res);
3918 return res;
3919 }
3920
round(sort * s,expr_ref & rm,expr_ref & sgn,expr_ref & sig,expr_ref & exp,expr_ref & result)3921 void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result) {
3922 unsigned ebits = m_util.get_ebits(s);
3923 unsigned sbits = m_util.get_sbits(s);
3924
3925 dbg_decouple("fpa2bv_rnd_rm", rm);
3926 dbg_decouple("fpa2bv_rnd_sgn", sgn);
3927 dbg_decouple("fpa2bv_rnd_sig", sig);
3928 dbg_decouple("fpa2bv_rnd_exp", exp);
3929
3930 SASSERT(is_well_sorted(m, rm));
3931 SASSERT(is_well_sorted(m, sgn));
3932 SASSERT(is_well_sorted(m, sig));
3933 SASSERT(is_well_sorted(m, exp));
3934
3935 TRACE("fpa2bv_dbg", tout << "RND: " << std::endl <<
3936 "ebits = " << ebits << std::endl <<
3937 "sbits = " << sbits << std::endl <<
3938 "sgn = " << mk_ismt2_pp(sgn, m) << std::endl <<
3939 "sig = " << mk_ismt2_pp(sig, m) << std::endl <<
3940 "exp = " << mk_ismt2_pp(exp, m) << std::endl; );
3941
3942 // Assumptions: sig is of the form f[-1:0] . f[1:sbits-1] [guard,round,sticky],
3943 // i.e., it has 2 + (sbits-1) + 3 = sbits + 4 bits, where the first one is in sgn.
3944 // Furthermore, note that sig is an unsigned bit-vector, while exp is signed.
3945
3946 SASSERT(m_bv_util.is_bv(rm) && m_bv_util.get_bv_size(rm) == 3);
3947 SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
3948 SASSERT(m_bv_util.is_bv(sig) && m_bv_util.get_bv_size(sig) >= 5);
3949 SASSERT(m_bv_util.is_bv(exp) && m_bv_util.get_bv_size(exp) >= 4);
3950
3951 SASSERT(m_bv_util.get_bv_size(sig) == sbits+4);
3952 SASSERT(m_bv_util.get_bv_size(exp) == ebits+2);
3953
3954 expr_ref e_min(m), e_max(m);
3955 mk_min_exp(ebits, e_min);
3956 mk_max_exp(ebits, e_max);
3957
3958 TRACE("fpa2bv_dbg", tout << "e_min = " << mk_ismt2_pp(e_min, m) << std::endl;
3959 tout << "e_max = " << mk_ismt2_pp(e_max, m) << std::endl;);
3960
3961 expr_ref OVF1(m), e_top_three(m), sigm1(m), e_eq_emax_and_sigm1(m), e_eq_emax(m);
3962 expr_ref e3(m), ne3(m), e2(m), e1(m), e21(m), one_1(m), h_exp(m), sh_exp(m), th_exp(m);
3963 one_1 = m_bv_util.mk_numeral(1, 1);
3964 h_exp = m_bv_util.mk_extract(ebits+1, ebits+1, exp);
3965 sh_exp = m_bv_util.mk_extract(ebits, ebits, exp);
3966 th_exp = m_bv_util.mk_extract(ebits-1, ebits-1, exp);
3967 m_simp.mk_eq(h_exp, one_1, e3);
3968 m_simp.mk_eq(sh_exp, one_1, e2);
3969 m_simp.mk_eq(th_exp, one_1, e1);
3970 m_simp.mk_or(e2, e1, e21);
3971 m_simp.mk_not(e3, ne3);
3972 m_simp.mk_and(ne3, e21, e_top_three);
3973
3974 expr_ref ext_emax(m), t_sig(m);
3975 ext_emax = m_bv_util.mk_zero_extend(2, e_max);
3976 t_sig = m_bv_util.mk_extract(sbits+3, sbits+3, sig);
3977 m_simp.mk_eq(ext_emax, exp, e_eq_emax);
3978 m_simp.mk_eq(t_sig, one_1, sigm1);
3979 m_simp.mk_and(e_eq_emax, sigm1, e_eq_emax_and_sigm1);
3980 m_simp.mk_or(e_top_three, e_eq_emax_and_sigm1, OVF1);
3981
3982 dbg_decouple("fpa2bv_rnd_OVF1", OVF1);
3983
3984 TRACE("fpa2bv_dbg", tout << "OVF1 = " << mk_ismt2_pp(OVF1, m) << std::endl;);
3985 SASSERT(is_well_sorted(m, OVF1));
3986
3987 expr_ref lz(m);
3988 mk_leading_zeros(sig, ebits+2, lz); // CMW: is this always large enough?
3989
3990 dbg_decouple("fpa2bv_rnd_lz", lz);
3991
3992 TRACE("fpa2bv_dbg", tout << "LZ = " << mk_ismt2_pp(lz, m) << std::endl;);
3993
3994 expr_ref t(m);
3995 t = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2));
3996 t = m_bv_util.mk_bv_sub(t, lz);
3997 t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min));
3998 dbg_decouple("fpa2bv_rnd_t", t);
3999 expr_ref TINY(m);
4000 TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral(rational(-1), ebits+2));
4001 dbg_decouple("fpa2bv_rnd_TINY", TINY);
4002 TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;);
4003 SASSERT(is_well_sorted(m, TINY));
4004
4005 expr_ref beta(m);
4006 beta = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(exp, lz), m_bv_util.mk_numeral(1, ebits+2));
4007
4008 TRACE("fpa2bv_dbg", tout << "beta = " << mk_ismt2_pp(beta, m) << std::endl; );
4009 SASSERT(is_well_sorted(m, beta));
4010
4011 dbg_decouple("fpa2bv_rnd_beta", beta);
4012 dbg_decouple("fpa2bv_rnd_e_min", e_min);
4013 dbg_decouple("fpa2bv_rnd_e_max", e_max);
4014
4015 expr_ref sigma(m), sigma_add(m);
4016 sigma_add = m_bv_util.mk_bv_sub(exp, m_bv_util.mk_sign_extend(2, e_min));
4017 sigma_add = m_bv_util.mk_bv_add(sigma_add, m_bv_util.mk_numeral(1, ebits+2));
4018 m_simp.mk_ite(TINY, sigma_add, lz, sigma);
4019
4020 dbg_decouple("fpa2bv_rnd_sigma", sigma);
4021
4022 TRACE("fpa2bv_dbg", tout << "Shift distance: " << mk_ismt2_pp(sigma, m) << std::endl;);
4023 SASSERT(is_well_sorted(m, sigma));
4024
4025 // Normalization shift
4026 dbg_decouple("fpa2bv_rnd_sig_before_shift", sig);
4027
4028 unsigned sig_size = m_bv_util.get_bv_size(sig);
4029 SASSERT(sig_size == sbits + 4);
4030 SASSERT(m_bv_util.get_bv_size(sigma) == ebits+2);
4031 unsigned sigma_size = ebits + 2;
4032
4033 expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m),
4034 rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m);
4035 sigma_neg = m_bv_util.mk_bv_neg(sigma);
4036 sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size);
4037 sigma_le_cap = m_bv_util.mk_ule(sigma_neg, sigma_cap);
4038 m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped);
4039 dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg);
4040 dbg_decouple("fpa2bv_rnd_sigma_cap", sigma_cap);
4041 dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped);
4042 sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(rational(-1), sigma_size));
4043 dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero);
4044
4045 sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size));
4046 rs_sig = m_bv_util.mk_bv_lshr(sig_ext, m_bv_util.mk_zero_extend(2*sig_size - sigma_size, sigma_neg_capped));
4047 ls_sig = m_bv_util.mk_bv_shl(sig_ext, m_bv_util.mk_zero_extend(2*sig_size - sigma_size, sigma));
4048 m_simp.mk_ite(sigma_lt_zero, rs_sig, ls_sig, big_sh_sig);
4049 SASSERT(m_bv_util.get_bv_size(big_sh_sig) == 2*sig_size);
4050
4051 dbg_decouple("fpa2bv_rnd_big_sh_sig", big_sh_sig);
4052
4053 unsigned sig_extract_low_bit = (2*sig_size-1)-(sbits+2)+1;
4054 sig = m_bv_util.mk_extract(2*sig_size-1, sig_extract_low_bit, big_sh_sig);
4055 SASSERT(m_bv_util.get_bv_size(sig) == sbits+2);
4056
4057 dbg_decouple("fpa2bv_rnd_shifted_sig", sig);
4058
4059 expr_ref sticky(m);
4060 sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sig_extract_low_bit-1, 0, big_sh_sig));
4061 SASSERT(is_well_sorted(m, sticky));
4062 SASSERT(is_well_sorted(m, sig));
4063
4064 // put the sticky bit into the significand.
4065 expr_ref ext_sticky(m);
4066 ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky);
4067 expr * tmp[2] = { sig, ext_sticky };
4068 sig = m_bv_util.mk_bv_or(2, tmp);
4069 SASSERT(is_well_sorted(m, sig));
4070 SASSERT(m_bv_util.get_bv_size(sig) == sbits+2);
4071
4072 expr_ref ext_emin(m);
4073 ext_emin = m_bv_util.mk_zero_extend(2, e_min);
4074 m_simp.mk_ite(TINY, ext_emin, beta, exp);
4075 SASSERT(is_well_sorted(m, exp));
4076
4077 // Significand rounding
4078 expr_ref round(m), last(m);
4079 sticky = m_bv_util.mk_extract(0, 0, sig); // new sticky bit!
4080 round = m_bv_util.mk_extract(1, 1, sig);
4081 last = m_bv_util.mk_extract(2, 2, sig);
4082
4083 TRACE("fpa2bv_dbg", tout << "sticky = " << mk_ismt2_pp(sticky, m) << std::endl;);
4084
4085 dbg_decouple("fpa2bv_rnd_sticky", sticky);
4086 dbg_decouple("fpa2bv_rnd_round", round);
4087 dbg_decouple("fpa2bv_rnd_last", last);
4088
4089 sig = m_bv_util.mk_extract(sbits+1, 2, sig);
4090
4091 expr_ref inc(m);
4092 inc = mk_rounding_decision(rm, sgn, last, round, sticky);
4093
4094 SASSERT(m_bv_util.get_bv_size(inc) == 1 && is_well_sorted(m, inc));
4095 dbg_decouple("fpa2bv_rnd_inc", inc);
4096
4097 sig = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(1, sig),
4098 m_bv_util.mk_zero_extend(sbits, inc));
4099 SASSERT(is_well_sorted(m, sig));
4100 dbg_decouple("fpa2bv_rnd_sig_plus_inc", sig);
4101
4102 // Post normalization
4103 SASSERT(m_bv_util.get_bv_size(sig) == sbits + 1);
4104 expr_ref SIGovf(m);
4105 t_sig = m_bv_util.mk_extract(sbits, sbits, sig);
4106 m_simp.mk_eq(t_sig, one_1, SIGovf);
4107 SASSERT(is_well_sorted(m, SIGovf));
4108 dbg_decouple("fpa2bv_rnd_SIGovf", SIGovf);
4109
4110 expr_ref hallbut1_sig(m), lallbut1_sig(m);
4111 hallbut1_sig = m_bv_util.mk_extract(sbits, 1, sig);
4112 lallbut1_sig = m_bv_util.mk_extract(sbits-1, 0, sig);
4113 m_simp.mk_ite(SIGovf, hallbut1_sig, lallbut1_sig, sig);
4114
4115 SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
4116
4117 expr_ref exp_p1(m);
4118 exp_p1 = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2));
4119 m_simp.mk_ite(SIGovf, exp_p1, exp, exp);
4120
4121 SASSERT(is_well_sorted(m, sig));
4122 SASSERT(is_well_sorted(m, exp));
4123 dbg_decouple("fpa2bv_rnd_sig_postnormalized", sig);
4124 dbg_decouple("fpa2bv_rnd_exp_postnormalized", exp);
4125
4126 SASSERT(m_bv_util.get_bv_size(sig) == sbits);
4127 SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
4128 SASSERT(m_bv_util.get_bv_size(e_max) == ebits);
4129
4130 // Exponent adjustment and rounding
4131 expr_ref biased_exp(m);
4132 mk_bias(m_bv_util.mk_extract(ebits-1, 0, exp), biased_exp);
4133 dbg_decouple("fpa2bv_rnd_unbiased_exp", exp);
4134 dbg_decouple("fpa2bv_rnd_biased_exp", biased_exp);
4135
4136 // AdjustExp
4137 SASSERT(is_well_sorted(m, OVF1));
4138 SASSERT(m.is_bool(OVF1));
4139
4140 expr_ref preOVF2(m), OVF2(m), OVF(m), exp_redand(m), pem2m1(m);
4141 exp_redand = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, biased_exp.get());
4142 m_simp.mk_eq(exp_redand, one_1, preOVF2);
4143 m_simp.mk_and(SIGovf, preOVF2, OVF2);
4144 pem2m1 = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-2), ebits);
4145 m_simp.mk_ite(OVF2, pem2m1, biased_exp, biased_exp);
4146 m_simp.mk_or(OVF1, OVF2, OVF);
4147
4148 SASSERT(is_well_sorted(m, OVF2));
4149 SASSERT(is_well_sorted(m, OVF));
4150
4151 SASSERT(m.is_bool(OVF2));
4152 SASSERT(m.is_bool(OVF));
4153 dbg_decouple("fpa2bv_rnd_OVF2", OVF2);
4154 dbg_decouple("fpa2bv_rnd_OVF", OVF);
4155
4156 // ExpRnd
4157 expr_ref top_exp(m), bot_exp(m);
4158 mk_top_exp(ebits, top_exp);
4159 mk_bot_exp(ebits, bot_exp);
4160
4161 expr_ref nil_1(m);
4162 nil_1 = m_bv_util.mk_numeral(0, 1);
4163
4164 expr_ref rm_is_to_zero(m), rm_is_to_neg(m), rm_is_to_pos(m), rm_zero_or_neg(m), rm_zero_or_pos(m);
4165 mk_is_rm(rm, BV_RM_TO_ZERO, rm_is_to_zero);
4166 mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
4167 mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_to_pos);
4168 m_simp.mk_or(rm_is_to_zero, rm_is_to_neg, rm_zero_or_neg);
4169 m_simp.mk_or(rm_is_to_zero, rm_is_to_pos, rm_zero_or_pos);
4170 dbg_decouple("fpa2bv_rnd_rm_is_to_zero", rm_is_to_zero);
4171 dbg_decouple("fpa2bv_rnd_rm_is_to_neg", rm_is_to_neg);
4172 dbg_decouple("fpa2bv_rnd_rm_is_to_pos", rm_is_to_pos);
4173
4174 expr_ref sgn_is_zero(m), zero1(m);
4175 zero1 = m_bv_util.mk_numeral(0, 1);
4176 m_simp.mk_eq(sgn, zero1, sgn_is_zero);
4177 dbg_decouple("fpa2bv_rnd_sgn_is_zero", sgn_is_zero);
4178
4179 expr_ref max_sig(m), max_exp(m), inf_sig(m), inf_exp(m);
4180 max_sig = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(sbits-1, false), sbits-1);
4181 max_exp = m_bv_util.mk_concat(m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1, false), ebits-1),
4182 m_bv_util.mk_numeral(0, 1));
4183 inf_sig = m_bv_util.mk_numeral(0, sbits-1);
4184 inf_exp = top_exp;
4185
4186 dbg_decouple("fpa2bv_rnd_max_exp", max_exp);
4187 dbg_decouple("fpa2bv_rnd_max_sig", max_sig);
4188 dbg_decouple("fpa2bv_rnd_inf_sig", inf_sig);
4189 dbg_decouple("fpa2bv_rnd_inf_exp", inf_exp);
4190
4191 expr_ref ovfl_exp(m), max_inf_exp_neg(m), max_inf_exp_pos(m), n_d_check(m), n_d_exp(m);
4192 m_simp.mk_ite(rm_zero_or_pos, max_exp, inf_exp, max_inf_exp_neg);
4193 m_simp.mk_ite(rm_zero_or_neg, max_exp, inf_exp, max_inf_exp_pos);
4194 m_simp.mk_ite(sgn_is_zero, max_inf_exp_pos, max_inf_exp_neg, ovfl_exp);
4195 t_sig = m_bv_util.mk_extract(sbits-1, sbits-1, sig);
4196 m_simp.mk_eq(t_sig, nil_1, n_d_check);
4197 m_simp.mk_ite(n_d_check, bot_exp /* denormal */, biased_exp, n_d_exp);
4198 m_simp.mk_ite(OVF, ovfl_exp, n_d_exp, exp);
4199
4200 expr_ref max_inf_sig_neg(m), max_inf_sig_pos(m), ovfl_sig(m), rest_sig(m);
4201 m_simp.mk_ite(rm_zero_or_pos, max_sig, inf_sig, max_inf_sig_neg);
4202 m_simp.mk_ite(rm_zero_or_neg, max_sig, inf_sig, max_inf_sig_pos);
4203 m_simp.mk_ite(sgn_is_zero, max_inf_sig_pos, max_inf_sig_neg, ovfl_sig);
4204 rest_sig = m_bv_util.mk_extract(sbits-2, 0, sig);
4205 m_simp.mk_ite(OVF, ovfl_sig, rest_sig, sig);
4206
4207 dbg_decouple("fpa2bv_rnd_max_inf_sig_neg", max_inf_sig_neg);
4208 dbg_decouple("fpa2bv_rnd_max_inf_sig_pos", max_inf_sig_pos);
4209 dbg_decouple("fpa2bv_rnd_rm_zero_or_neg", rm_zero_or_neg);
4210 dbg_decouple("fpa2bv_rnd_rm_zero_or_pos", rm_zero_or_pos);
4211
4212 dbg_decouple("fpa2bv_rnd_sgn_final", sgn);
4213 dbg_decouple("fpa2bv_rnd_sig_final", sig);
4214 dbg_decouple("fpa2bv_rnd_exp_final", exp);
4215
4216 expr_ref res_sgn(m), res_sig(m), res_exp(m);
4217 res_sgn = sgn;
4218 res_sig = sig;
4219 res_exp = exp;
4220
4221 SASSERT(m_bv_util.get_bv_size(res_sgn) == 1);
4222 SASSERT(is_well_sorted(m, res_sgn));
4223 SASSERT(m_bv_util.get_bv_size(res_sig) == sbits-1);
4224 SASSERT(is_well_sorted(m, res_sig));
4225 SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
4226 SASSERT(is_well_sorted(m, res_exp));
4227
4228 result = m_util.mk_fp(res_sgn, res_exp, res_sig);
4229
4230 TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
4231 }
4232
reset()4233 void fpa2bv_converter::reset() {
4234 dec_ref_map_key_values(m, m_const2bv);
4235 dec_ref_map_key_values(m, m_rm_const2bv);
4236 for (auto const& kv : m_uf2bvuf) {
4237 m.dec_ref(kv.m_key);
4238 m.dec_ref(kv.m_value);
4239 }
4240 for (auto const& kv : m_min_max_ufs) {
4241 m.dec_ref(kv.m_key);
4242 m.dec_ref(kv.m_value.first);
4243 m.dec_ref(kv.m_value.second);
4244 }
4245 m_uf2bvuf.reset();
4246 m_min_max_ufs.reset();
4247 m_extra_assertions.reset();
4248 }
4249
mk_bv_uf(func_decl * f,sort * const * domain,sort * range)4250 func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) {
4251 func_decl* res;
4252 if (!m_uf2bvuf.find(f, res)) {
4253 res = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
4254 m.inc_ref(f);
4255 m.inc_ref(res);
4256 m_uf2bvuf.insert(f, res);
4257 TRACE("fpa2bv", tout << "New UF func_decl: " << res->get_id() << std::endl << mk_ismt2_pp(res, m) << std::endl;);
4258 }
4259 return res;
4260 }
4261
mk_const(func_decl * f,expr_ref & result)4262 void fpa2bv_converter_wrapped::mk_const(func_decl* f, expr_ref& result) {
4263 SASSERT(f->get_family_id() == null_family_id);
4264 SASSERT(f->get_arity() == 0);
4265 expr* r;
4266 if (m_const2bv.find(f, r)) {
4267 result = r;
4268 }
4269 else {
4270 sort* s = f->get_range();
4271 expr_ref bv(m);
4272 bv = wrap(m.mk_const(f));
4273 unsigned bv_sz = m_bv_util.get_bv_size(bv);
4274 unsigned sbits = m_util.get_sbits(s);
4275 SASSERT(bv_sz == m_util.get_ebits(s) + sbits);
4276 result = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
4277 m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
4278 m_bv_util.mk_extract(sbits - 2, 0, bv));
4279 SASSERT(m_util.is_float(result));
4280 m_const2bv.insert(f, result);
4281 m.inc_ref(f);
4282 m.inc_ref(result);
4283 }
4284 }
4285
wrap(expr * e)4286 app_ref fpa2bv_converter_wrapped::wrap(expr* e) {
4287 SASSERT(m_util.is_float(e) || m_util.is_rm(e));
4288 SASSERT(!m_util.is_bvwrap(e));
4289 app_ref res(m);
4290
4291 if (m_util.is_fp(e)) {
4292 expr* cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
4293 expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);
4294 m_rw(tmp);
4295 res = to_app(tmp);
4296 }
4297 else {
4298 sort* es = e->get_sort();
4299
4300 sort_ref bv_srt(m);
4301 if (is_rm(es))
4302 bv_srt = m_bv_util.mk_sort(3);
4303 else {
4304 SASSERT(is_float(es));
4305 unsigned ebits = m_util.get_ebits(es);
4306 unsigned sbits = m_util.get_sbits(es);
4307 bv_srt = m_bv_util.mk_sort(ebits + sbits);
4308 }
4309
4310 func_decl_ref wrap_fd(m);
4311 wrap_fd = m.mk_func_decl(m_util.get_family_id(), OP_FPA_BVWRAP, 0, nullptr, 1, &es, bv_srt);
4312 res = m.mk_app(wrap_fd, e);
4313 }
4314
4315 return res;
4316 }
4317
unwrap(expr * e,sort * s)4318 app_ref fpa2bv_converter_wrapped::unwrap(expr* e, sort* s) {
4319 SASSERT(!m_util.is_fp(e));
4320 SASSERT(m_bv_util.is_bv(e));
4321 SASSERT(m_util.is_float(s) || m_util.is_rm(s));
4322 app_ref res(m);
4323
4324 unsigned bv_sz = m_bv_util.get_bv_size(e);
4325
4326 if (m_util.is_rm(s)) {
4327 SASSERT(bv_sz == 3);
4328 res = m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), m_util.mk_round_nearest_ties_to_away(),
4329 m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), m_util.mk_round_nearest_ties_to_even(),
4330 m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3)), m_util.mk_round_toward_negative(),
4331 m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), m_util.mk_round_toward_positive(),
4332 m_util.mk_round_toward_zero()))));
4333 }
4334 else {
4335 SASSERT(m_util.is_float(s));
4336 unsigned sbits = m_util.get_sbits(s);
4337 SASSERT(bv_sz == m_util.get_ebits(s) + sbits);
4338 res = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, e),
4339 m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e),
4340 m_bv_util.mk_extract(sbits - 2, 0, e));
4341 }
4342
4343 return res;
4344 }
4345
4346
mk_rm_const(func_decl * f,expr_ref & result)4347 void fpa2bv_converter_wrapped::mk_rm_const(func_decl* f, expr_ref& result) {
4348 SASSERT(f->get_family_id() == null_family_id);
4349 SASSERT(f->get_arity() == 0);
4350 expr* r;
4351 if (m_rm_const2bv.find(f, r)) {
4352 result = r;
4353 }
4354 else {
4355 SASSERT(is_rm(f->get_range()));
4356 expr_ref bv(m);
4357 bv = wrap(m.mk_const(f));
4358 result = m_util.mk_bv2rm(bv);
4359 m_rm_const2bv.insert(f, result);
4360 m.inc_ref(f);
4361 m.inc_ref(result);
4362 }
4363 }
4364
4365
bv2rm_value(expr * b)4366 expr* fpa2bv_converter_wrapped::bv2rm_value(expr* b) {
4367 app* result = nullptr;
4368 unsigned bv_sz;
4369 rational val(0);
4370 VERIFY(m_bv_util.is_numeral(b, val, bv_sz));
4371 SASSERT(bv_sz == 3);
4372
4373 switch (val.get_uint64()) {
4374 case BV_RM_TIES_TO_AWAY: result = m_util.mk_round_nearest_ties_to_away(); break;
4375 case BV_RM_TIES_TO_EVEN: result = m_util.mk_round_nearest_ties_to_even(); break;
4376 case BV_RM_TO_NEGATIVE: result = m_util.mk_round_toward_negative(); break;
4377 case BV_RM_TO_POSITIVE: result = m_util.mk_round_toward_positive(); break;
4378 case BV_RM_TO_ZERO:
4379 default: result = m_util.mk_round_toward_zero();
4380 }
4381
4382 TRACE("t_fpa", tout << "result: " << mk_ismt2_pp(result, m) << std::endl;);
4383 return result;
4384 }
4385
bv2fpa_value(sort * s,expr * a,expr * b,expr * c)4386 expr* fpa2bv_converter_wrapped::bv2fpa_value(sort* s, expr* a, expr* b, expr* c) {
4387 mpf_manager& mpfm = m_util.fm();
4388 unsynch_mpz_manager& mpzm = mpfm.mpz_manager();
4389 app* result;
4390 unsigned ebits = m_util.get_ebits(s);
4391 unsigned sbits = m_util.get_sbits(s);
4392
4393 scoped_mpz bias(mpzm);
4394 mpzm.power(mpz(2), ebits - 1, bias);
4395 mpzm.dec(bias);
4396
4397 scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm);
4398 unsigned bv_sz;
4399
4400 if (b == nullptr) {
4401 SASSERT(m_bv_util.is_bv(a));
4402 SASSERT(m_bv_util.get_bv_size(a) == (ebits + sbits));
4403
4404 rational all_r(0);
4405 scoped_mpz all_z(mpzm);
4406
4407 VERIFY(m_bv_util.is_numeral(a, all_r, bv_sz));
4408 SASSERT(bv_sz == (ebits + sbits));
4409 SASSERT(all_r.is_int());
4410 mpzm.set(all_z, all_r.to_mpq().numerator());
4411
4412 mpzm.machine_div2k(all_z, ebits + sbits - 1, sgn_z);
4413 mpzm.mod(all_z, mpfm.m_powers2(ebits + sbits - 1), all_z);
4414
4415 mpzm.machine_div2k(all_z, sbits - 1, exp_z);
4416 mpzm.mod(all_z, mpfm.m_powers2(sbits - 1), all_z);
4417
4418 mpzm.set(sig_z, all_z);
4419 }
4420 else {
4421 SASSERT(b);
4422 SASSERT(c);
4423 rational sgn_r(0), exp_r(0), sig_r(0);
4424
4425 bool r = m_bv_util.is_numeral(a, sgn_r, bv_sz);
4426 SASSERT(r && bv_sz == 1);
4427 r = m_bv_util.is_numeral(b, exp_r, bv_sz);
4428 SASSERT(r && bv_sz == ebits);
4429 r = m_bv_util.is_numeral(c, sig_r, bv_sz);
4430 SASSERT(r && bv_sz == sbits - 1);
4431 (void)r;
4432
4433 SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator()));
4434 SASSERT(mpzm.is_one(exp_r.to_mpq().denominator()));
4435 SASSERT(mpzm.is_one(sig_r.to_mpq().denominator()));
4436
4437 mpzm.set(sgn_z, sgn_r.to_mpq().numerator());
4438 mpzm.set(exp_z, exp_r.to_mpq().numerator());
4439 mpzm.set(sig_z, sig_r.to_mpq().numerator());
4440 }
4441
4442 scoped_mpz exp_u = exp_z - bias;
4443 SASSERT(mpzm.is_int64(exp_u));
4444
4445 scoped_mpf f(mpfm);
4446 mpfm.set(f, ebits, sbits, mpzm.is_one(sgn_z), mpzm.get_int64(exp_u), sig_z);
4447 result = m_util.mk_value(f);
4448
4449 TRACE("t_fpa", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << " result: [" <<
4450 mpzm.to_string(sgn_z) << "," <<
4451 mpzm.to_string(exp_z) << "," <<
4452 mpzm.to_string(sig_z) << "] --> " <<
4453 mk_ismt2_pp(result, m) << std::endl;);
4454
4455 return result;
4456 }
4457