1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Yoni Zohar |
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 |
|
* Int-blasting utility |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/bv/int_blaster.h" |
17 |
|
|
18 |
|
#include <cmath> |
19 |
|
#include <sstream> |
20 |
|
#include <string> |
21 |
|
#include <unordered_map> |
22 |
|
#include <vector> |
23 |
|
|
24 |
|
#include "expr/node.h" |
25 |
|
#include "expr/node_traversal.h" |
26 |
|
#include "expr/skolem_manager.h" |
27 |
|
#include "options/option_exception.h" |
28 |
|
#include "options/uf_options.h" |
29 |
|
#include "theory/bv/theory_bv_utils.h" |
30 |
|
#include "theory/rewriter.h" |
31 |
|
#include "util/bitvector.h" |
32 |
|
#include "util/iand.h" |
33 |
|
#include "util/rational.h" |
34 |
|
|
35 |
|
namespace cvc5 { |
36 |
|
using namespace cvc5::theory; |
37 |
|
|
38 |
|
namespace { |
39 |
|
|
40 |
|
// A helper function to compute 2^b as a Rational |
41 |
18 |
Rational intpow2(uint64_t b) { return Rational(Integer(2).pow(b), Integer(1)); } |
42 |
|
|
43 |
|
} // namespace |
44 |
|
|
45 |
8 |
IntBlaster::IntBlaster(context::Context* c, |
46 |
|
options::SolveBVAsIntMode mode, |
47 |
|
uint64_t granularity, |
48 |
8 |
bool introduceFreshIntVars) |
49 |
|
: d_binarizeCache(c), |
50 |
|
d_intblastCache(c), |
51 |
|
d_rangeAssertions(c), |
52 |
|
d_bitwiseAssertions(c), |
53 |
|
d_mode(mode), |
54 |
|
d_granularity(granularity), |
55 |
|
d_context(c), |
56 |
8 |
d_introduceFreshIntVars(introduceFreshIntVars) |
57 |
|
{ |
58 |
8 |
d_nm = NodeManager::currentNM(); |
59 |
8 |
d_zero = d_nm->mkConst<Rational>(0); |
60 |
8 |
d_one = d_nm->mkConst<Rational>(1); |
61 |
8 |
}; |
62 |
|
|
63 |
8 |
void IntBlaster::addRangeConstraint(Node node, |
64 |
|
uint64_t size, |
65 |
|
std::vector<Node>& lemmas) |
66 |
|
{ |
67 |
8 |
} |
68 |
|
|
69 |
|
void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint, |
70 |
|
std::vector<Node>& lemmas) |
71 |
|
{ |
72 |
|
} |
73 |
|
|
74 |
|
Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); } |
75 |
|
|
76 |
2 |
Node IntBlaster::maxInt(uint64_t k) |
77 |
|
{ |
78 |
2 |
Assert(k > 0); |
79 |
4 |
Rational max_value = intpow2(k) - 1; |
80 |
4 |
return d_nm->mkConst<Rational>(max_value); |
81 |
|
} |
82 |
|
|
83 |
12 |
Node IntBlaster::pow2(uint64_t k) |
84 |
|
{ |
85 |
12 |
Assert(k >= 0); |
86 |
12 |
return d_nm->mkConst<Rational>(intpow2(k)); |
87 |
|
} |
88 |
|
|
89 |
4 |
Node IntBlaster::modpow2(Node n, uint64_t exponent) |
90 |
|
{ |
91 |
8 |
Node p2 = d_nm->mkConst<Rational>(intpow2(exponent)); |
92 |
8 |
return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2); |
93 |
|
} |
94 |
|
|
95 |
|
Node IntBlaster::makeBinary(Node n) |
96 |
|
{ |
97 |
|
if (d_binarizeCache.find(n) != d_binarizeCache.end()) |
98 |
|
{ |
99 |
|
return d_binarizeCache[n]; |
100 |
|
} |
101 |
|
uint64_t numChildren = n.getNumChildren(); |
102 |
|
kind::Kind_t k = n.getKind(); |
103 |
|
Node result = n; |
104 |
|
if ((numChildren > 2) |
105 |
|
&& (k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT |
106 |
|
|| k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR |
107 |
|
|| k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT)) |
108 |
|
{ |
109 |
|
result = n[0]; |
110 |
|
for (uint64_t i = 1; i < numChildren; i++) |
111 |
|
{ |
112 |
|
result = d_nm->mkNode(n.getKind(), result, n[i]); |
113 |
|
} |
114 |
|
} |
115 |
|
d_binarizeCache[n] = result; |
116 |
|
Trace("int-blaster-debug") << "binarization result: " << result << std::endl; |
117 |
|
return result; |
118 |
|
} |
119 |
|
|
120 |
|
/** |
121 |
|
* Translate n to Integers via post-order traversal. |
122 |
|
*/ |
123 |
|
Node IntBlaster::intBlast(Node n, |
124 |
|
std::vector<Node>& lemmas, |
125 |
|
std::map<Node, Node>& skolems) |
126 |
|
{ |
127 |
|
// make sure the node is re-written |
128 |
|
n = Rewriter::rewrite(n); |
129 |
|
|
130 |
|
// helper vector for traversal. |
131 |
|
std::vector<Node> toVisit; |
132 |
|
toVisit.push_back(makeBinary(n)); |
133 |
|
|
134 |
|
while (!toVisit.empty()) |
135 |
|
{ |
136 |
|
Node current = toVisit.back(); |
137 |
|
uint64_t currentNumChildren = current.getNumChildren(); |
138 |
|
if (d_intblastCache.find(current) == d_intblastCache.end()) |
139 |
|
{ |
140 |
|
// This is the first time we visit this node and it is not in the cache. |
141 |
|
// We mark this node as visited but not translated by assiging |
142 |
|
// a null node to it. |
143 |
|
d_intblastCache[current] = Node(); |
144 |
|
// all the node's children are added to the stack to be visited |
145 |
|
// before visiting this node again. |
146 |
|
for (const Node& child : current) |
147 |
|
{ |
148 |
|
toVisit.push_back(makeBinary(child)); |
149 |
|
} |
150 |
|
// If this is a UF applicatinon, we also add the function to |
151 |
|
// toVisit. |
152 |
|
if (current.getKind() == kind::APPLY_UF) |
153 |
|
{ |
154 |
|
toVisit.push_back(current.getOperator()); |
155 |
|
} |
156 |
|
} |
157 |
|
else |
158 |
|
{ |
159 |
|
// We already visited and translated this node |
160 |
|
if (!d_intblastCache[current].get().isNull()) |
161 |
|
{ |
162 |
|
// We are done computing the translation for current |
163 |
|
toVisit.pop_back(); |
164 |
|
} |
165 |
|
else |
166 |
|
{ |
167 |
|
// We are now visiting current on the way back up. |
168 |
|
// This is when we do the actual translation. |
169 |
|
Node translation; |
170 |
|
if (currentNumChildren == 0) |
171 |
|
{ |
172 |
|
translation = translateNoChildren(current, lemmas, skolems); |
173 |
|
} |
174 |
|
else |
175 |
|
{ |
176 |
|
/** |
177 |
|
* The current node has children. |
178 |
|
* Since we are on the way back up, |
179 |
|
* these children were already translated. |
180 |
|
* We save their translation for easy access. |
181 |
|
* If the node's kind is APPLY_UF, |
182 |
|
* we also need to include the translated uninterpreted function in |
183 |
|
* this list. |
184 |
|
*/ |
185 |
|
std::vector<Node> translated_children; |
186 |
|
if (current.getKind() == kind::APPLY_UF) |
187 |
|
{ |
188 |
|
translated_children.push_back( |
189 |
|
d_intblastCache[current.getOperator()]); |
190 |
|
} |
191 |
|
for (uint64_t i = 0; i < currentNumChildren; i++) |
192 |
|
{ |
193 |
|
translated_children.push_back(d_intblastCache[current[i]]); |
194 |
|
} |
195 |
|
translation = |
196 |
|
translateWithChildren(current, translated_children, lemmas); |
197 |
|
} |
198 |
|
|
199 |
|
Assert(!translation.isNull()); |
200 |
|
// Map the current node to its translation in the cache. |
201 |
|
d_intblastCache[current] = translation; |
202 |
|
// Also map the translation to itself. |
203 |
|
d_intblastCache[translation] = translation; |
204 |
|
toVisit.pop_back(); |
205 |
|
} |
206 |
|
} |
207 |
|
} |
208 |
|
return d_intblastCache[n].get(); |
209 |
|
} |
210 |
|
|
211 |
|
Node IntBlaster::uts(Node n, uint64_t bw) { return Node(); } |
212 |
|
|
213 |
38 |
Node IntBlaster::translateWithChildren( |
214 |
|
Node original, |
215 |
|
const std::vector<Node>& translated_children, |
216 |
|
std::vector<Node>& lemmas) |
217 |
|
{ |
218 |
|
// The translation of the original node is determined by the kind of |
219 |
|
// the node. |
220 |
38 |
kind::Kind_t oldKind = original.getKind(); |
221 |
|
|
222 |
|
// Some BV operators were eliminated before this point. |
223 |
38 |
Assert(oldKind != kind::BITVECTOR_SDIV); |
224 |
38 |
Assert(oldKind != kind::BITVECTOR_SREM); |
225 |
38 |
Assert(oldKind != kind::BITVECTOR_SMOD); |
226 |
38 |
Assert(oldKind != kind::BITVECTOR_XNOR); |
227 |
38 |
Assert(oldKind != kind::BITVECTOR_NAND); |
228 |
38 |
Assert(oldKind != kind::BITVECTOR_SUB); |
229 |
38 |
Assert(oldKind != kind::BITVECTOR_REPEAT); |
230 |
38 |
Assert(oldKind != kind::BITVECTOR_ROTATE_RIGHT); |
231 |
38 |
Assert(oldKind != kind::BITVECTOR_ROTATE_LEFT); |
232 |
38 |
Assert(oldKind != kind::BITVECTOR_COMP); |
233 |
38 |
Assert(oldKind != kind::BITVECTOR_SGT); |
234 |
38 |
Assert(oldKind != kind::BITVECTOR_SLE); |
235 |
38 |
Assert(oldKind != kind::BITVECTOR_SGE); |
236 |
38 |
Assert(oldKind != kind::EXISTS); |
237 |
|
|
238 |
|
// BV division by zero was eliminated before this point. |
239 |
38 |
Assert(oldKind != kind::BITVECTOR_UDIV |
240 |
|
|| !(original[1].isConst() |
241 |
|
&& original[1].getConst<BitVector>().getValue().isZero())); |
242 |
|
|
243 |
|
// Store the translated node |
244 |
38 |
Node returnNode; |
245 |
|
|
246 |
|
// Translate according to the kind of the original node. |
247 |
38 |
switch (oldKind) |
248 |
|
{ |
249 |
2 |
case kind::BITVECTOR_ADD: |
250 |
|
{ |
251 |
2 |
Assert(original.getNumChildren() == 2); |
252 |
2 |
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
253 |
4 |
returnNode = createBVAddNode( |
254 |
4 |
translated_children[0], translated_children[1], bvsize); |
255 |
2 |
break; |
256 |
|
} |
257 |
2 |
case kind::BITVECTOR_MULT: |
258 |
|
{ |
259 |
2 |
Assert(original.getNumChildren() == 2); |
260 |
2 |
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
261 |
4 |
Node mult = d_nm->mkNode(kind::MULT, translated_children); |
262 |
4 |
Node p2 = pow2(bvsize); |
263 |
2 |
returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2); |
264 |
2 |
break; |
265 |
|
} |
266 |
2 |
case kind::BITVECTOR_UDIV: |
267 |
|
{ |
268 |
|
// we use an ITE for the case where the second operand is 0. |
269 |
2 |
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
270 |
4 |
Node pow2BvSize = pow2(bvsize); |
271 |
|
Node divNode = |
272 |
4 |
d_nm->mkNode(kind::INTS_DIVISION_TOTAL, translated_children); |
273 |
10 |
returnNode = d_nm->mkNode( |
274 |
|
kind::ITE, |
275 |
4 |
d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), |
276 |
4 |
d_nm->mkNode(kind::MINUS, pow2BvSize, d_one), |
277 |
|
divNode); |
278 |
2 |
break; |
279 |
|
} |
280 |
2 |
case kind::BITVECTOR_UREM: |
281 |
|
{ |
282 |
|
// we use an ITE for the case where the second operand is 0. |
283 |
|
Node modNode = |
284 |
4 |
d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children); |
285 |
8 |
returnNode = d_nm->mkNode( |
286 |
|
kind::ITE, |
287 |
4 |
d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), |
288 |
2 |
translated_children[0], |
289 |
|
modNode); |
290 |
2 |
break; |
291 |
|
} |
292 |
2 |
case kind::BITVECTOR_NOT: |
293 |
|
{ |
294 |
2 |
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
295 |
2 |
returnNode = createBVNotNode(translated_children[0], bvsize); |
296 |
2 |
break; |
297 |
|
} |
298 |
2 |
case kind::BITVECTOR_NEG: |
299 |
|
{ |
300 |
2 |
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
301 |
2 |
returnNode = createBVNegNode(translated_children[0], bvsize); |
302 |
2 |
break; |
303 |
|
} |
304 |
2 |
case kind::BITVECTOR_TO_NAT: |
305 |
|
{ |
306 |
|
// In this case, we already translated the child to integer. |
307 |
|
// The result is simply the translated child. |
308 |
2 |
returnNode = translated_children[0]; |
309 |
2 |
break; |
310 |
|
} |
311 |
2 |
case kind::INT_TO_BITVECTOR: |
312 |
|
{ |
313 |
|
// In this case we take the original integer, |
314 |
|
// modulo 2 to the power of the bit-width |
315 |
2 |
returnNode = |
316 |
4 |
modpow2(translated_children[0], |
317 |
4 |
original.getOperator().getConst<IntToBitVector>().d_size); |
318 |
2 |
break; |
319 |
|
} |
320 |
|
case kind::BITVECTOR_OR: |
321 |
|
{ |
322 |
|
Assert(translated_children.size() == 2); |
323 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
324 |
|
returnNode = createBVOrNode( |
325 |
|
translated_children[0], translated_children[1], bvsize, lemmas); |
326 |
|
break; |
327 |
|
} |
328 |
|
case kind::BITVECTOR_XOR: |
329 |
|
{ |
330 |
|
Assert(translated_children.size() == 2); |
331 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
332 |
|
// Based on Hacker's Delight section 2-2 equation n: |
333 |
|
// x xor y = x|y - x&y |
334 |
|
Node bvor = createBVOrNode( |
335 |
|
translated_children[0], translated_children[1], bvsize, lemmas); |
336 |
|
Node bvand = createBVAndNode( |
337 |
|
translated_children[0], translated_children[1], bvsize, lemmas); |
338 |
|
returnNode = createBVSubNode(bvor, bvand, bvsize); |
339 |
|
break; |
340 |
|
} |
341 |
|
case kind::BITVECTOR_AND: |
342 |
|
{ |
343 |
|
Assert(translated_children.size() == 2); |
344 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
345 |
|
returnNode = createBVAndNode( |
346 |
|
translated_children[0], translated_children[1], bvsize, lemmas); |
347 |
|
break; |
348 |
|
} |
349 |
|
case kind::BITVECTOR_SHL: |
350 |
|
{ |
351 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
352 |
|
returnNode = createShiftNode(translated_children, bvsize, true); |
353 |
|
break; |
354 |
|
} |
355 |
|
case kind::BITVECTOR_LSHR: |
356 |
|
{ |
357 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
358 |
|
returnNode = createShiftNode(translated_children, bvsize, false); |
359 |
|
break; |
360 |
|
} |
361 |
|
case kind::BITVECTOR_ASHR: |
362 |
|
{ |
363 |
|
/* From SMT-LIB2: |
364 |
|
* (bvashr s t) abbreviates |
365 |
|
* (ite (= ((_ extract |m-1| |m-1|) s) #b0) |
366 |
|
* (bvlshr s t) |
367 |
|
* (bvnot (bvlshr (bvnot s) t))) |
368 |
|
* |
369 |
|
* Equivalently: |
370 |
|
* (bvashr s t) abbreviates |
371 |
|
* (ite (bvult s 100000...) |
372 |
|
* (bvlshr s t) |
373 |
|
* (bvnot (bvlshr (bvnot s) t))) |
374 |
|
* |
375 |
|
*/ |
376 |
|
// signed_min is 100000... |
377 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
378 |
|
Node signed_min = pow2(bvsize - 1); |
379 |
|
Node condition = |
380 |
|
d_nm->mkNode(kind::LT, translated_children[0], signed_min); |
381 |
|
Node thenNode = createShiftNode(translated_children, bvsize, false); |
382 |
|
std::vector<Node> children = { |
383 |
|
createBVNotNode(translated_children[0], bvsize), |
384 |
|
translated_children[1]}; |
385 |
|
Node elseNode = |
386 |
|
createBVNotNode(createShiftNode(children, bvsize, false), bvsize); |
387 |
|
returnNode = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode); |
388 |
|
break; |
389 |
|
} |
390 |
2 |
case kind::BITVECTOR_ITE: |
391 |
|
{ |
392 |
|
// Lifted to a boolean ite. |
393 |
4 |
Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one); |
394 |
6 |
returnNode = d_nm->mkNode( |
395 |
4 |
kind::ITE, cond, translated_children[1], translated_children[2]); |
396 |
2 |
break; |
397 |
|
} |
398 |
2 |
case kind::BITVECTOR_ZERO_EXTEND: |
399 |
|
{ |
400 |
|
// zero extension does not change the integer translation. |
401 |
2 |
returnNode = translated_children[0]; |
402 |
2 |
break; |
403 |
|
} |
404 |
|
case kind::BITVECTOR_SIGN_EXTEND: |
405 |
|
{ |
406 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
407 |
|
returnNode = |
408 |
|
createSignExtendNode(translated_children[0], |
409 |
|
bvsize, |
410 |
|
bv::utils::getSignExtendAmount(original)); |
411 |
|
break; |
412 |
|
} |
413 |
2 |
case kind::BITVECTOR_CONCAT: |
414 |
|
{ |
415 |
|
// (concat a b) translates to a*2^k+b, k being the bitwidth of b. |
416 |
2 |
uint64_t bvsizeRight = original[1].getType().getBitVectorSize(); |
417 |
4 |
Node pow2BvSizeRight = pow2(bvsizeRight); |
418 |
|
Node a = |
419 |
4 |
d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight); |
420 |
4 |
Node b = translated_children[1]; |
421 |
2 |
returnNode = d_nm->mkNode(kind::PLUS, a, b); |
422 |
2 |
break; |
423 |
|
} |
424 |
2 |
case kind::BITVECTOR_EXTRACT: |
425 |
|
{ |
426 |
|
// ((_ extract i j) a) is a / 2^j mod 2^{i-j+1} |
427 |
|
// original = a[i:j] |
428 |
2 |
uint64_t i = bv::utils::getExtractHigh(original); |
429 |
2 |
uint64_t j = bv::utils::getExtractLow(original); |
430 |
2 |
Assert(i >= j); |
431 |
2 |
Node div = d_nm->mkNode( |
432 |
4 |
kind::INTS_DIVISION_TOTAL, translated_children[0], pow2(j)); |
433 |
2 |
returnNode = modpow2(div, i - j + 1); |
434 |
2 |
break; |
435 |
|
} |
436 |
2 |
case kind::EQUAL: |
437 |
|
{ |
438 |
2 |
returnNode = d_nm->mkNode(kind::EQUAL, translated_children); |
439 |
2 |
break; |
440 |
|
} |
441 |
2 |
case kind::BITVECTOR_ULT: |
442 |
|
{ |
443 |
2 |
returnNode = d_nm->mkNode(kind::LT, translated_children); |
444 |
2 |
break; |
445 |
|
} |
446 |
|
case kind::BITVECTOR_SLT: |
447 |
|
{ |
448 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
449 |
|
returnNode = d_nm->mkNode(kind::LT, |
450 |
|
uts(translated_children[0], bvsize), |
451 |
|
uts(translated_children[1], bvsize)); |
452 |
|
break; |
453 |
|
} |
454 |
2 |
case kind::BITVECTOR_ULE: |
455 |
|
{ |
456 |
2 |
returnNode = d_nm->mkNode(kind::LEQ, translated_children); |
457 |
2 |
break; |
458 |
|
} |
459 |
2 |
case kind::BITVECTOR_UGT: |
460 |
|
{ |
461 |
2 |
returnNode = d_nm->mkNode(kind::GT, translated_children); |
462 |
2 |
break; |
463 |
|
} |
464 |
2 |
case kind::BITVECTOR_UGE: |
465 |
|
{ |
466 |
2 |
returnNode = d_nm->mkNode(kind::GEQ, translated_children); |
467 |
2 |
break; |
468 |
|
} |
469 |
2 |
case kind::BITVECTOR_ULTBV: |
470 |
|
{ |
471 |
6 |
returnNode = d_nm->mkNode(kind::ITE, |
472 |
4 |
d_nm->mkNode(kind::LT, translated_children), |
473 |
|
d_one, |
474 |
|
d_zero); |
475 |
2 |
break; |
476 |
|
} |
477 |
|
case kind::BITVECTOR_SLTBV: |
478 |
|
{ |
479 |
|
uint64_t bvsize = original[0].getType().getBitVectorSize(); |
480 |
|
returnNode = |
481 |
|
d_nm->mkNode(kind::ITE, |
482 |
|
d_nm->mkNode(kind::LT, |
483 |
|
uts(translated_children[0], bvsize), |
484 |
|
uts(translated_children[1], bvsize)), |
485 |
|
d_one, |
486 |
|
d_zero); |
487 |
|
break; |
488 |
|
} |
489 |
|
case kind::ITE: |
490 |
|
{ |
491 |
|
returnNode = d_nm->mkNode(oldKind, translated_children); |
492 |
|
break; |
493 |
|
} |
494 |
2 |
case kind::APPLY_UF: |
495 |
|
{ |
496 |
|
/** |
497 |
|
* higher order logic allows comparing between functions |
498 |
|
* The translation does not support this, |
499 |
|
* as the translated functions may be different outside |
500 |
|
* of the bounds that were relevant for the original |
501 |
|
* bit-vectors. |
502 |
|
*/ |
503 |
2 |
if (childrenTypesChanged(original) && options::ufHo()) |
504 |
|
{ |
505 |
|
throw OptionException("bv-to-int does not support higher order logic "); |
506 |
|
} |
507 |
|
// Insert the translated application term to the cache |
508 |
2 |
returnNode = d_nm->mkNode(kind::APPLY_UF, translated_children); |
509 |
|
// Add range constraints if necessary. |
510 |
|
// If the original range was a BV sort, the original application of |
511 |
|
// the function must be within the range determined by the |
512 |
|
// bitwidth. |
513 |
2 |
if (original.getType().isBitVector()) |
514 |
|
{ |
515 |
2 |
addRangeConstraint( |
516 |
4 |
returnNode, original.getType().getBitVectorSize(), lemmas); |
517 |
|
} |
518 |
2 |
break; |
519 |
|
} |
520 |
|
case kind::BOUND_VAR_LIST: |
521 |
|
{ |
522 |
|
returnNode = d_nm->mkNode(oldKind, translated_children); |
523 |
|
break; |
524 |
|
} |
525 |
|
case kind::FORALL: |
526 |
|
{ |
527 |
|
returnNode = translateQuantifiedFormula(original); |
528 |
|
break; |
529 |
|
} |
530 |
|
default: |
531 |
|
{ |
532 |
|
// first, verify that we haven't missed |
533 |
|
// any bv operator |
534 |
|
Assert(theory::kindToTheoryId(oldKind) != THEORY_BV); |
535 |
|
|
536 |
|
// In the default case, we have reached an operator that we do not |
537 |
|
// translate directly to integers. The children whose types have |
538 |
|
// changed from bv to int should be adjusted back to bv and then |
539 |
|
// this term is reconstructed. |
540 |
|
TypeNode resultingType; |
541 |
|
if (original.getType().isBitVector()) |
542 |
|
{ |
543 |
|
resultingType = d_nm->integerType(); |
544 |
|
} |
545 |
|
else |
546 |
|
{ |
547 |
|
resultingType = original.getType(); |
548 |
|
} |
549 |
|
Node reconstruction = |
550 |
|
reconstructNode(original, resultingType, translated_children); |
551 |
|
returnNode = reconstruction; |
552 |
|
break; |
553 |
|
} |
554 |
|
} |
555 |
38 |
Trace("int-blaster-debug") << "original: " << original << std::endl; |
556 |
38 |
Trace("int-blaster-debug") << "returnNode: " << returnNode << std::endl; |
557 |
38 |
return returnNode; |
558 |
|
} |
559 |
|
|
560 |
|
Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount) |
561 |
|
{ |
562 |
|
return Node(); |
563 |
|
} |
564 |
|
|
565 |
16 |
Node IntBlaster::translateNoChildren(Node original, |
566 |
|
std::vector<Node>& lemmas, |
567 |
|
std::map<Node, Node>& skolems) |
568 |
|
{ |
569 |
32 |
Trace("int-blaster-debug") |
570 |
32 |
<< "translating leaf: " << original << "; of type: " << original.getType() |
571 |
16 |
<< std::endl; |
572 |
|
|
573 |
|
// The result of the translation |
574 |
16 |
Node translation; |
575 |
|
|
576 |
|
// The translation is done differently for variables (bound or free) and |
577 |
|
// constants (values) |
578 |
16 |
Assert(original.isVar() || original.isConst()); |
579 |
16 |
if (original.isVar()) |
580 |
|
{ |
581 |
12 |
if (original.getType().isBitVector()) |
582 |
|
{ |
583 |
|
// For bit-vector variables, we create fresh integer variables. |
584 |
6 |
if (original.getKind() == kind::BOUND_VARIABLE) |
585 |
|
{ |
586 |
|
// Range constraints for the bound integer variables are not added now. |
587 |
|
// they will be added once the quantifier itself is handled. |
588 |
|
std::stringstream ss; |
589 |
|
ss << original; |
590 |
|
translation = d_nm->mkBoundVar(ss.str() + "_int", d_nm->integerType()); |
591 |
|
} |
592 |
|
else |
593 |
|
{ |
594 |
|
// original is a bit-vector variable (symbolic constant). |
595 |
|
// Either we translate it to a fresh integer variable, |
596 |
|
// or we translate it to (bv2nat original). |
597 |
|
// In the former case, we must include range lemmas, while in the |
598 |
|
// latter we don't. |
599 |
|
// This is determined by the option bv-to-int-fresh-vars. |
600 |
|
// The variables intCast and bvCast are used for models: |
601 |
|
// even if we introduce a fresh variable, |
602 |
|
// it is associated with intCast (which is (bv2nat original)). |
603 |
|
// bvCast is either ( (_ nat2bv k) original) or just original. |
604 |
12 |
Node intCast = castToType(original, d_nm->integerType()); |
605 |
12 |
Node bvCast; |
606 |
6 |
if (d_introduceFreshIntVars) |
607 |
|
{ |
608 |
|
// we introduce a fresh variable, add range constraints, and save the |
609 |
|
// connection between original and the new variable via intCast |
610 |
12 |
translation = d_nm->getSkolemManager()->mkPurifySkolem( |
611 |
|
intCast, |
612 |
|
"__intblast__var", |
613 |
12 |
"Variable introduced in intblasting for " + original.toString()); |
614 |
6 |
uint64_t bvsize = original.getType().getBitVectorSize(); |
615 |
6 |
addRangeConstraint(translation, bvsize, lemmas); |
616 |
|
// put new definition of old variable in skolems |
617 |
6 |
bvCast = castToType(translation, original.getType()); |
618 |
|
} |
619 |
|
else |
620 |
|
{ |
621 |
|
// we just translate original to (bv2nat original) |
622 |
|
translation = intCast; |
623 |
|
// no need to do any casting back to bit-vector in this case. |
624 |
|
bvCast = original; |
625 |
|
} |
626 |
|
|
627 |
|
// add bvCast to skolems if it is not already there. |
628 |
6 |
if (skolems.find(original) == skolems.end()) |
629 |
|
{ |
630 |
6 |
skolems[original] = bvCast; |
631 |
|
} |
632 |
|
else |
633 |
|
{ |
634 |
|
Assert(skolems[original] == bvCast); |
635 |
|
} |
636 |
|
} |
637 |
|
} |
638 |
6 |
else if (original.getType().isFunction()) |
639 |
|
{ |
640 |
|
// translate function symbol |
641 |
4 |
translation = translateFunctionSymbol(original, skolems); |
642 |
|
} |
643 |
|
else |
644 |
|
{ |
645 |
|
// leave other variables intact |
646 |
2 |
translation = original; |
647 |
|
} |
648 |
|
} |
649 |
|
else |
650 |
|
{ |
651 |
|
// original is a constant (value) |
652 |
4 |
if (original.getKind() == kind::CONST_BITVECTOR) |
653 |
|
{ |
654 |
|
// Bit-vector constants are transformed into their integer value. |
655 |
4 |
BitVector constant(original.getConst<BitVector>()); |
656 |
4 |
Integer c = constant.toInteger(); |
657 |
2 |
translation = d_nm->mkConst<Rational>(c); |
658 |
|
} |
659 |
|
else |
660 |
|
{ |
661 |
|
// Other constants stay the same. |
662 |
2 |
translation = original; |
663 |
|
} |
664 |
|
} |
665 |
16 |
return translation; |
666 |
|
} |
667 |
|
|
668 |
4 |
Node IntBlaster::translateFunctionSymbol(Node bvUF, |
669 |
|
std::map<Node, Node>& skolems) |
670 |
|
{ |
671 |
|
// construct the new function symbol. |
672 |
4 |
Node intUF; |
673 |
|
|
674 |
|
// old and new types of domain and result |
675 |
8 |
TypeNode tn = bvUF.getType(); |
676 |
8 |
TypeNode bvRange = tn.getRangeType(); |
677 |
8 |
std::vector<TypeNode> bvDomain = tn.getArgTypes(); |
678 |
8 |
std::vector<TypeNode> intDomain; |
679 |
|
|
680 |
|
// if the original range is a bit-vector sort, |
681 |
|
// the new range should be an integer sort. |
682 |
|
// Otherwise, we keep the original range. |
683 |
|
// Similarly for the domain sorts. |
684 |
8 |
TypeNode intRange = bvRange.isBitVector() ? d_nm->integerType() : bvRange; |
685 |
10 |
for (const TypeNode& d : bvDomain) |
686 |
|
{ |
687 |
6 |
intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d); |
688 |
|
} |
689 |
|
|
690 |
|
// create the new function symbol as a skolem |
691 |
8 |
std::ostringstream os; |
692 |
4 |
os << "__intblast_fun_" << bvUF << "_int"; |
693 |
4 |
SkolemManager* sm = d_nm->getSkolemManager(); |
694 |
12 |
intUF = sm->mkDummySkolem( |
695 |
8 |
os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function"); |
696 |
|
|
697 |
|
// add definition of old function symbol to skolems. |
698 |
|
|
699 |
|
// formal arguments of the lambda expression. |
700 |
8 |
std::vector<Node> args; |
701 |
|
|
702 |
|
// arguments to be passed in the application. |
703 |
8 |
std::vector<Node> achildren; |
704 |
4 |
achildren.push_back(intUF); |
705 |
|
|
706 |
|
// iterate the arguments, cast BV arguments to integers |
707 |
4 |
int i = 0; |
708 |
10 |
for (const TypeNode& d : bvDomain) |
709 |
|
{ |
710 |
|
// Each bit-vector argument is casted to a natural number |
711 |
|
// Other arguments are left intact. |
712 |
12 |
Node fresh_bound_var = d_nm->mkBoundVar(d); |
713 |
6 |
args.push_back(fresh_bound_var); |
714 |
12 |
Node castedArg = args[i]; |
715 |
6 |
if (d.isBitVector()) |
716 |
|
{ |
717 |
4 |
castedArg = castToType(castedArg, d_nm->integerType()); |
718 |
|
} |
719 |
6 |
achildren.push_back(castedArg); |
720 |
6 |
i++; |
721 |
|
} |
722 |
|
|
723 |
|
// create the lambda expression, and add it to skolems |
724 |
8 |
Node app = d_nm->mkNode(kind::APPLY_UF, achildren); |
725 |
8 |
Node body = castToType(app, bvRange); |
726 |
8 |
Node bvlist = d_nm->mkNode(kind::BOUND_VAR_LIST, args); |
727 |
8 |
Node result = d_nm->mkNode(kind::LAMBDA, bvlist, body); |
728 |
4 |
if (skolems.find(bvUF) == skolems.end()) |
729 |
|
{ |
730 |
4 |
skolems[bvUF] = result; |
731 |
|
} |
732 |
8 |
return intUF; |
733 |
|
} |
734 |
|
|
735 |
2 |
bool IntBlaster::childrenTypesChanged(Node n) { return true; } |
736 |
|
|
737 |
20 |
Node IntBlaster::castToType(Node n, TypeNode tn) |
738 |
|
{ |
739 |
|
// If there is no reason to cast, return the |
740 |
|
// original node. |
741 |
20 |
if (n.getType().isSubtypeOf(tn)) |
742 |
|
{ |
743 |
2 |
return n; |
744 |
|
} |
745 |
|
// We only case int to bv or vice verse. |
746 |
18 |
Assert((n.getType().isBitVector() && tn.isInteger()) |
747 |
|
|| (n.getType().isInteger() && tn.isBitVector())); |
748 |
36 |
Trace("int-blaster") << "castToType from " << n.getType() << " to " << tn |
749 |
18 |
<< std::endl; |
750 |
|
|
751 |
|
// casting integers to bit-vectors |
752 |
18 |
if (n.getType().isInteger()) |
753 |
|
{ |
754 |
8 |
Assert(tn.isBitVector()); |
755 |
8 |
unsigned bvsize = tn.getBitVectorSize(); |
756 |
16 |
Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize)); |
757 |
8 |
return d_nm->mkNode(intToBVOp, n); |
758 |
|
} |
759 |
|
|
760 |
|
// casting bit-vectors to ingers |
761 |
10 |
Assert(n.getType().isBitVector()); |
762 |
10 |
Assert(tn.isInteger()); |
763 |
10 |
return d_nm->mkNode(kind::BITVECTOR_TO_NAT, n); |
764 |
|
} |
765 |
|
|
766 |
|
Node IntBlaster::reconstructNode(Node originalNode, |
767 |
|
TypeNode resultType, |
768 |
|
const std::vector<Node>& translated_children) |
769 |
|
{ |
770 |
|
return Node(); |
771 |
|
} |
772 |
|
|
773 |
|
Node IntBlaster::createShiftNode(std::vector<Node> children, |
774 |
|
uint64_t bvsize, |
775 |
|
bool isLeftShift) |
776 |
|
{ |
777 |
|
return Node(); |
778 |
|
} |
779 |
|
|
780 |
|
Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode) |
781 |
|
{ |
782 |
|
return Node(); |
783 |
|
} |
784 |
|
|
785 |
|
Node IntBlaster::createBVAndNode(Node x, |
786 |
|
Node y, |
787 |
|
uint64_t bvsize, |
788 |
|
std::vector<Node>& lemmas) |
789 |
|
{ |
790 |
|
return Node(); |
791 |
|
} |
792 |
|
|
793 |
|
Node IntBlaster::createBVOrNode(Node x, |
794 |
|
Node y, |
795 |
|
uint64_t bvsize, |
796 |
|
std::vector<Node>& lemmas) |
797 |
|
{ |
798 |
|
// Based on Hacker's Delight section 2-2 equation h: |
799 |
|
// x+y = x|y + x&y |
800 |
|
// from which we deduce: |
801 |
|
// x|y = x+y - x&y |
802 |
|
Node plus = createBVAddNode(x, y, bvsize); |
803 |
|
Node bvand = createBVAndNode(x, y, bvsize, lemmas); |
804 |
|
return createBVSubNode(plus, bvand, bvsize); |
805 |
|
} |
806 |
|
|
807 |
|
Node IntBlaster::createBVSubNode(Node x, Node y, uint64_t bvsize) |
808 |
|
{ |
809 |
|
Node minus = d_nm->mkNode(kind::MINUS, x, y); |
810 |
|
Node p2 = pow2(bvsize); |
811 |
|
return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, minus, p2); |
812 |
|
} |
813 |
|
|
814 |
2 |
Node IntBlaster::createBVAddNode(Node x, Node y, uint64_t bvsize) |
815 |
|
{ |
816 |
4 |
Node plus = d_nm->mkNode(kind::PLUS, x, y); |
817 |
4 |
Node p2 = pow2(bvsize); |
818 |
4 |
return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2); |
819 |
|
} |
820 |
|
|
821 |
2 |
Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize) |
822 |
|
{ |
823 |
|
// Based on Hacker's Delight section 2-2 equation a: |
824 |
|
// -x = ~x+1 |
825 |
4 |
Node p2 = pow2(bvsize); |
826 |
4 |
return d_nm->mkNode(kind::MINUS, p2, n); |
827 |
|
} |
828 |
|
|
829 |
2 |
Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) |
830 |
|
{ |
831 |
2 |
return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n); |
832 |
|
} |
833 |
|
|
834 |
22746 |
} // namespace cvc5 |