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 : : * Gaussian Elimination preprocessing pass.
11 : : *
12 : : * Simplify a given equation system modulo a (prime) number via Gaussian
13 : : * Elimination if possible.
14 : : */
15 : :
16 : : #include "preprocessing/passes/bv_gauss.h"
17 : :
18 : : #include <unordered_map>
19 : : #include <vector>
20 : :
21 : : #include "expr/node.h"
22 : : #include "preprocessing/assertion_pipeline.h"
23 : : #include "preprocessing/preprocessing_pass_context.h"
24 : : #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
25 : : #include "theory/bv/theory_bv_utils.h"
26 : : #include "theory/rewriter.h"
27 : : #include "util/bitvector.h"
28 : :
29 : : using namespace cvc5::internal;
30 : : using namespace cvc5::internal::theory;
31 : : using namespace cvc5::internal::theory::bv;
32 : :
33 : : namespace cvc5::internal {
34 : : namespace preprocessing {
35 : : namespace passes {
36 : :
37 : 3071 : bool BVGauss::is_bv_const(Node n)
38 : : {
39 [ + + ]: 3071 : if (n.isConst())
40 : : {
41 : 999 : return true;
42 : : }
43 : 2072 : return rewrite(n).getKind() == Kind::CONST_BITVECTOR;
44 : : }
45 : :
46 : 489 : Node BVGauss::get_bv_const(Node n)
47 : : {
48 [ - + ][ - + ]: 489 : Assert(is_bv_const(n));
[ - - ]
49 : 489 : return rewrite(n);
50 : : }
51 : :
52 : 267 : Integer BVGauss::get_bv_const_value(Node n)
53 : : {
54 [ - + ][ - + ]: 267 : Assert(is_bv_const(n));
[ - - ]
55 : 534 : return get_bv_const(n).getConst<BitVector>().getValue();
56 : : }
57 : :
58 : : /**
59 : : * Determines if an overflow may occur in given 'expr'.
60 : : *
61 : : * Returns 0 if an overflow may occur, and the minimum required
62 : : * bit-width such that no overflow occurs, otherwise.
63 : : *
64 : : * Note that it would suffice for this function to be Boolean.
65 : : * However, it is handy to determine the minimum required bit-width for
66 : : * debugging purposes.
67 : : *
68 : : * Note: getMinBwExpr assumes that 'expr' is rewritten.
69 : : *
70 : : * If not, all operators that are removed via rewriting (e.g., ror, rol, ...)
71 : : * will be handled via the default case, which is not incorrect but also not
72 : : * necessarily the minimum.
73 : : */
74 : 107 : uint32_t BVGauss::getMinBwExpr(Node expr)
75 : : {
76 : 107 : std::vector<Node> visit;
77 : : /* Maps visited nodes to the determined minimum bit-width required. */
78 : 107 : std::unordered_map<Node, unsigned> visited;
79 : 107 : std::unordered_map<Node, unsigned>::iterator it;
80 : :
81 : 107 : visit.push_back(expr);
82 : 107 : NodeManager* nm = nodeManager();
83 [ + + ]: 1513 : while (!visit.empty())
84 : : {
85 : 1409 : Node n = visit.back();
86 : 1409 : visit.pop_back();
87 : 1409 : it = visited.find(n);
88 [ + + ]: 1409 : if (it == visited.end())
89 : : {
90 [ + + ]: 775 : if (is_bv_const(n))
91 : : {
92 : : /* Rewrite const expr, overflows in consts are irrelevant. */
93 : 222 : visited[n] = get_bv_const(n).getConst<BitVector>().getValue().length();
94 : : }
95 : : else
96 : : {
97 : 553 : visited[n] = 0;
98 : 553 : visit.push_back(n);
99 [ + + ]: 1305 : for (const Node& nn : n)
100 : : {
101 : 752 : visit.push_back(nn);
102 : 752 : }
103 : : }
104 : : }
105 [ + + ]: 634 : else if (it->second == 0)
106 : : {
107 : 551 : Kind k = n.getKind();
108 [ - + ][ - + ]: 551 : Assert(k != Kind::CONST_BITVECTOR);
[ - - ]
109 [ - + ][ - + ]: 551 : Assert(!is_bv_const(n));
[ - - ]
110 [ + + ][ + + ]: 551 : switch (k)
[ + - ][ + + ]
111 : : {
112 : 28 : case Kind::BITVECTOR_EXTRACT:
113 : : {
114 : 28 : const unsigned size = bv::utils::getSize(n);
115 : 28 : const unsigned low = bv::utils::getExtractLow(n);
116 : 28 : const unsigned child_min_width = visited[n[0]];
117 : 28 : visited[n] = std::min(
118 [ + - ]: 28 : size, child_min_width >= low ? child_min_width - low : 0u);
119 [ - + ][ - + ]: 28 : Assert(visited[n] <= visited[n[0]]);
[ - - ]
120 : 28 : break;
121 : : }
122 : :
123 : 36 : case Kind::BITVECTOR_ZERO_EXTEND:
124 : : {
125 : 36 : visited[n] = visited[n[0]];
126 : 36 : break;
127 : : }
128 : :
129 : 69 : case Kind::BITVECTOR_MULT:
130 : : {
131 : 69 : Integer maxval = Integer(1);
132 [ + + ]: 213 : for (const Node& nn : n)
133 : : {
134 [ + + ]: 144 : if (is_bv_const(nn))
135 : : {
136 : 57 : maxval *= get_bv_const_value(nn);
137 : : }
138 : : else
139 : : {
140 : 87 : maxval *= BitVector::mkOnes(visited[nn]).getValue();
141 : : }
142 : 144 : }
143 : 69 : unsigned w = maxval.length();
144 [ + + ]: 69 : if (w > bv::utils::getSize(n))
145 : : {
146 : 2 : return 0;
147 : : } /* overflow */
148 : 67 : visited[n] = w;
149 : 67 : break;
150 [ + + ]: 69 : }
151 : :
152 : 170 : case Kind::BITVECTOR_CONCAT:
153 : : {
154 : : unsigned i, wnz, nc;
155 [ + + ]: 337 : for (i = 0, wnz = 0, nc = n.getNumChildren() - 1; i < nc; ++i)
156 : : {
157 : 195 : unsigned wni = bv::utils::getSize(n[i]);
158 [ + + ]: 195 : if (n[i] != bv::utils::mkZero(nm, wni))
159 : : {
160 : 28 : break;
161 : : }
162 : : /* sum of all bit-widths of leading zero concats */
163 : 167 : wnz += wni;
164 : : }
165 : : /* Do not consider leading zero concats, i.e.,
166 : : * min bw of current concat is determined as
167 : : * min bw of first non-zero term
168 : : * plus actual bw of all subsequent terms */
169 : : // Use nSize to ensure deterministic node ID assignments
170 : 170 : unsigned nSize = bv::utils::getSize(n);
171 : 170 : visited[n] = nSize + visited[n[i]] - bv::utils::getSize(n[i]) - wnz;
172 : 170 : break;
173 : : }
174 : :
175 : 3 : case Kind::BITVECTOR_UREM:
176 : : case Kind::BITVECTOR_LSHR:
177 : : case Kind::BITVECTOR_ASHR:
178 : : {
179 : 3 : visited[n] = visited[n[0]];
180 : 3 : break;
181 : : }
182 : :
183 : 0 : case Kind::BITVECTOR_OR:
184 : : case Kind::BITVECTOR_NOR:
185 : : case Kind::BITVECTOR_XOR:
186 : : case Kind::BITVECTOR_XNOR:
187 : : case Kind::BITVECTOR_AND:
188 : : case Kind::BITVECTOR_NAND:
189 : : {
190 : 0 : unsigned wmax = 0;
191 [ - - ]: 0 : for (const Node& nn : n)
192 : : {
193 [ - - ]: 0 : if (visited[nn] > wmax)
194 : : {
195 : 0 : wmax = visited[nn];
196 : : }
197 : 0 : }
198 : 0 : visited[n] = wmax;
199 : 0 : break;
200 : : }
201 : :
202 : 58 : case Kind::BITVECTOR_ADD:
203 : : {
204 : 58 : Integer maxval = Integer(0);
205 [ + + ]: 200 : for (const Node& nn : n)
206 : : {
207 [ + + ]: 142 : if (is_bv_const(nn))
208 : : {
209 : 6 : maxval += get_bv_const_value(nn);
210 : : }
211 : : else
212 : : {
213 : 136 : maxval += BitVector::mkOnes(visited[nn]).getValue();
214 : : }
215 : 142 : }
216 : 58 : unsigned w = maxval.length();
217 [ + + ]: 58 : if (w > bv::utils::getSize(n))
218 : : {
219 : 1 : return 0;
220 : : } /* overflow */
221 : 57 : visited[n] = w;
222 : 57 : break;
223 [ + + ]: 58 : }
224 : :
225 : 187 : default:
226 : : {
227 : : /* BITVECTOR_UDIV (since x / 0 = -1)
228 : : * BITVECTOR_NOT
229 : : * BITVECTOR_NEG
230 : : * BITVECTOR_SHL */
231 : 187 : visited[n] = bv::utils::getSize(n);
232 : : }
233 : : }
234 : : }
235 [ + + ]: 1409 : }
236 [ - + ][ - + ]: 104 : Assert(visited.find(expr) != visited.end());
[ - - ]
237 : 104 : return visited[expr];
238 : 107 : }
239 : :
240 : : /**
241 : : * Apply Gaussian Elimination modulo a (prime) number.
242 : : * The given equation system is represented as a matrix of Integers.
243 : : *
244 : : * Note that given 'prime' does not have to be prime but can be any
245 : : * arbitrary number. However, if 'prime' is indeed prime, GE is guaranteed
246 : : * to succeed, which is not the case, otherwise.
247 : : *
248 : : * Returns INVALID if GE can not be applied, UNIQUE and PARTIAL if GE was
249 : : * successful, and NONE, otherwise.
250 : : *
251 : : * Vectors 'rhs' and 'lhs' represent the right hand side and left hand side
252 : : * of the given matrix, respectively. The resulting matrix (in row echelon
253 : : * form) is stored in 'rhs' and 'lhs', i.e., the given matrix is overwritten
254 : : * with the resulting matrix.
255 : : */
256 : 73 : BVGauss::Result BVGauss::gaussElim(Integer prime,
257 : : std::vector<Integer>& rhs,
258 : : std::vector<std::vector<Integer>>& lhs)
259 : : {
260 [ - + ][ - + ]: 73 : Assert(prime > 0);
[ - - ]
261 [ - + ][ - + ]: 73 : Assert(lhs.size());
[ - - ]
262 [ - + ][ - + ]: 73 : Assert(lhs.size() == rhs.size());
[ - - ]
263 [ - + ][ - + ]: 73 : Assert(lhs.size() <= lhs[0].size());
[ - - ]
264 : :
265 : : /* special case: zero ring */
266 [ + + ]: 73 : if (prime == 1)
267 : : {
268 : 1 : rhs = std::vector<Integer>(rhs.size(), Integer(0));
269 : 3 : lhs = std::vector<std::vector<Integer>>(
270 : 3 : lhs.size(), std::vector<Integer>(lhs[0].size(), Integer(0)));
271 : 1 : return BVGauss::Result::UNIQUE;
272 : : }
273 : :
274 : 72 : size_t nrows = lhs.size();
275 : 72 : size_t ncols = lhs[0].size();
276 : :
277 : : #ifdef CVC5_ASSERTIONS
278 [ - + ][ - + ]: 201 : for (size_t i = 1; i < nrows; ++i) Assert(lhs[i].size() == ncols);
[ + + ][ - - ]
279 : : #endif
280 : : /* (1) if element in pivot column is non-zero and != 1, divide row elements
281 : : * by element in pivot column modulo prime, i.e., multiply row with
282 : : * multiplicative inverse of element in pivot column modulo prime
283 : : *
284 : : * (2) subtract pivot row from all rows below pivot row
285 : : *
286 : : * (3) subtract (multiple of) current row from all rows above s.t. all
287 : : * elements in current pivot column above current row become equal to one
288 : : *
289 : : * Note: we do not normalize the given matrix to values modulo prime
290 : : * beforehand but on-the-fly. */
291 : :
292 : : /* pivot = lhs[pcol][pcol] */
293 [ + + ][ + + ]: 243 : for (size_t pcol = 0, prow = 0; pcol < ncols && prow < nrows; ++pcol, ++prow)
294 : : {
295 : : /* lhs[j][pcol]: element in pivot column */
296 [ + + ]: 525 : for (size_t j = prow; j < nrows; ++j)
297 : : {
298 : : #ifdef CVC5_ASSERTIONS
299 [ + + ]: 584 : for (size_t k = 0; k < pcol; ++k)
300 : : {
301 [ - + ][ - + ]: 230 : Assert(lhs[j][k] == 0);
[ - - ]
302 : : }
303 : : #endif
304 : : /* normalize element in pivot column to modulo prime */
305 : 354 : lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime);
306 : : /* exchange rows if pivot elem is 0 */
307 [ + + ]: 354 : if (j == prow)
308 : : {
309 [ + + ]: 218 : while (lhs[j][pcol] == 0)
310 : : {
311 [ + + ]: 88 : for (size_t k = prow + 1; k < nrows; ++k)
312 : : {
313 : 56 : lhs[k][pcol] = lhs[k][pcol].euclidianDivideRemainder(prime);
314 [ + + ]: 56 : if (lhs[k][pcol] != 0)
315 : : {
316 : 30 : std::swap(rhs[j], rhs[k]);
317 : 30 : std::swap(lhs[j], lhs[k]);
318 : 30 : break;
319 : : }
320 : : }
321 [ + + ]: 62 : if (pcol >= ncols - 1) break;
322 [ + + ]: 41 : if (lhs[j][pcol] == 0)
323 : : {
324 : 16 : pcol += 1;
325 [ + + ]: 16 : if (lhs[j][pcol] != 0)
326 : 10 : lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime);
327 : : }
328 : : }
329 : : }
330 : :
331 [ + + ]: 354 : if (lhs[j][pcol] != 0)
332 : : {
333 : : /* (1) */
334 [ + + ]: 270 : if (lhs[j][pcol] != 1)
335 : : {
336 : 196 : Integer inv = lhs[j][pcol].modInverse(prime);
337 [ + + ]: 196 : if (inv == -1)
338 : : {
339 : 6 : return BVGauss::Result::INVALID; /* not coprime */
340 : : }
341 [ + + ]: 626 : for (size_t k = pcol; k < ncols; ++k)
342 : : {
343 : 436 : lhs[j][k] = lhs[j][k].modMultiply(inv, prime);
344 [ + + ]: 436 : if (j <= prow) continue; /* pivot */
345 : 246 : lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k], prime);
346 : : }
347 : 190 : rhs[j] = rhs[j].modMultiply(inv, prime);
348 [ + + ]: 190 : if (j > prow)
349 : : {
350 : 92 : rhs[j] = rhs[j].modAdd(-rhs[prow], prime);
351 : : }
352 [ + + ]: 196 : }
353 : : /* (2) */
354 [ + + ]: 74 : else if (j != prow)
355 : : {
356 [ + + ]: 46 : for (size_t k = pcol; k < ncols; ++k)
357 : : {
358 : 34 : lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k], prime);
359 : : }
360 : 12 : rhs[j] = rhs[j].modAdd(-rhs[prow], prime);
361 : : }
362 : : }
363 : : }
364 : : /* (3) */
365 [ + + ]: 314 : for (size_t j = 0; j < prow; ++j)
366 : : {
367 : 143 : Integer mul = lhs[j][pcol];
368 [ + + ]: 143 : if (mul != 0)
369 : : {
370 [ + + ]: 276 : for (size_t k = pcol; k < ncols; ++k)
371 : : {
372 : 162 : lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k] * mul, prime);
373 : : }
374 : 114 : rhs[j] = rhs[j].modAdd(-rhs[prow] * mul, prime);
375 : : }
376 : 143 : }
377 : : }
378 : :
379 : 66 : bool ispart = false;
380 [ + + ]: 245 : for (size_t i = 0; i < nrows; ++i)
381 : : {
382 : 183 : size_t pcol = i;
383 [ + + ][ + + ]: 235 : while (pcol < ncols && lhs[i][pcol] == 0) ++pcol;
[ + + ][ + + ]
[ - - ]
384 [ + + ]: 183 : if (pcol >= ncols)
385 : : {
386 : 29 : rhs[i] = rhs[i].euclidianDivideRemainder(prime);
387 [ + + ]: 29 : if (rhs[i] != 0)
388 : : {
389 : : /* no solution */
390 : 4 : return BVGauss::Result::NONE;
391 : : }
392 : 25 : continue;
393 : : }
394 : : // Normalize rhs to a value modulo prime. Constants subtracted from the
395 : : // rhs while parsing the equations are not reduced modulo prime, and pivot
396 : : // rows with pivot element 1 are not modified during elimination. Hence the
397 : : // rhs may still be negative or exceed prime here.
398 : : // Note: Reducing modulo 2^width via, e.g., the BitVector constructor, would
399 : : // yield an incorrect value, see euclidianDivideRemainder (Boute's
400 : : // Euclidean definition), which always returns a non-negative
401 : : // remainder in [0, prime).
402 : 154 : rhs[i] = rhs[i].euclidianDivideRemainder(prime);
403 [ + + ]: 503 : for (size_t j = i; j < ncols; ++j)
404 : : {
405 [ + + ][ - + ]: 349 : if (lhs[i][j] >= prime || lhs[i][j] <= -prime)
[ + + ][ + + ]
[ - - ]
406 : : {
407 : 1 : lhs[i][j] = lhs[i][j].euclidianDivideRemainder(prime);
408 : : }
409 [ + + ][ + + ]: 349 : if (j > pcol && lhs[i][j] != 0)
[ + + ][ + + ]
[ - - ]
410 : : {
411 : 36 : ispart = true;
412 : : }
413 : : }
414 : : }
415 : :
416 [ + + ]: 62 : if (ispart)
417 : : {
418 : 21 : return BVGauss::Result::PARTIAL;
419 : : }
420 : :
421 : 41 : return BVGauss::Result::UNIQUE;
422 : : }
423 : :
424 : : /**
425 : : * Apply Gaussian Elimination on a set of equations modulo some (prime)
426 : : * number given as bit-vector equations.
427 : : *
428 : : * IMPORTANT: Applying GE modulo some number (rather than modulo 2^bw)
429 : : * on a set of bit-vector equations is only sound if this set of equations
430 : : * has a solution that does not produce overflows. Consequently, we only
431 : : * apply GE if the given bit-width guarantees that no overflows can occur
432 : : * in the given set of equations.
433 : : *
434 : : * Note that the given set of equations does not have to be modulo a prime
435 : : * but can be modulo any arbitrary number. However, if it is indeed modulo
436 : : * prime, GE is guaranteed to succeed, which is not the case, otherwise.
437 : : *
438 : : * Returns INVALID if GE can not be applied, UNIQUE and PARTIAL if GE was
439 : : * successful, and NONE, otherwise.
440 : : *
441 : : * The resulting constraints are stored in 'res' as a mapping of unknown
442 : : * to result (modulo prime). These mapped results are added as constraints
443 : : * of the form 'unknown = mapped result' in applyInternal.
444 : : */
445 : 21 : BVGauss::Result BVGauss::gaussElimRewriteForUrem(
446 : : const std::vector<Node>& equations, std::unordered_map<Node, Node>& res)
447 : : {
448 [ - + ][ - + ]: 21 : Assert(res.empty());
[ - - ]
449 : :
450 : 21 : Node prime;
451 : 21 : Integer iprime;
452 : 21 : std::unordered_map<Node, std::vector<Integer>> vars;
453 : 21 : size_t neqs = equations.size();
454 : 21 : std::vector<Integer> rhs;
455 : : std::vector<std::vector<Integer>> lhs =
456 : 42 : std::vector<std::vector<Integer>>(neqs, std::vector<Integer>());
457 : :
458 : 21 : res = std::unordered_map<Node, Node>();
459 : :
460 : 21 : NodeManager* nm = nodeManager();
461 [ + + ]: 73 : for (size_t i = 0; i < neqs; ++i)
462 : : {
463 : 52 : Node eq = equations[i];
464 [ - + ][ - + ]: 52 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
465 : 52 : Node urem, eqrhs;
466 : :
467 [ + - ]: 52 : if (eq[0].getKind() == Kind::BITVECTOR_UREM)
468 : : {
469 : 52 : urem = eq[0];
470 [ - + ][ - + ]: 52 : Assert(is_bv_const(eq[1]));
[ - - ]
471 : 52 : eqrhs = eq[1];
472 : : }
473 : : else
474 : : {
475 : 0 : Assert(eq[1].getKind() == Kind::BITVECTOR_UREM);
476 : 0 : urem = eq[1];
477 : 0 : Assert(is_bv_const(eq[0]));
478 : 0 : eqrhs = eq[0];
479 : : }
480 [ - + ]: 52 : if (getMinBwExpr(rewrite(urem[0])) == 0)
481 : : {
482 [ - - ]: 0 : Trace("bv-gauss-elim")
483 : : << "Minimum required bit-width exceeds given bit-width, "
484 : 0 : "will not apply Gaussian Elimination."
485 : 0 : << std::endl;
486 : 0 : return BVGauss::Result::INVALID;
487 : : }
488 : 52 : rhs.push_back(get_bv_const_value(eqrhs));
489 : :
490 [ - + ][ - + ]: 52 : Assert(is_bv_const(urem[1]));
[ - - ]
491 : 52 : Assert(i == 0 || get_bv_const_value(urem[1]) == iprime);
492 [ + + ]: 52 : if (i == 0)
493 : : {
494 : 21 : prime = urem[1];
495 : 21 : iprime = get_bv_const_value(prime);
496 : : }
497 : :
498 : 52 : std::unordered_map<Node, Integer> tmp;
499 : 52 : std::vector<Node> stack;
500 : 52 : stack.push_back(urem[0]);
501 [ + + ]: 222 : while (!stack.empty())
502 : : {
503 : 170 : Node n = stack.back();
504 : 170 : stack.pop_back();
505 : :
506 : : /* Subtract from rhs if const */
507 [ + + ]: 170 : if (is_bv_const(n))
508 : : {
509 : 6 : Integer val = get_bv_const_value(n);
510 [ + - ]: 6 : if (val > 0) rhs.back() -= val;
511 : 6 : continue;
512 : 6 : }
513 : :
514 : : /* Split into matrix columns */
515 : 164 : Kind k = n.getKind();
516 [ + + ]: 164 : if (k == Kind::BITVECTOR_ADD)
517 : : {
518 [ + + ]: 177 : for (const Node& nn : n)
519 : : {
520 : 118 : stack.push_back(nn);
521 : 118 : }
522 : : }
523 [ + + ]: 105 : else if (k == Kind::BITVECTOR_MULT)
524 : : {
525 : 94 : Node n0, n1;
526 : : /* Flatten mult expression. */
527 : 94 : n = RewriteRule<FlattenAssocCommut>::run<true>(n);
528 : : /* Split operands into consts and non-consts */
529 : 94 : NodeBuilder nb_consts(nm, k);
530 : 94 : NodeBuilder nb_nonconsts(nm, k);
531 [ + + ]: 290 : for (const Node& nn : n)
532 : : {
533 : 196 : Node nnrw = rewrite(nn);
534 [ + + ]: 196 : if (is_bv_const(nnrw))
535 : : {
536 : 90 : nb_consts << nnrw;
537 : : }
538 : : else
539 : : {
540 : 106 : nb_nonconsts << nnrw;
541 : : }
542 : 196 : }
543 [ - + ][ - + ]: 94 : Assert(nb_nonconsts.getNumChildren() > 0);
[ - - ]
544 : : /* n0 is const */
545 : 94 : unsigned nc = nb_consts.getNumChildren();
546 [ - + ]: 94 : if (nc > 1)
547 : : {
548 : 0 : n0 = rewrite(nb_consts.constructNode());
549 : : }
550 [ + + ]: 94 : else if (nc == 1)
551 : : {
552 : 90 : n0 = nb_consts[0];
553 : : }
554 : : else
555 : : {
556 : 4 : n0 = bv::utils::mkOne(nm, bv::utils::getSize(n));
557 : : }
558 : : /* n1 is a mult with non-const operands */
559 [ + + ]: 94 : if (nb_nonconsts.getNumChildren() > 1)
560 : : {
561 : 10 : n1 = rewrite(nb_nonconsts.constructNode());
562 : : }
563 : : else
564 : : {
565 : 84 : n1 = nb_nonconsts[0];
566 : : }
567 [ - + ][ - + ]: 94 : Assert(is_bv_const(n0));
[ - - ]
568 [ - + ][ - + ]: 94 : Assert(!is_bv_const(n1));
[ - - ]
569 : 94 : tmp[n1] += get_bv_const_value(n0);
570 : 94 : }
571 : : else
572 : : {
573 : 11 : tmp[n] += Integer(1);
574 : : }
575 [ + + ]: 170 : }
576 : :
577 : : /* Note: "var" is not necessarily a VARIABLE but can be an arbitrary expr */
578 : :
579 [ + + ]: 157 : for (const auto& p : tmp)
580 : : {
581 : 105 : Node var = p.first;
582 : 105 : Integer val = p.second;
583 [ + + ][ + + ]: 105 : if (i > 0 && vars.find(var) == vars.end())
[ + + ]
584 : : {
585 : : /* Add column and fill column elements of rows above with 0. */
586 : 17 : vars[var].insert(vars[var].end(), i, Integer(0));
587 : : }
588 : 105 : vars[var].push_back(val);
589 : 105 : }
590 : :
591 [ + + ]: 181 : for (const auto& p : vars)
592 : : {
593 [ + + ]: 129 : if (tmp.find(p.first) == tmp.end())
594 : : {
595 : 24 : vars[p.first].push_back(Integer(0));
596 : : }
597 : : }
598 [ + - ][ + - ]: 52 : }
[ + - ]
599 : :
600 : 21 : size_t nvars = vars.size();
601 [ - + ]: 21 : if (nvars == 0)
602 : : {
603 : 0 : return BVGauss::Result::INVALID;
604 : : }
605 : 21 : size_t nrows = vars.begin()->second.size();
606 : : #ifdef CVC5_ASSERTIONS
607 [ + + ]: 80 : for (const auto& p : vars)
608 : : {
609 [ - + ][ - + ]: 59 : Assert(p.second.size() == nrows);
[ - - ]
610 : : }
611 : : #endif
612 : :
613 [ - + ]: 21 : if (nrows < 1)
614 : : {
615 : 0 : return BVGauss::Result::INVALID;
616 : : }
617 : :
618 [ + + ]: 73 : for (size_t i = 0; i < nrows; ++i)
619 : : {
620 [ + + ]: 200 : for (const auto& p : vars)
621 : : {
622 : 148 : lhs[i].push_back(p.second[i]);
623 : : }
624 : : }
625 : :
626 : : #ifdef CVC5_ASSERTIONS
627 [ + + ]: 73 : for (const auto& row : lhs)
628 : : {
629 [ - + ][ - + ]: 52 : Assert(row.size() == nvars);
[ - - ]
630 : : }
631 [ - + ][ - + ]: 21 : Assert(lhs.size() == rhs.size());
[ - - ]
632 : : #endif
633 : :
634 [ + + ]: 21 : if (lhs.size() > lhs[0].size())
635 : : {
636 : 1 : return BVGauss::Result::INVALID;
637 : : }
638 : :
639 [ + - ]: 20 : Trace("bv-gauss-elim") << "Applying Gaussian Elimination..." << std::endl;
640 : 20 : BVGauss::Result ret = gaussElim(iprime, rhs, lhs);
641 : :
642 [ + - ][ + - ]: 20 : if (ret != BVGauss::Result::NONE && ret != BVGauss::Result::INVALID)
643 : : {
644 : 20 : std::vector<Node> vvars;
645 [ + + ]: 77 : for (const auto& p : vars)
646 : : {
647 : 57 : vvars.push_back(p.first);
648 : : }
649 [ - + ][ - + ]: 20 : Assert(nvars == vvars.size());
[ - - ]
650 [ - + ][ - + ]: 20 : Assert(nrows == lhs.size());
[ - - ]
651 [ - + ][ - + ]: 20 : Assert(nrows == rhs.size());
[ - - ]
652 [ + + ]: 20 : if (ret == BVGauss::Result::UNIQUE)
653 : : {
654 [ + + ]: 36 : for (size_t i = 0; i < nvars; ++i)
655 : : {
656 : 52 : res[vvars[i]] = nm->mkConst<BitVector>(
657 : 78 : BitVector(bv::utils::getSize(vvars[i]), rhs[i]));
658 : : }
659 : : }
660 : : else
661 : : {
662 [ - + ][ - + ]: 10 : Assert(ret == BVGauss::Result::PARTIAL);
[ - - ]
663 : :
664 [ + - ][ + + ]: 30 : for (size_t pcol = 0, prow = 0; pcol < nvars && prow < nrows;
665 : 20 : ++pcol, ++prow)
666 : : {
667 : 22 : Assert(lhs[prow][pcol] == 0 || lhs[prow][pcol] == 1);
668 [ + + ][ + + ]: 25 : while (pcol < nvars && lhs[prow][pcol] == 0) pcol += 1;
[ + + ][ + + ]
[ - - ]
669 [ + + ]: 22 : if (pcol >= nvars)
670 : : {
671 [ - + ][ - + ]: 2 : Assert(rhs[prow] == 0);
[ - - ]
672 : 2 : break;
673 : : }
674 [ - + ]: 20 : if (lhs[prow][pcol] == 0)
675 : : {
676 : 0 : Assert(rhs[prow] == 0);
677 : 0 : continue;
678 : : }
679 [ - + ][ - + ]: 20 : Assert(lhs[prow][pcol] == 1);
[ - - ]
680 : 20 : std::vector<Node> stack;
681 [ + + ]: 51 : for (size_t i = pcol + 1; i < nvars; ++i)
682 : : {
683 [ + + ]: 31 : if (lhs[prow][i] == 0) continue;
684 : : /* Normalize (no negative numbers, hence no subtraction)
685 : : * e.g., x = 4 - 2y --> x = 4 + 9y (modulo 11) */
686 : 17 : Integer m = iprime - lhs[prow][i];
687 : 17 : Node bv = bv::utils::mkConst(nm, bv::utils::getSize(vvars[i]), m);
688 : 34 : Node mult = nm->mkNode(Kind::BITVECTOR_MULT, vvars[i], bv);
689 : 17 : stack.push_back(mult);
690 : 17 : }
691 : :
692 [ + + ]: 20 : if (stack.empty())
693 : : {
694 : 6 : res[vvars[pcol]] = nm->mkConst<BitVector>(
695 : 9 : BitVector(bv::utils::getSize(vvars[pcol]), rhs[prow]));
696 : : }
697 : : else
698 : : {
699 : 34 : Node tmp = stack.size() == 1 ? stack[0]
700 [ + - ]: 34 : : nm->mkNode(Kind::BITVECTOR_ADD, stack);
701 : :
702 [ + + ]: 17 : if (rhs[prow] != 0)
703 : : {
704 : : tmp =
705 : 64 : nm->mkNode(Kind::BITVECTOR_ADD,
706 : 32 : bv::utils::mkConst(
707 : 16 : nm, bv::utils::getSize(vvars[pcol]), rhs[prow]),
708 : 16 : tmp);
709 : : }
710 [ - + ][ - + ]: 17 : Assert(!is_bv_const(tmp));
[ - - ]
711 : 17 : res[vvars[pcol]] = nm->mkNode(Kind::BITVECTOR_UREM, tmp, prime);
712 : 17 : }
713 : 20 : }
714 : : }
715 : 20 : }
716 : 20 : return ret;
717 : 21 : }
718 : :
719 : 28747 : BVGauss::BVGauss(PreprocessingPassContext* preprocContext,
720 : 28747 : const std::string& name)
721 : 28747 : : PreprocessingPass(preprocContext, name)
722 : : {
723 : 28747 : }
724 : :
725 : 5 : PreprocessingPassResult BVGauss::applyInternal(
726 : : AssertionPipeline* assertionsToPreprocess)
727 : : {
728 : 5 : std::vector<Node> assertions(assertionsToPreprocess->ref());
729 : 5 : std::unordered_map<Node, std::vector<Node>> equations;
730 : :
731 [ + + ]: 19 : while (!assertions.empty())
732 : : {
733 : 14 : Node a = assertions.back();
734 : 14 : assertions.pop_back();
735 : 14 : cvc5::internal::Kind k = a.getKind();
736 : :
737 [ - + ]: 14 : if (k == Kind::AND)
738 : : {
739 [ - - ]: 0 : for (const Node& aa : a)
740 : : {
741 : 0 : assertions.push_back(aa);
742 : 0 : }
743 : : }
744 [ + - ]: 14 : else if (k == Kind::EQUAL)
745 : : {
746 : 14 : Node urem;
747 : :
748 : 14 : if (is_bv_const(a[1]) && a[0].getKind() == Kind::BITVECTOR_UREM)
749 : : {
750 : 14 : urem = a[0];
751 : : }
752 : 0 : else if (is_bv_const(a[0]) && a[1].getKind() == Kind::BITVECTOR_UREM)
753 : : {
754 : 0 : urem = a[1];
755 : : }
756 : : else
757 : : {
758 : 0 : continue;
759 : : }
760 : :
761 : 14 : if (urem[0].getKind() == Kind::BITVECTOR_ADD && is_bv_const(urem[1]))
762 : : {
763 : 14 : equations[urem[1]].push_back(a);
764 : : }
765 [ + - ]: 14 : }
766 [ + - ]: 14 : }
767 : :
768 : 5 : std::unordered_map<Node, Node> subst;
769 : :
770 : 5 : NodeManager* nm = nodeManager();
771 [ + + ]: 11 : for (const auto& eq : equations)
772 : : {
773 [ - + ]: 6 : if (eq.second.size() <= 1)
774 : : {
775 : 0 : continue;
776 : : }
777 : :
778 : 6 : std::unordered_map<Node, Node> res;
779 : 6 : BVGauss::Result ret = gaussElimRewriteForUrem(eq.second, res);
780 [ + - ]: 12 : Trace("bv-gauss-elim") << "result: "
781 : : << (ret == BVGauss::Result::INVALID
782 [ - - ]: 6 : ? "INVALID"
783 : : : (ret == BVGauss::Result::UNIQUE
784 [ - - ]: 0 : ? "UNIQUE"
785 : : : (ret == BVGauss::Result::PARTIAL
786 [ - - ]: 0 : ? "PARTIAL"
787 : 0 : : "NONE")))
788 : 6 : << std::endl;
789 [ + - ]: 6 : if (ret != BVGauss::Result::INVALID)
790 : : {
791 [ - + ]: 6 : if (ret == BVGauss::Result::NONE)
792 : : {
793 : 0 : Node n = nm->mkConst<bool>(false);
794 : 0 : assertionsToPreprocess->push_back(
795 : : n, false, nullptr, TrustId::PREPROCESS_BV_GUASS_LEMMA);
796 : 0 : return PreprocessingPassResult::CONFLICT;
797 : 0 : }
798 : : else
799 : : {
800 [ + + ]: 20 : for (const Node& e : eq.second)
801 : : {
802 : 14 : subst[e] = nm->mkConst<bool>(true);
803 : : }
804 : : /* add resulting constraints */
805 [ + + ]: 20 : for (const auto& p : res)
806 : : {
807 : 28 : Node a = nm->mkNode(Kind::EQUAL, p.first, p.second);
808 [ + - ]: 14 : Trace("bv-gauss-elim") << "added assertion: " << a << std::endl;
809 : : // add new assertion
810 : 14 : assertionsToPreprocess->push_back(
811 : : a, false, nullptr, TrustId::PREPROCESS_BV_GUASS_LEMMA);
812 : 14 : }
813 : : }
814 : : }
815 [ + - ]: 6 : }
816 : :
817 [ + - ]: 5 : if (!subst.empty())
818 : : {
819 : : /* delete (= substitute with true) obsolete assertions */
820 : 5 : const std::vector<Node>& aref = assertionsToPreprocess->ref();
821 [ + + ]: 33 : for (size_t i = 0, asize = aref.size(); i < asize; ++i)
822 : : {
823 : 28 : Node a = aref[i];
824 : 28 : Node as = a.substitute(subst.begin(), subst.end());
825 : : // replace the assertion
826 : 28 : assertionsToPreprocess->replace(
827 : : i, as, nullptr, TrustId::PREPROCESS_BV_GUASS);
828 : 28 : }
829 : : }
830 : 5 : return PreprocessingPassResult::NO_CONFLICT;
831 : 5 : }
832 : :
833 : : } // namespace passes
834 : : } // namespace preprocessing
835 : : } // namespace cvc5::internal
|
