GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bv_gauss.cpp Lines: 313 344 91.0 %
Date: 2021-03-23 Branches: 676 1688 40.0 %

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