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