src/theory/arith/nl/iand_utils.h

   1 /*********************                                                        */
   2 /*! \file iand_utils.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Yoni Zohar, Makai Mann, Andrew Reynolds
   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 Utilities to maintain finite tables that represent
  13  ** the value of iand.
  14  **/
  15
  16 #ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
  17 #define CVC4__THEORY__ARITH__IAND_TABLE_H
  18
  19 #include <map>
  20
  21 #include "expr/node.h"
  22
  23 namespace cvc5 {
  24 namespace theory {
  25 namespace arith {
  26 namespace nl {
  27
  28 /**
  29  * A class that computes tables for iand values
  30  * with various bit-widths
  31  */
  32 class IAndUtils
  33 {
  34  public:
  35   IAndUtils();
  36
  37   /**
  38    * A generic function that creates a node that represents a bvand
  39    * operation.
  40    *
  41    * For example: Suppose bvsize is 4, granularity is 1.
  42    * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)).
  43    * The result of this function would be:
  44    * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3
  45    *
  46    * For another example: Suppose bvsize is 4, granularity is 2,
  47    * and f(x,y) = x && y.
  48    * Denote by ITE(a,b) the term that corresponds to the following table:
  49    * a | b |  ITE(a,b)
  50    * ----------------
  51    * 0 | 0 | 0
  52    * 0 | 1 | 0
  53    * 0 | 2 | 0
  54    * 0 | 3 | 0
  55    * 1 | 0 | 0
  56    * 1 | 1 | 1
  57    * 1 | 2 | 0
  58    * 1 | 3 | 1
  59    * 2 | 0 | 0
  60    * 2 | 1 | 0
  61    * 2 | 2 | 2
  62    * 2 | 3 | 2
  63    * 3 | 0 | 0
  64    * 3 | 1 | 1
  65    * 3 | 2 | 2
  66    * 3 | 3 | 3
  67    *
  68    * For example, 2 in binary is 10 and 1 in binary is 01, and so doing
  69    * "bitwise f" on them gives 00.
  70    * The result of this function would be:
  71    * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2
  72    *
  73    * More precisely, the ITE term is optimized so that the most common
  74    * result is in the final "else" branch.
  75    * Hence in practice, the generated ITEs will be shorter.
  76    *
  77    * @param x is an integer operand that correspond to the first original
  78    *        bit-vector operand.
  79    * @param y is an integer operand that correspond to the second original
  80    *        bit-vector operand.
  81    * @param bvsize is the bit width of the original bit-vector variables.
  82    * @param granularity is specified in the options for this preprocessing
  83    *        pass.
  84    * @return A node that represents the operation, as described above.
  85    */
  86   Node createSumNode(Node x, Node y, uint64_t bvsize, uint64_t granularity);
  87
  88   /** Create a bitwise integer And node for two integers x and y for bits
  89    *  between hgih and low Example for high = 0, low = 0 (e.g. granularity 1)
  90    *    ite(x[0] == 1 & y[0] == 1, #b1, #b0)
  91    *
  92    *  It makes use of computeAndTable
  93    *
  94    *  @param x an integer operand corresponding to the first original
  95    *         bit-vector operand
  96    *  @param y an integer operand corresponding to the second original
  97    *         bit-vector operand
  98    *  @param high the upper bit index
  99    *  @param low the lower bit index
 100    *  @return an integer node corresponding to a bitwise AND applied to
 101    *          integers for the bits between high and low
 102    */
 103   Node createBitwiseIAndNode(Node x, Node y, uint64_t high, uint64_t low);
 104
 105   /** extract from integer
 106    *  ((_ extract i j) n) is n / 2^j mod 2^{i-j+1}
 107    */
 108   Node iextract(unsigned i, unsigned j, Node n) const;
 109
 110   // Helpers
 111
 112   /**
 113    * A helper function for createSumNode and createBitwiseIAndNode
 114    * @param x integer node corresponding to the original first bit-vector
 115    *        argument
 116    * @param y integer node corresponding to the original second bit-vector
 117    *        argument nodes.
 118    * @param granularity the bitwidth of the original bit-vector nodes.
 119    * @param table a function from pairs of integers to integers.
 120    *        The domain of this function consists of pairs of
 121    *        integers between 0 (inclusive) and 2^{bitwidth} (exclusive).
 122    *        The domain also includes one additional pair (-1, -1), that
 123    *        represents the default (most common) value.
 124    * @return An ite term that represents this table.
 125    */
 126   Node createITEFromTable(
 127       Node x,
 128       Node y,
 129       uint64_t granularity,
 130       const std::map<std::pair<int64_t, int64_t>, uint64_t>& table);
 131
 132   /**
 133    * updates  d_bvandTable[granularity] if it wasn't already computed.
 134    */
 135   void computeAndTable(uint64_t granularity);
 136
 137   /**
 138    * @param table a table that represents integer conjunction
 139    * @param num_of_values the number of rows in the table
 140    * The function will add a single row to the table.
 141    * the key will be (-1, -1) and the value will be the most common
 142    * value of the original table.
 143    */
 144   void addDefaultValue(std::map<std::pair<int64_t, int64_t>, uint64_t>& table,
 145                        uint64_t num_of_values);
 146
 147   /** 2^k */
 148   Node twoToK(unsigned k) const;
 149
 150   /** 2^k-1 */
 151   Node twoToKMinusOne(unsigned k) const;
 152
 153   /**
 154    * For each granularity between 1 and 8, we store a separate table
 155    * in d_bvandTable[granularity].
 156    * The definition of these tables is given in the description of
 157    * createSumNode.
 158    */
 159   std::map<uint64_t, std::map<std::pair<int64_t, int64_t>, uint64_t>>
 160       d_bvandTable;
 161
 162  private:
 163   /** commonly used terms */
 164   Node d_zero;
 165   Node d_one;
 166   Node d_two;
 167 };
 168
 169 }  // namespace nl
 170 }  // namespace arith
 171 }  // namespace theory
 172 }  // namespace cvc5
 173
 174 #endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */