diff options
Diffstat (limited to 'src/preprocessing/passes/bv_to_int.h')
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.h | 273 |
1 files changed, 273 insertions, 0 deletions
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h new file mode 100644 index 000000000..dd02d98ec --- /dev/null +++ b/src/preprocessing/passes/bv_to_int.h @@ -0,0 +1,273 @@ +/********************* */ +/*! \file bv_to_int.h + ** \verbatim + ** Top contributors (to current version): + ** Yoni Zohar and Ahmed Irfan + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The BVToInt preprocessing pass + ** + ** Converts bit-vector formulas to integer formulas. + ** The conversion is implemented using a translation function Tr, + ** roughly described as follows: + ** + ** Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh + ** integer variable. + ** Tr(c) = the integer value of c, for any bit-vector constant c. + ** Tr((bvadd s t)) = Tr(s) + Tr(t) mod 2^k, where k is the bit width of + ** s and t. + ** Similar transformations are done for bvmul, bvsub, bvudiv, bvurem, bvneg, + ** bvnot, bvconcat, bvextract + ** + ** Tr((bvand s t)) depends on the granularity, which is provided by the user + ** when enabling this preprocessing pass. + ** We divide s and t to blocks. + ** The size of each block is the granularity, and so the number of + ** blocks is: + ** bit width/granularity (rounded down). + ** We create an ITE that represents an arbitrary block, + ** and then create a sum by mutiplying each block by the + ** appropriate power of two. + ** More formally: + ** Let g denote the granularity. + ** Let k denote the bit width of s and t. + ** Let b denote floor(k/g) if k >= g, or just k otherwise. + ** Tr((bvand s t)) = + ** Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g) + ** + ** More details and examples for this case are described next to + ** the function createBitwiseNode. + ** Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor. + ** + ** Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of + ** a and b, and ITE represents exponentiation up to k, that is: + ** ITE = ite(Tr(b)=0, 1, ite(Tr(b)=1), 2, ite(Tr(b)=2, 4, ...)) + ** Similar transformations are done for bvlshr. + ** + ** Tr(a=b) = Tr(a)=Tr(b) + ** Tr((bvult a b)) = Tr(a) < Tr(b) + ** Similar transformations are done for bvule, bvugt, and bvuge. + ** + ** Bit-vector operators that are not listed above are either eliminated using + ** the function eliminationPass, or are not supported. + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H +#define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>; + +class BVToInt : public PreprocessingPass +{ + public: + BVToInt(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + /** + * A generic function that creates a node that represents a bitwise + * operation. + * + * For example: Suppose bvsize is 4, granularity is 1, and f(x,y) = x && y. + * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)). + * The result of this function would be: + * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3 + * + * For another example: Suppose bvsize is 4, granularity is 2, + * and f(x,y) = x && y. + * Denote by ITE(a,b) the term that corresponds to the following table: + * a | b | ITE(a,b) + * ---------------- + * 0 | 0 | 0 + * 0 | 1 | 0 + * 0 | 2 | 0 + * 0 | 3 | 0 + * 1 | 0 | 0 + * 1 | 1 | 1 + * 1 | 2 | 0 + * 1 | 3 | 1 + * 2 | 0 | 0 + * 2 | 1 | 0 + * 2 | 2 | 2 + * 2 | 3 | 2 + * 3 | 0 | 0 + * 3 | 1 | 1 + * 3 | 2 | 2 + * 3 | 3 | 3 + * + * For example, 2 in binary is 10 and 1 in binary is 01, and so doing + * "bitwise f" on them gives 00. + * The result of this function would be: + * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2 + * + * + * @param x is an integer operand that correspond to the first original + * bit-vector operand. + * @param y is an integer operand that correspond to the second original + * bit-vector operand. + * @param bvsize is the bit width of the original bit-vector variables. + * @param granularity is specified in the options for this preprocessing + * pass. + * @param f is a pointer to a boolean function that corresponds + * to the original bitwise operation. + * @return A node that represents the operation, as described above. + */ + Node createBitwiseNode(Node x, + Node y, + uint64_t bvsize, + uint64_t granularity, + bool (*f)(bool, bool)); + + /** + * A helper function for createBitwiseNode + * @param x integer node corresponding to the original first bit-vector + * argument + * @param y integer node corresponding to the original second bit-vector + * argument nodes. + * @param granularity the bitwidth of the original bit-vector nodes. + * @param table a function from pairs of integers to integers. + * The domain of this function consists of pairs of + * integers between 0 (inclusive) and 2^{bitwidth} (exclusive). + * @return An ite term that represents this table. + */ + Node createITEFromTable( + Node x, + Node y, + uint64_t granularity, + std::map<std::pair<uint64_t, uint64_t>, uint64_t> table); + + /** + * A generic function that creates a logical shift node (either left or + * right). a << b gets translated to a * 2^b mod 2^k, where k is the bit + * width. a >> b gets translated to a div 2^b mod 2^k, where k is the bit + * width. The exponentiation operation is translated to an ite for possible + * values of the exponent, from 0 to k-1. + * If the right operand of the shift is greater than k-1, + * the result is 0. + * @param children the two operands for the shift + * @param bvsize the original bit widths of the operands + * (before translation to integers) + * @param isLeftShift true iff the desired operation is a left shift. + * @return a node representing the shift. + * + */ + Node createShiftNode(vector<Node> children, + uint64_t bvsize, + bool isLeftShift); + + /** + * Returns a node that represents the bitwise negation of n. + */ + Node createBVNotNode(Node n, uint64_t bvsize); + + /** + * The result is an integer term and is computed + * according to the translation specified above. + * @param n is a bit-vector term or formula to be translated. + * @return integer node that corresponds to n. + */ + Node bvToInt(Node n); + + /** + * Whenever we introduce an integer variable that represents a bit-vector + * variable, we need to guard the range of the newly introduced variable. + * For bit width k, the constraint is 0 <= newVar < 2^k. + * @param newVar the newly introduced integer variable + * @param k the bit width of the original bit-vector variable. + * @return a node representing the range constraint. + */ + Node mkRangeConstraint(Node newVar, uint64_t k); + + /** + * In the translation to integers, it is convenient to assume that certain + * bit-vector operators do not occur in the original formula (e.g., repeat). + * This function eliminates all these operators. + */ + Node eliminationPass(Node n); + + /** + * Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more + * than two arguments as a syntactic sugar. + * For example, we can have a node for (bvand x y z), + * that represents (bvand (x (bvand y z))). + * This function makes all such operators strictly binary. + */ + Node makeBinary(Node n); + + /** + * @param k A non-negative integer + * @return A node that represents the constant 2^k + */ + Node pow2(uint64_t k); + + /** + * @param k A positive integer k + * @return A node that represent the constant 2^k-1 + * For example, if k is 4, the result is a node representing the + * constant 15. + */ + Node maxInt(uint64_t k); + + /** + * @param n A node representing an integer term + * @param exponent A non-negative integer + * @return A node representing (n mod (2^exponent)) + */ + Node modpow2(Node n, uint64_t exponent); + + /** + * Add the range assertions collected in d_rangeAssertions + * (using mkRangeConstraint) to the assertion pipeline. + * If there are no range constraints, do nothing. + * If there is a single range constraint, add it to the pipeline. + * Otherwise, add all of them as a single conjunction + */ + void addFinalizeRangeAssertions(AssertionPipeline* assertionsToPreprocess); + + /** + * Caches for the different functions + */ + NodeMap d_binarizeCache; + NodeMap d_eliminationCache; + NodeMap d_rebuildCache; + NodeMap d_bvToIntCache; + + /** + * Node manager that is used throughout the pass + */ + NodeManager* d_nm; + + /** + * A set of constraints of the form 0 <= x < 2^k + * These are added for every new integer variable that we introduce. + */ + unordered_set<Node, NodeHashFunction> d_rangeAssertions; + + /** + * Useful constants + */ + Node d_zero; + Node d_one; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */ |