1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 bv_size_reduction_tactic.cpp
7
8 Abstract:
9
10 Reduce the number of bits used to encode constants, by using signed bounds.
11 Example: suppose x is a bit-vector of size 8, and we have
12 signed bounds for x such that:
13 -2 <= x <= 2
14 Then, x can be replaced by ((sign-extend 5) k)
15 where k is a fresh bit-vector constant of size 3.
16
17 Author:
18
19 Leonardo (leonardo) 2012-02-19
20
21 Notes:
22
23 --*/
24 #include "tactic/tactical.h"
25 #include "ast/bv_decl_plugin.h"
26 #include "ast/rewriter/expr_replacer.h"
27 #include "tactic/generic_model_converter.h"
28 #include "ast/ast_smt2_pp.h"
29
30 namespace {
31 class bv_size_reduction_tactic : public tactic {
32 typedef rational numeral;
33 typedef generic_model_converter bv_size_reduction_mc;
34
35 ast_manager & m;
36 bv_util m_util;
37 obj_map<app, numeral> m_signed_lowers;
38 obj_map<app, numeral> m_signed_uppers;
39 obj_map<app, numeral> m_unsigned_lowers;
40 obj_map<app, numeral> m_unsigned_uppers;
41 ref<bv_size_reduction_mc> m_mc;
42 generic_model_converter_ref m_fmc;
43 scoped_ptr<expr_replacer> m_replacer;
44 bool m_produce_models;
45
46 public:
bv_size_reduction_tactic(ast_manager & m)47 bv_size_reduction_tactic(ast_manager & m) :
48 m(m),
49 m_util(m),
50 m_replacer(mk_default_expr_replacer(m, false)) {
51 }
52
translate(ast_manager & m)53 tactic * translate(ast_manager & m) override {
54 return alloc(bv_size_reduction_tactic, m);
55 }
56
57 void operator()(goal_ref const & g, goal_ref_buffer & result) override;
58
cleanup()59 void cleanup() override {
60 m_signed_lowers.reset();
61 m_signed_uppers.reset();
62 m_unsigned_lowers.reset();
63 m_unsigned_uppers.reset();
64 m_mc = nullptr;
65 m_fmc = nullptr;
66 m_replacer->reset();
67 }
68
update_signed_lower(app * v,numeral const & k)69 void update_signed_lower(app * v, numeral const & k) {
70 // k <= v
71 auto& value = m_signed_lowers.insert_if_not_there(v, k);
72 if (value < k) {
73 // improve bound
74 value = k;
75 }
76 }
77
update_signed_upper(app * v,numeral const & k)78 void update_signed_upper(app * v, numeral const & k) {
79 // v <= k
80 auto& value = m_signed_uppers.insert_if_not_there(v, k);
81 if (k < value) {
82 // improve bound
83 value = k;
84 }
85 }
86
update_unsigned_lower(app * v,numeral const & k)87 void update_unsigned_lower(app * v, numeral const & k) {
88 SASSERT(k > numeral(0));
89 // k <= v
90 auto& value = m_unsigned_lowers.insert_if_not_there(v, k);
91 if (value < k) {
92 // improve bound
93 value = k;
94 }
95 }
96
update_unsigned_upper(app * v,numeral const & k)97 void update_unsigned_upper(app * v, numeral const & k) {
98 SASSERT(k > numeral(0));
99 // v <= k
100 auto& value = m_unsigned_uppers.insert_if_not_there(v, k);
101 if (k < value) {
102 // improve bound
103 value = k;
104 }
105 }
106
collect_bounds(goal const & g)107 void collect_bounds(goal const & g) {
108 unsigned sz = g.size();
109 numeral val;
110 unsigned bv_sz;
111 expr * f, * lhs, * rhs;
112 for (unsigned i = 0; i < sz; i++) {
113 bool negated = false;
114 f = g.form(i);
115 if (m.is_not(f)) {
116 negated = true;
117 f = to_app(f)->get_arg(0);
118 }
119
120 if (m_util.is_bv_sle(f, lhs, rhs)) {
121 bv_sz = m_util.get_bv_size(lhs);
122 if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
123 TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
124 // v <= k
125 val = m_util.norm(val, bv_sz, true);
126 if (negated) {
127 val += numeral(1);
128 if (m_util.norm(val, bv_sz, true) != val) {
129 // bound is infeasible.
130 }
131 else {
132 update_signed_lower(to_app(lhs), val);
133 }
134 }
135 else update_signed_upper(to_app(lhs), val);
136 }
137 else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
138 TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
139 // k <= v
140 val = m_util.norm(val, bv_sz, true);
141 if (negated) {
142 val -= numeral(1);
143 if (m_util.norm(val, bv_sz, true) != val) {
144 // bound is infeasible.
145 }
146 else {
147 update_signed_upper(to_app(rhs), val);
148 }
149 }
150 else update_signed_lower(to_app(rhs), val);
151 }
152 }
153
154 #if 0
155 else if (m_util.is_bv_ule(f, lhs, rhs)) {
156 if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
157 TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
158 // v <= k
159 if (negated) update_unsigned_lower(to_app(lhs), val+numeral(1));
160 else update_unsigned_upper(to_app(lhs), val);
161 }
162 else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
163 TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
164 // k <= v
165 if (negated) update_unsigned_upper(to_app(rhs), val-numeral(1));
166 else update_unsigned_lower(to_app(rhs), val);
167 }
168 }
169 #endif
170 }
171 }
172
checkpoint()173 void checkpoint() {
174 if (!m.inc())
175 throw tactic_exception(m.limit().get_cancel_msg());
176 }
177
run(goal & g,model_converter_ref & mc)178 void run(goal & g, model_converter_ref & mc) {
179 if (g.inconsistent())
180 return;
181 TRACE("before_bv_size_reduction", g.display(tout););
182 m_produce_models = g.models_enabled();
183 mc = nullptr;
184 m_mc = nullptr;
185 unsigned num_reduced = 0;
186 {
187 tactic_report report("reduce-bv-size", g);
188 collect_bounds(g);
189
190 // create substitution
191 expr_substitution subst(m);
192
193 if (!(m_signed_lowers.empty() || m_signed_uppers.empty())) {
194 TRACE("bv_size_reduction",
195 tout << "m_signed_lowers: " << std::endl;
196 for (obj_map<app, numeral>::iterator it = m_signed_lowers.begin(); it != m_signed_lowers.end(); it++)
197 tout << mk_ismt2_pp(it->m_key, m) << " >= " << it->m_value.to_string() << std::endl;
198 tout << "m_signed_uppers: " << std::endl;
199 for (obj_map<app, numeral>::iterator it = m_signed_uppers.begin(); it != m_signed_uppers.end(); it++)
200 tout << mk_ismt2_pp(it->m_key, m) << " <= " << it->m_value.to_string() << std::endl;
201 );
202
203 obj_map<app, numeral>::iterator it = m_signed_lowers.begin();
204 obj_map<app, numeral>::iterator end = m_signed_lowers.end();
205 for (; it != end; ++it) {
206 app * v = it->m_key;
207 unsigned bv_sz = m_util.get_bv_size(v);
208 numeral l = m_util.norm(it->m_value, bv_sz, true);
209 obj_map<app, numeral>::obj_map_entry * entry = m_signed_uppers.find_core(v);
210 if (entry != nullptr) {
211 numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true);
212 TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
213 expr * new_def = nullptr;
214 app * new_const = nullptr;
215 if (l > u) {
216 g.assert_expr(m.mk_false());
217 return;
218 }
219 else if (l == u) {
220 new_def = m_util.mk_numeral(l, m.get_sort(v));
221 }
222 else {
223 // l < u
224 if (l.is_neg()) {
225 unsigned l_nb = (-l).get_num_bits();
226 unsigned v_nb = m_util.get_bv_size(v);
227
228 if (u.is_neg())
229 {
230 // l <= v <= u <= 0
231 unsigned i_nb = l_nb;
232 TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= u <= 0 " << " --> " << i_nb << " bits\n";);
233 if (i_nb < v_nb) {
234 new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(i_nb));
235 new_def = m_util.mk_concat(m_util.mk_numeral(numeral(-1), v_nb - i_nb), new_const);
236 }
237 }
238 else {
239 // l <= v <= 0 <= u
240 unsigned u_nb = u.get_num_bits();
241 unsigned i_nb = ((l_nb > u_nb) ? l_nb : u_nb) + 1;
242 TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= 0 <= u " << " --> " << i_nb << " bits\n";);
243 if (i_nb < v_nb) {
244 new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(i_nb));
245 new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
246 }
247 }
248 }
249 else {
250 // 0 <= l <= v <= u
251 unsigned u_nb = u.get_num_bits();
252 unsigned v_nb = m_util.get_bv_size(v);
253 TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << " --> " << u_nb << " bits\n";);
254 if (u_nb < v_nb) {
255 new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(u_nb));
256 new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
257 }
258 }
259 }
260
261 if (new_def) {
262 subst.insert(v, new_def);
263 if (m_produce_models) {
264 if (!m_mc)
265 m_mc = alloc(bv_size_reduction_mc, m, "bv_size_reduction");
266 m_mc->add(v, new_def);
267 if (!m_fmc && new_const)
268 m_fmc = alloc(generic_model_converter, m, "bv_size_reduction");
269 if (new_const)
270 m_fmc->hide(new_const);
271 }
272 num_reduced++;
273 }
274 }
275 }
276 }
277
278 #if 0
279 if (!(m_unsigned_lowers.empty() && m_unsigned_uppers.empty())) {
280 TRACE("bv_size_reduction",
281 tout << "m_unsigned_lowers: " << std::endl;
282 for (obj_map<app, numeral>::iterator it = m_unsigned_lowers.begin(); it != m_unsigned_lowers.end(); it++)
283 tout << mk_ismt2_pp(it->m_key, m) << " >= " << it->m_value.to_string() << std::endl;
284 tout << "m_unsigned_uppers: " << std::endl;
285 for (obj_map<app, numeral>::iterator it = m_unsigned_uppers.begin(); it != m_unsigned_uppers.end(); it++)
286 tout << mk_ismt2_pp(it->m_key, m) << " <= " << it->m_value.to_string() << std::endl;
287 );
288
289 obj_map<app, numeral>::iterator it = m_unsigned_uppers.begin();
290 obj_map<app, numeral>::iterator end = m_unsigned_uppers.end();
291 for (; it != end; ++it) {
292 app * v = it->m_key;
293 unsigned bv_sz = m_util.get_bv_size(v);
294 numeral u = m_util.norm(it->m_value, bv_sz, false);
295 obj_map<app, numeral>::obj_map_entry * entry = m_signed_lowers.find_core(v);
296 numeral l = (entry != 0) ? m_util.norm(entry->get_data().m_value, bv_sz, false) : numeral(0);
297
298 obj_map<app, numeral>::obj_map_entry * lse = m_signed_lowers.find_core(v);
299 obj_map<app, numeral>::obj_map_entry * use = m_signed_uppers.find_core(v);
300 if ((lse != 0 && lse->get_data().m_value > l) &&
301 (use != 0 && use->get_data().m_value < u))
302 continue; // Skip, we had better signed bounds.
303
304 if (lse != 0 && lse->get_data().m_value > l) l = lse->get_data().m_value;
305 if (use != 0 && use->get_data().m_value < u) u = use->get_data().m_value;
306
307 TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
308 expr * new_def = 0;
309 app * new_const = 0;
310 if (l > u) {
311 g.assert_expr(m.mk_false());
312 return;
313 }
314 else if (l == u) {
315 new_def = m_util.mk_numeral(l, m.get_sort(v));
316 }
317 else {
318 // 0 <= l <= v <= u
319 unsigned u_nb = u.get_num_bits();
320 unsigned v_nb = m_util.get_bv_size(v);
321 if (u_nb < v_nb) {
322 new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
323 new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
324 }
325 }
326
327 if (new_def) {
328 subst.insert(v, new_def);
329 if (m_produce_models) {
330 if (!m_mc)
331 m_mc = alloc(bv_size_reduction_mc, m);
332 m_mc->insert(v->get_decl(), new_def);
333 if (!m_fmc && new_const)
334 m_fmc = alloc(generic_model_converter, m, "bv_size_reduction");
335 if (new_const)
336 m_fmc->hide(new_const);
337 }
338 num_reduced++;
339 TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";);
340 }
341 }
342 }
343 #endif
344
345 if (subst.empty())
346 return;
347
348 m_replacer->set_substitution(&subst);
349
350 unsigned sz = g.size();
351 expr * f;
352 expr_ref new_f(m);
353 for (unsigned i = 0; i < sz; i++) {
354 if (g.inconsistent())
355 return;
356 f = g.form(i);
357 (*m_replacer)(f, new_f);
358 g.update(i, new_f);
359 }
360 mc = m_mc.get();
361 if (m_fmc) {
362 mc = concat(m_fmc.get(), mc.get());
363 }
364 m_mc = nullptr;
365 m_fmc = nullptr;
366 }
367 report_tactic_progress(":bv-reduced", num_reduced);
368 TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout););
369 }
370
371 };
372
operator ()(goal_ref const & g,goal_ref_buffer & result)373 void bv_size_reduction_tactic::operator()(goal_ref const & g,
374 goal_ref_buffer & result) {
375 fail_if_proof_generation("bv-size-reduction", g);
376 fail_if_unsat_core_generation("bv-size-reduction", g);
377 TRACE("goal", g->display(tout););
378 result.reset();
379 model_converter_ref mc;
380 run(*(g.get()), mc);
381 g->inc_depth();
382 g->add(mc.get());
383 result.push_back(g.get());
384 }
385 }
386
mk_bv_size_reduction_tactic(ast_manager & m,params_ref const & p)387 tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p) {
388 return clean(alloc(bv_size_reduction_tactic, m));
389 }
390