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