1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     fpa2bv_tactic.cpp
7 
8 Abstract:
9 
10     Tactic that converts floating points to bit-vectors
11 
12 Author:
13 
14     Christoph (cwinter) 2012-02-09
15 
16 Notes:
17 
18 --*/
19 #include "tactic/tactical.h"
20 #include "ast/fpa/fpa2bv_rewriter.h"
21 #include "tactic/core/simplify_tactic.h"
22 #include "tactic/fpa/fpa2bv_tactic.h"
23 #include "tactic/fpa/fpa2bv_model_converter.h"
24 
25 class fpa2bv_tactic : public tactic {
26     struct imp {
27         ast_manager &     m;
28         fpa2bv_converter  m_conv;
29         fpa2bv_rewriter   m_rw;
30         unsigned          m_num_steps;
31 
impfpa2bv_tactic::imp32         imp(ast_manager & _m, params_ref const & p):
33             m(_m),
34             m_conv(m),
35             m_rw(m, m_conv, p) {
36             }
37 
updt_paramsfpa2bv_tactic::imp38         void updt_params(params_ref const & p) {
39             m_rw.cfg().updt_params(p);
40         }
41 
operator ()fpa2bv_tactic::imp42         void operator()(goal_ref const & g,
43                         goal_ref_buffer & result) {
44             bool proofs_enabled      = g->proofs_enabled();
45             result.reset();
46             tactic_report report("fpa2bv", *g);
47             m_rw.reset();
48 
49             TRACE("fpa2bv", g->display(tout << "BEFORE: " << std::endl););
50 
51             if (g->inconsistent()) {
52                 result.push_back(g.get());
53                 return;
54             }
55 
56             m_num_steps = 0;
57             expr_ref   new_curr(m);
58             proof_ref  new_pr(m);
59             unsigned size = g->size();
60             for (unsigned idx = 0; idx < size; idx++) {
61                 if (g->inconsistent())
62                     break;
63                 expr * curr = g->form(idx);
64                 m_rw(curr, new_curr, new_pr);
65                 m_num_steps += m_rw.get_num_steps();
66                 if (proofs_enabled) {
67                     proof * pr = g->pr(idx);
68                     new_pr     = m.mk_modus_ponens(pr, new_pr);
69                 }
70                 g->update(idx, new_curr, new_pr, g->dep(idx));
71 
72                 if (is_app(new_curr)) {
73                     const app * a = to_app(new_curr.get());
74                     if (a->get_family_id() == m_conv.fu().get_family_id() &&
75                         a->get_decl_kind() == OP_FPA_IS_NAN) {
76                         // Inject auxiliary lemmas that fix e to the one and only NaN value,
77                         // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
78                         // has a value to propagate.
79                         expr_ref sgn(m), sig(m), exp(m);
80                         m_conv.split_fp(new_curr, sgn, exp, sig);
81                         result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)));
82                         result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_bv_neg(m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(exp)))));
83                         result.back()->assert_expr(m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig))));
84                     }
85                 }
86             }
87 
88             if (g->models_enabled())
89                 g->add(mk_fpa2bv_model_converter(m, m_conv));
90 
91             g->inc_depth();
92             result.push_back(g.get());
93 
94             for (expr* e : m_conv.m_extra_assertions) {
95                 proof* pr = nullptr;
96                 if (proofs_enabled)
97                     pr = m.mk_asserted(e);
98                 result.back()->assert_expr(e, pr);
99             }
100 
101             TRACE("fpa2bv", g->display(tout << "AFTER:\n");
102             if (g->mc()) g->mc()->display(tout); tout << std::endl; );
103         }
104     };
105 
106     imp *      m_imp;
107     params_ref m_params;
108 
109 public:
fpa2bv_tactic(ast_manager & m,params_ref const & p)110     fpa2bv_tactic(ast_manager & m, params_ref const & p):
111         m_params(p) {
112         m_imp = alloc(imp, m, p);
113     }
114 
translate(ast_manager & m)115     tactic * translate(ast_manager & m) override {
116         return alloc(fpa2bv_tactic, m, m_params);
117     }
118 
~fpa2bv_tactic()119     ~fpa2bv_tactic() override {
120         dealloc(m_imp);
121     }
122 
updt_params(params_ref const & p)123     void updt_params(params_ref const & p) override {
124         m_params = p;
125         m_imp->updt_params(p);
126     }
127 
collect_param_descrs(param_descrs & r)128     void collect_param_descrs(param_descrs & r) override {
129     }
130 
operator ()(goal_ref const & in,goal_ref_buffer & result)131     void operator()(goal_ref const & in,
132                     goal_ref_buffer & result) override {
133         try {
134             (*m_imp)(in, result);
135         }
136         catch (rewriter_exception & ex) {
137             throw tactic_exception(ex.msg());
138         }
139     }
140 
cleanup()141     void cleanup() override {
142         imp * d = alloc(imp, m_imp->m, m_params);
143         std::swap(d, m_imp);
144         dealloc(d);
145     }
146 
147 };
148 
mk_fpa2bv_tactic(ast_manager & m,params_ref const & p)149 tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) {
150     return clean(alloc(fpa2bv_tactic, m, p));
151 }
152