Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Utilities to maintain finite tables that represent the value of iand.
11 : : */
12 : :
13 : : #include "theory/arith/nl/iand_utils.h"
14 : :
15 : : #include <cmath>
16 : : #include <limits>
17 : :
18 : : #include "cvc5_private.h"
19 : : #include "theory/arith/nl/nl_model.h"
20 : : #include "theory/rewriter.h"
21 : : #include "util/rational.h"
22 : :
23 : : using namespace cvc5::internal::kind;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace arith {
28 : : namespace nl {
29 : :
30 : 470 : static Rational intpow2(uint32_t b)
31 : : {
32 : : // b must be <= max-int to prevent a failure when using gmp.
33 [ - + ][ - + ]: 470 : Assert(b <= static_cast<uint32_t>(std::numeric_limits<int32_t>::max()));
[ - - ]
34 : 940 : return Rational(Integer(2).pow(b), Integer(1));
35 : : }
36 : :
37 : 470 : Node pow2(NodeManager* nm, uint32_t k)
38 : : {
39 : 940 : return nm->mkConstInt(Rational(intpow2(k)));
40 : : }
41 : :
42 [ + + ][ + + ]: 6372 : bool oneBitAnd(bool a, bool b) { return (a && b); }
43 : :
44 : : // computes (bv_to_int ((_ extract i+size-1 i) (int_to_bv x))))
45 : 188 : Node intExtract(Node x, uint32_t i, uint32_t size)
46 : : {
47 : 188 : NodeManager* nm = x.getNodeManager();
48 [ - + ][ - + ]: 188 : Assert(size > 0);
[ - - ]
49 : : // extract definition in integers is:
50 : : // (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
51 : 564 : Node extract = NodeManager::mkNode(
52 : : Kind::INTS_MODULUS_TOTAL,
53 : 376 : {NodeManager::mkNode(Kind::INTS_DIVISION_TOTAL, x, pow2(nm, i * size)),
54 : 376 : pow2(nm, size)});
55 : 188 : return extract;
56 : : }
57 : :
58 : 119425 : IAndUtils::IAndUtils(NodeManager* nm) : d_nm(nm)
59 : : {
60 : 119425 : d_zero = nm->mkConstInt(Rational(0));
61 : 119425 : d_one = nm->mkConstInt(Rational(1));
62 : 119425 : d_two = nm->mkConstInt(Rational(2));
63 : 119425 : }
64 : :
65 : 161 : Node IAndUtils::createITEFromTable(
66 : : Node x,
67 : : Node y,
68 : : uint32_t granularity,
69 : : const std::map<std::pair<int64_t, int64_t>, uint64_t>& table)
70 : : {
71 [ - + ][ - + ]: 161 : Assert(granularity <= 8);
[ - - ]
72 : 161 : uint64_t num_of_values = ((uint64_t)pow(2, granularity));
73 : : // The table represents a function from pairs of integers to integers, where
74 : : // all integers are between 0 (inclusive) and num_of_values (exclusive).
75 : : // additionally, there is a default value (-1, -1).
76 [ - + ][ - + ]: 161 : Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values)));
[ - - ]
77 : : // start with the default, most common value.
78 : : // this value is represented in the table by (-1, -1).
79 : 161 : Node ite = d_nm->mkConstInt(Rational(table.at(std::make_pair(-1, -1))));
80 [ + + ]: 571 : for (uint64_t i = 0; i < num_of_values; i++)
81 : : {
82 [ + + ]: 2590 : for (uint64_t j = 0; j < num_of_values; j++)
83 : : {
84 : : // skip the most common value, as it was already stored.
85 [ + + ]: 2180 : if (table.at(std::make_pair(i, j)) == table.at(std::make_pair(-1, -1)))
86 : : {
87 : 963 : continue;
88 : : }
89 : : // append the current value to the ite.
90 [ + + ][ - - ]: 7302 : ite = NodeManager::mkNode(
91 : : Kind::ITE,
92 [ + + ][ - - ]: 6085 : {NodeManager::mkNode(
93 : : Kind::AND,
94 : 2434 : {NodeManager::mkNode(
95 : 2434 : Kind::EQUAL, x, d_nm->mkConstInt(Rational(i))),
96 : 2434 : NodeManager::mkNode(
97 : 2434 : Kind::EQUAL, y, d_nm->mkConstInt(Rational(j)))}),
98 : 2434 : d_nm->mkConstInt(Rational(table.at(std::make_pair(i, j)))),
99 : 1217 : ite});
100 : : }
101 : : }
102 : 161 : return ite;
103 : 0 : }
104 : :
105 : 27 : Node IAndUtils::createSumNode(Node x,
106 : : Node y,
107 : : uint32_t bvsize,
108 : : uint32_t granularity)
109 : : {
110 [ + - ][ + - ]: 27 : Assert(0 < granularity && granularity <= 8);
[ - + ][ - + ]
[ - - ]
111 : : // Standardize granularity.
112 : : // If it is greater than bvsize, it is set to bvsize.
113 : : // Otherwise, it is set to the closest (going down) divider of bvsize.
114 [ - + ]: 27 : if (granularity > bvsize)
115 : : {
116 : 0 : granularity = bvsize;
117 : : }
118 : : else
119 : : {
120 [ - + ]: 27 : while (bvsize % granularity != 0)
121 : : {
122 : 0 : granularity = granularity - 1;
123 : : }
124 : : }
125 : :
126 : : // Create the sum.
127 : : // For granularity 1, the sum has bvsize elements.
128 : : // In contrast, if bvsize = granularity, sum has one element.
129 : : // Each element in the sum is an ite that corresponds to the generated table,
130 : : // multiplied by the appropriate power of two.
131 : : // More details are in bv_to_int.h .
132 : :
133 : : // number of elements in the sum expression
134 : 27 : uint32_t sumSize = bvsize / granularity;
135 : : // initialize the sum
136 : 27 : Node sumNode = d_nm->mkConstInt(Rational(0));
137 : : // compute the table for the current granularity if needed
138 [ + + ]: 27 : if (d_bvandTable.find(granularity) == d_bvandTable.end())
139 : : {
140 : 20 : computeAndTable(granularity);
141 : : }
142 : : const std::map<std::pair<int64_t, int64_t>, uint64_t>& table =
143 : 27 : d_bvandTable[granularity];
144 [ + + ]: 121 : for (uint32_t i = 0; i < sumSize; i++)
145 : : {
146 : : // compute the current blocks of x and y
147 : 94 : Node xExtract = intExtract(x, i, granularity);
148 : 94 : Node yExtract = intExtract(y, i, granularity);
149 : : // compute the ite for this part
150 : 188 : Node sumPart = createITEFromTable(xExtract, yExtract, granularity, table);
151 : : // append the current block to the sum
152 : 188 : sumNode = NodeManager::mkNode(
153 : : Kind::ADD,
154 : : sumNode,
155 : 282 : NodeManager::mkNode(Kind::MULT, pow2(d_nm, i * granularity), sumPart));
156 : 94 : }
157 : 27 : return sumNode;
158 : 0 : }
159 : :
160 : 67 : Node IAndUtils::createBitwiseIAndNode(Node x,
161 : : Node y,
162 : : uint32_t high,
163 : : uint32_t low)
164 : : {
165 : 67 : uint32_t granularity = high - low + 1;
166 [ - + ][ - + ]: 67 : Assert(granularity <= 8);
[ - - ]
167 : : // compute the table for the current granularity if needed
168 [ + + ]: 67 : if (d_bvandTable.find(granularity) == d_bvandTable.end())
169 : : {
170 : 29 : computeAndTable(granularity);
171 : : }
172 : : const std::map<std::pair<int64_t, int64_t>, uint64_t>& table =
173 : 67 : d_bvandTable[granularity];
174 : : // Use iextractX and iextractY to ensure deterministic node ID assignments
175 : 67 : Node iextractX = iextract(high, low, x);
176 : 67 : Node iextractY = iextract(high, low, y);
177 : 134 : return createITEFromTable(iextractX, iextractY, granularity, table);
178 : 67 : }
179 : :
180 : 201 : Node IAndUtils::iextract(uint32_t i, uint32_t j, Node n) const
181 : : {
182 : : // ((_ extract i j) n) is n / 2^j mod 2^{i-j+1}
183 : 402 : Node n2j = NodeManager::mkNode(Kind::INTS_DIVISION_TOTAL, n, twoToK(j));
184 : 402 : return NodeManager::mkNode(Kind::INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1));
185 : 201 : }
186 : :
187 : 49 : void IAndUtils::computeAndTable(uint32_t granularity)
188 : : {
189 [ - + ][ - + ]: 49 : Assert(d_bvandTable.find(granularity) == d_bvandTable.end());
[ - - ]
190 : : // the table was not yet computed
191 : 49 : std::map<std::pair<int64_t, int64_t>, uint64_t> table;
192 : 49 : uint64_t num_of_values = ((uint64_t)pow(2, granularity));
193 : : // populate the table with all the values
194 [ + + ]: 235 : for (uint64_t i = 0; i < num_of_values; i++)
195 : : {
196 [ + + ]: 1918 : for (uint64_t j = 0; j < num_of_values; j++)
197 : : {
198 : : // compute
199 : : // (bv_to_int (bvand ((int_to_bv granularity) i) ((int_to_bv granularity)
200 : : // j)))
201 : 1732 : int64_t sum = 0;
202 [ + + ]: 8104 : for (uint64_t n = 0; n < granularity; n++)
203 : : {
204 : : // b is the result of f on the current bit
205 : 6372 : bool b = oneBitAnd((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
206 : : // add the corresponding power of 2 only if the result is 1
207 [ + + ]: 6372 : if (b)
208 : : {
209 : 1593 : sum += 1 << n;
210 : : }
211 : : }
212 : 1732 : table[std::make_pair(i, j)] = sum;
213 : : }
214 : : }
215 : : // optimize the table by identifying and adding the default value
216 : 49 : addDefaultValue(table, num_of_values);
217 [ - + ][ - + ]: 49 : Assert(table.size()
[ - - ]
218 : : == 1 + (static_cast<uint64_t>(num_of_values * num_of_values)));
219 : : // store the table in the cache and return it
220 : 49 : d_bvandTable[granularity] = table;
221 : 49 : }
222 : :
223 : 49 : void IAndUtils::addDefaultValue(
224 : : std::map<std::pair<int64_t, int64_t>, uint64_t>& table,
225 : : uint64_t num_of_values)
226 : : {
227 : : // map each result to the number of times it occurs
228 : 49 : std::map<uint64_t, uint64_t> counters;
229 [ + + ]: 284 : for (uint64_t i = 0; i <= num_of_values; i++)
230 : : {
231 : 235 : counters[i] = 0;
232 : : }
233 [ + + ]: 1781 : for (const auto& element : table)
234 : : {
235 : 1732 : uint64_t result = element.second;
236 : 1732 : counters[result]++;
237 : : }
238 : :
239 : : // compute the most common result
240 : 49 : uint64_t most_common_result = 0;
241 : 49 : uint64_t max_num_of_occ = 0;
242 [ + + ]: 284 : for (uint64_t i = 0; i <= num_of_values; i++)
243 : : {
244 [ + + ]: 235 : if (counters[i] >= max_num_of_occ)
245 : : {
246 : 49 : max_num_of_occ = counters[i];
247 : 49 : most_common_result = i;
248 : : }
249 : : }
250 : : // sanity check: some value appears at least once.
251 [ - + ][ - + ]: 49 : Assert(max_num_of_occ != 0);
[ - - ]
252 : :
253 : : // -1 is the default case of the table.
254 : : // add it to the table
255 : 49 : table[std::make_pair(-1, -1)] = most_common_result;
256 : 49 : }
257 : :
258 : 569 : Node IAndUtils::twoToK(unsigned k) const
259 : : {
260 : : // could be faster
261 : 569 : return d_nm->mkNode(Kind::POW, d_two, d_nm->mkConstInt(Rational(k)));
262 : : }
263 : :
264 : 0 : Node IAndUtils::twoToKMinusOne(unsigned k) const
265 : : {
266 : : // could be faster
267 : 0 : return NodeManager::mkNode(Kind::SUB, twoToK(k), d_one);
268 : : }
269 : :
270 : : } // namespace nl
271 : : } // namespace arith
272 : : } // namespace theory
273 : : } // namespace cvc5::internal
|
