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 "util/bitvector.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 |
25052 |
T DefaultEqBB(TNode node, TBitblaster<T>* bb) { |
51 |
25052 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
52 |
|
|
53 |
25052 |
Assert(node.getKind() == kind::EQUAL); |
54 |
50104 |
std::vector<T> lhs, rhs; |
55 |
25052 |
bb->bbTerm(node[0], lhs); |
56 |
25052 |
bb->bbTerm(node[1], rhs); |
57 |
|
|
58 |
25052 |
Assert(lhs.size() == rhs.size()); |
59 |
|
|
60 |
50104 |
std::vector<T> bits_eq; |
61 |
333172 |
for (unsigned i = 0; i < lhs.size(); i++) { |
62 |
616240 |
T bit_eq = mkIff(lhs[i], rhs[i]); |
63 |
308120 |
bits_eq.push_back(bit_eq); |
64 |
|
} |
65 |
25052 |
T bv_eq = mkAnd(bits_eq); |
66 |
50104 |
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 |
4031 |
T DefaultUltBB(TNode node, TBitblaster<T>* bb) { |
94 |
4031 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
95 |
4031 |
Assert(node.getKind() == kind::BITVECTOR_ULT); |
96 |
8062 |
std::vector<T> a, b; |
97 |
4031 |
bb->bbTerm(node[0], a); |
98 |
4031 |
bb->bbTerm(node[1], b); |
99 |
4031 |
Assert(a.size() == b.size()); |
100 |
|
|
101 |
|
// construct bitwise comparison |
102 |
4031 |
T res = uLessThanBB(a, b, false); |
103 |
8062 |
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 |
4130 |
T DefaultSltBB(TNode node, TBitblaster<T>* bb){ |
135 |
4130 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
136 |
|
|
137 |
8260 |
std::vector<T> a, b; |
138 |
4130 |
bb->bbTerm(node[0], a); |
139 |
4130 |
bb->bbTerm(node[1], b); |
140 |
4130 |
Assert(a.size() == b.size()); |
141 |
|
|
142 |
4130 |
T res = sLessThanBB(a, b, false); |
143 |
8260 |
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 |
11036 |
void DefaultVarBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
192 |
11036 |
Assert(bits.size() == 0); |
193 |
11036 |
bb->makeVariable(node, bits); |
194 |
|
|
195 |
11036 |
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 |
11036 |
} |
200 |
|
|
201 |
|
template <class T> |
202 |
9045 |
void DefaultConstBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
203 |
9045 |
Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; |
204 |
9045 |
Assert(node.getKind() == kind::CONST_BITVECTOR); |
205 |
9045 |
Assert(bits.size() == 0); |
206 |
|
|
207 |
123795 |
for (unsigned i = 0; i < utils::getSize(node); ++i) { |
208 |
229500 |
Integer bit = node.getConst<BitVector>().extract(i, i).getValue(); |
209 |
114750 |
if(bit == Integer(0)){ |
210 |
78539 |
bits.push_back(mkFalse<T>()); |
211 |
|
} else { |
212 |
36211 |
Assert(bit == Integer(1)); |
213 |
36211 |
bits.push_back(mkTrue<T>()); |
214 |
|
} |
215 |
|
} |
216 |
9045 |
if(Debug.isOn("bitvector-bb")) { |
217 |
|
Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; |
218 |
|
} |
219 |
9045 |
} |
220 |
|
|
221 |
|
|
222 |
|
template <class T> |
223 |
2943 |
void DefaultNotBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
224 |
2943 |
Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; |
225 |
2943 |
Assert(node.getKind() == kind::BITVECTOR_NOT); |
226 |
2943 |
Assert(bits.size() == 0); |
227 |
5886 |
std::vector<T> bv; |
228 |
2943 |
bb->bbTerm(node[0], bv); |
229 |
2943 |
negateBits(bv, bits); |
230 |
2943 |
} |
231 |
|
|
232 |
|
template <class T> |
233 |
5420 |
void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
234 |
5420 |
Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; |
235 |
5420 |
Assert(bits.size() == 0); |
236 |
|
|
237 |
5420 |
Assert(node.getKind() == kind::BITVECTOR_CONCAT); |
238 |
20113 |
for (int i = node.getNumChildren() -1 ; i >= 0; --i ) { |
239 |
29386 |
TNode current = node[i]; |
240 |
29386 |
std::vector<T> current_bits; |
241 |
14693 |
bb->bbTerm(current, current_bits); |
242 |
|
|
243 |
91145 |
for(unsigned j = 0; j < utils::getSize(current); ++j) { |
244 |
76452 |
bits.push_back(current_bits[j]); |
245 |
|
} |
246 |
|
} |
247 |
5420 |
Assert(bits.size() == utils::getSize(node)); |
248 |
5420 |
if(Debug.isOn("bitvector-bb")) { |
249 |
|
Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; |
250 |
|
} |
251 |
5420 |
} |
252 |
|
|
253 |
|
template <class T> |
254 |
3058 |
void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
255 |
3058 |
Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; |
256 |
|
|
257 |
3058 |
Assert(node.getKind() == kind::BITVECTOR_AND && bits.size() == 0); |
258 |
|
|
259 |
3058 |
bb->bbTerm(node[0], bits); |
260 |
6116 |
std::vector<T> current; |
261 |
8395 |
for(unsigned j = 1; j < node.getNumChildren(); ++j) { |
262 |
5337 |
bb->bbTerm(node[j], current); |
263 |
16041 |
for (unsigned i = 0; i < utils::getSize(node); ++i) { |
264 |
10704 |
bits[i] = mkAnd(bits[i], current[i]); |
265 |
|
} |
266 |
5337 |
current.clear(); |
267 |
|
} |
268 |
3058 |
Assert(bits.size() == utils::getSize(node)); |
269 |
3058 |
} |
270 |
|
|
271 |
|
template <class T> |
272 |
4148 |
void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
273 |
4148 |
Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; |
274 |
|
|
275 |
4148 |
Assert(node.getKind() == kind::BITVECTOR_OR && bits.size() == 0); |
276 |
|
|
277 |
4148 |
bb->bbTerm(node[0], bits); |
278 |
8296 |
std::vector<T> current; |
279 |
29824 |
for(unsigned j = 1; j < node.getNumChildren(); ++j) { |
280 |
25676 |
bb->bbTerm(node[j], current); |
281 |
53515 |
for (unsigned i = 0; i < utils::getSize(node); ++i) { |
282 |
27839 |
bits[i] = mkOr(bits[i], current[i]); |
283 |
|
} |
284 |
25676 |
current.clear(); |
285 |
|
} |
286 |
4148 |
Assert(bits.size() == utils::getSize(node)); |
287 |
4148 |
} |
288 |
|
|
289 |
|
template <class T> |
290 |
207 |
void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
291 |
207 |
Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; |
292 |
|
|
293 |
207 |
Assert(node.getKind() == kind::BITVECTOR_XOR && bits.size() == 0); |
294 |
|
|
295 |
207 |
bb->bbTerm(node[0], bits); |
296 |
414 |
std::vector<T> current; |
297 |
418 |
for(unsigned j = 1; j < node.getNumChildren(); ++j) { |
298 |
211 |
bb->bbTerm(node[j], current); |
299 |
1444 |
for (unsigned i = 0; i < utils::getSize(node); ++i) { |
300 |
1233 |
bits[i] = mkXor(bits[i], current[i]); |
301 |
|
} |
302 |
211 |
current.clear(); |
303 |
|
} |
304 |
207 |
Assert(bits.size() == utils::getSize(node)); |
305 |
207 |
} |
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 |
4064 |
void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
338 |
4064 |
Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; |
339 |
|
|
340 |
4064 |
Assert(utils::getSize(node) == 1 && bits.size() == 0 |
341 |
|
&& node.getKind() == kind::BITVECTOR_COMP); |
342 |
8128 |
std::vector<T> a, b; |
343 |
4064 |
bb->bbTerm(node[0], a); |
344 |
4064 |
bb->bbTerm(node[1], b); |
345 |
|
|
346 |
8128 |
std::vector<T> bit_eqs; |
347 |
46231 |
for (unsigned i = 0; i < a.size(); ++i) { |
348 |
84334 |
T eq = mkIff(a[i], b[i]); |
349 |
42167 |
bit_eqs.push_back(eq); |
350 |
|
} |
351 |
8128 |
T a_eq_b = mkAnd(bit_eqs); |
352 |
4064 |
bits.push_back(a_eq_b); |
353 |
4064 |
} |
354 |
|
|
355 |
|
template <class T> |
356 |
604 |
void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
357 |
604 |
Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; |
358 |
604 |
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 |
1208 |
std::vector<T> newres; |
381 |
604 |
bb->bbTerm(node[0], res); |
382 |
1226 |
for(unsigned i = 1; i < node.getNumChildren(); ++i) { |
383 |
1244 |
std::vector<T> current; |
384 |
622 |
bb->bbTerm(node[i], current); |
385 |
622 |
newres.clear(); |
386 |
|
// constructs a simple shift and add multiplier building the result |
387 |
|
// in res |
388 |
622 |
shiftAddMultiplier(res, current, newres); |
389 |
622 |
res = newres; |
390 |
|
} |
391 |
604 |
if(Debug.isOn("bitvector-bb")) { |
392 |
|
Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; |
393 |
|
} |
394 |
604 |
} |
395 |
|
|
396 |
|
template <class T> |
397 |
1862 |
void DefaultAddBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) |
398 |
|
{ |
399 |
1862 |
Debug("bitvector-bb") << "theory::bv::DefaultAddBB bitblasting " << node |
400 |
|
<< "\n"; |
401 |
1862 |
Assert(node.getKind() == kind::BITVECTOR_ADD && res.size() == 0); |
402 |
|
|
403 |
1862 |
bb->bbTerm(node[0], res); |
404 |
|
|
405 |
3724 |
std::vector<T> newres; |
406 |
|
|
407 |
3821 |
for(unsigned i = 1; i < node.getNumChildren(); ++i) { |
408 |
3918 |
std::vector<T> current; |
409 |
1959 |
bb->bbTerm(node[i], current); |
410 |
1959 |
newres.clear(); |
411 |
1959 |
rippleCarryAdder(res, current, newres, mkFalse<T>()); |
412 |
1959 |
res = newres; |
413 |
|
} |
414 |
|
|
415 |
1862 |
Assert(res.size() == utils::getSize(node)); |
416 |
1862 |
} |
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 |
870 |
void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
437 |
870 |
Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n"; |
438 |
870 |
Assert(node.getKind() == kind::BITVECTOR_NEG); |
439 |
|
|
440 |
1740 |
std::vector<T> a; |
441 |
870 |
bb->bbTerm(node[0], a); |
442 |
870 |
Assert(utils::getSize(node) == a.size()); |
443 |
|
|
444 |
|
// -a = add(~a, 0, 1). |
445 |
1740 |
std::vector<T> not_a; |
446 |
870 |
negateBits(a, not_a); |
447 |
1740 |
std::vector<T> zero; |
448 |
870 |
makeZero(zero, utils::getSize(node)); |
449 |
|
|
450 |
870 |
rippleCarryAdder(not_a, zero, bits, mkTrue<T>()); |
451 |
870 |
} |
452 |
|
|
453 |
|
template <class T> |
454 |
4041 |
void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T>& q, std::vector<T>& r, unsigned rec_width) { |
455 |
4041 |
Assert(q.size() == 0 && r.size() == 0); |
456 |
|
|
457 |
4041 |
if(rec_width == 0 || isZero(a)) { |
458 |
560 |
makeZero(q, a.size()); |
459 |
560 |
makeZero(r, a.size()); |
460 |
560 |
return; |
461 |
|
} |
462 |
|
|
463 |
6962 |
std::vector<T> q1, r1; |
464 |
6962 |
std::vector<T> a1 = a; |
465 |
3481 |
rshift(a1, 1); |
466 |
|
|
467 |
3481 |
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 |
3481 |
lshift(q1, 1); |
470 |
3481 |
lshift(r1, 1); |
471 |
|
|
472 |
|
|
473 |
6962 |
T is_odd = mkIff(a[0], mkTrue<T>()); |
474 |
6962 |
T one_if_odd = mkIte(is_odd, mkTrue<T>(), mkFalse<T>()); |
475 |
|
|
476 |
6962 |
std::vector<T> zero; |
477 |
3481 |
makeZero(zero, b.size()); |
478 |
|
|
479 |
6962 |
std::vector<T> r1_shift_add; |
480 |
|
// account for a being odd |
481 |
3481 |
rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd); |
482 |
|
// now check if the remainder is greater than b |
483 |
6962 |
std::vector<T> not_b; |
484 |
3481 |
negateBits(b, not_b); |
485 |
6962 |
std::vector<T> r_minus_b; |
486 |
6962 |
T co1; |
487 |
|
// use adder because we need r_minus_b anyway |
488 |
3481 |
co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue<T>()); |
489 |
|
// sign is true if r1 < b |
490 |
6962 |
T sign = mkNot(co1); |
491 |
|
|
492 |
3481 |
q1[0] = mkIte(sign, q1[0], mkTrue<T>()); |
493 |
|
|
494 |
|
// would be nice to have a high level ITE instead of bitwise |
495 |
51204 |
for(unsigned i = 0; i < a.size(); ++i) { |
496 |
47723 |
r1_shift_add[i] = mkIte(sign, r1_shift_add[i], r_minus_b[i]); |
497 |
|
} |
498 |
|
|
499 |
|
// check if a < b |
500 |
|
|
501 |
6962 |
std::vector<T> a_minus_b; |
502 |
6962 |
T co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue<T>()); |
503 |
|
// Node a_lt_b = a_minus_b.back(); |
504 |
6962 |
T a_lt_b = mkNot(co2); |
505 |
|
|
506 |
51204 |
for(unsigned i = 0; i < a.size(); ++i) { |
507 |
95446 |
T qval = mkIte(a_lt_b, mkFalse<T>(), q1[i]); |
508 |
95446 |
T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]); |
509 |
47723 |
q.push_back(qval); |
510 |
47723 |
r.push_back(rval); |
511 |
|
} |
512 |
|
|
513 |
|
} |
514 |
|
|
515 |
|
template <class T> |
516 |
560 |
void UdivUremBB(TNode node, |
517 |
|
std::vector<T>& quot, |
518 |
|
std::vector<T>& rem, |
519 |
|
TBitblaster<T>* bb) |
520 |
|
{ |
521 |
560 |
Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node |
522 |
|
<< "\n"; |
523 |
560 |
Assert(quot.empty()); |
524 |
560 |
Assert(rem.empty()); |
525 |
560 |
Assert(node.getKind() == kind::BITVECTOR_UDIV |
526 |
|
|| node.getKind() == kind::BITVECTOR_UREM); |
527 |
|
|
528 |
1120 |
std::vector<T> a, b; |
529 |
560 |
bb->bbTerm(node[0], a); |
530 |
560 |
bb->bbTerm(node[1], b); |
531 |
|
|
532 |
560 |
uDivModRec(a, b, quot, rem, utils::getSize(node)); |
533 |
|
// adding a special case for division by 0 |
534 |
1120 |
std::vector<T> iszero; |
535 |
4514 |
for (size_t i = 0, size = b.size(); i < size; ++i) |
536 |
|
{ |
537 |
3954 |
iszero.push_back(mkIff(b[i], mkFalse<T>())); |
538 |
|
} |
539 |
1120 |
T b_is_0 = mkAnd(iszero); |
540 |
|
|
541 |
4514 |
for (size_t i = 0, size = quot.size(); i < size; ++i) |
542 |
|
{ |
543 |
3954 |
quot[i] = mkIte(b_is_0, mkTrue<T>(), quot[i]); // a udiv 0 is 11..11 |
544 |
3954 |
rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a |
545 |
|
} |
546 |
560 |
} |
547 |
|
|
548 |
|
template <class T> |
549 |
326 |
void DefaultUdivBB(TNode node, std::vector<T>& quot, TBitblaster<T>* bb) |
550 |
|
{ |
551 |
326 |
Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node |
552 |
|
<< "\n"; |
553 |
326 |
Assert(quot.empty()); |
554 |
326 |
Assert(node.getKind() == kind::BITVECTOR_UDIV); |
555 |
|
|
556 |
652 |
std::vector<T> r; |
557 |
326 |
UdivUremBB(node, quot, r, bb); |
558 |
326 |
} |
559 |
|
|
560 |
|
template <class T> |
561 |
234 |
void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb) |
562 |
|
{ |
563 |
234 |
Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node |
564 |
|
<< "\n"; |
565 |
234 |
Assert(rem.empty()); |
566 |
234 |
Assert(node.getKind() == kind::BITVECTOR_UREM); |
567 |
|
|
568 |
468 |
std::vector<T> q; |
569 |
234 |
UdivUremBB(node, q, rem, bb); |
570 |
234 |
} |
571 |
|
|
572 |
|
template <class T> |
573 |
|
void DefaultSdivBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
574 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
575 |
|
<< node.getKind() << "\n"; |
576 |
|
Unimplemented(); |
577 |
|
} |
578 |
|
template <class T> |
579 |
|
void DefaultSremBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
580 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
581 |
|
<< node.getKind() << "\n"; |
582 |
|
Unimplemented(); |
583 |
|
} |
584 |
|
template <class T> |
585 |
|
void DefaultSmodBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
586 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
587 |
|
<< node.getKind() << "\n"; |
588 |
|
Unimplemented(); |
589 |
|
} |
590 |
|
|
591 |
|
template <class T> |
592 |
416 |
void DefaultShlBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) |
593 |
|
{ |
594 |
416 |
Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node |
595 |
|
<< "\n"; |
596 |
416 |
Assert(node.getKind() == kind::BITVECTOR_SHL && res.size() == 0); |
597 |
832 |
std::vector<T> a, b; |
598 |
416 |
bb->bbTerm(node[0], a); |
599 |
416 |
bb->bbTerm(node[1], b); |
600 |
|
|
601 |
|
// check for b < log2(n) |
602 |
416 |
unsigned size = utils::getSize(node); |
603 |
416 |
unsigned log2_size = std::ceil(log2((double)size)); |
604 |
832 |
Node a_size = utils::mkConst(size, size); |
605 |
|
|
606 |
832 |
std::vector<T> a_size_bits; |
607 |
416 |
DefaultConstBB(a_size, a_size_bits, bb); |
608 |
832 |
T b_ult_a_size = uLessThanBB(b, a_size_bits, false); |
609 |
|
|
610 |
832 |
std::vector<T> prev_res; |
611 |
416 |
res = a; |
612 |
|
// we only need to look at the bits bellow log2_a_size |
613 |
1345 |
for (unsigned s = 0; s < log2_size; ++s) |
614 |
|
{ |
615 |
|
// barrel shift stage: at each stage you can either shift by 2^s bits |
616 |
|
// or leave the previous stage untouched |
617 |
929 |
prev_res = res; |
618 |
929 |
unsigned threshold = pow(2, s); |
619 |
8279 |
for (unsigned i = 0; i < a.size(); ++i) |
620 |
|
{ |
621 |
7350 |
if (i < threshold) |
622 |
|
{ |
623 |
|
// if b[s] is true then we must have shifted by at least 2^b bits so |
624 |
|
// all bits bellow 2^s will be 0, otherwise just use previous shift |
625 |
|
// value |
626 |
2190 |
res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]); |
627 |
|
} |
628 |
|
else |
629 |
|
{ |
630 |
|
// if b[s]= 0, use previous value, otherwise shift by threshold bits |
631 |
5160 |
Assert(i >= threshold); |
632 |
5160 |
res[i] = mkIte(b[s], prev_res[i - threshold], prev_res[i]); |
633 |
|
} |
634 |
|
} |
635 |
|
} |
636 |
416 |
prev_res = res; |
637 |
2818 |
for (unsigned i = 0; i < b.size(); ++i) |
638 |
|
{ |
639 |
|
// this is fine because b_ult_a_size has been bit-blasted |
640 |
2402 |
res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); |
641 |
|
} |
642 |
|
|
643 |
416 |
if (Debug.isOn("bitvector-bb")) |
644 |
|
{ |
645 |
|
Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; |
646 |
|
} |
647 |
416 |
} |
648 |
|
|
649 |
|
template <class T> |
650 |
481 |
void DefaultLshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) |
651 |
|
{ |
652 |
481 |
Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node |
653 |
|
<< "\n"; |
654 |
481 |
Assert(node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0); |
655 |
962 |
std::vector<T> a, b; |
656 |
481 |
bb->bbTerm(node[0], a); |
657 |
481 |
bb->bbTerm(node[1], b); |
658 |
|
|
659 |
|
// check for b < log2(n) |
660 |
481 |
unsigned size = utils::getSize(node); |
661 |
481 |
unsigned log2_size = std::ceil(log2((double)size)); |
662 |
962 |
Node a_size = utils::mkConst(size, size); |
663 |
|
|
664 |
962 |
std::vector<T> a_size_bits; |
665 |
481 |
DefaultConstBB(a_size, a_size_bits, bb); |
666 |
962 |
T b_ult_a_size = uLessThanBB(b, a_size_bits, false); |
667 |
|
|
668 |
481 |
res = a; |
669 |
962 |
std::vector<T> prev_res; |
670 |
|
|
671 |
1736 |
for (unsigned s = 0; s < log2_size; ++s) |
672 |
|
{ |
673 |
|
// barrel shift stage: at each stage you can either shift by 2^s bits |
674 |
|
// or leave the previous stage untouched |
675 |
1255 |
prev_res = res; |
676 |
1255 |
int threshold = pow(2, s); |
677 |
15435 |
for (unsigned i = 0; i < a.size(); ++i) |
678 |
|
{ |
679 |
14180 |
if (i + threshold >= a.size()) |
680 |
|
{ |
681 |
|
// if b[s] is true then we must have shifted by at least 2^b bits so |
682 |
|
// all bits above 2^s will be 0, otherwise just use previous shift value |
683 |
3620 |
res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]); |
684 |
|
} |
685 |
|
else |
686 |
|
{ |
687 |
|
// if b[s]= 0, use previous value, otherwise shift by threshold bits |
688 |
10560 |
Assert(i + threshold < a.size()); |
689 |
10560 |
res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); |
690 |
|
} |
691 |
|
} |
692 |
|
} |
693 |
|
|
694 |
481 |
prev_res = res; |
695 |
4459 |
for (unsigned i = 0; i < b.size(); ++i) |
696 |
|
{ |
697 |
|
// this is fine because b_ult_a_size has been bit-blasted |
698 |
3978 |
res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>()); |
699 |
|
} |
700 |
|
|
701 |
481 |
if (Debug.isOn("bitvector-bb")) |
702 |
|
{ |
703 |
|
Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; |
704 |
|
} |
705 |
481 |
} |
706 |
|
|
707 |
|
template <class T> |
708 |
296 |
void DefaultAshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) |
709 |
|
{ |
710 |
296 |
Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node |
711 |
|
<< "\n"; |
712 |
296 |
Assert(node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0); |
713 |
592 |
std::vector<T> a, b; |
714 |
296 |
bb->bbTerm(node[0], a); |
715 |
296 |
bb->bbTerm(node[1], b); |
716 |
|
|
717 |
|
// check for b < n |
718 |
296 |
unsigned size = utils::getSize(node); |
719 |
296 |
unsigned log2_size = std::ceil(log2((double)size)); |
720 |
592 |
Node a_size = utils::mkConst(size, size); |
721 |
|
|
722 |
592 |
std::vector<T> a_size_bits; |
723 |
296 |
DefaultConstBB(a_size, a_size_bits, bb); |
724 |
592 |
T b_ult_a_size = uLessThanBB(b, a_size_bits, false); |
725 |
|
|
726 |
296 |
res = a; |
727 |
592 |
T sign_bit = a.back(); |
728 |
592 |
std::vector<T> prev_res; |
729 |
|
|
730 |
933 |
for (unsigned s = 0; s < log2_size; ++s) |
731 |
|
{ |
732 |
|
// barrel shift stage: at each stage you can either shift by 2^s bits |
733 |
|
// or leave the previous stage untouched |
734 |
637 |
prev_res = res; |
735 |
637 |
int threshold = pow(2, s); |
736 |
5282 |
for (unsigned i = 0; i < a.size(); ++i) |
737 |
|
{ |
738 |
4645 |
if (i + threshold >= a.size()) |
739 |
|
{ |
740 |
|
// if b[s] is true then we must have shifted by at least 2^b bits so |
741 |
|
// all bits above 2^s will be the sign bit, otherwise just use previous |
742 |
|
// shift value |
743 |
1432 |
res[i] = mkIte(b[s], sign_bit, prev_res[i]); |
744 |
|
} |
745 |
|
else |
746 |
|
{ |
747 |
|
// if b[s]= 0, use previous value, otherwise shift by threshold bits |
748 |
3213 |
Assert(i + threshold < a.size()); |
749 |
3213 |
res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); |
750 |
|
} |
751 |
|
} |
752 |
|
} |
753 |
|
|
754 |
296 |
prev_res = res; |
755 |
1895 |
for (unsigned i = 0; i < b.size(); ++i) |
756 |
|
{ |
757 |
|
// this is fine because b_ult_a_size has been bit-blasted |
758 |
1599 |
res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit); |
759 |
|
} |
760 |
|
|
761 |
296 |
if (Debug.isOn("bitvector-bb")) |
762 |
|
{ |
763 |
|
Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; |
764 |
|
} |
765 |
296 |
} |
766 |
|
|
767 |
|
template <class T> |
768 |
611 |
void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
769 |
611 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
770 |
611 |
Assert(node.getKind() == kind::BITVECTOR_ULTBV); |
771 |
1222 |
std::vector<T> a, b; |
772 |
611 |
bb->bbTerm(node[0], a); |
773 |
611 |
bb->bbTerm(node[1], b); |
774 |
611 |
Assert(a.size() == b.size()); |
775 |
|
|
776 |
|
// construct bitwise comparison |
777 |
611 |
res.push_back(uLessThanBB(a, b, false)); |
778 |
611 |
} |
779 |
|
|
780 |
|
template <class T> |
781 |
929 |
void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
782 |
929 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
783 |
929 |
Assert(node.getKind() == kind::BITVECTOR_SLTBV); |
784 |
1858 |
std::vector<T> a, b; |
785 |
929 |
bb->bbTerm(node[0], a); |
786 |
929 |
bb->bbTerm(node[1], b); |
787 |
929 |
Assert(a.size() == b.size()); |
788 |
|
|
789 |
|
// construct bitwise comparison |
790 |
929 |
res.push_back(sLessThanBB(a, b, false)); |
791 |
929 |
} |
792 |
|
|
793 |
|
template <class T> |
794 |
2766 |
void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
795 |
2766 |
Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; |
796 |
2766 |
Assert(node.getKind() == kind::BITVECTOR_ITE); |
797 |
5532 |
std::vector<T> cond, thenpart, elsepart; |
798 |
2766 |
bb->bbTerm(node[0], cond); |
799 |
2766 |
bb->bbTerm(node[1], thenpart); |
800 |
2766 |
bb->bbTerm(node[2], elsepart); |
801 |
|
|
802 |
2766 |
Assert(cond.size() == 1); |
803 |
2766 |
Assert(thenpart.size() == elsepart.size()); |
804 |
|
|
805 |
38140 |
for (unsigned i = 0; i < thenpart.size(); ++i) { |
806 |
|
// (~cond OR thenpart) AND (cond OR elsepart) |
807 |
35374 |
res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i]))); |
808 |
|
} |
809 |
2766 |
} |
810 |
|
|
811 |
|
template <class T> |
812 |
5301 |
void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
813 |
5301 |
Assert(node.getKind() == kind::BITVECTOR_EXTRACT); |
814 |
5301 |
Assert(bits.size() == 0); |
815 |
|
|
816 |
10602 |
std::vector<T> base_bits; |
817 |
5301 |
bb->bbTerm(node[0], base_bits); |
818 |
5301 |
unsigned high = utils::getExtractHigh(node); |
819 |
5301 |
unsigned low = utils::getExtractLow(node); |
820 |
|
|
821 |
44991 |
for (unsigned i = low; i <= high; ++i) { |
822 |
39690 |
bits.push_back(base_bits[i]); |
823 |
|
} |
824 |
5301 |
Assert(bits.size() == high - low + 1); |
825 |
|
|
826 |
5301 |
if(Debug.isOn("bitvector-bb")) { |
827 |
|
Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; |
828 |
|
Debug("bitvector-bb") << " with bits " << toString(bits); |
829 |
|
} |
830 |
5301 |
} |
831 |
|
|
832 |
|
|
833 |
|
template <class T> |
834 |
|
void DefaultRepeatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
835 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
836 |
|
<< node.getKind() << "\n"; |
837 |
|
// this should be rewritten |
838 |
|
Unimplemented(); |
839 |
|
} |
840 |
|
|
841 |
|
template <class T> |
842 |
|
void DefaultZeroExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) { |
843 |
|
|
844 |
|
Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; |
845 |
|
|
846 |
|
// this should be rewritten |
847 |
|
Unimplemented(); |
848 |
|
|
849 |
|
} |
850 |
|
|
851 |
|
template <class T> |
852 |
1974 |
void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) { |
853 |
1974 |
Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; |
854 |
|
|
855 |
1974 |
Assert(node.getKind() == kind::BITVECTOR_SIGN_EXTEND && res_bits.size() == 0); |
856 |
|
|
857 |
3948 |
std::vector<T> bits; |
858 |
1974 |
bb->bbTerm(node[0], bits); |
859 |
|
|
860 |
3948 |
T sign_bit = bits.back(); |
861 |
1974 |
unsigned amount = |
862 |
3948 |
node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount; |
863 |
|
|
864 |
8161 |
for (unsigned i = 0; i < bits.size(); ++i ) { |
865 |
6187 |
res_bits.push_back(bits[i]); |
866 |
|
} |
867 |
|
|
868 |
11739 |
for (unsigned i = 0 ; i < amount ; ++i ) { |
869 |
9765 |
res_bits.push_back(sign_bit); |
870 |
|
} |
871 |
|
|
872 |
1974 |
Assert(res_bits.size() == amount + bits.size()); |
873 |
1974 |
} |
874 |
|
|
875 |
|
template <class T> |
876 |
|
void DefaultRotateRightBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { |
877 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
878 |
|
<< node.getKind() << "\n"; |
879 |
|
|
880 |
|
Unimplemented(); |
881 |
|
} |
882 |
|
|
883 |
|
template <class T> |
884 |
|
void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { |
885 |
|
Debug("bitvector") << "theory::bv:: Unimplemented kind " |
886 |
|
<< node.getKind() << "\n"; |
887 |
|
Unimplemented(); |
888 |
|
} |
889 |
|
|
890 |
|
|
891 |
|
} |
892 |
|
} |
893 |
|
} // namespace cvc5 |
894 |
|
|
895 |
|
#endif |