1 /*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 Module Name:
5
6 elim_small_bv.h
7
8 Abstract:
9
10 Tactic that eliminates small, quantified bit-vectors.
11
12 Author:
13
14 Christoph (cwinter) 2015-11-09
15
16 Revision History:
17
18 --*/
19 #include "tactic/tactical.h"
20 #include "ast/rewriter/rewriter_def.h"
21 #include "tactic/generic_model_converter.h"
22 #include "ast/bv_decl_plugin.h"
23 #include "ast/used_vars.h"
24 #include "ast/well_sorted.h"
25 #include "ast/rewriter/var_subst.h"
26 #include "ast/rewriter/th_rewriter.h"
27
28 #include "tactic/bv/elim_small_bv_tactic.h"
29
30 namespace {
31 class elim_small_bv_tactic : public tactic {
32
33 struct rw_cfg : public default_rewriter_cfg {
34 ast_manager & m;
35 params_ref m_params;
36 bv_util m_util;
37 th_rewriter m_simp;
38 ref<generic_model_converter> m_mc;
39 unsigned m_max_bits;
40 unsigned long long m_max_steps;
41 unsigned long long m_max_memory; // in bytes
42 bool m_produce_models;
43 sort_ref_vector m_bindings;
44 unsigned long m_num_eliminated;
45
rw_cfg__anonc279b6710111::elim_small_bv_tactic::rw_cfg46 rw_cfg(ast_manager & _m, params_ref const & p) :
47 m(_m),
48 m_params(p),
49 m_util(_m),
50 m_simp(_m),
51 m_bindings(_m),
52 m_num_eliminated(0) {
53 updt_params(p);
54 m_max_steps = UINT_MAX;
55 }
56
max_steps_exceeded__anonc279b6710111::elim_small_bv_tactic::rw_cfg57 bool max_steps_exceeded(unsigned long long num_steps) const {
58 if (num_steps > m_max_steps)
59 return true;
60 if (memory::get_allocation_size() > m_max_memory)
61 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
62 return false;
63 }
64
is_small_bv__anonc279b6710111::elim_small_bv_tactic::rw_cfg65 bool is_small_bv(sort * s) {
66 return m_util.is_bv_sort(s) && m_util.get_bv_size(s) <= m_max_bits;
67 }
68
replace_var__anonc279b6710111::elim_small_bv_tactic::rw_cfg69 expr_ref replace_var(used_vars & uv,
70 unsigned num_decls, unsigned max_var_idx_p1,
71 unsigned idx, sort * s, expr * e, expr * replacement) {
72 TRACE("elim_small_bv", tout << "replace idx " << idx << " with " << mk_ismt2_pp(replacement, m) <<
73 " in " << mk_ismt2_pp(e, m) << std::endl;);
74 expr_ref res(m);
75 ptr_vector<expr> substitution;
76
77 substitution.resize(num_decls, nullptr);
78 substitution[num_decls - idx - 1] = replacement;
79
80 // (VAR 0) is in the first position of substitution; (VAR num_decls-1) is in the last position.
81
82 for (unsigned i = 0; i < max_var_idx_p1; i++)
83 substitution.push_back(nullptr);
84
85 // (VAR num_decls) ... (VAR num_decls+sz-1); are in positions num_decls .. num_decls+sz-1
86
87 std::reverse(substitution.data(), substitution.data() + substitution.size());
88
89 // (VAR 0) should be in the last position of substitution.
90
91 TRACE("elim_small_bv", tout << "substitution: " << std::endl;
92 for (unsigned k = 0; k < substitution.size(); k++) {
93 expr * se = substitution[k];
94 tout << k << " = ";
95 if (se == 0) tout << "0";
96 else tout << mk_ismt2_pp(se, m);
97 tout << std::endl;
98 });
99
100 var_subst vsbst(m);
101 res = vsbst(e, substitution.size(), substitution.data());
102 SASSERT(is_well_sorted(m, res));
103
104 proof_ref pr(m);
105 m_simp(res, res, pr);
106 TRACE("elim_small_bv", tout << "replace done: " << mk_ismt2_pp(res, m) << std::endl;);
107
108 return res;
109 }
110
reduce_app__anonc279b6710111::elim_small_bv_tactic::rw_cfg111 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
112 TRACE("elim_small_bv_app", expr_ref tmp(m.mk_app(f, num, args), m); tout << "reduce " << tmp << std::endl; );
113 return BR_FAILED;
114 }
115
reduce_quantifier__anonc279b6710111::elim_small_bv_tactic::rw_cfg116 bool reduce_quantifier(
117 quantifier * q,
118 expr * old_body,
119 expr * const * new_patterns,
120 expr * const * new_no_patterns,
121 expr_ref & result,
122 proof_ref & result_pr) {
123 if (is_lambda(q)) {
124 return false;
125 }
126 TRACE("elim_small_bv", tout << "reduce_quantifier " << mk_ismt2_pp(q, m) << std::endl; );
127 unsigned long long num_steps = 0;
128 unsigned curr_sz = m_bindings.size();
129 SASSERT(q->get_num_decls() <= curr_sz);
130 unsigned num_decls = q->get_num_decls();
131 unsigned old_sz = curr_sz - num_decls;
132
133 used_vars uv;
134 uv(q);
135 SASSERT(is_well_sorted(m, q));
136 unsigned max_var_idx_p1 = uv.get_max_found_var_idx_plus_1();
137
138 expr_ref body(old_body, m);
139 for (unsigned i = num_decls; i-- > 0 && !max_steps_exceeded(num_steps); ) {
140 sort * s = q->get_decl_sort(i);
141 expr_ref_vector new_bodies(m);
142 if (is_small_bv(s) && !max_steps_exceeded(num_steps)) {
143 unsigned bv_sz = m_util.get_bv_size(s);
144 TRACE("elim_small_bv", tout << "eliminating " << q->get_decl_name(i) <<
145 "; sort = " << mk_ismt2_pp(s, m) <<
146 "; body = " << mk_ismt2_pp(body, m) << std::endl;);
147
148 if (bv_sz >= 31ul || ((unsigned)(1ul << bv_sz)) + num_steps > m_max_steps) {
149 return false;
150 }
151
152 for (unsigned j = 0; j < (1ul << bv_sz) && !max_steps_exceeded(num_steps); j++) {
153 expr_ref n(m_util.mk_numeral(j, bv_sz), m);
154 new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n));
155 num_steps++;
156 }
157 }
158 else if (m.is_bool(s)) {
159 new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, m.mk_true()));
160 new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, m.mk_false()));
161 }
162 else {
163 continue;
164 }
165
166 if (max_steps_exceeded(num_steps)) {
167 return false;
168 }
169
170 TRACE("elim_small_bv", tout << "new bodies: " << std::endl;
171 for (unsigned k = 0; k < new_bodies.size(); k++)
172 tout << mk_ismt2_pp(new_bodies[k].get(), m) << std::endl; );
173
174 body = is_forall(q) ? m.mk_and(new_bodies.size(), new_bodies.data()) :
175 m.mk_or(new_bodies.size(), new_bodies.data());
176 SASSERT(is_well_sorted(m, body));
177
178 proof_ref pr(m);
179 m_simp(body, body, pr);
180 m_num_eliminated++;
181 }
182
183 quantifier_ref new_q(m);
184 new_q = m.update_quantifier(q, body);
185 unused_vars_eliminator el(m, m_params);
186 result = el(new_q);
187
188 TRACE("elim_small_bv", tout << "elimination result: " << mk_ismt2_pp(result, m) << std::endl; );
189
190 result_pr = nullptr; // proofs NIY
191 m_bindings.shrink(old_sz);
192 return true;
193 }
194
pre_visit__anonc279b6710111::elim_small_bv_tactic::rw_cfg195 bool pre_visit(expr * t) {
196 TRACE("elim_small_bv_pre", tout << "pre_visit: " << mk_ismt2_pp(t, m) << std::endl;);
197 if (is_quantifier(t)) {
198 quantifier * q = to_quantifier(t);
199 TRACE("elim_small_bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m) << std::endl;);
200 sort_ref_vector new_bindings(m);
201 for (unsigned i = 0; i < q->get_num_decls(); i++)
202 new_bindings.push_back(q->get_decl_sort(i));
203 SASSERT(new_bindings.size() == q->get_num_decls());
204 m_bindings.append(new_bindings);
205 }
206 return true;
207 }
208
updt_params__anonc279b6710111::elim_small_bv_tactic::rw_cfg209 void updt_params(params_ref const & p) {
210 m_params = p;
211 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
212 m_max_steps = p.get_uint("max_steps", UINT_MAX);
213 m_max_bits = p.get_uint("max_bits", 4);
214 }
215 };
216
217 struct rw : public rewriter_tpl<rw_cfg> {
218 rw_cfg m_cfg;
219
rw__anonc279b6710111::elim_small_bv_tactic::rw220 rw(ast_manager & m, params_ref const & p) :
221 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
222 m_cfg(m, p) {
223 }
224 };
225
226 ast_manager & m;
227 rw m_rw;
228 params_ref m_params;
229
230 public:
elim_small_bv_tactic(ast_manager & m,params_ref const & p)231 elim_small_bv_tactic(ast_manager & m, params_ref const & p) :
232 m(m),
233 m_rw(m, p),
234 m_params(p) {
235 }
236
translate(ast_manager & m)237 tactic * translate(ast_manager & m) override {
238 return alloc(elim_small_bv_tactic, m, m_params);
239 }
240
updt_params(params_ref const & p)241 void updt_params(params_ref const & p) override {
242 m_params = p;
243 m_rw.cfg().updt_params(p);
244 }
245
collect_param_descrs(param_descrs & r)246 void collect_param_descrs(param_descrs & r) override {
247 insert_max_memory(r);
248 insert_max_steps(r);
249 r.insert("max_bits", CPK_UINT, "(default: 4) maximum bit-vector size of quantified bit-vectors to be eliminated.");
250 }
251
operator ()(goal_ref const & g,goal_ref_buffer & result)252 void operator()(goal_ref const & g,
253 goal_ref_buffer & result) override {
254 tactic_report report("elim-small-bv", *g);
255 bool produce_proofs = g->proofs_enabled();
256 fail_if_proof_generation("elim-small-bv", g);
257 fail_if_unsat_core_generation("elim-small-bv", g);
258 m_rw.cfg().m_produce_models = g->models_enabled();
259
260 expr_ref new_curr(m);
261 proof_ref new_pr(m);
262 unsigned size = g->size();
263 for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) {
264 expr * curr = g->form(idx);
265 m_rw(curr, new_curr, new_pr);
266 if (produce_proofs) {
267 proof * pr = g->pr(idx);
268 new_pr = m.mk_modus_ponens(pr, new_pr);
269 }
270 g->update(idx, new_curr, new_pr, g->dep(idx));
271 }
272 g->add(m_rw.m_cfg.m_mc.get());
273
274 report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated);
275 g->inc_depth();
276 result.push_back(g.get());
277 }
278
cleanup()279 void cleanup() override {
280 m_rw.~rw();
281 new (&m_rw) rw(m, m_params);
282 }
283
284 };
285 }
286
mk_elim_small_bv_tactic(ast_manager & m,params_ref const & p)287 tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p) {
288 return clean(alloc(elim_small_bv_tactic, m, p));
289 }
290
291