1 /*++
2 Copyright (c) 2016 Microsoft Corporation
3
4 Module Name:
5
6 enum2bv_rewriter.cpp
7
8 Abstract:
9
10 Conversion from enumeration types to bit-vectors.
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2016-10-18
15
16 Notes:
17
18 --*/
19
20 #include "ast/rewriter/rewriter.h"
21 #include "ast/rewriter/rewriter_def.h"
22 #include "ast/rewriter/enum2bv_rewriter.h"
23 #include "ast/ast_util.h"
24 #include "ast/ast_pp.h"
25
26 struct enum2bv_rewriter::imp {
27 ast_manager& m;
28 params_ref m_params;
29 obj_map<func_decl, func_decl*> m_enum2bv;
30 obj_map<func_decl, func_decl*> m_bv2enum;
31 obj_map<func_decl, expr*> m_enum2def;
32 expr_ref_vector m_bounds;
33 datatype_util m_dt;
34 func_decl_ref_vector m_enum_consts;
35 func_decl_ref_vector m_enum_bvs;
36 expr_ref_vector m_enum_defs;
37 unsigned_vector m_enum_consts_lim;
38 unsigned m_num_translated;
39 i_sort_pred* m_sort_pred;
40
41 struct rw_cfg : public default_rewriter_cfg {
42 imp& m_imp;
43 ast_manager& m;
44 datatype_util m_dt;
45 bv_util m_bv;
46 bool m_enable_unate { false };
47 unsigned m_unate_bound { 30 };
48
rw_cfgenum2bv_rewriter::imp::rw_cfg49 rw_cfg(imp& i, ast_manager & m) :
50 m_imp(i),
51 m(m),
52 m_dt(m),
53 m_bv(m)
54 {}
55
is_unateenum2bv_rewriter::imp::rw_cfg56 bool is_unate(sort* s) {
57 if (!m_enable_unate)
58 return false;
59 unsigned nc = m_dt.get_datatype_num_constructors(s);
60 return 1 < nc && nc <= m_unate_bound;
61 }
62
value2bvenum2bv_rewriter::imp::rw_cfg63 expr* value2bv(unsigned idx, sort* s) {
64 unsigned bv_size = get_bv_size(s);
65 sort_ref bv_sort(m_bv.mk_sort(bv_size), m);
66 if (is_unate(s))
67 return m_bv.mk_numeral(rational((1 << idx) - 1), bv_sort.get());
68 else
69 return m_bv.mk_numeral(rational(idx), bv_sort.get());
70 }
71
constrain_domainenum2bv_rewriter::imp::rw_cfg72 void constrain_domain(expr_ref_vector& bounds, expr* x, sort* s, sort* bv_sort) {
73 unsigned domain_size = m_dt.get_datatype_num_constructors(s);
74 if (is_unate(s)) {
75 expr_ref one(m_bv.mk_numeral(rational::one(), 1), m);
76 for (unsigned i = 0; i + 2 < domain_size; ++i) {
77 bounds.push_back(m.mk_implies(m.mk_eq(one, m_bv.mk_extract(i + 1, i + 1, x)),
78 m.mk_eq(one, m_bv.mk_extract(i, i, x))));
79 }
80 }
81 else {
82 if (!is_power_of_two(domain_size) || domain_size == 1) {
83 bounds.push_back(m_bv.mk_ule(x, value2bv(domain_size - 1, s)));
84 }
85 }
86 }
87
reduce_appenum2bv_rewriter::imp::rw_cfg88 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
89 expr_ref a0(m), a1(m);
90 expr_ref_vector _args(m);
91 result_pr = nullptr;
92 if (m.is_eq(f) && reduce_arg(args[0], a0) && reduce_arg(args[1], a1)) {
93 result = m.mk_eq(a0, a1);
94 return BR_DONE;
95 }
96 else if (m.is_distinct(f) && reduce_args(num, args, _args)) {
97 result = m.mk_distinct(_args.size(), _args.data());
98 return BR_DONE;
99 }
100 else if (m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) {
101 unsigned idx = m_dt.get_recognizer_constructor_idx(f);
102 a1 = value2bv(idx, args[0]->get_sort());
103 result = m.mk_eq(a0, a1);
104 return BR_DONE;
105 }
106 else {
107 check_for_fd(num, args);
108 return BR_FAILED;
109 }
110 }
111
reduce_argsenum2bv_rewriter::imp::rw_cfg112 bool reduce_args(unsigned sz, expr*const* as, expr_ref_vector& result) {
113 expr_ref tmp(m);
114 for (unsigned i = 0; i < sz; ++i) {
115 if (!reduce_arg(as[i], tmp)) return false;
116 result.push_back(tmp);
117 }
118 return true;
119 }
120
throw_non_fdenum2bv_rewriter::imp::rw_cfg121 void throw_non_fd(expr* e) {
122 std::stringstream strm;
123 strm << "unable to handle nested data-type expression " << mk_pp(e, m);
124 throw rewriter_exception(strm.str());
125 }
126
check_for_fdenum2bv_rewriter::imp::rw_cfg127 void check_for_fd(unsigned n, expr* const* args) {
128 for (unsigned i = 0; i < n; ++i) {
129 if (m_imp.is_fd(args[i]->get_sort())) {
130 throw_non_fd(args[i]);
131 }
132 }
133 }
134
reduce_argenum2bv_rewriter::imp::rw_cfg135 bool reduce_arg(expr* a, expr_ref& result) {
136
137 sort* s = a->get_sort();
138 if (!m_imp.is_fd(s)) {
139 return false;
140 }
141 unsigned bv_size = get_bv_size(s);
142 sort_ref bv_sort(m_bv.mk_sort(bv_size), m);
143
144 if (is_var(a)) {
145 result = m.mk_var(to_var(a)->get_idx(), m_bv.mk_sort(bv_size));
146 return true;
147 }
148 SASSERT(is_app(a));
149 func_decl* f = to_app(a)->get_decl();
150 if (m_dt.is_constructor(f)) {
151 unsigned idx = m_dt.get_constructor_idx(f);
152 result = value2bv(idx, s);
153 }
154 else if (is_uninterp_const(a)) {
155 func_decl* f_fresh;
156 if (m_imp.m_enum2bv.find(f, f_fresh)) {
157 result = m.mk_const(f_fresh);
158 return true;
159 }
160
161 // create a fresh variable, add bounds constraints for it.
162 unsigned nc = m_dt.get_datatype_num_constructors(s);
163 result = m.mk_fresh_const(f->get_name(), bv_sort);
164 f_fresh = to_app(result)->get_decl();
165 constrain_domain(m_imp.m_bounds, result, s, bv_sort);
166 expr_ref f_def(m);
167 ptr_vector<func_decl> const& cs = *m_dt.get_datatype_constructors(s);
168 f_def = m.mk_const(cs[nc-1]);
169 for (unsigned i = nc - 1; i-- > 0; ) {
170 f_def = m.mk_ite(m.mk_eq(result, value2bv(i, s)), m.mk_const(cs[i]), f_def);
171 }
172 m_imp.m_enum2def.insert(f, f_def);
173 m_imp.m_enum2bv.insert(f, f_fresh);
174 m_imp.m_bv2enum.insert(f_fresh, f);
175 m_imp.m_enum_consts.push_back(f);
176 m_imp.m_enum_bvs.push_back(f_fresh);
177 m_imp.m_enum_defs.push_back(f_def);
178 }
179 else {
180 throw_non_fd(a);
181 }
182 ++m_imp.m_num_translated;
183 return true;
184 }
185
186 ptr_buffer<sort> m_sorts;
187
reduce_quantifierenum2bv_rewriter::imp::rw_cfg188 bool reduce_quantifier(
189 quantifier * q,
190 expr * old_body,
191 expr * const * new_patterns,
192 expr * const * new_no_patterns,
193 expr_ref & result,
194 proof_ref & result_pr) {
195
196 if (q->get_kind() == lambda_k) return false;
197 m_sorts.reset();
198 expr_ref_vector bounds(m);
199 bool found = false;
200 for (unsigned i = 0; i < q->get_num_decls(); ++i) {
201 sort* s = q->get_decl_sort(i);
202 if (m_imp.is_fd(s)) {
203 unsigned bv_size = get_bv_size(s);
204 sort* bv_sort = m_bv.mk_sort(bv_size);
205 m_sorts.push_back(bv_sort);
206 expr_ref var(m.mk_var(q->get_num_decls()-i-1, bv_sort), m);
207 constrain_domain(bounds, var, s, bv_sort);
208 found = true;
209 }
210 else {
211 m_sorts.push_back(s);
212 }
213 }
214 if (!found) {
215 return false;
216 }
217 expr_ref new_body_ref(old_body, m), tmp(m);
218 if (!bounds.empty()) {
219 switch (q->get_kind()) {
220 case forall_k:
221 new_body_ref = m.mk_implies(mk_and(bounds), new_body_ref);
222 break;
223 case exists_k:
224 bounds.push_back(new_body_ref);
225 new_body_ref = mk_and(bounds);
226 break;
227 case lambda_k:
228 UNREACHABLE();
229 break;
230 }
231 }
232 result = m.mk_quantifier(q->get_kind(), q->get_num_decls(), m_sorts.data(), q->get_decl_names(), new_body_ref,
233 q->get_weight(), q->get_qid(), q->get_skid(),
234 q->get_num_patterns(), new_patterns,
235 q->get_num_no_patterns(), new_no_patterns);
236 if (m.proofs_enabled())
237 result_pr = m.mk_rewrite(q, result);
238 return true;
239 }
240
get_bv_sizeenum2bv_rewriter::imp::rw_cfg241 unsigned get_bv_size(sort* s) {
242 unsigned nc = m_dt.get_datatype_num_constructors(s);
243 if (is_unate(s))
244 return nc - 1;
245 unsigned bv_size = 1;
246 while ((unsigned)(1 << bv_size) < nc) {
247 ++bv_size;
248 }
249 return bv_size;
250 }
251 };
252
253 struct rw : public rewriter_tpl<rw_cfg> {
254 rw_cfg m_cfg;
255
rwenum2bv_rewriter::imp::rw256 rw(imp& t, ast_manager & m, params_ref const & p) :
257 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
258 m_cfg(t, m) {
259 }
260 };
261
262 rw m_rw;
263
impenum2bv_rewriter::imp264 imp(ast_manager& m, params_ref const& p):
265 m(m), m_params(p), m_bounds(m),
266 m_dt(m),
267 m_enum_consts(m),
268 m_enum_bvs(m),
269 m_enum_defs(m),
270 m_num_translated(0),
271 m_sort_pred(nullptr),
272 m_rw(*this, m, p) {
273 }
274
updt_paramsenum2bv_rewriter::imp275 void updt_params(params_ref const & p) {}
get_num_stepsenum2bv_rewriter::imp276 unsigned get_num_steps() const { return m_rw.get_num_steps(); }
cleanupenum2bv_rewriter::imp277 void cleanup() { m_rw.cleanup(); }
operator ()enum2bv_rewriter::imp278 void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
279 m_rw(e, result, result_proof);
280 }
pushenum2bv_rewriter::imp281 void push() {
282 m_enum_consts_lim.push_back(m_enum_consts.size());
283 }
popenum2bv_rewriter::imp284 void pop(unsigned num_scopes) {
285 SASSERT(m_bounds.empty()); // bounds must be flushed before pop.
286 if (num_scopes > 0) {
287 SASSERT(num_scopes <= m_enum_consts_lim.size());
288 unsigned new_sz = m_enum_consts_lim.size() - num_scopes;
289 unsigned lim = m_enum_consts_lim[new_sz];
290 for (unsigned i = m_enum_consts.size(); i > lim; ) {
291 --i;
292 func_decl* f = m_enum_consts[i].get();
293 func_decl* f_fresh = m_enum2bv.find(f);
294 m_bv2enum.erase(f_fresh);
295 m_enum2bv.erase(f);
296 m_enum2def.erase(f);
297 }
298 m_enum_consts_lim.resize(new_sz);
299 m_enum_consts.resize(lim);
300 m_enum_defs.resize(lim);
301 m_enum_bvs.resize(lim);
302 }
303 m_rw.reset();
304 }
305
flush_side_constraintsenum2bv_rewriter::imp306 void flush_side_constraints(expr_ref_vector& side_constraints) {
307 side_constraints.append(m_bounds);
308 m_bounds.reset();
309 }
310
is_fdenum2bv_rewriter::imp311 bool is_fd(sort* s) {
312 return m_dt.is_enum_sort(s) && (!m_sort_pred || (*m_sort_pred)(s));
313 }
314
set_is_fdenum2bv_rewriter::imp315 void set_is_fd(i_sort_pred* sp) {
316 m_sort_pred = sp;
317 }
318 };
319
320
enum2bv_rewriter(ast_manager & m,params_ref const & p)321 enum2bv_rewriter::enum2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); }
~enum2bv_rewriter()322 enum2bv_rewriter::~enum2bv_rewriter() { dealloc(m_imp); }
updt_params(params_ref const & p)323 void enum2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
m() const324 ast_manager & enum2bv_rewriter::m() const { return m_imp->m; }
get_num_steps() const325 unsigned enum2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
cleanup()326 void enum2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); }
enum2bv() const327 obj_map<func_decl, func_decl*> const& enum2bv_rewriter::enum2bv() const { return m_imp->m_enum2bv; }
bv2enum() const328 obj_map<func_decl, func_decl*> const& enum2bv_rewriter::bv2enum() const { return m_imp->m_bv2enum; }
enum2def() const329 obj_map<func_decl, expr*> const& enum2bv_rewriter::enum2def() const { return m_imp->m_enum2def; }
operator ()(expr * e,expr_ref & result,proof_ref & result_proof)330 void enum2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
push()331 void enum2bv_rewriter::push() { m_imp->push(); }
pop(unsigned num_scopes)332 void enum2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
flush_side_constraints(expr_ref_vector & side_constraints)333 void enum2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); }
num_translated() const334 unsigned enum2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
set_is_fd(i_sort_pred * sp) const335 void enum2bv_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); }
336