GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/iand_utils.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
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 CVC4 {
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
13382
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 CVC4
173
174
#endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */