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