GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bv_to_int.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_to_int.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, Gereon Kremer, Makai Mann
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 formulas to integer formulas.
15
 ** The conversion is implemented using a translation function Tr,
16
 ** roughly described as follows:
17
 **
18
 ** Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh
19
 **         integer variable.
20
 ** Tr(c) = the integer value of c, for any bit-vector constant c.
21
 ** Tr((bvadd s t)) = Tr(s) + Tr(t) mod 2^k, where k is the bit width of
22
 **         s and t.
23
 ** Similar transformations are done for bvmul, bvsub, bvudiv, bvurem, bvneg,
24
 **         bvnot, bvconcat, bvextract
25
 ** Tr((_ zero_extend m) x) = Tr(x)
26
 ** Tr((_ sign_extend m) x) = ite(msb(x)=0, x, 2^k*(2^m-1) + x))
27
 ** explanation: if the msb is 0, this is the same as zero_extend,
28
 ** which does not change the integer value.
29
 ** If the msb is 1, then the result should correspond to
30
 ** concat(1...1, x), with m 1's.
31
 ** m 1's is 2^m-1, and multiplying it by x's width (k) moves it
32
 ** to the front.
33
 **
34
 ** Tr((bvand s t)) depends on the granularity, which is provided by the user
35
 ** when enabling this preprocessing pass.
36
 ** We divide s and t to blocks.
37
 ** The size of each block is the granularity, and so the number of
38
 ** blocks is:
39
 ** bit width/granularity (rounded down).
40
 ** We create an ITE that represents an arbitrary block,
41
 ** and then create a sum by mutiplying each block by the
42
 ** appropriate power of two.
43
 ** More formally:
44
 ** Let g denote the granularity.
45
 ** Let k denote the bit width of s and t.
46
 ** Let b denote floor(k/g) if k >= g, or just k otherwise.
47
 ** Tr((bvand s t)) =
48
 ** Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g)
49
 **
50
 ** Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor.
51
 **
52
 ** Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of
53
 **         a and b, and ITE represents exponentiation up to k, that is:
54
 ** ITE = ite(Tr(b)=0, 1, ite(Tr(b)=1), 2, ite(Tr(b)=2, 4, ...))
55
 ** Similar transformations are done for bvlshr.
56
 **
57
 ** Tr(a=b) = Tr(a)=Tr(b)
58
 ** Tr((bvult a b)) = Tr(a) < Tr(b)
59
 ** Similar transformations are done for bvule, bvugt, and bvuge.
60
 **
61
 ** Bit-vector operators that are not listed above are either eliminated using
62
 ** the function eliminationPass, or are not supported.
63
 **
64
 **/
