GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/int_to_bv.cpp Lines: 93 133 69.9 %
Date: 2021-03-22 Branches: 193 612 31.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file int_to_bv.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Yoni Zohar, Alex Ozdemir
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 IntToBV preprocessing pass
13
 **
14
 ** Converts integer operations into bitvector operations. The width of the
15
 ** bitvectors is controlled through the `--solve-int-as-bv` command line
16
 ** option.
17
 **/
18
19
#include "preprocessing/passes/int_to_bv.h"
20
21
#include <string>
22
#include <unordered_map>
23
#include <vector>
24
25
#include "expr/node.h"
26
#include "expr/node_traversal.h"
27
#include "options/smt_options.h"
28
#include "preprocessing/assertion_pipeline.h"
29
#include "theory/rewriter.h"
30
#include "theory/theory.h"
31
32
namespace CVC4 {
33
namespace preprocessing {
34
namespace passes {
35
36
using namespace std;
37
using namespace CVC4::theory;
38
39
using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
40
41
namespace {
42
43
2
bool childrenTypesChanged(Node n, NodeMap& cache) {
44
4
  for (Node child : n) {
45
4
    TypeNode originalType = child.getType();
46
4
    TypeNode newType = cache[child].getType();
47
2
    if (! newType.isSubtypeOf(originalType)) {
48
      return true;
49
    }
50
  }
51
2
  return false;
52
}
53
54
55
16
Node intToBVMakeBinary(TNode n, NodeMap& cache)
56
{
57
43
  for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER,
58
118
           [&cache](TNode nn) { return cache.count(nn) > 0; }))
59
  {
60
86
    Node result;
61
43
    NodeManager* nm = NodeManager::currentNM();
62
43
    if (current.getNumChildren() == 0)
63
    {
64
22
      result = current;
65
    }
66
42
    else if (current.getNumChildren() > 2
67
21
             && (current.getKind() == kind::PLUS
68
                 || current.getKind() == kind::MULT))
69
    {
70
      Assert(cache.find(current[0]) != cache.end());
71
      result = cache[current[0]];
72
      for (unsigned i = 1; i < current.getNumChildren(); ++i)
73
      {
74
        Assert(cache.find(current[i]) != cache.end());
75
        Node child = current[i];
76
        Node childRes = cache[current[i]];
77
        result = nm->mkNode(current.getKind(), result, childRes);
78
      }
79
    }
80
    else
81
    {
82
42
      NodeBuilder<> builder(current.getKind());
83
21
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
84
2
        builder << current.getOperator();
85
      }
86
87
55
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
88
      {
89
34
        Assert(cache.find(current[i]) != cache.end());
90
34
        builder << cache[current[i]];
91
      }
92
21
      result = builder;
93
    }
94
43
    cache[current] = result;
95
  }
96
16
  return cache[n];
97
}
98
99
16
Node intToBV(TNode n, NodeMap& cache)
100
{
101
33295
  int size = options::solveIntAsBV();
102
16
  AlwaysAssert(size > 0);
103
16
  AlwaysAssert(!options::incrementalSolving());
104
105
32
  NodeMap binaryCache;
106
32
  Node n_binary = intToBVMakeBinary(n, binaryCache);
107
108
37
  for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER,
109
108
           [&cache](TNode nn) { return cache.count(nn) > 0; }))
110
  {
111
37
    NodeManager* nm = NodeManager::currentNM();
112
37
    if (current.getNumChildren() > 0)
113
    {
114
      // Not a leaf
115
34
      vector<Node> children;
116
17
      unsigned max = 0;
117
45
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
118
      {
119
28
        Assert(cache.find(current[i]) != cache.end());
120
56
        TNode childRes = cache[current[i]];
121
56
        TypeNode type = childRes.getType();
122
28
        if (type.isBitVector())
123
        {
124
14
          unsigned bvsize = type.getBitVectorSize();
125
14
          if (bvsize > max)
126
          {
127
8
            max = bvsize;
128
          }
129
        }
130
28
        children.push_back(childRes);
131
      }
132
133
17
      kind::Kind_t newKind = current.getKind();
134
17
      if (max > 0)
135
      {
136
8
        switch (newKind)
137
        {
138
          case kind::PLUS:
139
            Assert(children.size() == 2);
140
            newKind = kind::BITVECTOR_PLUS;
141
            max = max + 1;
142
            break;
143
          case kind::MULT:
144
            Assert(children.size() == 2);
145
            newKind = kind::BITVECTOR_MULT;
146
            max = max * 2;
147
            break;
148
          case kind::MINUS:
149
            Assert(children.size() == 2);
150
            newKind = kind::BITVECTOR_SUB;
151
            max = max + 1;
152
            break;
153
          case kind::UMINUS:
154
            Assert(children.size() == 1);
155
            newKind = kind::BITVECTOR_NEG;
156
            max = max + 1;
157
            break;
158
          case kind::LT: newKind = kind::BITVECTOR_SLT; break;
159
          case kind::LEQ: newKind = kind::BITVECTOR_SLE; break;
160
          case kind::GT: newKind = kind::BITVECTOR_SGT; break;
161
          case kind::GEQ: newKind = kind::BITVECTOR_SGE; break;
162
6
          case kind::EQUAL:
163
6
          case kind::ITE: break;
164
2
          default:
165
2
            if (childrenTypesChanged(current, cache)) {
166
              throw TypeCheckingExceptionPrivate(
167
                  current,
168
                  string("Cannot translate to BV: ") + current.toString());
169
            }
170
2
            break;
171
        }
172
22
        for (unsigned i = 0; i < children.size(); ++i)
173
        {
174
28
          TypeNode type = children[i].getType();
175
14
          if (!type.isBitVector())
176
          {
177
            continue;
178
          }
179
14
          unsigned bvsize = type.getBitVectorSize();
180
14
          if (bvsize < max)
181
          {
182
            // sign extend
183
            Node signExtendOp = nm->mkConst<BitVectorSignExtend>(
184
                BitVectorSignExtend(max - bvsize));
185
            children[i] = nm->mkNode(signExtendOp, children[i]);
186
          }
187
        }
188
      }
189
34
      NodeBuilder<> builder(newKind);
190
17
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
191
2
        builder << current.getOperator();
192
      }
193
45
      for (unsigned i = 0; i < children.size(); ++i)
194
      {
195
28
        builder << children[i];
196
      }
197
      // Mark the substitution and continue
198
34
      Node result = builder;
199
200
17
      result = Rewriter::rewrite(result);
201
17
      cache[current] = result;
202
    }
203
    else
204
    {
205
      // It's a leaf: could be a variable or a numeral
206
40
      Node result = current;
207
20
      if (current.isVar())
208
      {
209
9
        if (current.getType() == nm->integerType())
210
        {
211
18
          result = nm->mkSkolem("__intToBV_var",
212
12
                                nm->mkBitVectorType(size),
213
                                "Variable introduced in intToBV pass");
214
        }
215
      }
216
11
      else if (current.isConst())
217
      {
218
11
        switch (current.getKind())
219
        {
220
2
          case kind::CONST_RATIONAL:
221
          {
222
4
            Rational constant = current.getConst<Rational>();
223
2
            if (constant.isIntegral()) {
224
2
              AlwaysAssert(constant >= 0);
225
4
              BitVector bv(size, constant.getNumerator());
226
2
              if (bv.toSignedInteger() != constant.getNumerator())
227
              {
228
                throw TypeCheckingExceptionPrivate(
229
                    current,
230
                    string("Not enough bits for constant in intToBV: ")
231
                        + current.toString());
232
              }
233
2
              result = nm->mkConst(bv);
234
            }
235
2
            break;
236
          }
237
9
          default: break;
238
        }
239
      }
240
      else
241
      {
242
        throw TypeCheckingExceptionPrivate(
243
            current, string("Cannot translate to BV: ") + current.toString());
244
      }
245
20
      cache[current] = result;
246
    }
247
  }
248
32
  return cache[n_binary];
249
}
250
}  // namespace
251
252
8995
IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
253
8995
    : PreprocessingPass(preprocContext, "int-to-bv"){};
254
255
7
PreprocessingPassResult IntToBV::applyInternal(
256
    AssertionPipeline* assertionsToPreprocess)
257
{
258
14
  NodeMap cache;
259
23
  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
260
  {
261
16
    assertionsToPreprocess->replace(
262
32
        i, intToBV((*assertionsToPreprocess)[i], cache));
263
  }
264
14
  return PreprocessingPassResult::NO_CONFLICT;
265
}
266
267
268
}  // namespace passes
269
}  // namespace preprocessing
270
59955
}  // namespace CVC4