1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Liana Hadarean, Aina Niemetz, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of bitblasting functions for various operators. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H |
19 |
|
#define CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H |
20 |
|
|
21 |
|
#include <cmath> |
22 |
|
#include <ostream> |
23 |
|
|
24 |
|
#include "expr/node.h" |
25 |
|
#include "theory/bv/bitblast/bitblast_utils.h" |
26 |
|
#include "theory/bv/theory_bv_utils.h" |
27 |
|
#include "theory/rewriter.h" |
28 |
|
#include "util/bitvector.h" |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
|
32 |
|
namespace theory { |
33 |
|
namespace bv { |
34 |
|
|
35 |
|
/** |
36 |
|
* Default Atom Bitblasting strategies: |
37 |
|
* |
38 |
|
* @param node the atom to be bitblasted |
39 |
|
* @param bb the bitblaster |
40 |
|
*/ |
41 |
|
|
42 |
|
template <class T> |
43 |
|
T UndefinedAtomBBStrategy(TNode node, TBitblaster<T>* bb) { |
44 |
|
Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " |
45 |
|
<< node.getKind() << "\n"; |
46 |
|
Unreachable(); |
47 |
|
} |
48 |
|
|
49 |
|
|
50 |
|
template <class T> |
51 |
38269 |
T DefaultEqBB(TNode node, TBitblaster<T>* bb) { |
52 |
38269 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
53 |
|
|
54 |
38269 |
Assert(node.getKind() == kind::EQUAL); |
55 |
76538 |
std::vector<T> lhs, rhs; |
56 |
38269 |
bb->bbTerm(node[0], lhs); |
57 |
38269 |
bb->bbTerm(node[1], rhs); |
58 |
|
|
59 |
38269 |
Assert(lhs.size() == rhs.size()); |
60 |
|
|
61 |
76538 |
std::vector<T> bits_eq; |
62 |
455130 |
for (unsigned i = 0; i < lhs.size(); i++) { |
63 |
833722 |
T bit_eq = mkIff(lhs[i], rhs[i]); |
64 |
416861 |
bits_eq.push_back(bit_eq); |
65 |
|
} |
66 |
38269 |
T bv_eq = mkAnd(bits_eq); |
67 |
76538 |
return bv_eq; |
68 |
|
} |
69 |
|
|
70 |
|
template <class T> |
71 |
|
T AdderUltBB(TNode node, TBitblaster<T>* bb) { |
72 |
|
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
73 |
|
Assert(node.getKind() == kind::BITVECTOR_ULT); |
74 |
|
std::vector<T> a, b; |
75 |
|
bb->bbTerm(node[0], a); |
76 |
|
bb->bbTerm(node[1], b); |
77 |
|
Assert(a.size() == b.size()); |
78 |
|
|
79 |
|
// a < b <=> ~ (add(a, ~b, 1).carry_out) |
80 |
|
std::vector<T> not_b; |
81 |
|
negateBits(b, not_b); |
82 |
|
T carry = mkTrue<T>(); |
83 |
|
|
84 |
|
for (unsigned i = 0 ; i < a.size(); ++i) { |
85 |
|
carry = mkOr( mkAnd(a[i], not_b[i]), |
86 |
|
mkAnd( mkXor(a[i], not_b[i]), |
87 |
|
carry)); |
88 |
|
} |
89 |
|
return mkNot(carry); |
90 |
|
} |
91 |
|
|
92 |
|
|
93 |
|
template <class T> |
94 |
6314 |
T DefaultUltBB(TNode node, TBitblaster<T>* bb) { |
95 |
6314 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
96 |
6314 |
Assert(node.getKind() == kind::BITVECTOR_ULT); |
97 |
12628 |
std::vector<T> a, b; |
98 |
6314 |
bb->bbTerm(node[0], a); |
99 |
6314 |
bb->bbTerm(node[1], b); |
100 |
6314 |
Assert(a.size() == b.size()); |
101 |
|
|
102 |
|
// construct bitwise comparison |
103 |
6314 |
T res = uLessThanBB(a, b, false); |
104 |
12628 |
return res; |
105 |
|
} |
106 |
|
|
107 |
|
template <class T> |
108 |
|
T DefaultUleBB(TNode node, TBitblaster<T>* bb){ |
109 |
|
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
110 |
|
Assert(node.getKind() == kind::BITVECTOR_ULE); |
111 |
|
std::vector<T> a, b; |
112 |
|
|
113 |
|
bb->bbTerm(node[0], a); |
114 |
|
bb->bbTerm(node[1], b); |
115 |
|
Assert(a.size() == b.size()); |
116 |
|
// construct bitwise comparison |
117 |
|
T res = uLessThanBB(a, b, true); |
118 |
|
return res; |
119 |
|
} |
120 |
|
|
121 |
|
template <class T> |
122 |
|
T DefaultUgtBB(TNode node, TBitblaster<T>* bb){ |
123 |
|
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
124 |
|
// should be rewritten |
125 |
|
Unimplemented(); |
126 |
|
} |
127 |
|
template <class T> |
128 |
|
T DefaultUgeBB(TNode node, TBitblaster<T>* bb){ |
129 |
|
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
130 |
|
// should be rewritten |
131 |
|
Unimplemented(); |
132 |
|
} |
133 |
|
|
134 |
|
template <class T> |
135 |
6500 |
T DefaultSltBB(TNode node, TBitblaster<T>* bb){ |
136 |
6500 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
137 |
|
|
138 |
13000 |
std::vector<T> a, b; |
139 |
6500 |
bb->bbTerm(node[0], a); |
140 |
6500 |
bb->bbTerm(node[1], b); |
141 |
6500 |
Assert(a.size() == b.size()); |
142 |
|
|
143 |
6500 |
T res = sLessThanBB(a, b, false); |
144 |
13000 |
return res; |
145 |
|
} |
146 |
|
|
147 |
|
template <class T> |
148 |
|
T DefaultSleBB(TNode node, TBitblaster<T>* bb){ |
149 |
|
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
150 |
|
|
151 |
|
std::vector<T> a, b; |
152 |
|
bb->bbTerm(node[0], a); |
153 |
|
bb->bbTerm(node[1], b); |
154 |
|
Assert(a.size() == b.size()); |
155 |
|
|
156 |
|
T res = sLessThanBB(a, b, true); |
157 |
|
return res; |
158 |
|
} |
159 |
|
|
160 |
|
template <class T> |
161 |
|
T DefaultSgtBB(TNode node, TBitblaster<T>* bb){ |
162 |
|
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
163 |
|
// should be rewritten |
164 |
|
Unimplemented(); |
165 |
|
} |
166 |
|
|
167 |
|
template <class T> |
168 |
|
T DefaultSgeBB(TNode node, TBitblaster<T>* bb){ |
169 |
|
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
170 |
|
// should be rewritten |
171 |
|
Unimplemented(); |
172 |
|
} |
173 |
|
|
174 |
|
|
175 |
|
/// Term bitblasting strategies |
176 |
|
|
177 |
|
/** |
178 |
|
* Default Term Bitblasting strategies |
179 |
|
* |
180 |
|
* @param node the term to be bitblasted |
181 |
|
* @param bits [output parameter] bits representing the new term |
182 |
|
* @param bb the bitblaster in which the clauses are added |
183 |
|
*/ |
184 |
|
template <class T> |
185 |
|
void UndefinedTermBBStrategy(TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
186 |
|
Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " |
187 |
|
<< node.getKind() << "\n"; |
188 |
|
Unreachable(); |
189 |
|
} |
190 |
|
|
191 |
|
template <class T> |
192 |
19566 |
void DefaultVarBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
193 |
19566 |
Assert(bits.size() == 0); |
194 |
19566 |
bb->makeVariable(node, bits); |
195 |
|
|
196 |
19566 |
if(Debug.isOn("bitvector-bb")) { |
197 |
|
Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; |
198 |
|
Debug("bitvector-bb") << " with bits " << toString(bits); |
199 |
|
} |
200 |
19566 |
} |
201 |
|
|
202 |
|
template <class T> |
203 |
14700 |
void DefaultConstBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
204 |
14700 |
Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; |
205 |
14700 |
Assert(node.getKind() == kind::CONST_BITVECTOR); |
206 |
14700 |
Assert(bits.size() == 0); |
207 |
|
|
208 |
178430 |
for (unsigned i = 0; i < utils::getSize(node); ++i) { |
209 |
327460 |
Integer bit = node.getConst<BitVector>().extract(i, i).getValue(); |
210 |
163730 |
if(bit == Integer(0)){ |
211 |
110455 |
bits.push_back(mkFalse<T>()); |
212 |
|
} else { |
213 |
53275 |
Assert(bit == Integer(1)); |
214 |
53275 |
bits.push_back(mkTrue<T>()); |
215 |
|
} |
216 |
|
} |
217 |
14700 |
if(Debug.isOn("bitvector-bb")) { |
218 |
|
Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; |
219 |
|
} |
220 |
14700 |
} |
221 |
|
|
222 |
|
|
223 |
|
template <class T> |
224 |
5126 |
void DefaultNotBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
225 |
5126 |
Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; |
226 |
5126 |
Assert(node.getKind() == kind::BITVECTOR_NOT); |
227 |
5126 |
Assert(bits.size() == 0); |
228 |
10252 |
std::vector<T> bv; |
229 |
5126 |
bb->bbTerm(node[0], bv); |
230 |
5126 |
negateBits(bv, bits); |
231 |
5126 |
} |
232 |
|
|
233 |
|
template <class T> |
234 |
9110 |
void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
235 |
9110 |
Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; |
236 |
9110 |
Assert(bits.size() == 0); |
237 |
|
|
238 |
9110 |
Assert(node.getKind() == kind::BITVECTOR_CONCAT); |
239 |
33543 |
for (int i = node.getNumChildren() -1 ; i >= 0; --i ) { |
240 |
48866 |
TNode current = node[i]; |
241 |
48866 |
std::vector<T> current_bits; |
242 |
24433 |
bb->bbTerm(current, current_bits); |
243 |
|
|
244 |
149878 |
for(unsigned j = 0; j < utils::getSize(current); ++j) { |
245 |
125445 |
bits.push_back(current_bits[j]); |
246 |
|
} |
247 |
|
} |
248 |
9110 |
Assert(bits.size() == utils::getSize(node)); |
249 |
9110 |
if(Debug.isOn("bitvector-bb")) { |
250 |
|
Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; |
251 |
|
} |
252 |
9110 |
} |
253 |
|
|
254 |
|
template <class T> |
255 |
4358 |
void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
256 |
4358 |
Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; |
257 |
|
|
258 |
4358 |
Assert(node.getKind() == kind::BITVECTOR_AND && bits.size() == 0); |
259 |
|
|
260 |
4358 |
bb->bbTerm(node[0], bits); |
261 |
8716 |
std::vector<T> current; |
262 |
11804 |
for(unsigned j = 1; j < node.getNumChildren(); ++j) { |
263 |
7446 |
bb->bbTerm(node[j], current); |
264 |
24541 |
for (unsigned i = 0; i < utils::getSize(node); ++i) { |
265 |
17095 |
bits[i] = mkAnd(bits[i], current[i]); |
266 |
|
} |
267 |
7446 |
current.clear(); |
268 |
|
} |
269 |
4358 |
Assert(bits.size() == utils::getSize(node)); |
270 |
4358 |
} |
271 |
|
|
272 |
|
template <class T> |
273 |
5756 |
void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
274 |
5756 |
Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; |
275 |
|
|
276 |
5756 |
Assert(node.getKind() == kind::BITVECTOR_OR && bits.size() == 0); |
277 |
|
|
278 |
5756 |
bb->bbTerm(node[0], bits); |
279 |
11512 |
std::vector<T> current; |
280 |
52774 |
for(unsigned j = 1; j < node.getNumChildren(); ++j) { |
281 |
47018 |
bb->bbTerm(node[j], current); |
282 |
97649 |
for (unsigned i = 0; i < utils::getSize(node); ++i) { |
283 |
50631 |
bits[i] = mkOr(bits[i], current[i]); |
284 |
|
} |
285 |
47018 |
current.clear(); |
286 |
|
} |
287 |
5756 |
Assert(bits.size() == utils::getSize(node)); |
288 |
5756 |
} |
289 |
|
|
290 |
|
template <class T> |
291 |
517 |
void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
292 |
517 |
Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; |
293 |
|
|
294 |
517 |
Assert(node.getKind() == kind::BITVECTOR_XOR && bits.size() == 0); |
295 |
|
|
296 |
517 |
bb->bbTerm(node[0], bits); |
297 |
1034 |
std::vector<T> current; |
298 |
1041 |
for(unsigned j = 1; j < node.getNumChildren(); ++j) { |
299 |
524 |
bb->bbTerm(node[j], current); |
300 |
2858 |
for (unsigned i = 0; i < utils::getSize(node); ++i) { |
301 |
2334 |
bits[i] = mkXor(bits[i], current[i]); |
302 |
|
} |
303 |
524 |
current.clear(); |
304 |
|
} |
305 |
517 |
Assert(bits.size() == utils::getSize(node)); |
306 |
517 |
} |
307 |
|
|
308 |
|
template <class T> |
309 |
|
void DefaultXnorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
310 |
|
Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n"; |
311 |
|
|
312 |
|
Assert(node.getNumChildren() == 2 && node.getKind() == kind::BITVECTOR_XNOR |
313 |
|
&& bits.size() == 0); |
314 |
|
std::vector<T> lhs, rhs; |
315 |
|
bb->bbTerm(node[0], lhs); |
316 |
|
bb->bbTerm(node[1], rhs); |
317 |
|
Assert(lhs.size() == rhs.size()); |
318 |
|
|
319 |
|
for (unsigned i = 0; i < lhs.size(); ++i) { |
320 |
|
bits.push_back(mkIff(lhs[i], rhs[i])); |
321 |
|
} |
322 |
|
} |
323 |
|
|
324 |
|
|
325 |
|
template <class T> |
326 |
|
void DefaultNandBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
327 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
328 |
|
<< node.getKind() << "\n"; |
329 |
|
Unimplemented(); |
330 |
|
} |
331 |
|
template <class T> |
332 |
|
void DefaultNorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
333 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
334 |
|
<< node.getKind() << "\n"; |
335 |
|
Unimplemented(); |
336 |
|
} |
337 |
|
template <class T> |
338 |
6728 |
void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
339 |
6728 |
Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; |
340 |
|
|
341 |
6728 |
Assert(utils::getSize(node) == 1 && bits.size() == 0 |
342 |
|
&& node.getKind() == kind::BITVECTOR_COMP); |
343 |
13456 |
std::vector<T> a, b; |
344 |
6728 |
bb->bbTerm(node[0], a); |
345 |
6728 |
bb->bbTerm(node[1], b); |
346 |
|
|
347 |
13456 |
std::vector<T> bit_eqs; |
348 |
74586 |
for (unsigned i = 0; i < a.size(); ++i) { |
349 |
135716 |
T eq = mkIff(a[i], b[i]); |
350 |
67858 |
bit_eqs.push_back(eq); |
351 |
|
} |
352 |
13456 |
T a_eq_b = mkAnd(bit_eqs); |
353 |
6728 |
bits.push_back(a_eq_b); |
354 |
6728 |
} |
355 |
|
|
356 |
|
template <class T> |
357 |
1192 |
void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
358 |
1192 |
Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; |
359 |
1192 |
Assert(res.size() == 0 && node.getKind() == kind::BITVECTOR_MULT); |
360 |
|
|
361 |
|
// if (node.getNumChildren() == 2) { |
362 |
|
// std::vector<T> a; |
363 |
|
// std::vector<T> b; |
364 |
|
// bb->bbTerm(node[0], a); |
365 |
|
// bb->bbTerm(node[1], b); |
366 |
|
// unsigned bw = utils::getSize(node); |
367 |
|
// unsigned thresh = bw % 2 ? bw/2 : bw/2 - 1; |
368 |
|
// bool no_overflow = true; |
369 |
|
// for (unsigned i = thresh; i < bw; ++i) { |
370 |
|
// if (a[i] != mkFalse<T> || b[i] != mkFalse<T> ) { |
371 |
|
// no_overflow = false; |
372 |
|
// } |
373 |
|
// } |
374 |
|
// if (no_overflow) { |
375 |
|
// shiftAddMultiplier(); |
376 |
|
// return; |
377 |
|
// } |
378 |
|
|
379 |
|
// } |
380 |
|
|
381 |
2384 |
std::vector<T> newres; |
382 |
1192 |
bb->bbTerm(node[0], res); |
383 |
2420 |
for(unsigned i = 1; i < node.getNumChildren(); ++i) { |
384 |
2456 |
std::vector<T> current; |
385 |
1228 |
bb->bbTerm(node[i], current); |
386 |
1228 |
newres.clear(); |
387 |
|
// constructs a simple shift and add multiplier building the result |
388 |
|
// in res |
389 |
1228 |
shiftAddMultiplier(res, current, newres); |
390 |
1228 |
res = newres; |
391 |
|
} |
392 |
1192 |
if(Debug.isOn("bitvector-bb")) { |
393 |
|
Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; |
394 |
|
} |
395 |
1192 |
} |
396 |
|
|
397 |
|
template <class T> |
398 |
2893 |
void DefaultAddBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) |
399 |
|
{ |
400 |
2893 |
Debug("bitvector-bb") << "theory::bv::DefaultAddBB bitblasting " << node |
401 |
|
<< "\n"; |
402 |
2893 |
Assert(node.getKind() == kind::BITVECTOR_ADD && res.size() == 0); |
403 |
|
|
404 |
2893 |
bb->bbTerm(node[0], res); |
405 |
|
|
406 |
5786 |
std::vector<T> newres; |
407 |
|
|
408 |
5941 |
for(unsigned i = 1; i < node.getNumChildren(); ++i) { |
409 |
6096 |
std::vector<T> current; |
410 |
3048 |
bb->bbTerm(node[i], current); |
411 |
3048 |
newres.clear(); |
412 |
3048 |
rippleCarryAdder(res, current, newres, mkFalse<T>()); |
413 |
3048 |
res = newres; |
414 |
|
} |
415 |
|
|
416 |
2893 |
Assert(res.size() == utils::getSize(node)); |
417 |
2893 |
} |
418 |
|
|
419 |
|
template <class T> |
420 |
|
void DefaultSubBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
421 |
|
Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n"; |
422 |
|
Assert(node.getKind() == kind::BITVECTOR_SUB && node.getNumChildren() == 2 |
423 |
|
&& bits.size() == 0); |
424 |
|
|
425 |
|
std::vector<T> a, b; |
426 |
|
bb->bbTerm(node[0], a); |
427 |
|
bb->bbTerm(node[1], b); |
428 |
|
Assert(a.size() == b.size() && utils::getSize(node) == a.size()); |
429 |
|
|
430 |
|
// bvsub a b = adder(a, ~b, 1) |
431 |
|
std::vector<T> not_b; |
432 |
|
negateBits(b, not_b); |
433 |
|
rippleCarryAdder(a, not_b, bits, mkTrue<T>()); |
434 |
|
} |
435 |
|
|
436 |
|
template <class T> |
437 |
1482 |
void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
438 |
1482 |
Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n"; |
439 |
1482 |
Assert(node.getKind() == kind::BITVECTOR_NEG); |
440 |
|
|
441 |
2964 |
std::vector<T> a; |
442 |
1482 |
bb->bbTerm(node[0], a); |
443 |
1482 |
Assert(utils::getSize(node) == a.size()); |
444 |
|
|
445 |
|
// -a = add(~a, 0, 1). |
446 |
2964 |
std::vector<T> not_a; |
447 |
1482 |
negateBits(a, not_a); |
448 |
2964 |
std::vector<T> zero; |
449 |
1482 |
makeZero(zero, utils::getSize(node)); |
450 |
|
|
451 |
1482 |
rippleCarryAdder(not_a, zero, bits, mkTrue<T>()); |
452 |
1482 |
} |
453 |
|
|
454 |
|
template <class T> |
455 |
4867 |
void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T>& q, std::vector<T>& r, unsigned rec_width) { |
456 |
4867 |
Assert(q.size() == 0 && r.size() == 0); |
457 |
|
|
458 |
4867 |
if(rec_width == 0 || isZero(a)) { |
459 |
683 |
makeZero(q, a.size()); |
460 |
683 |
makeZero(r, a.size()); |
461 |
683 |
return; |
462 |
|
} |
463 |
|
|
464 |
8368 |
std::vector<T> q1, r1; |
465 |
8368 |
std::vector<T> a1 = a; |
466 |
4184 |
rshift(a1, 1); |
467 |
|
|
468 |
4184 |
uDivModRec(a1, b, q1, r1, rec_width - 1); |
469 |
|
// shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd |
470 |
4184 |
lshift(q1, 1); |
471 |
4184 |
lshift(r1, 1); |
472 |
|
|
473 |
|
|
474 |
8368 |
T is_odd = mkIff(a[0], mkTrue<T>()); |
475 |
8368 |
T one_if_odd = mkIte(is_odd, mkTrue<T>(), mkFalse<T>()); |
476 |
|
|
477 |
8368 |
std::vector<T> zero; |
478 |
4184 |
makeZero(zero, b.size()); |
479 |
|
|
480 |
8368 |
std::vector<T> r1_shift_add; |
481 |
|
// account for a being odd |
482 |
4184 |
rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd); |
483 |
|
// now check if the remainder is greater than b |
484 |
8368 |
std::vector<T> not_b; |
485 |
4184 |
negateBits(b, not_b); |
486 |
8368 |
std::vector<T> r_minus_b; |
487 |
8368 |
T co1; |
488 |
|
// use adder because we need r_minus_b anyway |
489 |
4184 |
co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue<T>()); |
490 |
|
// sign is true if r1 < b |
491 |
8368 |
T sign = mkNot(co1); |
492 |
|
|
493 |
4184 |
q1[0] = mkIte(sign, q1[0], mkTrue<T>()); |
494 |
|
|
495 |
|
// would be nice to have a high level ITE instead of bitwise |
496 |
54755 |
for(unsigned i = 0; i < a.size(); ++i) { |
497 |
50571 |
r1_shift_add[i] = mkIte(sign, r1_shift_add[i], r_minus_b[i]); |
498 |
|
} |
499 |
|
|
500 |
|
// check if a < b |
501 |
|
|
502 |
8368 |
std::vector<T> a_minus_b; |
503 |
8368 |
T co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue<T>()); |
504 |
|
// Node a_lt_b = a_minus_b.back(); |
505 |
8368 |
T a_lt_b = mkNot(co2); |
506 |
|
|
507 |
54755 |
for(unsigned i = 0; i < a.size(); ++i) { |
508 |
101142 |
T qval = mkIte(a_lt_b, mkFalse<T>(), q1[i]); |
509 |
101142 |
T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]); |
510 |
50571 |
q.push_back(qval); |
511 |
50571 |
r.push_back(rval); |
512 |
|
} |
513 |
|
|
514 |
|
} |
515 |
|
|
516 |
|
template <class T> |
517 |
381 |
void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb) |
518 |
|
{ |
519 |
381 |
Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node |
520 |
|
<< "\n"; |
521 |
381 |
Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); |
522 |
|
|
523 |
762 |
std::vector<T> a, b; |
524 |
381 |
bb->bbTerm(node[0], a); |
525 |
381 |
bb->bbTerm(node[1], b); |
526 |
|
|
527 |
762 |
std::vector<T> r; |
528 |
381 |
uDivModRec(a, b, q, r, utils::getSize(node)); |
529 |
|
// adding a special case for division by 0 |
530 |
762 |
std::vector<T> iszero; |
531 |
3058 |
for (unsigned i = 0; i < b.size(); ++i) |
532 |
|
{ |
533 |
2677 |
iszero.push_back(mkIff(b[i], mkFalse<T>())); |
534 |
|
} |
535 |
762 |
T b_is_0 = mkAnd(iszero); |
536 |
|
|
537 |
3058 |
for (unsigned i = 0; i < q.size(); ++i) |
538 |
|
{ |
539 |
2677 |
q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11 |
540 |
2677 |
r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a |
541 |
|
} |
542 |
|
|
543 |
|
// cache the remainder in case we need it later |
544 |
762 |
Node remainder = Rewriter::rewrite( |
545 |
|
NodeManager::currentNM()->mkNode(kind::BITVECTOR_UREM, node[0], node[1])); |
546 |
381 |
bb->storeBBTerm(remainder, r); |
547 |
381 |
} |
548 |
|
|
549 |
|
template <class T> |
550 |
302 |
void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb) |
551 |
|
{ |
552 |
302 |
Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node |
553 |
|
<< "\n"; |
554 |
302 |
Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); |
555 |
|
|
556 |
604 |
std::vector<T> a, b; |
557 |
302 |
bb->bbTerm(node[0], a); |
558 |
302 |
bb->bbTerm(node[1], b); |
559 |
|
|
560 |
604 |
std::vector<T> q; |
561 |
302 |
uDivModRec(a, b, q, rem, utils::getSize(node)); |
562 |
|
// adding a special case for division by 0 |
563 |
604 |
std::vector<T> iszero; |
564 |
2432 |
for (unsigned i = 0; i < b.size(); ++i) |
565 |
|
{ |
566 |
2130 |
iszero.push_back(mkIff(b[i], mkFalse<T>())); |
567 |
|
} |
568 |
604 |
T b_is_0 = mkAnd(iszero); |
569 |
|
|
570 |
2432 |
for (unsigned i = 0; i < q.size(); ++i) |
571 |
|
{ |
572 |
2130 |
q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11 |
573 |
2130 |
rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a |
574 |
|
} |
575 |
|
|
576 |
|
// cache the quotient in case we need it later |
577 |
604 |
Node quotient = Rewriter::rewrite( |
578 |
|
NodeManager::currentNM()->mkNode(kind::BITVECTOR_UDIV, node[0], node[1])); |
579 |
302 |
bb->storeBBTerm(quotient, q); |
580 |
302 |
} |
581 |
|
|
582 |
|
template <class T> |
583 |
|
void DefaultSdivBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
584 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
585 |
|
<< node.getKind() << "\n"; |
586 |
|
Unimplemented(); |
587 |
|
} |
588 |
|
template <class T> |
589 |
|
void DefaultSremBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
590 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
591 |
|
<< node.getKind() << "\n"; |
592 |
|
Unimplemented(); |
593 |
|
} |
594 |
|
template <class T> |
595 |
|
void DefaultSmodBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
596 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
597 |
|
<< node.getKind() << "\n"; |
598 |
|
Unimplemented(); |
599 |
|
} |
600 |
|
|
601 |
|
template <class T> |
602 |
691 |
void DefaultShlBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) |
603 |
|
{ |
604 |
691 |
Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node |
605 |
|
<< "\n"; |
606 |
691 |
Assert(node.getKind() == kind::BITVECTOR_SHL && res.size() == 0); |
607 |
1382 |
std::vector<T> a, b; |
608 |
691 |
bb->bbTerm(node[0], a); |
609 |
691 |
bb->bbTerm(node[1], b); |
610 |
|
|
611 |
|
// check for b < log2(n) |
612 |
691 |
unsigned size = utils::getSize(node); |
613 |
691 |
unsigned log2_size = std::ceil(log2((double)size)); |
614 |
1382 |
Node a_size = utils::mkConst(size, size); |
615 |
|
|
616 |
1382 |
std::vector<T> a_size_bits; |
617 |
691 |
DefaultConstBB(a_size, a_size_bits, bb); |
618 |
1382 |
T b_ult_a_size = uLessThanBB(b, a_size_bits, false); |
619 |
|
|
620 |
1382 |
std::vector<T> prev_res; |
621 |
691 |
res = a; |
622 |
|
// we only need to look at the bits bellow log2_a_size |
623 |
2321 |
for (unsigned s = 0; s < log2_size; ++s) |
624 |
|
{ |
625 |
|
// barrel shift stage: at each stage you can either shift by 2^s bits |
626 |
|
// or leave the previous stage untouched |
627 |
1630 |
prev_res = res; |
628 |
1630 |
unsigned threshold = pow(2, s); |
629 |
17800 |
for (unsigned i = 0; i < a.size(); ++i) |
630 |
|
{ |
631 |
16170 |
if (i < threshold) |
632 |
|
{ |
633 |
|
// if b[s] is true then we must have shifted by at least 2^b bits so |
634 |
|
// all bits bellow 2^s will be 0, otherwise just use previous shift |
635 |
|
// value |
636 |
4672 |
res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]); |
637 |
|
} |
638 |
|
else |
639 |
|
{ |
640 |
|
// if b[s]= 0, use previous value, otherwise shift by threshold bits |
641 |
11498 |
Assert(i >= threshold); |
642 |
11498 |
res[i] = mkIte(b[s], prev_res[i - threshold], prev_res[i]); |
643 |
|
} |
644 |
|
} |
645 |
|
} |
646 |
691 |
prev_res = res; |
647 |
5340 |
for (unsigned i = 0; i < b.size(); ++i) |
648 |
|
{ |
649 |
|
// this is fine because b_ult_a_size has been bit-blasted |
650 |
4649 |
res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); |
651 |
|
} |
652 |
|
|
653 |
691 |
if (Debug.isOn("bitvector-bb")) |
654 |
|
{ |
655 |
|
Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; |
656 |
|
} |
657 |
691 |
} |
658 |
|
|
659 |
|
template <class T> |
660 |
804 |
void DefaultLshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) |
661 |
|
{ |
662 |
804 |
Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node |
663 |
|
<< "\n"; |
664 |
804 |
Assert(node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0); |
665 |
1608 |
std::vector<T> a, b; |
666 |
804 |
bb->bbTerm(node[0], a); |
667 |
804 |
bb->bbTerm(node[1], b); |
668 |
|
|
669 |
|
// check for b < log2(n) |
670 |
804 |
unsigned size = utils::getSize(node); |
671 |
804 |
unsigned log2_size = std::ceil(log2((double)size)); |
672 |
1608 |
Node a_size = utils::mkConst(size, size); |
673 |
|
|
674 |
1608 |
std::vector<T> a_size_bits; |
675 |
804 |
DefaultConstBB(a_size, a_size_bits, bb); |
676 |
1608 |
T b_ult_a_size = uLessThanBB(b, a_size_bits, false); |
677 |
|
|
678 |
804 |
res = a; |
679 |
1608 |
std::vector<T> prev_res; |
680 |
|
|
681 |
2749 |
for (unsigned s = 0; s < log2_size; ++s) |
682 |
|
{ |
683 |
|
// barrel shift stage: at each stage you can either shift by 2^s bits |
684 |
|
// or leave the previous stage untouched |
685 |
1945 |
prev_res = res; |
686 |
1945 |
int threshold = pow(2, s); |
687 |
22425 |
for (unsigned i = 0; i < a.size(); ++i) |
688 |
|
{ |
689 |
20480 |
if (i + threshold >= a.size()) |
690 |
|
{ |
691 |
|
// if b[s] is true then we must have shifted by at least 2^b bits so |
692 |
|
// all bits above 2^s will be 0, otherwise just use previous shift value |
693 |
5341 |
res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]); |
694 |
|
} |
695 |
|
else |
696 |
|
{ |
697 |
|
// if b[s]= 0, use previous value, otherwise shift by threshold bits |
698 |
15139 |
Assert(i + threshold < a.size()); |
699 |
15139 |
res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); |
700 |
|
} |
701 |
|
} |
702 |
|
} |
703 |
|
|
704 |
804 |
prev_res = res; |
705 |
6730 |
for (unsigned i = 0; i < b.size(); ++i) |
706 |
|
{ |
707 |
|
// this is fine because b_ult_a_size has been bit-blasted |
708 |
5926 |
res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); |
709 |
|
} |
710 |
|
|
711 |
804 |
if (Debug.isOn("bitvector-bb")) |
712 |
|
{ |
713 |
|
Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; |
714 |
|
} |
715 |
804 |
} |
716 |
|
|
717 |
|
template <class T> |
718 |
621 |
void DefaultAshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) |
719 |
|
{ |
720 |
621 |
Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node |
721 |
|
<< "\n"; |
722 |
621 |
Assert(node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0); |
723 |
1242 |
std::vector<T> a, b; |
724 |
621 |
bb->bbTerm(node[0], a); |
725 |
621 |
bb->bbTerm(node[1], b); |
726 |
|
|
727 |
|
// check for b < n |
728 |
621 |
unsigned size = utils::getSize(node); |
729 |
621 |
unsigned log2_size = std::ceil(log2((double)size)); |
730 |
1242 |
Node a_size = utils::mkConst(size, size); |
731 |
|
|
732 |
1242 |
std::vector<T> a_size_bits; |
733 |
621 |
DefaultConstBB(a_size, a_size_bits, bb); |
734 |
1242 |
T b_ult_a_size = uLessThanBB(b, a_size_bits, false); |
735 |
|
|
736 |
621 |
res = a; |
737 |
1242 |
T sign_bit = a.back(); |
738 |
1242 |
std::vector<T> prev_res; |
739 |
|
|
740 |
1905 |
for (unsigned s = 0; s < log2_size; ++s) |
741 |
|
{ |
742 |
|
// barrel shift stage: at each stage you can either shift by 2^s bits |
743 |
|
// or leave the previous stage untouched |
744 |
1284 |
prev_res = res; |
745 |
1284 |
int threshold = pow(2, s); |
746 |
10583 |
for (unsigned i = 0; i < a.size(); ++i) |
747 |
|
{ |
748 |
9299 |
if (i + threshold >= a.size()) |
749 |
|
{ |
750 |
|
// if b[s] is true then we must have shifted by at least 2^b bits so |
751 |
|
// all bits above 2^s will be the sign bit, otherwise just use previous |
752 |
|
// shift value |
753 |
2884 |
res[i] = mkIte(b[s], sign_bit, prev_res[i]); |
754 |
|
} |
755 |
|
else |
756 |
|
{ |
757 |
|
// if b[s]= 0, use previous value, otherwise shift by threshold bits |
758 |
6415 |
Assert(i + threshold < a.size()); |
759 |
6415 |
res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); |
760 |
|
} |
761 |
|
} |
762 |
|
} |
763 |
|
|
764 |
621 |
prev_res = res; |
765 |
3854 |
for (unsigned i = 0; i < b.size(); ++i) |
766 |
|
{ |
767 |
|
// this is fine because b_ult_a_size has been bit-blasted |
768 |
3233 |
res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit); |
769 |
|
} |
770 |
|
|
771 |
621 |
if (Debug.isOn("bitvector-bb")) |
772 |
|
{ |
773 |
|
Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; |
774 |
|
} |
775 |
621 |
} |
776 |
|
|
777 |
|
template <class T> |
778 |
578 |
void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
779 |
578 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
780 |
578 |
Assert(node.getKind() == kind::BITVECTOR_ULTBV); |
781 |
1156 |
std::vector<T> a, b; |
782 |
578 |
bb->bbTerm(node[0], a); |
783 |
578 |
bb->bbTerm(node[1], b); |
784 |
578 |
Assert(a.size() == b.size()); |
785 |
|
|
786 |
|
// construct bitwise comparison |
787 |
578 |
res.push_back(uLessThanBB(a, b, false)); |
788 |
578 |
} |
789 |
|
|
790 |
|
template <class T> |
791 |
1163 |
void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
792 |
1163 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
793 |
1163 |
Assert(node.getKind() == kind::BITVECTOR_SLTBV); |
794 |
2326 |
std::vector<T> a, b; |
795 |
1163 |
bb->bbTerm(node[0], a); |
796 |
1163 |
bb->bbTerm(node[1], b); |
797 |
1163 |
Assert(a.size() == b.size()); |
798 |
|
|
799 |
|
// construct bitwise comparison |
800 |
1163 |
res.push_back(sLessThanBB(a, b, false)); |
801 |
1163 |
} |
802 |
|
|
803 |
|
template <class T> |
804 |
3506 |
void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
805 |
3506 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
806 |
3506 |
Assert(node.getKind() == kind::BITVECTOR_ITE); |
807 |
7012 |
std::vector<T> cond, thenpart, elsepart; |
808 |
3506 |
bb->bbTerm(node[0], cond); |
809 |
3506 |
bb->bbTerm(node[1], thenpart); |
810 |
3506 |
bb->bbTerm(node[2], elsepart); |
811 |
|
|
812 |
3506 |
Assert(cond.size() == 1); |
813 |
3506 |
Assert(thenpart.size() == elsepart.size()); |
814 |
|
|
815 |
58531 |
for (unsigned i = 0; i < thenpart.size(); ++i) { |
816 |
|
// (~cond OR thenpart) AND (cond OR elsepart) |
817 |
55025 |
res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i]))); |
818 |
|
} |
819 |
3506 |
} |
820 |
|
|
821 |
|
template <class T> |
822 |
9036 |
void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
823 |
9036 |
Assert(node.getKind() == kind::BITVECTOR_EXTRACT); |
824 |
9036 |
Assert(bits.size() == 0); |
825 |
|
|
826 |
18072 |
std::vector<T> base_bits; |
827 |
9036 |
bb->bbTerm(node[0], base_bits); |
828 |
9036 |
unsigned high = utils::getExtractHigh(node); |
829 |
9036 |
unsigned low = utils::getExtractLow(node); |
830 |
|
|
831 |
70840 |
for (unsigned i = low; i <= high; ++i) { |
832 |
61804 |
bits.push_back(base_bits[i]); |
833 |
|
} |
834 |
9036 |
Assert(bits.size() == high - low + 1); |
835 |
|
|
836 |
9036 |
if(Debug.isOn("bitvector-bb")) { |
837 |
|
Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; |
838 |
|
Debug("bitvector-bb") << " with bits " << toString(bits); |
839 |
|
} |
840 |
9036 |
} |
841 |
|
|
842 |
|
|
843 |
|
template <class T> |
844 |
|
void DefaultRepeatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
845 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
846 |
|
<< node.getKind() << "\n"; |
847 |
|
// this should be rewritten |
848 |
|
Unimplemented(); |
849 |
|
} |
850 |
|
|
851 |
|
template <class T> |
852 |
|
void DefaultZeroExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) { |
853 |
|
|
854 |
|
Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; |
855 |
|
|
856 |
|
// this should be rewritten |
857 |
|
Unimplemented(); |
858 |
|
|
859 |
|
} |
860 |
|
|
861 |
|
template <class T> |
862 |
4076 |
void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) { |
863 |
4076 |
Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; |
864 |
|
|
865 |
4076 |
Assert(node.getKind() == kind::BITVECTOR_SIGN_EXTEND && res_bits.size() == 0); |
866 |
|
|
867 |
8152 |
std::vector<T> bits; |
868 |
4076 |
bb->bbTerm(node[0], bits); |
869 |
|
|
870 |
8152 |
T sign_bit = bits.back(); |
871 |
4076 |
unsigned amount = |
872 |
8152 |
node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount; |
873 |
|
|
874 |
15525 |
for (unsigned i = 0; i < bits.size(); ++i ) { |
875 |
11449 |
res_bits.push_back(bits[i]); |
876 |
|
} |
877 |
|
|
878 |
23213 |
for (unsigned i = 0 ; i < amount ; ++i ) { |
879 |
19137 |
res_bits.push_back(sign_bit); |
880 |
|
} |
881 |
|
|
882 |
4076 |
Assert(res_bits.size() == amount + bits.size()); |
883 |
4076 |
} |
884 |
|
|
885 |
|
template <class T> |
886 |
|
void DefaultRotateRightBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
887 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
888 |
|
<< node.getKind() << "\n"; |
889 |
|
|
890 |
|
Unimplemented(); |
891 |
|
} |
892 |
|
|
893 |
|
template <class T> |
894 |
|
void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
895 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
896 |
|
<< node.getKind() << "\n"; |
897 |
|
Unimplemented(); |
898 |
|
} |
899 |
|
|
900 |
|
|
901 |
|
} |
902 |
|
} |
903 |
|
} // namespace cvc5 |
904 |
|
|
905 |
|
#endif |