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