1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 fpa2bv_rewriter.cpp
7
8 Abstract:
9
10 Rewriter for converting FPA to BV
11
12 Author:
13
14 Christoph (cwinter) 2012-02-09
15
16 Notes:
17
18 --*/
19
20
21 #include "ast/rewriter/rewriter_def.h"
22 #include "ast/fpa/fpa2bv_rewriter.h"
23 #include "params/fpa2bv_rewriter_params.hpp"
24
25
fpa2bv_rewriter_cfg(ast_manager & m,fpa2bv_converter & c,params_ref const & p)26 fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p) :
27 m_manager(m),
28 m_out(m),
29 m_conv(c),
30 m_bindings(m)
31 {
32 updt_params(p);
33 // We need to make sure that the manager has the BV plugin loaded.
34 symbol s_bv("bv");
35 if (!m_manager.has_plugin(s_bv))
36 m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
37 }
38
updt_local_params(params_ref const & _p)39 void fpa2bv_rewriter_cfg::updt_local_params(params_ref const & _p) {
40 fpa2bv_rewriter_params p(_p);
41 bool v = p.hi_fp_unspecified();
42 m_conv.set_unspecified_fp_hi(v);
43 }
44
updt_params(params_ref const & p)45 void fpa2bv_rewriter_cfg::updt_params(params_ref const & p) {
46 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
47 m_max_steps = p.get_uint("max_steps", UINT_MAX);
48 updt_local_params(p);
49 }
50
max_steps_exceeded(unsigned num_steps) const51 bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const {
52 return num_steps > m_max_steps;
53 }
54
55
reduce_app(func_decl * f,unsigned num,expr * const * args,expr_ref & result,proof_ref & result_pr)56 br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
57 TRACE("fpa2bv_rw", tout << "func: " << f->get_name() << std::endl;
58 tout << "args: " << std::endl;
59 for (unsigned i = 0; i < num; i++)
60 tout << mk_ismt2_pp(args[i], m()) << std::endl;);
61
62 if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
63 m_conv.mk_const(f, result);
64 return BR_DONE;
65 }
66
67 if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
68 m_conv.mk_rm_const(f, result);
69 return BR_DONE;
70 }
71
72 if (m().is_eq(f)) {
73 SASSERT(num == 2);
74 TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " <<
75 mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
76 SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
77 sort * ds = f->get_domain()[0];
78 if (m_conv.is_float(ds)) {
79 m_conv.mk_eq(args[0], args[1], result);
80 return BR_DONE;
81 }
82 else if (m_conv.is_rm(ds)) {
83 result = m().mk_eq(args[0], args[1]);
84 return BR_DONE;
85 }
86 return BR_FAILED;
87 }
88 else if (m().is_ite(f)) {
89 SASSERT(num == 3);
90 if (m_conv.is_float(args[1]) || m_conv.is_rm(args[1])) {
91 m_conv.mk_ite(args[0], args[1], args[2], result);
92 return BR_DONE;
93 }
94 return BR_FAILED;
95 }
96 else if (m().is_distinct(f)) {
97 sort * ds = f->get_domain()[0];
98 if (m_conv.is_float(ds) || m_conv.is_rm(ds)) {
99 m_conv.mk_distinct(f, num, args, result);
100 return BR_DONE;
101 }
102 return BR_FAILED;
103 }
104
105 if (m_conv.is_float_family(f)) {
106 switch (f->get_decl_kind()) {
107 case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
108 case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
109 case OP_FPA_RM_TOWARD_NEGATIVE:
110 case OP_FPA_RM_TOWARD_POSITIVE:
111 case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f->get_decl_kind(), result); return BR_DONE;
112 case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE;
113 case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE;
114 case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE;
115 case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
116 case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
117 case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE;
118 case OP_FPA_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
119 case OP_FPA_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
120 case OP_FPA_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE;
121 case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
122 case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
123 case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
124 case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
125 case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
126 case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
127 case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
128 case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
129 case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
130 case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
131 case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
132 case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
133 case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
134 case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
135 case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
136 case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
137 case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
138 case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
139 case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
140 case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
141 case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
142 case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE;
143 case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
144 case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
145 case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
146 case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
147 case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
148 case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
149
150 case OP_FPA_BVWRAP:
151 case OP_FPA_BV2RM:
152 return BR_FAILED;
153
154 default:
155 TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
156 for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
157 NOT_IMPLEMENTED_YET();
158 }
159 }
160 else
161 {
162 SASSERT(!m_conv.is_float_family(f));
163 if (m_conv.fu().contains_floats(f)) {
164 m_conv.mk_uf(f, num, args, result);
165 return BR_DONE;
166 }
167 }
168
169 return BR_FAILED;
170 }
171
pre_visit(expr * t)172 bool fpa2bv_rewriter_cfg::pre_visit(expr * t)
173 {
174 TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;);
175
176 if (is_quantifier(t)) {
177 quantifier * q = to_quantifier(t);
178 TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
179 sort_ref_vector new_bindings(m_manager);
180 for (unsigned i = 0 ; i < q->get_num_decls(); i++)
181 new_bindings.push_back(q->get_decl_sort(i));
182 SASSERT(new_bindings.size() == q->get_num_decls());
183 m_bindings.append(new_bindings);
184 }
185 return true;
186 }
187
188
reduce_quantifier(quantifier * old_q,expr * new_body,expr * const * new_patterns,expr * const * new_no_patterns,expr_ref & result,proof_ref & result_pr)189 bool fpa2bv_rewriter_cfg::reduce_quantifier(
190 quantifier * old_q,
191 expr * new_body,
192 expr * const * new_patterns,
193 expr * const * new_no_patterns,
194 expr_ref & result,
195 proof_ref & result_pr) {
196 if (is_lambda(old_q)) {
197 return false;
198 }
199 unsigned curr_sz = m_bindings.size();
200 SASSERT(old_q->get_num_decls() <= curr_sz);
201 unsigned num_decls = old_q->get_num_decls();
202 unsigned old_sz = curr_sz - num_decls;
203 string_buffer<> name_buffer;
204 ptr_buffer<sort> new_decl_sorts;
205 sbuffer<symbol> new_decl_names;
206 for (unsigned i = 0; i < num_decls; i++) {
207 symbol const & n = old_q->get_decl_name(i);
208 sort * s = old_q->get_decl_sort(i);
209 if (m_conv.is_float(s)) {
210 unsigned ebits = m_conv.fu().get_ebits(s);
211 unsigned sbits = m_conv.fu().get_sbits(s);
212 name_buffer.reset();
213 name_buffer << n << ".bv";
214 new_decl_names.push_back(symbol(name_buffer.c_str()));
215 new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits));
216 }
217 else if (m_conv.is_rm(s)) {
218 name_buffer.reset();
219 name_buffer << n << ".bv";
220 new_decl_names.push_back(symbol(name_buffer.c_str()));
221 new_decl_sorts.push_back(m_conv.bu().mk_sort(3));
222 }
223 else {
224 new_decl_sorts.push_back(s);
225 new_decl_names.push_back(n);
226 }
227 }
228 result = m().mk_quantifier(old_q->get_kind(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
229 new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
230 old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
231 result_pr = nullptr;
232 if (m().proofs_enabled()) {
233 result_pr = m().mk_rewrite(old_q, result);
234 }
235 m_bindings.shrink(old_sz);
236 TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
237 mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
238 " new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
239 tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
240 return true;
241 }
242
reduce_var(var * t,expr_ref & result,proof_ref & result_pr)243 bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
244 if (t->get_idx() >= m_bindings.size())
245 return false;
246 // unsigned inx = m_bindings.size() - t->get_idx() - 1;
247
248 expr_ref new_exp(m());
249 sort * s = t->get_sort();
250 if (m_conv.is_float(s)) {
251 expr_ref new_var(m());
252 unsigned ebits = m_conv.fu().get_ebits(s);
253 unsigned sbits = m_conv.fu().get_sbits(s);
254 new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
255 new_exp = m_conv.fu().mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
256 m_conv.bu().mk_extract(ebits - 1, 0, new_var),
257 m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var));
258 }
259 else if (m_conv.is_rm(s)) {
260 expr_ref new_var(m());
261 new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(3));
262 new_exp = m_conv.fu().mk_bv2rm(new_var);
263 }
264 else
265 new_exp = m().mk_var(t->get_idx(), s);
266
267 result = new_exp;
268 result_pr = nullptr;
269 TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
270 return true;
271 }
272
273 template class rewriter_tpl<fpa2bv_rewriter_cfg>;
274
convert_atom(th_rewriter & rw,expr * e)275 expr_ref fpa2bv_rewriter::convert_atom(th_rewriter& rw, expr * e) {
276 TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, m_cfg.m()) << std::endl;);
277 expr_ref res(m_cfg.m());
278 proof_ref pr(m_cfg.m());
279 (*this)(e, res);
280 rw(res, res);
281 SASSERT(is_app(res));
282 SASSERT(m_cfg.m().is_bool(res));
283 return res;
284 }
285
convert_term(th_rewriter & rw,expr * e)286 expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) {
287 SASSERT(fu().is_rm(e) || fu().is_float(e));
288 ast_manager& m = m_cfg.m();
289
290 expr_ref e_conv(m), res(m);
291 proof_ref pr(m);
292
293 (*this)(e, e_conv);
294
295 TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, m) << std::endl;
296 tout << "converted term: " << mk_ismt2_pp(e_conv, m) << std::endl;);
297
298 if (fu().is_rm(e)) {
299 SASSERT(fu().is_bv2rm(e_conv));
300 expr_ref bv_rm(m);
301 rw(to_app(e_conv)->get_arg(0), bv_rm);
302 res = fu().mk_bv2rm(bv_rm);
303 }
304 else if (fu().is_float(e)) {
305 SASSERT(fu().is_fp(e_conv));
306 expr_ref sgn(m), sig(m), exp(m);
307 m_cfg.m_conv.split_fp(e_conv, sgn, exp, sig);
308 rw(sgn);
309 rw(exp);
310 rw(sig);
311 res = fu().mk_fp(sgn, exp, sig);
312 }
313 else
314 UNREACHABLE();
315
316 return res;
317 }
318
convert_conversion_term(th_rewriter & rw,expr * e)319 expr_ref fpa2bv_rewriter::convert_conversion_term(th_rewriter& rw, expr * e) {
320 SASSERT(to_app(e)->get_family_id() == fu().get_family_id());
321 /* This is for the conversion functions fp.to_* */
322 expr_ref res(m_cfg.m());
323 (*this)(e, res);
324 rw(res, res);
325 return res;
326 }
327
convert(th_rewriter & rw,expr * e)328 expr_ref fpa2bv_rewriter::convert(th_rewriter& rw, expr * e) {
329 ast_manager& m = m_cfg.m();
330 expr_ref res(m);
331 TRACE("t_fpa", tout << "converting " << mk_ismt2_pp(e, m) << std::endl;);
332
333 if (fu().is_fp(e))
334 res = e;
335 else if (m.is_bool(e))
336 res = convert_atom(rw, e);
337 else if (fu().is_float(e) || fu().is_rm(e))
338 res = convert_term(rw, e);
339 else
340 res = convert_conversion_term(rw, e);
341
342 TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
343 tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
344 mk_ismt2_pp(res, m) << std::endl;);
345
346 return res;
347 }
348