src/preprocessing/passes/bv_to_int.h

   1 /*********************                                                        */
   2 /*! \file bv_to_int.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Yoni Zohar
   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
  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 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 */