GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bv_to_int.cpp Lines: 414 467 88.7 %
Date: 2021-03-22 Branches: 837 2037 41.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_to_int.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, Mathias Preiner, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The BVToInt preprocessing pass
13
 **
14
 ** Converts bit-vector operations into integer operations.
15
 **
16
 **/
17
18
#include "preprocessing/passes/bv_to_int.h"
19
20
#include <cmath>
21
#include <sstream>
22
#include <string>
23
#include <unordered_map>
24
#include <vector>
25
26
#include "expr/node.h"
27
#include "expr/node_traversal.h"
28
#include "options/smt_options.h"
29
#include "options/uf_options.h"
30
#include "preprocessing/assertion_pipeline.h"
31
#include "preprocessing/preprocessing_pass_context.h"
32
#include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
33
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
34
#include "theory/rewriter.h"
35
36
namespace CVC4 {
37
namespace preprocessing {
38
namespace passes {
39
40
using namespace std;
41
using namespace CVC4::theory;
42
using namespace CVC4::theory::bv;
43
44
namespace {
45
46
906
Rational intpow2(uint64_t b)
47
{
48
906
  return Rational(Integer(2).pow(b), Integer(1));
49
}
50
51
} //end empty namespace
52
53
292
Node BVToInt::mkRangeConstraint(Node newVar, uint64_t k)
54
{
55
584
  Node lower = d_nm->mkNode(kind::LEQ, d_zero, newVar);
56
584
  Node upper = d_nm->mkNode(kind::LT, newVar, pow2(k));
57
584
  Node result = d_nm->mkNode(kind::AND, lower, upper);
58
584
  return Rewriter::rewrite(result);
59
}
60
61
36
Node BVToInt::maxInt(uint64_t k)
62
{
63
36
  Assert(k > 0);
64
72
  Rational max_value = intpow2(k) - 1;
65
72
  return d_nm->mkConst<Rational>(max_value);
66
}
67
68
864
Node BVToInt::pow2(uint64_t k)
69
{
70
864
  Assert(k >= 0);
71
864
  return d_nm->mkConst<Rational>(intpow2(k));
72
}
73
74
4
Node BVToInt::modpow2(Node n, uint64_t exponent)
75
{
76
8
  Node p2 = d_nm->mkConst<Rational>(intpow2(exponent));
77
8
  return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
78
}
79
80
/**
81
 * Binarizing n via post-order traversal.
82
 */
83
850
Node BVToInt::makeBinary(Node n)
84
{
85
1709
  for (TNode current : NodeDfsIterable(n,
86
                                       VisitOrder::POSTORDER,
87
                                       // skip visited nodes
88
5082
                                       [this](TNode tn) {
89
5082
                                         return d_binarizeCache.find(tn)
90
5082
                                                != d_binarizeCache.end();
91
8491
                                       }))
92
  {
93
1709
    uint64_t numChildren = current.getNumChildren();
94
    /*
95
     * We already visited the sub-dag rooted at the current node,
96
     * and binarized all its children.
97
     * Now we binarize the current node itself.
98
     */
99
1709
    kind::Kind_t k = current.getKind();
100
1709
    if ((numChildren > 2)
101
6
        && (k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
102
6
            || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
103
6
            || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT))
104
    {
105
      // We only binarize bvadd, bvmul, bvand, bvor, bvxor, bvconcat
106
      Assert(d_binarizeCache.find(current[0]) != d_binarizeCache.end());
107
      Node result = d_binarizeCache[current[0]];
108
      for (uint64_t i = 1; i < numChildren; i++)
109
      {
110
        Assert(d_binarizeCache.find(current[i]) != d_binarizeCache.end());
111
        Node child = d_binarizeCache[current[i]];
112
        result = d_nm->mkNode(current.getKind(), result, child);
113
      }
114
      d_binarizeCache[current] = result;
115
    }
116
1709
    else if (numChildren > 0)
117
    {
118
      // current has children, but we do not binarize it
119
2180
      NodeBuilder<> builder(k);
120
1090
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
121
      {
122
115
        builder << current.getOperator();
123
      }
124
2984
      for (Node child : current)
125
      {
126
1894
        builder << d_binarizeCache[child].get();
127
      }
128
1090
      d_binarizeCache[current] = builder.constructNode();
129
    }
130
    else
131
    {
132
      // current has no children
133
619
      d_binarizeCache[current] = current;
134
    }
135
  }
136
850
  return d_binarizeCache[n];
137
}
138
139
/**
140
 * We traverse n and perform rewrites both on the way down and on the way up.
141
 * On the way down we rewrite the node but not it's children.
142
 * On the way up, we update the node's children to the rewritten ones.
143
 * For each sub-node, we perform rewrites to eliminate operators.
144
 * Then, the original children are added to toVisit stack so that we rewrite
145
 * them as well.
146
 */
147
425
Node BVToInt::eliminationPass(Node n)
148
{
149
850
  std::vector<Node> toVisit;
150
425
  toVisit.push_back(n);
151
850
  Node current;
152
7809
  while (!toVisit.empty())
153
  {
154
3692
    current = toVisit.back();
155
    // assert that the node is binarized
156
    // The following variable is only used in assertions
157
3692
    CVC4_UNUSED kind::Kind_t k = current.getKind();
158
3692
    uint64_t numChildren = current.getNumChildren();
159
3692
    Assert((numChildren == 2)
160
           || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
161
                || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
162
                || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT));
163
3692
    toVisit.pop_back();
164
    bool inEliminationCache =
165
3692
        (d_eliminationCache.find(current) != d_eliminationCache.end());
166
    bool inRebuildCache =
167
3692
        (d_rebuildCache.find(current) != d_rebuildCache.end());
168
3692
    if (!inEliminationCache)
169
    {
170
      // current is not the elimination of any previously-visited node
171
      // current hasn't been eliminated yet.
172
      // eliminate operators from it using rewrite rules
173
      Node currentEliminated =
174
          FixpointRewriteStrategy<RewriteRule<UdivZero>,
175
                                  RewriteRule<SdivEliminateFewerBitwiseOps>,
176
                                  RewriteRule<SremEliminateFewerBitwiseOps>,
177
                                  RewriteRule<SmodEliminateFewerBitwiseOps>,
178
                                  RewriteRule<XnorEliminate>,
179
                                  RewriteRule<NandEliminate>,
180
                                  RewriteRule<NorEliminate>,
181
                                  RewriteRule<NegEliminate>,
182
                                  RewriteRule<XorEliminate>,
183
                                  RewriteRule<OrEliminate>,
184
                                  RewriteRule<SubEliminate>,
185
                                  RewriteRule<RepeatEliminate>,
186
                                  RewriteRule<RotateRightEliminate>,
187
                                  RewriteRule<RotateLeftEliminate>,
188
                                  RewriteRule<CompEliminate>,
189
                                  RewriteRule<SleEliminate>,
190
                                  RewriteRule<SltEliminate>,
191
                                  RewriteRule<SgtEliminate>,
192
3162
                                  RewriteRule<SgeEliminate>>::apply(current);
193
194
      // save in the cache
195
1581
      d_eliminationCache[current] = currentEliminated;
196
      // also assign the eliminated now to itself to avoid revisiting.
197
1581
      d_eliminationCache[currentEliminated] = currentEliminated;
198
      // put the eliminated node in the rebuild cache, but mark that it hasn't
199
      // yet been rebuilt by assigning null.
200
1581
      d_rebuildCache[currentEliminated] = Node();
201
      // Push the eliminated node to the stack
202
1581
      toVisit.push_back(currentEliminated);
203
      // Add the children to the stack for future processing.
204
1581
      toVisit.insert(
205
3162
          toVisit.end(), currentEliminated.begin(), currentEliminated.end());
206
    }
207
3692
    if (inRebuildCache)
208
    {
209
      // current was already added to the rebuild cache.
210
2111
      if (d_rebuildCache[current].get().isNull())
211
      {
212
        // current wasn't rebuilt yet.
213
1581
        numChildren = current.getNumChildren();
214
1581
        if (numChildren == 0)
215
        {
216
          // We only eliminate operators that are not nullary.
217
619
          d_rebuildCache[current] = current;
218
        }
219
        else
220
        {
221
          // The main operator is replaced, and the children
222
          // are replaced with their eliminated counterparts.
223
1924
          NodeBuilder<> builder(current.getKind());
224
962
          if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
225
          {
226
99
            builder << current.getOperator();
227
          }
228
2648
          for (Node child : current)
229
          {
230
1686
            Assert(d_eliminationCache.find(child) != d_eliminationCache.end());
231
3372
            Node eliminatedChild = d_eliminationCache[child];
232
1686
            Assert(d_rebuildCache.find(eliminatedChild) != d_eliminationCache.end());
233
1686
            Assert(!d_rebuildCache[eliminatedChild].get().isNull());
234
1686
            builder << d_rebuildCache[eliminatedChild].get();
235
          }
236
962
          d_rebuildCache[current] = builder.constructNode();
237
        }
238
      }
239
    }
240
  }
241
425
  Assert(d_eliminationCache.find(n) != d_eliminationCache.end());
242
850
  Node eliminated = d_eliminationCache[n];
243
425
  Assert(d_rebuildCache.find(eliminated) != d_rebuildCache.end());
244
425
  Assert(!d_rebuildCache[eliminated].get().isNull());
245
850
  return d_rebuildCache[eliminated];
246
}
247
248
/**
249
 * Translate n to Integers via post-order traversal.
250
 */
251
425
Node BVToInt::bvToInt(Node n)
252
{
253
  // make sure the node is re-written before processing it.
254
425
  n = Rewriter::rewrite(n);
255
425
  n = makeBinary(n);
256
425
  n = eliminationPass(n);
257
  // binarize again, in case the elimination pass introduced
258
  // non-binary terms (as can happen by RepeatEliminate, for example).
259
425
  n = makeBinary(n);
260
850
  vector<Node> toVisit;
261
425
  toVisit.push_back(n);
262
263
7921
  while (!toVisit.empty())
264
  {
265
7496
    Node current = toVisit.back();
266
3748
    uint64_t currentNumChildren = current.getNumChildren();
267
3748
    if (d_bvToIntCache.find(current) == d_bvToIntCache.end())
268
    {
269
      // This is the first time we visit this node and it is not in the cache.
270
      // We mark this node as visited but not translated by assiging
271
      // a null node to it.
272
1591
      d_bvToIntCache[current] = Node();
273
      // all the node's children are added to the stack to be visited
274
      // before visiting this node again.
275
1591
      toVisit.insert(toVisit.end(), current.begin(), current.end());
276
      // If this is a UF applicatinon, we also add the function to
277
      // toVisit.
278
1591
      if (current.getKind() == kind::APPLY_UF)
279
      {
280
48
        toVisit.push_back(current.getOperator());
281
      }
282
    }
283
    else
284
    {
285
      // We already visited and translated this node
286
2157
      if (!d_bvToIntCache[current].get().isNull())
287
      {
288
        // We are done computing the translation for current
289
566
        toVisit.pop_back();
290
      }
291
      else
292
      {
293
        // We are now visiting current on the way back up.
294
        // This is when we do the actual translation.
295
3182
        Node translation;
296
1591
        if (currentNumChildren == 0)
297
        {
298
631
          translation = translateNoChildren(current);
299
        }
300
        else
301
        {
302
          /**
303
           * The current node has children.
304
           * Since we are on the way back up,
305
           * these children were already translated.
306
           * We save their translation for easy access.
307
           * If the node's kind is APPLY_UF,
308
           * we also need to include the translated uninterpreted function in
309
           * this list.
310
           */
311
1920
          vector<Node> translated_children;
312
960
          if (current.getKind() == kind::APPLY_UF)
313
          {
314
48
            translated_children.push_back(
315
96
                d_bvToIntCache[current.getOperator()]);
316
          }
317
2644
          for (uint64_t i = 0; i < currentNumChildren; i++)
318
          {
319
1684
            translated_children.push_back(d_bvToIntCache[current[i]]);
320
          }
321
960
          translation = translateWithChildren(current, translated_children);
322
        }
323
        // Map the current node to its translation in the cache.
324
1591
        d_bvToIntCache[current] = translation;
325
        // Also map the translation to itself.
326
1591
        d_bvToIntCache[translation] = translation;
327
1591
        toVisit.pop_back();
328
      }
329
    }
330
  }
331
850
  return d_bvToIntCache[n].get();
332
}
333
334
960
Node BVToInt::translateWithChildren(Node original,
335
                                    const vector<Node>& translated_children)
336
{
337
  // The translation of the original node is determined by the kind of
338
  // the node.
339
960
  kind::Kind_t oldKind = original.getKind();
340
  // ultbv and sltbv were supposed to be eliminated before this point.
341
960
  Assert(oldKind != kind::BITVECTOR_ULTBV);
342
960
  Assert(oldKind != kind::BITVECTOR_SLTBV);
343
  // The following variable will only be used in assertions.
344
960
  CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren();
345
960
  Node returnNode;
346
960
  switch (oldKind)
347
  {
348
142
    case kind::BITVECTOR_PLUS:
349
    {
350
142
      Assert(originalNumChildren == 2);
351
142
      uint64_t bvsize = original[0].getType().getBitVectorSize();
352
284
      Node plus = d_nm->mkNode(kind::PLUS, translated_children);
353
284
      Node p2 = pow2(bvsize);
354
142
      returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2);
355
142
      break;
356
    }
357
6
    case kind::BITVECTOR_MULT:
358
    {
359
6
      Assert(originalNumChildren == 2);
360
6
      uint64_t bvsize = original[0].getType().getBitVectorSize();
361
12
      Node mult = d_nm->mkNode(kind::MULT, translated_children);
362
12
      Node p2 = pow2(bvsize);
363
6
      returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2);
364
6
      break;
365
    }
366
8
    case kind::BITVECTOR_UDIV:
367
    {
368
8
      uint64_t bvsize = original[0].getType().getBitVectorSize();
369
      // we use an ITE for the case where the second operand is 0.
370
16
      Node pow2BvSize = pow2(bvsize);
371
      Node divNode =
372
16
          d_nm->mkNode(kind::INTS_DIVISION_TOTAL, translated_children);
373
40
      returnNode = d_nm->mkNode(
374
          kind::ITE,
375
16
          d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
376
16
          d_nm->mkNode(kind::MINUS, pow2BvSize, d_one),
377
          divNode);
378
8
      break;
379
    }
380
    case kind::BITVECTOR_UREM:
381
    {
382
      // we use an ITE for the case where the second operand is 0.
383
      Node modNode =
384
          d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children);
385
      returnNode = d_nm->mkNode(
386
          kind::ITE,
387
          d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
388
          translated_children[0],
389
          modNode);
390
      break;
391
    }
392
22
    case kind::BITVECTOR_NOT:
393
    {
394
22
      uint64_t bvsize = original[0].getType().getBitVectorSize();
395
      // we use a specified function to generate the node.
396
22
      returnNode = createBVNotNode(translated_children[0], bvsize);
397
22
      break;
398
    }
399
    case kind::BITVECTOR_TO_NAT:
400
    {
401
      // In this case, we already translated the child to integer.
402
      // So the result is the translated child.
403
      returnNode = translated_children[0];
404
      break;
405
    }
406
32
    case kind::BITVECTOR_AND:
407
    {
408
      // We support three configurations:
409
      // 1. translating to IAND
410
      // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV
411
      // operators)
412
      // 3. translating into a sum
413
32
      uint64_t bvsize = original[0].getType().getBitVectorSize();
414
29641
      if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND)
415
      {
416
24
        Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
417
36
        returnNode = d_nm->mkNode(
418
24
            kind::IAND, iAndOp, translated_children[0], translated_children[1]);
419
      }
420
20
      else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV)
421
      {
422
        // translate the children back to BV
423
16
        Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
424
16
        Node x = translated_children[0];
425
16
        Node y = translated_children[1];
426
16
        Node bvx = d_nm->mkNode(intToBVOp, x);
427
16
        Node bvy = d_nm->mkNode(intToBVOp, y);
428
        // perform bvand on the bit-vectors
429
16
        Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy);
430
        // translate the result to integers
431
8
        returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand);
432
      }
433
      else
434
      {
435
12
        Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM);
436
        // Construct a sum of ites, based on granularity.
437
12
        Assert(translated_children.size() == 2);
438
12
        returnNode =
439
48
            d_iandUtils.createSumNode(translated_children[0],
440
12
                                      translated_children[1],
441
                                      bvsize,
442
306
                                      options::BVAndIntegerGranularity());
443
      }
444
32
      break;
445
    }
446
2
    case kind::BITVECTOR_SHL:
447
    {
448
      /**
449
       * a << b is a*2^b.
450
       * The exponentiation is simulated by an ite.
451
       * Only cases where b <= bit width are considered.
452
       * Otherwise, the result is 0.
453
       */
454
2
      uint64_t bvsize = original[0].getType().getBitVectorSize();
455
2
      returnNode = createShiftNode(translated_children, bvsize, true);
456
2
      break;
457
    }
458
66
    case kind::BITVECTOR_LSHR:
459
    {
460
      /**
461
       * a >> b is a div 2^b.
462
       * The exponentiation is simulated by an ite.
463
       * Only cases where b <= bit width are considered.
464
       * Otherwise, the result is 0.
465
       */
466
66
      uint64_t bvsize = original[0].getType().getBitVectorSize();
467
66
      returnNode = createShiftNode(translated_children, bvsize, false);
468
66
      break;
469
    }
470
6
    case kind::BITVECTOR_ASHR:
471
    {
472
      /*  From SMT-LIB2:
473
       *  (bvashr s t) abbreviates
474
       *     (ite (= ((_ extract |m-1| |m-1|) s) #b0)
475
       *          (bvlshr s t)
476
       *          (bvnot (bvlshr (bvnot s) t)))
477
       *
478
       *  Equivalently:
479
       *  (bvashr s t) abbreviates
480
       *      (ite (bvult s 100000...)
481
       *           (bvlshr s t)
482
       *           (bvnot (bvlshr (bvnot s) t)))
483
       *
484
       */
485
6
      uint64_t bvsize = original[0].getType().getBitVectorSize();
486
      // signed_min is 100000...
487
12
      Node signed_min = pow2(bvsize - 1);
488
      Node condition =
489
12
          d_nm->mkNode(kind::LT, translated_children[0], signed_min);
490
12
      Node thenNode = createShiftNode(translated_children, bvsize, false);
491
6
      vector<Node> children = {createBVNotNode(translated_children[0], bvsize),
492
12
                               translated_children[1]};
493
      Node elseNode =
494
12
          createBVNotNode(createShiftNode(children, bvsize, false), bvsize);
495
6
      returnNode = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode);
496
6
      break;
497
    }
498
    case kind::BITVECTOR_ITE:
499
    {
500
      // Lifted to a boolean ite.
501
      Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one);
502
      returnNode = d_nm->mkNode(
503
          kind::ITE, cond, translated_children[1], translated_children[2]);
504
      break;
505
    }
506
    case kind::BITVECTOR_ZERO_EXTEND:
507
    {
508
      returnNode = translated_children[0];
509
      break;
510
    }
511
8
    case kind::BITVECTOR_SIGN_EXTEND:
512
    {
513
8
      uint64_t bvsize = original[0].getType().getBitVectorSize();
514
16
      Node arg = translated_children[0];
515
8
      if (arg.isConst())
516
      {
517
        Rational c(arg.getConst<Rational>());
518
        Rational twoToKMinusOne(intpow2(bvsize - 1));
519
        uint64_t amount = bv::utils::getSignExtendAmount(original);
520
        /* if the msb is 0, this is like zero_extend.
521
         *  msb is 0 <-> the value is less than 2^{bvsize-1}
522
         */
523
        if (c < twoToKMinusOne || amount == 0)
524
        {
525
          returnNode = arg;
526
        }
527
        else
528
        {
529
          /* otherwise, we add the integer equivalent of
530
           * 11....1 `amount` times
531
           */
532
          Rational max_of_amount = intpow2(amount) - 1;
533
          Rational mul = max_of_amount * intpow2(bvsize);
534
          Rational sum = mul + c;
535
          returnNode = d_nm->mkConst(sum);
536
        }
537
      }
538
      else
539
      {
540
8
        uint64_t amount = bv::utils::getSignExtendAmount(original);
541
8
        if (amount == 0)
542
        {
543
6
          returnNode = translated_children[0];
544
        }
545
        else
546
        {
547
4
          Rational twoToKMinusOne(intpow2(bvsize - 1));
548
4
          Node minSigned = d_nm->mkConst(twoToKMinusOne);
549
          /* condition checks whether the msb is 1.
550
           * This holds when the integer value is smaller than
551
           * 100...0, which is 2^{bvsize-1}.
552
           */
553
4
          Node condition = d_nm->mkNode(kind::LT, arg, minSigned);
554
4
          Node thenResult = arg;
555
4
          Node left = maxInt(amount);
556
4
          Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize));
557
4
          Node sum = d_nm->mkNode(kind::PLUS, mul, arg);
558
4
          Node elseResult = sum;
559
4
          Node ite = d_nm->mkNode(kind::ITE, condition, thenResult, elseResult);
560
2
          returnNode = ite;
561
        }
562
      }
563
8
      break;
564
    }
565
8
    case kind::BITVECTOR_CONCAT:
566
    {
567
      // (concat a b) translates to a*2^k+b, k being the bitwidth of b.
568
8
      uint64_t bvsizeRight = original[1].getType().getBitVectorSize();
569
16
      Node pow2BvSizeRight = pow2(bvsizeRight);
570
      Node a =
571
16
          d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight);
572
16
      Node b = translated_children[1];
573
8
      returnNode = d_nm->mkNode(kind::PLUS, a, b);
574
8
      break;
575
    }
576
4
    case kind::BITVECTOR_EXTRACT:
577
    {
578
      // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1}
579
      // original = a[i:j]
580
4
      uint64_t i = bv::utils::getExtractHigh(original);
581
4
      uint64_t j = bv::utils::getExtractLow(original);
582
4
      Assert(i >= j);
583
4
      Node div = d_nm->mkNode(
584
8
          kind::INTS_DIVISION_TOTAL, translated_children[0], pow2(j));
585
4
      returnNode = modpow2(div, i - j + 1);
586
4
      break;
587
    }
588
185
    case kind::EQUAL:
589
    {
590
185
      returnNode = d_nm->mkNode(kind::EQUAL, translated_children);
591
185
      break;
592
    }
593
107
    case kind::BITVECTOR_ULT:
594
    {
595
107
      returnNode = d_nm->mkNode(kind::LT, translated_children);
596
107
      break;
597
    }
598
    case kind::BITVECTOR_ULE:
599
    {
600
      returnNode = d_nm->mkNode(kind::LEQ, translated_children);
601
      break;
602
    }
603
    case kind::BITVECTOR_UGT:
604
    {
605
      returnNode = d_nm->mkNode(kind::GT, translated_children);
606
      break;
607
    }
608
    case kind::BITVECTOR_UGE:
609
    {
610
      returnNode = d_nm->mkNode(kind::GEQ, translated_children);
611
      break;
612
    }
613
    case kind::LT:
614
    {
615
      returnNode = d_nm->mkNode(kind::LT, translated_children);
616
      break;
617
    }
618
    case kind::LEQ:
619
    {
620
      returnNode = d_nm->mkNode(kind::LEQ, translated_children);
621
      break;
622
    }
623
    case kind::GT:
624
    {
625
      returnNode = d_nm->mkNode(kind::GT, translated_children);
626
      break;
627
    }
628
16
    case kind::GEQ:
629
    {
630
16
      returnNode = d_nm->mkNode(kind::GEQ, translated_children);
631
16
      break;
632
    }
633
2
    case kind::ITE:
634
    {
635
2
      returnNode = d_nm->mkNode(oldKind, translated_children);
636
2
      break;
637
    }
638
48
    case kind::APPLY_UF:
639
    {
640
      /**
641
       * higher order logic allows comparing between functions
642
       * The translation does not support this,
643
       * as the translated functions may be different outside
644
       * of the bounds that were relevant for the original
645
       * bit-vectors.
646
       */
647
16771902
      if (childrenTypesChanged(original) && options::ufHo())
648
      {
649
        throw TypeCheckingExceptionPrivate(
650
            original,
651
            string("Cannot translate to Int: ") + original.toString());
652
      }
653
      // Insert the translated application term to the cache
654
48
      returnNode = d_nm->mkNode(kind::APPLY_UF, translated_children);
655
      // Add range constraints if necessary.
656
      // If the original range was a BV sort, the original application of
657
      // the function Must be within the range determined by the
658
      // bitwidth.
659
48
      if (original.getType().isBitVector())
660
      {
661
20
        d_rangeAssertions.insert(mkRangeConstraint(
662
20
            returnNode, original.getType().getBitVectorSize()));
663
      }
664
48
      break;
665
    }
666
41
    case kind::BOUND_VAR_LIST:
667
    {
668
41
      returnNode = d_nm->mkNode(oldKind, translated_children);
669
41
      break;
670
    }
671
41
    case kind::FORALL:
672
    {
673
41
      returnNode = translateQuantifiedFormula(original);
674
41
      break;
675
    }
676
216
    default:
677
    {
678
216
      Assert(oldKind != kind::EXISTS);  // Exists is eliminated by the rewriter.
679
      // In the default case, we have reached an operator that we do not
680
      // translate directly to integers. The children whose types have
681
      // changed from bv to int should be adjusted back to bv and then
682
      // this term is reconstructed.
683
432
      TypeNode resultingType;
684
216
      if (original.getType().isBitVector())
685
      {
686
37
        resultingType = d_nm->integerType();
687
      }
688
      else
689
      {
690
179
        resultingType = original.getType();
691
      }
692
      Node reconstruction =
693
432
          reconstructNode(original, resultingType, translated_children);
694
216
      returnNode = reconstruction;
695
216
      break;
696
    }
697
  }
698
960
  Trace("bv-to-int-debug") << "original: " << original << endl;
699
960
  Trace("bv-to-int-debug") << "returnNode: " << returnNode << endl;
700
960
  return returnNode;
701
}
702
703
631
Node BVToInt::translateNoChildren(Node original)
704
{
705
631
  Node translation;
706
631
  Assert(original.isVar() || original.isConst());
707
631
  if (original.isVar())
708
  {
709
363
    if (original.getType().isBitVector())
710
    {
711
      // For bit-vector variables, we create fresh integer variables.
712
282
      if (original.getKind() == kind::BOUND_VARIABLE)
713
      {
714
        // Range constraints for the bound integer variables are not added now.
715
        // they will be added once the quantifier itself is handled.
716
82
        std::stringstream ss;
717
41
        ss << original;
718
41
        translation = d_nm->mkBoundVar(ss.str() + "_int", d_nm->integerType());
719
      }
720
      else
721
      {
722
        // New integer variables  that are not bound (symbolic constants)
723
        // are added together with range constraints induced by the
724
        // bit-width of the original bit-vector variables.
725
241
        Node newVar = d_nm->mkSkolem("__bvToInt_var",
726
482
                                     d_nm->integerType(),
727
                                     "Variable introduced in bvToInt "
728
                                     "pass instead of original variable "
729
964
                                         + original.toString());
730
241
        uint64_t bvsize = original.getType().getBitVectorSize();
731
241
        translation = newVar;
732
241
        d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize));
733
241
        defineBVUFAsIntUF(original, newVar);
734
      }
735
    }
736
81
    else if (original.getType().isFunction())
737
    {
738
30
      translation = translateFunctionSymbol(original);
739
    }
740
    else
741
    {
742
      // variables other than bit-vector variables and function symbols
743
      // are left intact
744
51
      translation = original;
745
    }
746
  }
747
  else
748
  {
749
    // original is a const
750
268
    if (original.getKind() == kind::CONST_BITVECTOR)
751
    {
752
      // Bit-vector constants are transformed into their integer value.
753
252
      BitVector constant(original.getConst<BitVector>());
754
252
      Integer c = constant.toInteger();
755
126
      translation = d_nm->mkConst<Rational>(c);
756
    }
757
    else
758
    {
759
      // Other constants stay the same.
760
142
      translation = original;
761
    }
762
  }
763
631
  return translation;
764
}
765
766
30
Node BVToInt::translateFunctionSymbol(Node bvUF)
767
{
768
  // construct the new function symbol.
769
30
  Node intUF;
770
60
  TypeNode tn = bvUF.getType();
771
60
  TypeNode bvRange = tn.getRangeType();
772
  // The function symbol has not been converted yet
773
60
  vector<TypeNode> bvDomain = tn.getArgTypes();
774
60
  vector<TypeNode> intDomain;
775
  /**
776
   * if the original range is a bit-vector sort,
777
   * the new range should be an integer sort.
778
   * Otherwise, we keep the original range.
779
   * Similarly for the domains.
780
   */
781
60
  TypeNode intRange = bvRange.isBitVector() ? d_nm->integerType() : bvRange;
782
62
  for (TypeNode d : bvDomain)
783
  {
784
32
    intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d);
785
  }
786
60
  ostringstream os;
787
30
  os << "__bvToInt_fun_" << bvUF << "_int";
788
90
  intUF = d_nm->mkSkolem(
789
60
      os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function");
790
  // introduce a `define-fun` in the smt-engine to keep
791
  // the correspondence between the original
792
  // function symbol and the new one.
793
30
  defineBVUFAsIntUF(bvUF, intUF);
794
60
  return intUF;
795
}
796
797
271
void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
798
{
799
  // The resulting term
800
542
  Node result;
801
  // The type of the resulting term
802
542
  TypeNode resultType;
803
  // symbolic arguments of original function
804
542
  vector<Node> args;
805
271
  if (!bvUF.getType().isFunction()) {
806
    // bvUF is a variable.
807
    // in this case, the result is just the original term
808
    // (it will be casted later if needed)
809
241
    result = intUF;
810
241
    resultType = bvUF.getType();
811
  } else {
812
    // bvUF is a function with arguments
813
    // The arguments need to be casted as well.
814
60
    TypeNode tn = bvUF.getType();
815
30
    resultType = tn.getRangeType();
816
60
    vector<TypeNode> bvDomain = tn.getArgTypes();
817
    // children of the new symbolic application
818
60
    vector<Node> achildren;
819
30
    achildren.push_back(intUF);
820
30
    int i = 0;
821
62
    for (const TypeNode& d : bvDomain)
822
    {
823
      // Each bit-vector argument is casted to a natural number
824
      // Other arguments are left intact.
825
64
      Node fresh_bound_var = d_nm->mkBoundVar(d);
826
32
      args.push_back(fresh_bound_var);
827
64
      Node castedArg = args[i];
828
32
      if (d.isBitVector())
829
      {
830
26
        castedArg = castToType(castedArg, d_nm->integerType());
831
      }
832
32
      achildren.push_back(castedArg);
833
32
      i++;
834
    }
835
30
    result = d_nm->mkNode(kind::APPLY_UF, achildren);
836
  }
837
  // If the result is BV, it needs to be casted back.
838
271
  result = castToType(result, resultType);
839
  // add the function definition to the smt engine.
840
271
  d_preprocContext->getSmt()->defineFunction(bvUF, args, result, true);
841
271
}
842
843
48
bool BVToInt::childrenTypesChanged(Node n)
844
{
845
48
  bool result = false;
846
54
  for (const Node& child : n)
847
  {
848
54
    TypeNode originalType = child.getType();
849
54
    TypeNode newType = d_bvToIntCache[child].get().getType();
850
48
    if (!newType.isSubtypeOf(originalType))
851
    {
852
42
      result = true;
853
42
      break;
854
    }
855
  }
856
48
  return result;
857
}
858
859
826
Node BVToInt::castToType(Node n, TypeNode tn)
860
{
861
  // If there is no reason to cast, return the
862
  // original node.
863
826
  if (n.getType().isSubtypeOf(tn))
864
  {
865
510
    return n;
866
  }
867
  // We only case int to bv or vice verse.
868
316
  Assert((n.getType().isBitVector() && tn.isInteger())
869
         || (n.getType().isInteger() && tn.isBitVector()));
870
316
  if (n.getType().isInteger())
871
  {
872
253
    Assert(tn.isBitVector());
873
253
    unsigned bvsize = tn.getBitVectorSize();
874
506
    Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
875
253
    return d_nm->mkNode(intToBVOp, n);
876
  }
877
63
  Assert(n.getType().isBitVector());
878
63
  Assert(tn.isInteger());
879
63
  return d_nm->mkNode(kind::BITVECTOR_TO_NAT, n);
880
}
881
882
216
Node BVToInt::reconstructNode(Node originalNode,
883
                              TypeNode resultType,
884
                              const vector<Node>& translated_children)
885
{
886
  // first, we adjust the children of the node as needed.
887
  // re-construct the term with the adjusted children.
888
216
  kind::Kind_t oldKind = originalNode.getKind();
889
432
  NodeBuilder<> builder(oldKind);
890
216
  if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
891
  {
892
37
    builder << originalNode.getOperator();
893
  }
894
529
  for (size_t i = 0; i < originalNode.getNumChildren(); i++)
895
  {
896
626
    Node originalChild = originalNode[i];
897
626
    Node translatedChild = translated_children[i];
898
626
    Node adjustedChild = castToType(translatedChild, originalChild.getType());
899
313
    builder << adjustedChild;
900
  }
901
216
  Node reconstruction = builder.constructNode();
902
  // cast to tn in case the reconstruction is a bit-vector.
903
216
  reconstruction = castToType(reconstruction, resultType);
904
432
  return reconstruction;
905
}
906
907
8995
BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
908
    : PreprocessingPass(preprocContext, "bv-to-int"),
909
      d_binarizeCache(preprocContext->getUserContext()),
910
      d_eliminationCache(preprocContext->getUserContext()),
911
      d_rebuildCache(preprocContext->getUserContext()),
912
      d_bvToIntCache(preprocContext->getUserContext()),
913
8995
      d_rangeAssertions(preprocContext->getUserContext())
914
{
915
8995
  d_nm = NodeManager::currentNM();
916
8995
  d_zero = d_nm->mkConst<Rational>(0);
917
8995
  d_one = d_nm->mkConst<Rational>(1);
918
8995
};
919
920
147
PreprocessingPassResult BVToInt::applyInternal(
921
    AssertionPipeline* assertionsToPreprocess)
922
{
923
572
  for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i)
924
  {
925
850
    Node bvNode = (*assertionsToPreprocess)[i];
926
850
    Node intNode = bvToInt(bvNode);
927
850
    Node rwNode = Rewriter::rewrite(intNode);
928
425
    Trace("bv-to-int-debug") << "bv node: " << bvNode << std::endl;
929
425
    Trace("bv-to-int-debug") << "int node: " << intNode << std::endl;
930
425
    Trace("bv-to-int-debug") << "rw node: " << rwNode << std::endl;
931
425
    assertionsToPreprocess->replace(i, rwNode);
932
  }
933
147
  addFinalizeRangeAssertions(assertionsToPreprocess);
934
147
  return PreprocessingPassResult::NO_CONFLICT;
935
}
936
937
147
void BVToInt::addFinalizeRangeAssertions(
938
    AssertionPipeline* assertionsToPreprocess)
939
{
940
  // collect the range assertions from d_rangeAssertions
941
  // (which is a context-dependent set)
942
  // into a vector.
943
294
  vector<Node> vec_range;
944
147
  vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end());
945
  // conjoin all range assertions and add the conjunction
946
  // as a new assertion
947
294
  Node rangeAssertions = Rewriter::rewrite(d_nm->mkAnd(vec_range));
948
147
  assertionsToPreprocess->push_back(rangeAssertions);
949
294
  Trace("bv-to-int-debug") << "range constraints: "
950
147
                           << rangeAssertions.toString() << std::endl;
951
147
}
952
953
80
Node BVToInt::createShiftNode(vector<Node> children,
954
                              uint64_t bvsize,
955
                              bool isLeftShift)
956
{
957
  /**
958
   * from SMT-LIB:
959
   * [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]])))
960
   * [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]])))
961
   * Since we don't have exponentiation, we use an ite.
962
   * Important note: below we use INTS_DIVISION_TOTAL, which is safe here
963
   * because we divide by 2^... which is never 0.
964
   */
965
160
  Node x = children[0];
966
160
  Node y = children[1];
967
  // shifting by const is eliminated by the theory rewriter
968
80
  Assert(!y.isConst());
969
80
  Node ite = d_zero;
970
160
  Node body;
971
460
  for (uint64_t i = 0; i < bvsize; i++)
972
  {
973
380
    if (isLeftShift)
974
    {
975
64
      body = d_nm->mkNode(kind::INTS_MODULUS_TOTAL,
976
32
                          d_nm->mkNode(kind::MULT, x, pow2(i)),
977
32
                          pow2(bvsize));
978
    }
979
    else
980
    {
981
364
      body = d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i));
982
    }
983
1140
    ite = d_nm->mkNode(kind::ITE,
984
760
                       d_nm->mkNode(kind::EQUAL, y, d_nm->mkConst<Rational>(i)),
985
                       body,
986
                       ite);
987
  }
988
160
  return ite;
989
}
990
991
41
Node BVToInt::translateQuantifiedFormula(Node quantifiedNode)
992
{
993
41
  kind::Kind_t k = quantifiedNode.getKind();
994
82
  Node boundVarList = quantifiedNode[0];
995
41
  Assert(boundVarList.getKind() == kind::BOUND_VAR_LIST);
996
  // Since bit-vector variables are being translated to
997
  // integer variables, we need to substitute the new ones
998
  // for the old ones.
999
82
  vector<Node> oldBoundVars;
1000
82
  vector<Node> newBoundVars;
1001
82
  vector<Node> rangeConstraints;
1002
82
  for (Node bv : quantifiedNode[0])
1003
  {
1004
41
    oldBoundVars.push_back(bv);
1005
41
    if (bv.getType().isBitVector())
1006
    {
1007
      // bit-vector variables are replaced by integer ones.
1008
      // the new variables induce range constraints based on the
1009
      // original bit-width.
1010
82
      Node newBoundVar = d_bvToIntCache[bv];
1011
41
      newBoundVars.push_back(newBoundVar);
1012
41
      rangeConstraints.push_back(
1013
82
          mkRangeConstraint(newBoundVar, bv.getType().getBitVectorSize()));
1014
    }
1015
    else
1016
    {
1017
      // variables that are not bit-vectors are not changed
1018
      newBoundVars.push_back(bv);
1019
    }
1020
  }
1021
1022
  // the body of the quantifier
1023
82
  Node matrix = d_bvToIntCache[quantifiedNode[1]];
1024
  // make the substitution
1025
41
  matrix = matrix.substitute(oldBoundVars.begin(),
1026
                             oldBoundVars.end(),
1027
                             newBoundVars.begin(),
1028
                             newBoundVars.end());
1029
  // A node to represent all the range constraints.
1030
82
  Node ranges = d_nm->mkAnd(rangeConstraints);
1031
  // Add the range constraints to the body of the quantifier.
1032
  // For "exists", this is added conjunctively
1033
  // For "forall", this is added to the left side of an implication.
1034
41
  matrix = d_nm->mkNode(
1035
      k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix);
1036
  // create the new quantified formula and return it.
1037
82
  Node newBoundVarsList = d_nm->mkNode(kind::BOUND_VAR_LIST, newBoundVars);
1038
41
  Node result = d_nm->mkNode(kind::FORALL, newBoundVarsList, matrix);
1039
82
  return result;
1040
}
1041
1042
34
Node BVToInt::createBVNotNode(Node n, uint64_t bvsize)
1043
{
1044
34
  return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
1045
}
1046
1047
}  // namespace passes
1048
}  // namespace preprocessing
1049
16828433
}  // namespace CVC4