65
66
#include "cvc4_private.h"
67
68
#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
69
#define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
70
71
#include "context/cdhashmap.h"
72
#include "context/cdhashset.h"
73
#include "preprocessing/preprocessing_pass.h"
74
#include "theory/arith/nl/iand_utils.h"
75
76
namespace CVC4 {
77
namespace preprocessing {
78
namespace passes {
79
80
using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
81
82
17984
class BVToInt : public PreprocessingPass
83
{
84
 public:
85
  BVToInt(PreprocessingPassContext* preprocContext);
86
87
 protected:
88
  PreprocessingPassResult applyInternal(
89
      AssertionPipeline* assertionsToPreprocess) override;
90
  /**
91
   * A generic function that creates a logical shift node (either left or
92
   * right). a << b gets translated to a * 2^b mod 2^k, where k is the bit
93
   * width. a >> b gets translated to a div 2^b mod 2^k, where k is the bit
94
   * width. The exponentiation operation is translated to an ite for possible
95
   * values of the exponent, from 0 to k-1.
96
   * If the right operand of the shift is greater than k-1,
97
   * the result is 0.
98
   * @param children the two operands for the shift
99
   * @param bvsize the original bit widths of the operands
100
   *                (before translation to integers)
101
   * @param  isLeftShift true iff the desired operation is a left shift.
102
   * @return a node representing the shift.
103
   *
104
   */
105
  Node createShiftNode(std::vector<Node> children,
106
                       uint64_t bvsize,
107
                       bool isLeftShift);
108
109
  /**
110
   * Returns a node that represents the bitwise negation of n.
111
   */
112
  Node createBVNotNode(Node n, uint64_t bvsize);
113
114
  /**
115
   * The result is an integer term and is computed
116
   * according to the translation specified above.
117
   * @param n is a bit-vector term or formula to be translated.
118
   * @return integer node that corresponds to n.
119
   */
120
  Node bvToInt(Node n);
121
122
  /**
123
   * Whenever we introduce an integer variable that represents a bit-vector
124
   * variable, we need to guard the range of the newly introduced variable.
125
   * For bit width k, the constraint is 0 <= newVar < 2^k.
126
   * @param newVar the newly introduced integer variable
127
   * @param k the bit width of the original bit-vector variable.
128
   * @return a node representing the range constraint.
129
   */
130
  Node mkRangeConstraint(Node newVar, uint64_t k);
131
132
  /**
133
   * In the translation to integers, it is convenient to assume that certain
134
   * bit-vector operators do not occur in the original formula (e.g., repeat).
135
   * This function eliminates all these operators.
136
   */
137
  Node eliminationPass(Node n);
138
139
  /**
140
   * Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more
141
   * than two arguments as a syntactic sugar.
142
   * For example, we can have a node for (bvand x y z),
143
   * that represents (bvand (x (bvand y z))).
144
   * This function makes all such operators strictly binary.
145
   */
146
  Node makeBinary(Node n);
147
148
  /**
149
   * @param k A non-negative integer
150
   * @return A node that represents the constant 2^k
151
   */
152
  Node pow2(uint64_t k);
153
154
  /**
155
   * @param k A positive integer k
156
   * @return A node that represent the constant 2^k-1
157
   * For example, if k is 4, the result is a node representing the
158
   * constant 15.
159
   */
160
  Node maxInt(uint64_t k);
161
162
  /**
163
   * @param n A node representing an integer term
164
   * @param exponent A non-negative integer
165
   * @return A node representing (n mod (2^exponent))
166
   */
167
  Node modpow2(Node n, uint64_t exponent);
168
169
  bool childrenTypesChanged(Node n);
170
171
  /**
172
   * Add the range assertions collected in d_rangeAssertions
173
   * (using mkRangeConstraint) to the assertion pipeline.
174
   * If there are no range constraints, do nothing.
175
   * If there is a single range constraint, add it to the pipeline.
176
   * Otherwise, add all of them as a single conjunction
177
   */
178
  void addFinalizeRangeAssertions(AssertionPipeline* assertionsToPreprocess);
179
180
  /**
181
   * @param quantifiedNode a node whose main operator is forall/exists.
182
   * @return a node opbtained from quantifiedNode by:
183
   * 1. Replacing all bound BV variables by new bound integer variables.
184
   * 2. Add range constraints for the new variables, induced by the original
185
   * bit-width. These range constraints are added with "AND" in case of exists
186
   * and with "IMPLIES" in case of forall.
187
   */
188
  Node translateQuantifiedFormula(Node quantifiedNode);
189
190
  /**
191
   * Reconstructs a node whose main operator cannot be
192
   * translated to integers.
193
   * Reconstruction is done by casting to integers/bit-vectors
194
   * as needed.
195
   * For example, if node is (select A x) where A
196
   * is a bit-vector array, we do not change A to be
197
   * an integer array, even though x was translated
198
   * to integers.
199
   * In this case we cast x to (bv2nat x) during
200
   * the reconstruction.
201
   *
202
   * @param originalNode the node that we are reconstructing
203
   * @param resultType the desired type for the reconstruction
204
   * @param translated_children the children of originalNode
205
   *        after their translation to integers.
206
   * @return A node with originalNode's operator that has type resultType.
207
   */
208
  Node reconstructNode(Node originalNode,
209
                       TypeNode resultType,
210
                       const std::vector<Node>& translated_children);
211
212
  /**
213
   * A useful utility function.
214
   * if n is an integer and tn is bit-vector,
215
   * applies the IntToBitVector operator on n.
216
   * if n is a vit-vector and tn is integer,
217
   * applies BitVector_TO_NAT operator.
218
   * Otherwise, keeps n intact.
219
   */
220
  Node castToType(Node n, TypeNode tn);
221
222
  /**
223
   * When a UF f is translated to a UF g,
224
   * we add a define-fun command to the smt-engine
225
   * to relate between f and g.
226
   * We do the same when f and g are just variables.
227
   * This is useful, for example, when asking
228
   * for a model-value of a term that includes the
229
   * original UF f.
230
   * @param bvUF the original function or variable
231
   * @param intUF the translated function or variable
232
   */
233
  void defineBVUFAsIntUF(Node bvUF, Node intUF);
234
235
  /**
236
   * @param bvUF is an uninterpreted function symbol from the original formula
237
   * @return a fresh uninterpreted function symbol, obtained from bvUF
238
     by replacing every argument of type BV to an argument of type Integer,
239
     and the return type becomes integer in case it was BV.
240
   */
241
  Node translateFunctionSymbol(Node bvUF);
242
243
  /**
244
   * Performs the actual translation to integers for nodes
245
   * that have children.
246
   */
247
  Node translateWithChildren(Node original,
248
                             const std::vector<Node>& translated_children);
249
250
  /**
251
   * Performs the actual translation to integers for nodes
252
   * that don't have children (variables, constants, uninterpreted function
253
   * symbols).
254
   */
255
  Node translateNoChildren(Node original);
256
257
  /**
258
   * Caches for the different functions
259
   */
260
  CDNodeMap d_binarizeCache;
261
  CDNodeMap d_eliminationCache;
262
  CDNodeMap d_rebuildCache;
263
  CDNodeMap d_bvToIntCache;
264
265
  /**
266
   * Node manager that is used throughout the pass
267
   */
268
  NodeManager* d_nm;
269
270
  /**
271
   * A set of constraints of the form 0 <= x < 2^k
272
   * These are added for every new integer variable that we introduce.
273
   */
274
  context::CDHashSet<Node, NodeHashFunction> d_rangeAssertions;
275
276
  /**
277
   * Useful constants
278
   */
279
  Node d_zero;
280
  Node d_one;
281
282
  /** helper class for handeling bvand translation */
283
  theory::arith::nl::IAndUtils d_iandUtils;
284
};
285
286
}  // namespace passes
287
}  // namespace preprocessing
288
}  // namespace CVC4
289
290
#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */