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