1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 bit_blaster.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2008-06-05.
15
16 Revision History:
17
18 --*/
19
20 #include "ast/ast_pp.h"
21 #include "ast/ast_ll_pp.h"
22 #include "ast/reg_decl_plugins.h"
23 #include "ast/rewriter/bit_blaster/bit_blaster.h"
24 #include "model/model.h"
25 #include "model/model_evaluator.h"
26
mk_bits(ast_manager & m,char const * prefix,unsigned sz,expr_ref_vector & r)27 void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector & r) {
28 sort_ref b(m);
29 b = m.mk_bool_sort();
30 for (unsigned i = 0; i < sz; ++i) {
31 char buffer[128];
32 #ifdef _WINDOWS
33 sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "%s%d.smt", prefix, i);
34 #else
35 sprintf(buffer, "%s%d.smt", prefix, i);
36 #endif
37 r.push_back(m.mk_const(symbol(buffer), b));
38 }
39 }
40
display(std::ostream & out,expr_ref_vector & r,bool ll=true)41 void display(std::ostream & out, expr_ref_vector & r, bool ll=true) {
42 for (unsigned i = 0; i < r.size(); i++) {
43 out << "bit " << i << ":\n";
44 if (ll)
45 ast_ll_pp(out, r.get_manager(), r.get(i));
46 else
47 out << mk_pp(r.get(i), r.get_manager()) << "\n";
48 }
49 }
50
to_int(model_core & mdl,expr_ref_vector & out)51 static unsigned to_int(model_core & mdl, expr_ref_vector & out) {
52 SASSERT(out.size() <= sizeof(unsigned) * 8);
53 ast_manager & m = mdl.get_manager();
54 model_evaluator eval(mdl);
55 expr_ref bit(m);
56 unsigned actual = 0;
57 for (unsigned i = 0; i < out.size(); i++) {
58 eval(out.get(i), bit);
59 if (m.is_true(bit))
60 actual |= 1 << i;
61 else
62 ENSURE(m.is_false(bit));
63 }
64 return actual;
65 }
66
67 #define ENSURE_INT(mdl, out, expected) \
68 do { \
69 unsigned actual = to_int(mdl, out); \
70 TRACE("bit_blaster", \
71 display(tout, out); \
72 tout << "expected=" << (expected) << ", actual=" << actual << "\n"; \
73 ); \
74 ENSURE(actual == (expected)); \
75 } while (0)
76
tst_adder(ast_manager & m,bit_blaster & blaster)77 void tst_adder(ast_manager & m, bit_blaster & blaster) {
78 model mdl(m);
79 expr_ref_vector c(m);
80 app_ref b1(m.mk_const("b1", m.mk_bool_sort()), m);
81 app_ref b2(m.mk_const("b2", m.mk_bool_sort()), m);
82 expr_ref not_b1(m.mk_not(b1), m);
83
84 {
85 expr * const a[] = { b1, b1, b1 };
86 expr * const b[] = { m.mk_false(), m.mk_true(), m.mk_true() };
87 c.reset();
88 blaster.mk_adder(3, a, b, c);
89 }
90
91 mdl.register_decl(b1->get_decl(), m.mk_false());
92 ENSURE_INT(mdl, c, 6); // b000 + b110
93
94 mdl.register_decl(b1->get_decl(), m.mk_true());
95 ENSURE_INT(mdl, c, 5); // b111 + b110
96
97 {
98 expr * const a[] = { m.mk_false(), m.mk_true(), m.mk_true() };
99 expr * const b[] = { b1, not_b1, m.mk_false() };
100 c.reset();
101 blaster.mk_adder(3, a, b, c);
102 }
103
104 mdl.register_decl(b1->get_decl(), m.mk_false());
105 ENSURE_INT(mdl, c, 0); // b110 + b010
106
107 mdl.register_decl(b1->get_decl(), m.mk_true());
108 ENSURE_INT(mdl, c, 7); // b110 + b001
109
110 {
111 expr * const a[] = { b1, b2, m.mk_true() };
112 expr * const b[] = { b1, not_b1, m.mk_false() };
113 c.reset();
114 blaster.mk_adder(3, a, b, c);
115 }
116
117 mdl.register_decl(b1->get_decl(), m.mk_false());
118 mdl.register_decl(b2->get_decl(), m.mk_false());
119 ENSURE_INT(mdl, c, 6); // b100 + b010
120
121 mdl.register_decl(b1->get_decl(), m.mk_false());
122 mdl.register_decl(b2->get_decl(), m.mk_true());
123 ENSURE_INT(mdl, c, 0); // b110 + b010
124
125 mdl.register_decl(b1->get_decl(), m.mk_true());
126 mdl.register_decl(b2->get_decl(), m.mk_false());
127 ENSURE_INT(mdl, c, 6); // b101 + b001
128
129 mdl.register_decl(b1->get_decl(), m.mk_true());
130 mdl.register_decl(b2->get_decl(), m.mk_true());
131 ENSURE_INT(mdl, c, 0); // b111 + b001
132 }
133
tst_multiplier(ast_manager & m,bit_blaster & blaster)134 void tst_multiplier(ast_manager & m, bit_blaster & blaster) {
135 model mdl(m);
136 expr_ref_vector c(m);
137 app_ref b1(m.mk_const("b1", m.mk_bool_sort()), m);
138 app_ref b2(m.mk_const("b2", m.mk_bool_sort()), m);
139 expr_ref not_b1(m.mk_not(b1), m);
140
141 {
142 expr * const a[] = { b1, b1, b1 };
143 expr * const b[] = { m.mk_false(), m.mk_true(), m.mk_true() };
144 c.reset();
145 blaster.mk_multiplier(3, a, b, c);
146 }
147
148 mdl.register_decl(b1->get_decl(), m.mk_false());
149 ENSURE_INT(mdl, c, 0); // b000 * b110
150
151 mdl.register_decl(b1->get_decl(), m.mk_true());
152 ENSURE_INT(mdl, c, 2); // b111 * b110
153
154 {
155 expr * const a[] = { m.mk_false(), m.mk_true(), m.mk_true() };
156 expr * const b[] = { b1, not_b1, m.mk_false() };
157 c.reset();
158 blaster.mk_multiplier(3, a, b, c);
159 }
160
161 mdl.register_decl(b1->get_decl(), m.mk_false());
162 ENSURE_INT(mdl, c, 4); // b110 * b010
163
164 mdl.register_decl(b1->get_decl(), m.mk_true());
165 ENSURE_INT(mdl, c, 6); // b110 * b001
166
167 {
168 expr * const a[] = { b1, b2, m.mk_true() };
169 expr * const b[] = { b1, not_b1, m.mk_false() };
170 c.reset();
171 blaster.mk_multiplier(3, a, b, c);
172 }
173
174 mdl.register_decl(b1->get_decl(), m.mk_false());
175 mdl.register_decl(b2->get_decl(), m.mk_false());
176 ENSURE_INT(mdl, c, 0); // b100 * b010
177
178 mdl.register_decl(b1->get_decl(), m.mk_false());
179 mdl.register_decl(b2->get_decl(), m.mk_true());
180 ENSURE_INT(mdl, c, 4); // b110 * b010
181
182 mdl.register_decl(b1->get_decl(), m.mk_true());
183 mdl.register_decl(b2->get_decl(), m.mk_false());
184 ENSURE_INT(mdl, c, 5); // b101 * b001
185
186 mdl.register_decl(b1->get_decl(), m.mk_true());
187 mdl.register_decl(b2->get_decl(), m.mk_true());
188 ENSURE_INT(mdl, c, 7); // b111 * b001
189 }
190
tst_le(ast_manager & m,unsigned sz)191 void tst_le(ast_manager & m, unsigned sz) {
192 // expr_ref_vector a(m);
193 // expr_ref_vector b(m);
194 // expr_ref out(m);
195 // mk_bits(m, "a", sz, a);
196 // mk_bits(m, "b", sz, b);
197 // bool t = true;
198 // bit_blaster blaster(m, t);
199 // blaster.mk_ule(sz, a.c_ptr(), b.c_ptr(), out);
200 // TRACE("bit_blaster", tout << mk_pp(out, m) << "\n";);
201 // blaster.mk_sle(sz, a.c_ptr(), b.c_ptr(), out);
202 // TRACE("bit_blaster", tout << mk_pp(out, m) << "\n";);
203 }
204
tst_eqs(ast_manager & m,unsigned sz)205 void tst_eqs(ast_manager & m, unsigned sz) {
206 // expr_ref_vector a(m);
207 // expr_ref_vector b(m);
208 // expr_ref out(m);
209 // mk_bits(m, "a", sz, a);
210 // bool t = true;
211 // bit_blaster blaster(m, t);
212 // blaster.mk_eqs(sz, a.c_ptr(), b);
213 // TRACE("bit_blaster", display(tout, b, false););
214 }
215
tst_sh(ast_manager & m,unsigned sz)216 void tst_sh(ast_manager & m, unsigned sz) {
217 // expr_ref_vector a(m);
218 // expr_ref_vector b(m);
219 // expr_ref_vector c(m);
220 // mk_bits(m, "a", sz, a);
221 // mk_bits(m, "b", sz, b);
222 // bool t = true;
223 // bit_blaster blaster(m, t);
224 // blaster.mk_shl(sz, a.c_ptr(), b.c_ptr(), c);
225 // TRACE("bit_blaster", tout << "shl\n"; display(tout, c););
226 // c.reset();
227 // blaster.mk_lshr(sz, a.c_ptr(), b.c_ptr(), c);
228 // TRACE("bit_blaster", tout << "lshr\n"; display(tout, c););
229 // c.reset();
230 // blaster.mk_ashr(sz, a.c_ptr(), b.c_ptr(), c);
231 // TRACE("bit_blaster", tout << "ashr " << c.size() << "\n"; display(tout, c, false););
232 }
233
tst_bit_blaster()234 void tst_bit_blaster() {
235 ast_manager m;
236 reg_decl_plugins(m);
237 bit_blaster_params params;
238 bit_blaster blaster(m, params);
239
240 tst_adder(m, blaster);
241 tst_multiplier(m, blaster);
242 tst_le(m, 4);
243 tst_eqs(m, 8);
244 tst_sh(m, 4);
245 }
246