1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief The BVToInt preprocessing pass
14 ** Converts bit-vector formulas to integer formulas.
15 ** The conversion is implemented using a translation function Tr,
16 ** roughly described as follows:
18 ** Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh
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
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
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
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.
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.
48 ** Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g)
50 ** Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor.
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.
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.
61 ** Bit-vector operators that are not listed above are either eliminated using
62 ** the function eliminationPass, or are not supported.
66 #include "cvc4_private.h"
68 #ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
69 #define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
71 #include "context/cdhashmap.h"
72 #include "context/cdhashset.h"
73 #include "preprocessing/preprocessing_pass.h"
74 #include "theory/arith/nl/iand_utils.h"
77 namespace preprocessing
{
80 using CDNodeMap
= context::CDHashMap
<Node
, Node
, NodeHashFunction
>;
82 class BVToInt
: public PreprocessingPass
85 BVToInt(PreprocessingPassContext
* preprocContext
);
88 PreprocessingPassResult
applyInternal(
89 AssertionPipeline
* assertionsToPreprocess
) override
;
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,
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.
105 Node
createShiftNode(std::vector
<Node
> children
,
110 * Returns a node that represents the bitwise negation of n.
112 Node
createBVNotNode(Node n
, uint64_t bvsize
);
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.
120 Node
bvToInt(Node n
);
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.
130 Node
mkRangeConstraint(Node newVar
, uint64_t k
);
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.
137 Node
eliminationPass(Node n
);
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.
146 Node
makeBinary(Node n
);
149 * @param k A non-negative integer
150 * @return A node that represents the constant 2^k
152 Node
pow2(uint64_t k
);
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
160 Node
maxInt(uint64_t k
);
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))
167 Node
modpow2(Node n
, uint64_t exponent
);
169 bool childrenTypesChanged(Node n
);
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
178 void addFinalizeRangeAssertions(AssertionPipeline
* assertionsToPreprocess
);
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.
188 Node
translateQuantifiedFormula(Node quantifiedNode
);
191 * Reconstructs a node whose main operator cannot be
192 * translated to integers.
193 * Reconstruction is done by casting to integers/bit-vectors
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
199 * In this case we cast x to (bv2nat x) during
200 * the reconstruction.
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.
208 Node
reconstructNode(Node originalNode
,
210 const std::vector
<Node
>& translated_children
);
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.
220 Node
castToType(Node n
, TypeNode tn
);
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
230 * @param bvUF the original function or variable
231 * @param intUF the translated function or variable
233 void defineBVUFAsIntUF(Node bvUF
, Node intUF
);
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.
241 Node
translateFunctionSymbol(Node bvUF
);
244 * Performs the actual translation to integers for nodes
245 * that have children.
247 Node
translateWithChildren(Node original
,
248 const std::vector
<Node
>& translated_children
);
251 * Performs the actual translation to integers for nodes
252 * that don't have children (variables, constants, uninterpreted function
255 Node
translateNoChildren(Node original
);
258 * Caches for the different functions
260 CDNodeMap d_binarizeCache
;
261 CDNodeMap d_eliminationCache
;
262 CDNodeMap d_rebuildCache
;
263 CDNodeMap d_bvToIntCache
;
266 * Node manager that is used throughout the pass
271 * A set of constraints of the form 0 <= x < 2^k
272 * These are added for every new integer variable that we introduce.
274 context::CDHashSet
<Node
, NodeHashFunction
> d_rangeAssertions
;
282 /** helper class for handeling bvand translation */
283 theory::arith::nl::IAndUtils d_iandUtils
;
286 } // namespace passes
287 } // namespace preprocessing
290 #endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */