Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Yoni Zohar, Aina Niemetz, Makai Mann
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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_algorithm.h"
26 : : #include "expr/node_traversal.h"
27 : : #include "expr/skolem_manager.h"
28 : : #include "options/option_exception.h"
29 : : #include "options/uf_options.h"
30 : : #include "proof/proof.h"
31 : : #include "theory/bv/theory_bv_utils.h"
32 : : #include "theory/logic_info.h"
33 : : #include "theory/rewriter.h"
34 : : #include "util/bitvector.h"
35 : : #include "util/iand.h"
36 : : #include "util/rational.h"
37 : :
38 : : using namespace cvc5::internal::kind;
39 : : using namespace cvc5::internal::theory;
40 : : using namespace cvc5::internal::theory::bv;
41 : :
42 : : namespace cvc5::internal {
43 : :
44 : : namespace {
45 : :
46 : : // A helper function to compute 2^b as a Rational
47 : 6374 : Rational intpow2(uint32_t b) { return Rational(Integer(2).pow(b), Integer(1)); }
48 : :
49 : : } // namespace
50 : :
51 : 51039 : IntBlaster::IntBlaster(Env& env,
52 : : options::SolveBVAsIntMode mode,
53 : 51039 : uint64_t granularity)
54 : : : EnvObj(env),
55 : 102078 : d_binarizeCache(userContext()),
56 : 102078 : d_intblastCache(userContext()),
57 : 102078 : d_rangeAssertions(userContext()),
58 : 102078 : d_bitwiseAssertions(userContext()),
59 : : d_mode(mode),
60 : 51039 : d_context(userContext())
61 : : {
62 : 51039 : d_nm = nodeManager();
63 : 51039 : d_zero = d_nm->mkConstInt(0);
64 : 51039 : d_one = d_nm->mkConstInt(1);
65 [ - + ][ - + ]: 51039 : Assert(granularity <= 8);
[ - - ]
66 : 51039 : d_granularity = static_cast<uint32_t>(granularity);
67 : 51039 : };
68 : :
69 : 50783 : IntBlaster::~IntBlaster() {}
70 : :
71 : 741 : std::shared_ptr<ProofNode> IntBlaster::getProofFor(Node fact)
72 : : {
73 : : // proofs not yet supported
74 : 1482 : CDProof cdp(d_env);
75 : 741 : cdp.addTrustedStep(fact, TrustId::INT_BLASTER, {}, {});
76 : 1482 : return cdp.getProofFor(fact);
77 : : }
78 : :
79 : 0 : std::string IntBlaster::identify() const { return "IntBlaster"; }
80 : :
81 : 1122 : void IntBlaster::addRangeConstraint(Node node,
82 : : uint32_t size,
83 : : std::vector<TrustNode>& lemmas)
84 : : {
85 : 2244 : Node rangeConstraint = mkRangeConstraint(node, size);
86 [ + - ]: 2244 : Trace("int-blaster-debug")
87 : 1122 : << "range constraint computed: " << rangeConstraint << std::endl;
88 [ + + ]: 1122 : if (d_rangeAssertions.find(rangeConstraint) == d_rangeAssertions.end())
89 : : {
90 [ + - ]: 2240 : Trace("int-blaster-debug")
91 : 1120 : << "range constraint added to cache and lemmas " << std::endl;
92 : 1120 : d_rangeAssertions.insert(rangeConstraint);
93 : 2240 : TrustNode trn = TrustNode::mkTrustLemma(rangeConstraint, this);
94 : 1120 : lemmas.push_back(trn);
95 : : }
96 : 1122 : }
97 : :
98 : 39 : void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint,
99 : : std::vector<TrustNode>& lemmas)
100 : : {
101 [ + + ]: 39 : if (d_bitwiseAssertions.find(bitwiseConstraint) == d_bitwiseAssertions.end())
102 : : {
103 [ + - ]: 66 : Trace("int-blaster-debug")
104 : 0 : << "bitwise constraint added to cache and lemmas: " << bitwiseConstraint
105 : 33 : << std::endl;
106 : 33 : d_bitwiseAssertions.insert(bitwiseConstraint);
107 : 66 : TrustNode trn = TrustNode::mkTrustLemma(bitwiseConstraint, this);
108 : 33 : lemmas.push_back(trn);
109 : : }
110 : 39 : }
111 : :
112 : 1234 : Node IntBlaster::mkRangeConstraint(Node newVar, uint32_t k)
113 : : {
114 : 3702 : Node lower = d_nm->mkNode(Kind::LEQ, d_zero, newVar);
115 : 3702 : Node upper = d_nm->mkNode(Kind::LT, newVar, pow2(k));
116 : 2468 : Node result = d_nm->mkNode(Kind::AND, lower, upper);
117 : 2468 : return rewrite(result);
118 : : }
119 : :
120 : 71 : Node IntBlaster::maxInt(uint32_t k)
121 : : {
122 [ - + ][ - + ]: 71 : Assert(k > 0);
[ - - ]
123 : 213 : Rational max_value = intpow2(k) - 1;
124 : 142 : return d_nm->mkConstInt(max_value);
125 : : }
126 : :
127 : 3089 : Node IntBlaster::pow2(uint32_t k)
128 : : {
129 : : Assert(k >= 0);
130 : 6178 : return d_nm->mkConstInt(intpow2(k));
131 : : }
132 : :
133 : 22 : Node IntBlaster::modpow2(Node n, uint32_t exponent)
134 : : {
135 : 22 : Node p2 = d_nm->mkConstInt(intpow2(exponent));
136 : 44 : return d_nm->mkNode(Kind::INTS_MODULUS_TOTAL, n, p2);
137 : : }
138 : :
139 : 14802 : Node IntBlaster::makeBinary(Node n)
140 : : {
141 [ + + ]: 14802 : if (d_binarizeCache.find(n) != d_binarizeCache.end())
142 : : {
143 : 8636 : return d_binarizeCache[n];
144 : : }
145 : 6166 : uint64_t numChildren = n.getNumChildren();
146 : 6166 : Kind k = n.getKind();
147 : 12332 : Node result = n;
148 [ + + ]: 6166 : if ((numChildren > 2)
149 [ + - ][ + - ]: 97 : && (k == Kind::BITVECTOR_ADD || k == Kind::BITVECTOR_MULT
150 [ + - ][ + - ]: 97 : || k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_OR
151 [ + - ][ + + ]: 97 : || k == Kind::BITVECTOR_XOR || k == Kind::BITVECTOR_CONCAT))
152 : : {
153 : 2 : result = n[0];
154 [ + + ]: 6 : for (uint32_t i = 1; i < numChildren; i++)
155 : : {
156 : 4 : result = d_nm->mkNode(n.getKind(), result, n[i]);
157 : : }
158 : : }
159 : 6166 : d_binarizeCache[n] = result;
160 [ + - ]: 6166 : Trace("int-blaster-debug") << "binarization result: " << result << std::endl;
161 : 6166 : return result;
162 : : }
163 : :
164 : : /**
165 : : * Translate n to Integers via post-order traversal.
166 : : */
167 : 1734 : TrustNode IntBlaster::trustedIntBlast(Node n,
168 : : std::vector<TrustNode>& lemmas,
169 : : std::map<Node, Node>& skolems)
170 : : {
171 : : // make sure the node is re-written
172 [ + - ]: 1734 : Trace("int-blaster-debug") << "n before rewriting: " << n << std::endl;
173 [ - + ][ - + ]: 1734 : Assert(n == rewrite(n));
[ - - ]
174 [ + - ]: 1734 : Trace("int-blaster-debug") << "n after rewriting: " << n << std::endl;
175 : :
176 : : // helper vector for traversal.
177 : 3468 : std::vector<Node> toVisit;
178 : 1734 : toVisit.push_back(makeBinary(n));
179 : :
180 [ + + ]: 16341 : while (!toVisit.empty())
181 : : {
182 : 29218 : Node current = toVisit.back();
183 [ + - ]: 14609 : Trace("int-blaster-debug") << "current: " << current << std::endl;
184 : 14609 : uint64_t currentNumChildren = current.getNumChildren();
185 [ + + ]: 14609 : if (d_intblastCache.find(current) == d_intblastCache.end())
186 : : {
187 : : // This is the first time we visit this node and it is not in the cache.
188 : : // We mark this node as visited but not translated by assiging
189 : : // a null node to it.
190 : 6206 : d_intblastCache[current] = Node();
191 : : // all the node's children are added to the stack to be visited
192 : : // before visiting this node again.
193 [ + + ]: 12742 : for (const Node& child : current)
194 : : {
195 : 6536 : toVisit.push_back(makeBinary(child));
196 : : }
197 : : // If this is a UF applicatinon, we also add the function to
198 : : // toVisit.
199 [ + + ]: 6206 : if (current.getKind() == Kind::APPLY_UF)
200 : : {
201 : 135 : toVisit.push_back(current.getOperator());
202 : : }
203 : : }
204 : : else
205 : : {
206 : : // We already visited and translated this node
207 [ + + ]: 8403 : if (!d_intblastCache[current].get().isNull())
208 : : {
209 : : // We are done computing the translation for current
210 : 2199 : toVisit.pop_back();
211 : : }
212 : : else
213 : : {
214 : : // We are now visiting current on the way back up.
215 : : // This is when we do the actual translation.
216 : 12408 : Node translation;
217 [ + + ]: 6204 : if (currentNumChildren == 0)
218 : : {
219 : 2557 : translation = translateNoChildren(current, lemmas, skolems);
220 : : }
221 : : else
222 : : {
223 : : /**
224 : : * The current node has children.
225 : : * Since we are on the way back up,
226 : : * these children were already translated.
227 : : * We save their translation for easy access.
228 : : * If the node's kind is APPLY_UF,
229 : : * we also need to include the translated uninterpreted function in
230 : : * this list.
231 : : */
232 : 3649 : std::vector<Node> translated_children;
233 [ + + ]: 3647 : if (current.getKind() == Kind::APPLY_UF)
234 : : {
235 [ - + ][ - + ]: 135 : Assert(d_intblastCache.find(current.getOperator())
[ - - ]
236 : : != d_intblastCache.end());
237 : 135 : translated_children.push_back(
238 : 270 : d_intblastCache[current.getOperator()]);
239 : : }
240 [ + + ]: 10179 : for (const Node& cc : current)
241 : : {
242 : 6532 : Node ccb = makeBinary(cc);
243 [ - + ][ - + ]: 6532 : Assert(d_intblastCache.find(ccb) != d_intblastCache.end());
[ - - ]
244 : 6532 : translated_children.push_back(d_intblastCache[ccb]);
245 : : }
246 : : translation =
247 : 3649 : translateWithChildren(current, translated_children, lemmas);
248 : : }
249 [ - + ][ - + ]: 6202 : Assert(!translation.isNull());
[ - - ]
250 : : // Map the current node to its translation in the cache.
251 : 6202 : d_intblastCache[current] = translation;
252 : : // Also map the translation to itself.
253 : 6202 : d_intblastCache[translation] = translation;
254 : 6202 : toVisit.pop_back();
255 : : }
256 : : }
257 : : }
258 [ - + ][ - + ]: 1732 : Assert(d_intblastCache.find(n) != d_intblastCache.end());
[ - - ]
259 : 3464 : Node res = d_intblastCache[n].get();
260 [ + + ]: 1732 : if (res == n)
261 : : {
262 : 733 : return TrustNode::null();
263 : : }
264 : 999 : return TrustNode::mkTrustRewrite(n, res, this);
265 : : }
266 : :
267 : 0 : Node IntBlaster::intBlast(Node n,
268 : : std::vector<Node>& lemmas,
269 : : std::map<Node, Node>& skolems)
270 : : {
271 : 0 : std::vector<TrustNode> tlemmas;
272 : 0 : TrustNode tr = trustedIntBlast(n, tlemmas, skolems);
273 [ - - ]: 0 : for (TrustNode& tlem : tlemmas)
274 : : {
275 : 0 : lemmas.emplace_back(tlem.getProven());
276 : : }
277 [ - - ]: 0 : if (tr.isNull())
278 : : {
279 : 0 : return n;
280 : : }
281 : 0 : Assert(tr.getKind() == TrustNodeKind::REWRITE);
282 : 0 : Assert(tr.getProven()[0] == n);
283 : 0 : return tr.getProven()[1];
284 : : }
285 : :
286 : 3672 : Node IntBlaster::translateWithChildren(
287 : : Node original,
288 : : const std::vector<Node>& translated_children,
289 : : std::vector<TrustNode>& lemmas)
290 : : {
291 : : // The translation of the original node is determined by the kind of
292 : : // the node.
293 : 3672 : Kind oldKind = original.getKind();
294 : : // Some BV operators were eliminated before this point.
295 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_SDIV);
[ - - ]
296 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_SREM);
[ - - ]
297 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_SMOD);
[ - - ]
298 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_XNOR);
[ - - ]
299 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_NOR);
[ - - ]
300 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_NAND);
[ - - ]
301 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_SUB);
[ - - ]
302 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_REPEAT);
[ - - ]
303 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_ROTATE_RIGHT);
[ - - ]
304 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_ROTATE_LEFT);
[ - - ]
305 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_SGT);
[ - - ]
306 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_SLE);
[ - - ]
307 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::BITVECTOR_SGE);
[ - - ]
308 [ - + ][ - + ]: 3672 : Assert(oldKind != Kind::EXISTS);
[ - - ]
309 : : // BV division by zero was eliminated before this point.
310 : 3672 : Assert(oldKind != Kind::BITVECTOR_UDIV
311 : : || !(original[1].isConst()
312 : : && original[1].getConst<BitVector>().getValue().isZero()));
313 : :
314 : : // Store the translated node
315 : 3672 : Node returnNode;
316 : :
317 : : /**
318 : : * higher order logic allows comparing between functions
319 : : * The translation does not support this,
320 : : * as the translated functions may be different outside
321 : : * of the bounds that were relevant for the original
322 : : * bit-vectors.
323 : : */
324 [ + + ][ + + ]: 3672 : if (childrenTypesChanged(original) && logicInfo().isHigherOrder())
[ + - ][ + + ]
[ - - ]
325 : : {
326 : 1 : throw OptionException("bv-to-int does not support higher order logic ");
327 : : }
328 : : // Translate according to the kind of the original node.
329 [ + + ][ + + ]: 3671 : switch (oldKind)
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + ]
330 : : {
331 : 136 : case Kind::BITVECTOR_ADD:
332 : : {
333 [ - + ][ - + ]: 136 : Assert(original.getNumChildren() == 2);
[ - - ]
334 : 136 : uint32_t bvsize = original[0].getType().getBitVectorSize();
335 : 408 : returnNode = createBVAddNode(
336 : 408 : translated_children[0], translated_children[1], bvsize);
337 : 136 : break;
338 : : }
339 : 69 : case Kind::BITVECTOR_MULT:
340 : : {
341 [ - + ][ - + ]: 69 : Assert(original.getNumChildren() == 2);
[ - - ]
342 : 69 : uint32_t bvsize = original[0].getType().getBitVectorSize();
343 : 138 : Node mult = d_nm->mkNode(Kind::MULT, translated_children);
344 : 138 : Node p2 = pow2(bvsize);
345 : 69 : returnNode = d_nm->mkNode(Kind::INTS_MODULUS_TOTAL, mult, p2);
346 : 69 : break;
347 : : }
348 : 21 : case Kind::BITVECTOR_UDIV:
349 : : {
350 : : // we use an ITE for the case where the second operand is 0.
351 : 21 : uint32_t bvsize = original[0].getType().getBitVectorSize();
352 : 42 : Node pow2BvSize = pow2(bvsize);
353 : : Node divNode =
354 : 42 : d_nm->mkNode(Kind::INTS_DIVISION_TOTAL, translated_children);
355 : 84 : returnNode = d_nm->mkNode(
356 : : Kind::ITE,
357 : 42 : d_nm->mkNode(Kind::EQUAL, translated_children[1], d_zero),
358 : 42 : d_nm->mkNode(Kind::SUB, pow2BvSize, d_one),
359 : 21 : divNode);
360 : 21 : break;
361 : : }
362 : 1 : case Kind::BITVECTOR_UREM:
363 : : {
364 : : // we use an ITE for the case where the second operand is 0.
365 : : Node modNode =
366 : 2 : d_nm->mkNode(Kind::INTS_MODULUS_TOTAL, translated_children);
367 : 5 : returnNode = d_nm->mkNode(
368 : : Kind::ITE,
369 : 2 : d_nm->mkNode(Kind::EQUAL, translated_children[1], d_zero),
370 : 1 : translated_children[0],
371 : 1 : modNode);
372 : 1 : break;
373 : : }
374 : 3 : case Kind::BITVECTOR_NOT:
375 : : {
376 : 3 : uint32_t bvsize = original[0].getType().getBitVectorSize();
377 : 3 : returnNode = createBVNotNode(translated_children[0], bvsize);
378 : 3 : break;
379 : : }
380 : 21 : case Kind::BITVECTOR_NEG:
381 : : {
382 : 21 : uint32_t bvsize = original[0].getType().getBitVectorSize();
383 : 21 : returnNode = createBVNegNode(translated_children[0], bvsize);
384 : 21 : break;
385 : : }
386 : 103 : case Kind::BITVECTOR_TO_NAT:
387 : : {
388 : : // In this case, we already translated the child to integer.
389 : : // The result is simply the translated child.
390 : 103 : returnNode = translated_children[0];
391 : 103 : break;
392 : : }
393 : 3 : case Kind::INT_TO_BITVECTOR:
394 : : {
395 : : // In this case we take the original integer,
396 : : // modulo 2 to the power of the bit-width
397 : : returnNode =
398 : 6 : modpow2(translated_children[0],
399 : 9 : original.getOperator().getConst<IntToBitVector>().d_size);
400 : 3 : break;
401 : : }
402 : 15 : case Kind::BITVECTOR_OR:
403 : : {
404 [ - + ][ - + ]: 15 : Assert(translated_children.size() == 2);
[ - - ]
405 : 15 : uint32_t bvsize = original[0].getType().getBitVectorSize();
406 : 45 : returnNode = createBVOrNode(
407 : 45 : translated_children[0], translated_children[1], bvsize, lemmas);
408 : 15 : break;
409 : : }
410 : 0 : case Kind::BITVECTOR_XOR:
411 : : {
412 : 0 : Assert(translated_children.size() == 2);
413 : 0 : uint32_t bvsize = original[0].getType().getBitVectorSize();
414 : : // Based on Hacker's Delight section 2-2 equation n:
415 : : // x xor y = x|y - x&y
416 : : Node bvor = createBVOrNode(
417 : 0 : translated_children[0], translated_children[1], bvsize, lemmas);
418 : : Node bvand = createBVAndNode(
419 : 0 : translated_children[0], translated_children[1], bvsize, lemmas);
420 : 0 : returnNode = createBVSubNode(bvor, bvand, bvsize);
421 : 0 : break;
422 : : }
423 : 43 : case Kind::BITVECTOR_AND:
424 : : {
425 [ - + ][ - + ]: 43 : Assert(translated_children.size() == 2);
[ - - ]
426 : 43 : uint32_t bvsize = original[0].getType().getBitVectorSize();
427 : 129 : returnNode = createBVAndNode(
428 : 129 : translated_children[0], translated_children[1], bvsize, lemmas);
429 : 43 : break;
430 : : }
431 : 5 : case Kind::BITVECTOR_SHL:
432 : : {
433 : 5 : uint32_t bvsize = original[0].getType().getBitVectorSize();
434 : 5 : returnNode = createShiftNode(translated_children, bvsize, true);
435 : 5 : break;
436 : : }
437 : 221 : case Kind::BITVECTOR_LSHR:
438 : : {
439 : 221 : uint32_t bvsize = original[0].getType().getBitVectorSize();
440 : 221 : returnNode = createShiftNode(translated_children, bvsize, false);
441 : 221 : break;
442 : : }
443 : 21 : case Kind::BITVECTOR_ASHR:
444 : : {
445 : : /* From SMT-LIB2:
446 : : * (bvashr s t) abbreviates
447 : : * (ite (= ((_ extract |m-1| |m-1|) s) #b0)
448 : : * (bvlshr s t)
449 : : * (bvnot (bvlshr (bvnot s) t)))
450 : : *
451 : : * Equivalently:
452 : : * (bvashr s t) abbreviates
453 : : * (ite (bvult s 100000...)
454 : : * (bvlshr s t)
455 : : * (bvnot (bvlshr (bvnot s) t)))
456 : : *
457 : : */
458 : : // signed_min is 100000...
459 : 21 : uint32_t bvsize = original[0].getType().getBitVectorSize();
460 : 42 : Node signed_min = pow2(bvsize - 1);
461 : : Node condition =
462 : 63 : d_nm->mkNode(Kind::LT, translated_children[0], signed_min);
463 : 42 : Node thenNode = createShiftNode(translated_children, bvsize, false);
464 : : std::vector<Node> children = {
465 : 21 : createBVNotNode(translated_children[0], bvsize),
466 : 126 : translated_children[1]};
467 : : Node elseNode =
468 : 63 : createBVNotNode(createShiftNode(children, bvsize, false), bvsize);
469 : 21 : returnNode = d_nm->mkNode(Kind::ITE, condition, thenNode, elseNode);
470 : 21 : break;
471 : : }
472 : 1 : case Kind::BITVECTOR_ITE:
473 : : {
474 : : // Lifted to a boolean ite.
475 : 3 : Node cond = d_nm->mkNode(Kind::EQUAL, translated_children[0], d_one);
476 : 3 : returnNode = d_nm->mkNode(
477 : 3 : Kind::ITE, cond, translated_children[1], translated_children[2]);
478 : 1 : break;
479 : : }
480 : 1 : case Kind::BITVECTOR_ZERO_EXTEND:
481 : : {
482 : : // zero extension does not change the integer translation.
483 : 1 : returnNode = translated_children[0];
484 : 1 : break;
485 : : }
486 : 15 : case Kind::BITVECTOR_SIGN_EXTEND:
487 : : {
488 : 15 : uint32_t bvsize = original[0].getType().getBitVectorSize();
489 : : returnNode =
490 : 30 : createSignExtendNode(translated_children[0],
491 : : bvsize,
492 : 15 : bv::utils::getSignExtendAmount(original));
493 : 15 : break;
494 : : }
495 : 65 : case Kind::BITVECTOR_CONCAT:
496 : : {
497 : : // (concat a b) translates to a*2^k+b, k being the bitwidth of b.
498 : 65 : uint32_t bvsizeRight = original[1].getType().getBitVectorSize();
499 : 130 : Node pow2BvSizeRight = pow2(bvsizeRight);
500 : : Node a =
501 : 195 : d_nm->mkNode(Kind::MULT, translated_children[0], pow2BvSizeRight);
502 : 130 : Node b = translated_children[1];
503 : 65 : returnNode = d_nm->mkNode(Kind::ADD, a, b);
504 : 65 : break;
505 : : }
506 : 19 : case Kind::BITVECTOR_EXTRACT:
507 : : {
508 : : // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1}
509 : : // original = a[i:j]
510 : 19 : uint32_t i = bv::utils::getExtractHigh(original);
511 : 19 : uint32_t j = bv::utils::getExtractLow(original);
512 [ - + ][ - + ]: 19 : Assert(i >= j);
[ - - ]
513 : : Node div = d_nm->mkNode(
514 : 57 : Kind::INTS_DIVISION_TOTAL, translated_children[0], pow2(j));
515 : 19 : returnNode = modpow2(div, i - j + 1);
516 : 19 : break;
517 : : }
518 : 950 : case Kind::EQUAL:
519 : : {
520 : 950 : returnNode = d_nm->mkNode(Kind::EQUAL, translated_children);
521 : 950 : break;
522 : : }
523 : 229 : case Kind::BITVECTOR_ULT:
524 : : {
525 : 229 : returnNode = d_nm->mkNode(Kind::LT, translated_children);
526 : 229 : break;
527 : : }
528 : 72 : case Kind::BITVECTOR_SLT:
529 : : {
530 : 72 : uint32_t bvsize = original[0].getType().getBitVectorSize();
531 : 216 : returnNode = d_nm->mkNode(Kind::LT,
532 : 144 : uts(translated_children[0], bvsize),
533 : 216 : uts(translated_children[1], bvsize));
534 : 72 : break;
535 : : }
536 : 1 : case Kind::BITVECTOR_ULE:
537 : : {
538 : 1 : returnNode = d_nm->mkNode(Kind::LEQ, translated_children);
539 : 1 : break;
540 : : }
541 : 1 : case Kind::BITVECTOR_UGT:
542 : : {
543 : 1 : returnNode = d_nm->mkNode(Kind::GT, translated_children);
544 : 1 : break;
545 : : }
546 : 1 : case Kind::BITVECTOR_UGE:
547 : : {
548 : 1 : returnNode = d_nm->mkNode(Kind::GEQ, translated_children);
549 : 1 : break;
550 : : }
551 : 2 : case Kind::BITVECTOR_ULTBV:
552 : : {
553 : 6 : returnNode = d_nm->mkNode(Kind::ITE,
554 : 4 : d_nm->mkNode(Kind::LT, translated_children),
555 : 2 : d_one,
556 : 4 : d_zero);
557 : 2 : break;
558 : : }
559 : 1 : case Kind::BITVECTOR_SLTBV:
560 : : {
561 : 1 : uint32_t bvsize = original[0].getType().getBitVectorSize();
562 : : returnNode =
563 : 3 : d_nm->mkNode(Kind::ITE,
564 : 3 : d_nm->mkNode(Kind::LT,
565 : 2 : uts(translated_children[0], bvsize),
566 : 2 : uts(translated_children[1], bvsize)),
567 : 1 : d_one,
568 : 2 : d_zero);
569 : 1 : break;
570 : : }
571 : 8 : case Kind::BITVECTOR_COMP:
572 : : {
573 : 24 : returnNode = d_nm->mkNode(
574 : : Kind::ITE,
575 : 24 : d_nm->mkNode(
576 : 16 : Kind::EQUAL, translated_children[0], translated_children[1]),
577 : 8 : d_one,
578 : 16 : d_zero);
579 : 8 : break;
580 : : }
581 : 10 : case Kind::BITVECTOR_UADDO:
582 : : {
583 : 10 : uint32_t bvsize = original[0].getType().getBitVectorSize();
584 : : Node sum = d_nm->mkNode(
585 : 30 : Kind::ADD, translated_children[0], translated_children[1]);
586 : 10 : returnNode = d_nm->mkNode(Kind::GEQ, sum, pow2(bvsize));
587 : 10 : break;
588 : : }
589 : 10 : case Kind::BITVECTOR_SADDO:
590 : : {
591 : 10 : uint32_t bvsize = original[0].getType().getBitVectorSize();
592 : 20 : Node signed0 = uts(translated_children[0], bvsize);
593 : 20 : Node signed1 = uts(translated_children[1], bvsize);
594 : 30 : Node sum = d_nm->mkNode(Kind::ADD, signed0, signed1);
595 : 30 : Node disj1 = d_nm->mkNode(Kind::GEQ, sum, pow2(bvsize - 1));
596 : : Node disj2 = d_nm->mkNode(
597 : 30 : Kind::LT, sum, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
598 : 10 : returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
599 : 10 : break;
600 : : }
601 : 10 : case Kind::BITVECTOR_UMULO:
602 : : {
603 : 10 : uint32_t bvsize = original[0].getType().getBitVectorSize();
604 : : Node mul = d_nm->mkNode(
605 : 30 : Kind::MULT, translated_children[0], translated_children[1]);
606 : 10 : returnNode = d_nm->mkNode(Kind::GEQ, mul, pow2(bvsize));
607 : 10 : break;
608 : : }
609 : 10 : case Kind::BITVECTOR_SMULO:
610 : : {
611 : 10 : uint32_t bvsize = original[0].getType().getBitVectorSize();
612 : 20 : Node signed0 = uts(translated_children[0], bvsize);
613 : 20 : Node signed1 = uts(translated_children[1], bvsize);
614 : 30 : Node mul = d_nm->mkNode(Kind::MULT, signed0, signed1);
615 : 30 : Node disj1 = d_nm->mkNode(Kind::GEQ, mul, pow2(bvsize - 1));
616 : : Node disj2 = d_nm->mkNode(
617 : 30 : Kind::LT, mul, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
618 : 10 : returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
619 : 10 : break;
620 : : }
621 : 10 : case Kind::BITVECTOR_USUBO:
622 : : {
623 : 30 : returnNode = d_nm->mkNode(
624 : 30 : Kind::LT, translated_children[0], translated_children[1]);
625 : 10 : break;
626 : : }
627 : 10 : case Kind::BITVECTOR_SSUBO:
628 : : {
629 : 10 : uint32_t bvsize = original[0].getType().getBitVectorSize();
630 : 20 : Node signed0 = uts(translated_children[0], bvsize);
631 : 20 : Node signed1 = uts(translated_children[1], bvsize);
632 : 30 : Node sub = d_nm->mkNode(Kind::SUB, signed0, signed1);
633 : 30 : Node disj1 = d_nm->mkNode(Kind::GEQ, sub, pow2(bvsize - 1));
634 : : Node disj2 = d_nm->mkNode(
635 : 30 : Kind::LT, sub, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
636 : 10 : returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
637 : 10 : break;
638 : : }
639 : 24 : case Kind::ITE:
640 : : {
641 : 24 : returnNode = d_nm->mkNode(oldKind, translated_children);
642 : 24 : break;
643 : : }
644 : 135 : case Kind::APPLY_UF:
645 : : {
646 : : // Insert the translated application term to the cache
647 : 135 : returnNode = d_nm->mkNode(Kind::APPLY_UF, translated_children);
648 : : // Add range constraints if necessary.
649 : : // If the original range was a BV sort, the original application of
650 : : // the function must be within the range determined by the
651 : : // bitwidth.
652 : : // function applications that include bound variables
653 : : // are ignored at this stage.
654 : : // Their range constraints are added later under the
655 : : // appropriate quantifier.
656 : 135 : if (original.getType().isBitVector() && !expr::hasBoundVar(original))
657 : : {
658 : 36 : addRangeConstraint(
659 : 72 : returnNode, original.getType().getBitVectorSize(), lemmas);
660 : : }
661 : 135 : break;
662 : : }
663 : 115 : case Kind::BOUND_VAR_LIST:
664 : : {
665 : 115 : returnNode = d_nm->mkNode(oldKind, translated_children);
666 [ + + ]: 115 : if (d_mode == options::SolveBVAsIntMode::BITWISE)
667 : : {
668 : : throw OptionException(
669 : 1 : "--solve-bv-as-int=bitwise does not support quantifiers");
670 : : }
671 : 114 : break;
672 : : }
673 : 128 : case Kind::FORALL:
674 : : {
675 : 128 : returnNode = translateQuantifiedFormula(original);
676 : 128 : break;
677 : : }
678 : 1181 : default:
679 : : {
680 : : // first, verify that we haven't missed
681 : : // any bv operator
682 [ - + ][ - + ]: 1181 : Assert(theory::kindToTheoryId(oldKind) != THEORY_BV);
[ - - ]
683 : :
684 : : // In the default case, we have reached an operator that we do not
685 : : // translate directly to integers. The children whose types have
686 : : // changed from bv to int should be adjusted back to bv and then
687 : : // this term is reconstructed.
688 : 2362 : TypeNode resultingType;
689 [ + + ]: 1181 : if (original.getType().isBitVector())
690 : : {
691 : 10 : resultingType = d_nm->integerType();
692 : : }
693 : : else
694 : : {
695 : 1171 : resultingType = original.getType();
696 : : }
697 : : Node reconstruction =
698 : 3543 : reconstructNode(original, resultingType, translated_children);
699 : 1181 : returnNode = reconstruction;
700 : 1181 : break;
701 : : }
702 : : }
703 [ + - ]: 3670 : Trace("int-blaster-debug") << "original: " << original << std::endl;
704 [ + - ]: 3670 : Trace("int-blaster-debug") << "returnNode: " << returnNode << std::endl;
705 : 3670 : return returnNode;
706 : : }
707 : :
708 : 206 : Node IntBlaster::uts(Node x, uint32_t bvsize)
709 : : {
710 : 412 : Node signedMin = pow2(bvsize - 1);
711 : 618 : Node msbOne = d_nm->mkNode(Kind::LT, x, signedMin);
712 : 618 : Node ite = d_nm->mkNode(Kind::ITE, msbOne, d_zero, pow2(bvsize));
713 : 412 : Node result = d_nm->mkNode(Kind::SUB, x, ite);
714 : 412 : return result;
715 : : }
716 : :
717 : 15 : Node IntBlaster::createSignExtendNode(Node x, uint32_t bvsize, uint32_t amount)
718 : : {
719 : 15 : Node returnNode;
720 [ - + ]: 15 : if (x.isConst())
721 : : {
722 : 0 : Rational c(x.getConst<Rational>());
723 : 0 : Rational twoToKMinusOne(intpow2(bvsize - 1));
724 : : /* if the msb is 0, this is like zero_extend.
725 : : * msb is 0 <-> the value is less than 2^{bvsize-1}
726 : : */
727 : 0 : if (c < twoToKMinusOne || amount == 0)
728 : : {
729 : 0 : returnNode = x;
730 : : }
731 : : else
732 : : {
733 : : /* otherwise, we add the integer equivalent of
734 : : * 11....1 `amount` times
735 : : */
736 : 0 : Rational max_of_amount = intpow2(amount) - 1;
737 : 0 : Rational mul = max_of_amount * intpow2(bvsize);
738 : 0 : Rational sum = mul + c;
739 : 0 : returnNode = d_nm->mkConstInt(sum);
740 : : }
741 : : }
742 : : else
743 : : {
744 [ + + ]: 15 : if (amount == 0)
745 : : {
746 : 10 : returnNode = x;
747 : : }
748 : : else
749 : : {
750 : 10 : Rational twoToKMinusOne(intpow2(bvsize - 1));
751 : 10 : Node minSigned = d_nm->mkConstInt(twoToKMinusOne);
752 : : /* condition checks whether the msb is 1.
753 : : * This holds when the integer value is smaller than
754 : : * 100...0, which is 2^{bvsize-1}.
755 : : */
756 : 15 : Node condition = d_nm->mkNode(Kind::LT, x, minSigned);
757 : 10 : Node thenResult = x;
758 : 10 : Node left = maxInt(amount);
759 : 15 : Node mul = d_nm->mkNode(Kind::MULT, left, pow2(bvsize));
760 : 15 : Node sum = d_nm->mkNode(Kind::ADD, mul, x);
761 : 10 : Node elseResult = sum;
762 : 15 : Node ite = d_nm->mkNode(Kind::ITE, condition, thenResult, elseResult);
763 : 5 : returnNode = ite;
764 : : }
765 : : }
766 : 15 : return returnNode;
767 : : }
768 : :
769 : 2566 : Node IntBlaster::translateNoChildren(Node original,
770 : : std::vector<TrustNode>& lemmas,
771 : : std::map<Node, Node>& skolems)
772 : : {
773 [ + - ]: 5132 : Trace("int-blaster-debug")
774 [ - + ][ - - ]: 2566 : << "translating leaf: " << original << "; of type: " << original.getType()
775 : 2566 : << std::endl;
776 : : // The result of the translation
777 : 2566 : Node translation;
778 : :
779 : : // The translation is done differently for variables (bound or free) and
780 : : // constants (values)
781 [ + + ]: 2566 : if (original.isVar())
782 : : {
783 [ + + ]: 1347 : if (original.getType().isBitVector())
784 : : {
785 : : // For bit-vector variables, we create fresh integer variables.
786 [ + + ]: 1182 : if (original.getKind() == Kind::BOUND_VARIABLE)
787 : : {
788 : : // Range constraints for the bound integer variables are not added now.
789 : : // they will be added once the quantifier itself is handled.
790 : 107 : std::stringstream ss;
791 : 107 : ss << original;
792 : : translation =
793 : 107 : NodeManager::mkBoundVar(ss.str() + "_int", d_nm->integerType());
794 : : }
795 : : else
796 : : {
797 : 3225 : Node intCast = castToType(original, d_nm->integerType());
798 : 2150 : Node bvCast;
799 : : // we introduce a fresh variable, add range constraints, and save the
800 : : // connection between original and the new variable via intCast
801 : 1075 : translation = d_nm->getSkolemManager()->mkPurifySkolem(intCast);
802 : 1075 : uint32_t bvsize = original.getType().getBitVectorSize();
803 : 1075 : addRangeConstraint(translation, bvsize, lemmas);
804 : : // put new definition of old variable in skolems
805 : 1075 : bvCast = castToType(translation, original.getType());
806 : :
807 : : // add bvCast to skolems if it is not already there.
808 [ + - ]: 1075 : if (skolems.find(original) == skolems.end())
809 : : {
810 : 1075 : skolems[original] = bvCast;
811 : : }
812 : : else
813 : : {
814 : 0 : Assert(skolems[original] == bvCast);
815 : : }
816 : : }
817 : : }
818 [ + + ]: 165 : else if (original.getType().isFunction())
819 : : {
820 : : // translate function symbol
821 : 84 : translation = translateFunctionSymbol(original, skolems);
822 : : }
823 : : else
824 : : {
825 : : // leave other variables intact
826 : 81 : translation = original;
827 : : }
828 : : }
829 : : else
830 : : {
831 : : // original is a constant (value) or an operator with no arguments (e.g., PI)
832 [ + + ]: 1219 : if (original.getKind() == Kind::CONST_BITVECTOR)
833 : : {
834 : : // Bit-vector constants are transformed into their integer value.
835 : 948 : BitVector constant(original.getConst<BitVector>());
836 : 948 : Integer c = constant.toInteger();
837 : 474 : Rational r = Rational(c, Integer(1));
838 : 474 : translation = d_nm->mkConstInt(r);
839 : : }
840 : : else
841 : : {
842 : : // Other constants or operators stay the same.
843 : 745 : translation = original;
844 : : }
845 : : }
846 : 2566 : return translation;
847 : : }
848 : :
849 : 84 : Node IntBlaster::translateFunctionSymbol(Node bvUF,
850 : : std::map<Node, Node>& skolems)
851 : : {
852 : : // create the new function symbol as a skolem
853 : 84 : SkolemManager* sm = d_nm->getSkolemManager();
854 : 84 : Node intUF = sm->mkSkolemFunction(SkolemId::BV_TO_INT_UF, bvUF);
855 : :
856 : : // formal arguments of the lambda expression.
857 : 168 : std::vector<Node> args;
858 : :
859 : : // arguments to be passed in the application.
860 : 168 : std::vector<Node> achildren;
861 : 84 : achildren.push_back(intUF);
862 : :
863 : : // iterate the arguments, cast BV arguments to integers
864 : 84 : int i = 0;
865 : 168 : TypeNode tn = bvUF.getType();
866 : 168 : TypeNode bvRange = tn.getRangeType();
867 : 168 : std::vector<TypeNode> bvDomain = tn.getArgTypes();
868 [ + + ]: 197 : for (const TypeNode& d : bvDomain)
869 : : {
870 : : // Each bit-vector argument is casted to a natural number
871 : : // Other arguments are left intact.
872 : 226 : Node fresh_bound_var = NodeManager::mkBoundVar(d);
873 : 113 : args.push_back(fresh_bound_var);
874 : 113 : Node castedArg = args[i];
875 [ + + ]: 113 : if (d.isBitVector())
876 : : {
877 : 56 : castedArg = castToType(castedArg, d_nm->integerType());
878 : : }
879 : 113 : achildren.push_back(castedArg);
880 : 113 : i++;
881 : : }
882 : : // create the lambda expression, and add it to skolems
883 : 168 : Node app = d_nm->mkNode(Kind::APPLY_UF, achildren);
884 : 252 : Node body = castToType(app, bvRange);
885 : 168 : Node bvlist = d_nm->mkNode(Kind::BOUND_VAR_LIST, args);
886 : 252 : Node result = d_nm->mkNode(Kind::LAMBDA, bvlist, body);
887 [ + - ]: 84 : if (skolems.find(bvUF) == skolems.end())
888 : : {
889 : 84 : skolems[bvUF] = result;
890 : : }
891 : 168 : return intUF;
892 : : }
893 : :
894 : 3672 : bool IntBlaster::childrenTypesChanged(Node n)
895 : : {
896 : 3672 : bool result = false;
897 [ + + ]: 6531 : for (const Node& child : n)
898 : : {
899 : : // the child's type has changed only if it has been
900 : : // processed already
901 [ + + ]: 4876 : if (d_intblastCache.find(child) != d_intblastCache.end())
902 : : {
903 : 4830 : TypeNode originalType = child.getType();
904 : 4830 : TypeNode newType = d_intblastCache[child].get().getType();
905 [ + + ]: 4830 : if (newType != originalType)
906 : : {
907 : 2017 : result = true;
908 : 2017 : break;
909 : : }
910 : : }
911 : : }
912 : 3672 : return result;
913 : : }
914 : :
915 : 5379 : Node IntBlaster::castToType(Node n, TypeNode tn)
916 : : {
917 : : // If there is no reason to cast, return the
918 : : // original node.
919 [ + + ]: 5379 : if (n.getType() == tn)
920 : : {
921 : 3122 : return n;
922 : : }
923 : : // We only case int to bv or vice verse.
924 : 4514 : Assert((n.getType().isBitVector() && tn.isInteger())
925 : : || (n.getType().isInteger() && tn.isBitVector()));
926 [ + - ][ - + ]: 4514 : Trace("int-blaster") << "castToType from " << n.getType() << " to " << tn
[ - - ]
927 : 2257 : << std::endl;
928 : :
929 : : // casting integers to bit-vectors
930 [ + + ]: 2257 : if (n.getType().isInteger())
931 : : {
932 [ - + ][ - + ]: 1116 : Assert(tn.isBitVector());
[ - - ]
933 : 1116 : unsigned bvsize = tn.getBitVectorSize();
934 : 1116 : Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
935 : 1116 : return d_nm->mkNode(intToBVOp, n);
936 : : }
937 : : // casting bit-vectors to ingers
938 [ - + ][ - + ]: 1141 : Assert(n.getType().isBitVector());
[ - - ]
939 [ - + ][ - + ]: 1141 : Assert(tn.isInteger());
[ - - ]
940 : 1141 : return d_nm->mkNode(Kind::BITVECTOR_TO_NAT, n);
941 : : }
942 : :
943 : 1181 : Node IntBlaster::reconstructNode(Node originalNode,
944 : : TypeNode resultType,
945 : : const std::vector<Node>& translated_children)
946 : : {
947 : : // first, we adjust the children of the node as needed.
948 : : // re-construct the term with the adjusted children.
949 : 1181 : Kind oldKind = originalNode.getKind();
950 : 2362 : NodeBuilder builder(nodeManager(), oldKind);
951 [ + + ]: 1181 : if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
952 : : {
953 : 8 : builder << originalNode.getOperator();
954 : : }
955 [ + + ]: 3089 : for (uint32_t i = 0; i < originalNode.getNumChildren(); i++)
956 : : {
957 : 3816 : Node originalChild = originalNode[i];
958 : 3816 : Node translatedChild = translated_children[i];
959 : 3816 : Node adjustedChild = castToType(translatedChild, originalChild.getType());
960 : 1908 : builder << adjustedChild;
961 : : }
962 : 1181 : Node reconstruction = builder.constructNode();
963 : : // cast to tn in case the reconstruction is a bit-vector.
964 : 1181 : reconstruction = castToType(reconstruction, resultType);
965 : 2362 : return reconstruction;
966 : : }
967 : :
968 : 268 : Node IntBlaster::createShiftNode(std::vector<Node> children,
969 : : uint32_t bvsize,
970 : : bool isLeftShift)
971 : : {
972 : : /**
973 : : * from SMT-LIB:
974 : : * [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]])))
975 : : * [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]])))
976 : : * Since we don't have exponentiation, we use an ite.
977 : : * Important note: below we use INTS_DIVISION_TOTAL, which is safe here
978 : : * because we divide by 2^... which is never 0.
979 : : */
980 : 536 : Node x = children[0];
981 : 536 : Node y = children[1];
982 : : // shifting by const is eliminated by the theory rewriter
983 [ - + ][ - + ]: 268 : Assert(!y.isConst());
[ - - ]
984 : :
985 : : // if we use the internal pow2 operator, the translation does not
986 : : // have any ites
987 [ + + ]: 268 : if (options().smt.bvToIntUsePow2)
988 : : {
989 : 128 : Node pow2Node = d_nm->mkNode(Kind::POW2, y);
990 [ - + ]: 64 : if (isLeftShift)
991 : : {
992 : : return d_nm->mkNode(Kind::INTS_MODULUS_TOTAL,
993 : 0 : d_nm->mkNode(Kind::MULT, x, pow2Node),
994 : 0 : pow2(bvsize));
995 : : }
996 : : else
997 : : {
998 : 64 : return d_nm->mkNode(Kind::INTS_DIVISION_TOTAL, x, pow2Node);
999 : : }
1000 : : }
1001 : :
1002 : : // if we do not use the internal pow2 operator, we use ites.
1003 : 408 : Node ite = d_zero;
1004 : 408 : Node body;
1005 [ + + ]: 1144 : for (uint32_t i = 0; i < bvsize; i++)
1006 : : {
1007 [ + + ]: 940 : if (isLeftShift)
1008 : : {
1009 : 108 : body = d_nm->mkNode(Kind::INTS_MODULUS_TOTAL,
1010 : 72 : d_nm->mkNode(Kind::MULT, x, pow2(i)),
1011 : 108 : pow2(bvsize));
1012 : : }
1013 : : else
1014 : : {
1015 : 904 : body = d_nm->mkNode(Kind::INTS_DIVISION_TOTAL, x, pow2(i));
1016 : : }
1017 : 3760 : ite = d_nm->mkNode(
1018 : : Kind::ITE,
1019 : 1880 : d_nm->mkNode(
1020 : 1880 : Kind::EQUAL, y, d_nm->mkConstInt(Rational(Integer(i), Integer(1)))),
1021 : : body,
1022 : 940 : ite);
1023 : : }
1024 : 204 : return ite;
1025 : : }
1026 : :
1027 : 128 : Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode)
1028 : : {
1029 : 128 : Kind k = quantifiedNode.getKind();
1030 : 256 : Node boundVarList = quantifiedNode[0];
1031 [ - + ][ - + ]: 128 : Assert(boundVarList.getKind() == Kind::BOUND_VAR_LIST);
[ - - ]
1032 : : // Since bit-vector variables are being translated to
1033 : : // integer variables, we need to substitute the new ones
1034 : : // for the old ones.
1035 : 256 : std::vector<Node> oldBoundVars;
1036 : 256 : std::vector<Node> newBoundVars;
1037 : :
1038 : : // range constraints for quantified variables and terms
1039 : 256 : std::vector<Node> rangeConstraints;
1040 : :
1041 : : // collect range constraints for quantified variables
1042 [ + + ]: 256 : for (Node bv : quantifiedNode[0])
1043 : : {
1044 : 128 : oldBoundVars.push_back(bv);
1045 [ + + ]: 128 : if (bv.getType().isBitVector())
1046 : : {
1047 : : // bit-vector variables are replaced by integer ones.
1048 : : // the new variables induce range constraints based on the
1049 : : // original bit-width.
1050 : 106 : Node newBoundVar = d_intblastCache[bv];
1051 : 106 : newBoundVars.push_back(newBoundVar);
1052 : 106 : rangeConstraints.push_back(
1053 : 212 : mkRangeConstraint(newBoundVar, bv.getType().getBitVectorSize()));
1054 : : }
1055 : : else
1056 : : {
1057 : : // variables that are not bit-vectors are not changed
1058 : 22 : newBoundVars.push_back(bv);
1059 : : }
1060 : : }
1061 : :
1062 : : // collect range constraints for UF applciations
1063 : : // that involve quantified variables
1064 : 256 : std::unordered_set<Node> applys;
1065 : 128 : expr::getKindSubterms(quantifiedNode[1], Kind::APPLY_UF, true, applys);
1066 [ + + ]: 170 : for (const Node& apply : applys)
1067 : : {
1068 [ + - ]: 84 : Trace("int-blaster-debug")
1069 : 42 : << "quantified uf application: " << apply << std::endl;
1070 : 84 : Node f = apply.getOperator();
1071 [ + - ]: 42 : Trace("int-blaster-debug") << "quantified uf symbol: " << f << std::endl;
1072 : 84 : TypeNode range = f.getType().getRangeType();
1073 [ + + ]: 42 : if (range.isBitVector())
1074 : : {
1075 : 6 : unsigned bvsize = range.getBitVectorSize();
1076 : 6 : rangeConstraints.push_back(
1077 : 12 : mkRangeConstraint(d_intblastCache[apply], bvsize));
1078 : : }
1079 : : }
1080 : :
1081 : : // the body of the quantifier
1082 : 256 : Node matrix = d_intblastCache[quantifiedNode[1]];
1083 : : // make the substitution
1084 : 256 : matrix = matrix.substitute(oldBoundVars.begin(),
1085 : : oldBoundVars.end(),
1086 : : newBoundVars.begin(),
1087 : 128 : newBoundVars.end());
1088 : : // A node to represent all the range constraints.
1089 : 256 : Node ranges = d_nm->mkAnd(rangeConstraints);
1090 : : // Add the range constraints to the body of the quantifier.
1091 : : // For "exists", this is added conjunctively
1092 : : // For "forall", this is added to the left side of an implication.
1093 [ + - ]: 256 : matrix = d_nm->mkNode(
1094 : 128 : k == Kind::FORALL ? Kind::IMPLIES : Kind::AND, ranges, matrix);
1095 : : // create the new quantified formula and return it.
1096 : 256 : Node newBoundVarsList = d_nm->mkNode(Kind::BOUND_VAR_LIST, newBoundVars);
1097 : 256 : Node result = d_nm->mkNode(Kind::FORALL, newBoundVarsList, matrix);
1098 : 256 : return result;
1099 : : }
1100 : :
1101 : 58 : Node IntBlaster::createBVAndNode(Node x,
1102 : : Node y,
1103 : : uint32_t bvsize,
1104 : : std::vector<TrustNode>& lemmas)
1105 : : {
1106 : : // We support three configurations:
1107 : : // 1. translating to IAND
1108 : : // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV
1109 : : // operators)
1110 : : // 3. translating into a sum
1111 : 58 : Node returnNode;
1112 [ + + ]: 58 : if (d_mode == options::SolveBVAsIntMode::IAND)
1113 : : {
1114 : 23 : Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
1115 : 23 : returnNode = d_nm->mkNode(Kind::IAND, iAndOp, x, y);
1116 : : }
1117 [ + + ]: 35 : else if (d_mode == options::SolveBVAsIntMode::BV)
1118 : : {
1119 : : // translate the children back to BV
1120 : 22 : Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
1121 : 33 : Node bvx = d_nm->mkNode(intToBVOp, x);
1122 : 33 : Node bvy = d_nm->mkNode(intToBVOp, y);
1123 : : // perform bvand on the bit-vectors
1124 : 22 : Node bvand = d_nm->mkNode(Kind::BITVECTOR_AND, bvx, bvy);
1125 : : // translate the result to integers
1126 : 11 : returnNode = d_nm->mkNode(Kind::BITVECTOR_TO_NAT, bvand);
1127 : : }
1128 [ + + ]: 24 : else if (d_mode == options::SolveBVAsIntMode::SUM)
1129 : : {
1130 : : // Construct a sum of ites, based on granularity.
1131 : 13 : returnNode = d_iandUtils.createSumNode(x, y, bvsize, d_granularity);
1132 : : }
1133 : : else
1134 : : {
1135 [ - + ][ - + ]: 11 : Assert(d_mode == options::SolveBVAsIntMode::BITWISE);
[ - - ]
1136 : : // Enforce semantics over individual bits with iextract and ites
1137 : :
1138 : 22 : Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
1139 : 33 : Node iAnd = d_nm->mkNode(Kind::IAND, iAndOp, x, y);
1140 : : // get a skolem so the IAND solver knows not to do work
1141 : 11 : returnNode = d_nm->getSkolemManager()->mkPurifySkolem(iAnd);
1142 : 11 : addRangeConstraint(returnNode, bvsize, lemmas);
1143 : :
1144 : : // eagerly add bitwise lemmas according to the provided granularity
1145 : : uint32_t high_bit;
1146 [ + + ]: 50 : for (uint32_t j = 0; j < bvsize; j += d_granularity)
1147 : : {
1148 : 39 : high_bit = j + d_granularity - 1;
1149 : : // don't let high_bit pass bvsize
1150 [ - + ]: 39 : if (high_bit >= bvsize)
1151 : : {
1152 : 0 : high_bit = bvsize - 1;
1153 : : }
1154 : 39 : Node extractedReturnNode = d_iandUtils.iextract(high_bit, j, returnNode);
1155 : 39 : addBitwiseConstraint(
1156 : 78 : extractedReturnNode.eqNode(
1157 : 78 : d_iandUtils.createBitwiseIAndNode(x, y, high_bit, j)),
1158 : : lemmas);
1159 : : }
1160 : : }
1161 : 58 : return returnNode;
1162 : : }
1163 : :
1164 : 15 : Node IntBlaster::createBVOrNode(Node x,
1165 : : Node y,
1166 : : uint32_t bvsize,
1167 : : std::vector<TrustNode>& lemmas)
1168 : : {
1169 : : // Based on Hacker's Delight section 2-2 equation h:
1170 : : // x+y = x|y + x&y
1171 : : // from which we deduce:
1172 : : // x|y = x+y - x&y
1173 : 45 : Node plus = createBVAddNode(x, y, bvsize);
1174 : 30 : Node bvand = createBVAndNode(x, y, bvsize, lemmas);
1175 : 30 : return createBVSubNode(plus, bvand, bvsize);
1176 : : }
1177 : :
1178 : 15 : Node IntBlaster::createBVSubNode(Node x, Node y, uint32_t bvsize)
1179 : : {
1180 : 45 : Node minus = d_nm->mkNode(Kind::SUB, x, y);
1181 : 15 : Node p2 = pow2(bvsize);
1182 : 30 : return d_nm->mkNode(Kind::INTS_MODULUS_TOTAL, minus, p2);
1183 : : }
1184 : :
1185 : 172 : Node IntBlaster::createBVAddNode(Node x, Node y, uint32_t bvsize)
1186 : : {
1187 : 516 : Node plus = d_nm->mkNode(Kind::ADD, x, y);
1188 : 172 : Node p2 = pow2(bvsize);
1189 : 344 : return d_nm->mkNode(Kind::INTS_MODULUS_TOTAL, plus, p2);
1190 : : }
1191 : :
1192 : 21 : Node IntBlaster::createBVNegNode(Node n, uint32_t bvsize)
1193 : : {
1194 : : // Based on Hacker's Delight section 2-2 equation a:
1195 : : // -x = ~x+1
1196 : 21 : Node bvNotNode = createBVNotNode(n, bvsize);
1197 : 42 : return createBVAddNode(bvNotNode, d_one, bvsize);
1198 : : }
1199 : :
1200 : 66 : Node IntBlaster::createBVNotNode(Node n, uint32_t bvsize)
1201 : : {
1202 : 66 : return d_nm->mkNode(Kind::SUB, maxInt(bvsize), n);
1203 : : }
1204 : :
1205 : : } // namespace cvc5::internal
|
