GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/preprocessing/pass_bv_gauss_white.cpp Lines: 1279 1314 97.3 %
Date: 2021-03-23 Branches: 4785 11225 42.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file pass_bv_gauss_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Mathias Preiner, Andres Noetzli
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 Unit tests for Gaussian Elimination preprocessing pass.
13
 **
14
 ** Unit tests for Gaussian Elimination preprocessing pass.
15
 **/
16
17
#include <iostream>
18
#include <vector>
19
20
#include "context/context.h"
21
#include "expr/node.h"
22
#include "expr/node_manager.h"
23
#include "preprocessing/assertion_pipeline.h"
24
#include "preprocessing/passes/bv_gauss.h"
25
#include "smt/smt_engine.h"
26
#include "smt/smt_engine_scope.h"
27
#include "test_smt.h"
28
#include "theory/bv/theory_bv_utils.h"
29
#include "theory/rewriter.h"
30
#include "util/bitvector.h"
31
32
namespace CVC4 {
33
34
using namespace preprocessing;
35
using namespace preprocessing::passes;
36
using namespace theory;
37
using namespace smt;
38
39
namespace test {
40
41
148
class TestPPWhiteBVGauss : public TestSmt
42
{
43
 protected:
44
74
  void SetUp() override
45
  {
46
74
    TestSmt::SetUp();
47
48
74
    d_zero = bv::utils::mkZero(16);
49
50
148
    d_p = bv::utils::mkConcat(
51
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 11u)));
52
148
    d_x = bv::utils::mkConcat(
53
222
        d_zero, d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)));
54
148
    d_y = bv::utils::mkConcat(
55
222
        d_zero, d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)));
56
148
    d_z = bv::utils::mkConcat(
57
222
        d_zero, d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16)));
58
59
148
    d_one = bv::utils::mkConcat(
60
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 1u)));
61
148
    d_two = bv::utils::mkConcat(
62
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 2u)));
63
148
    d_three = bv::utils::mkConcat(
64
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 3u)));
65
148
    d_four = bv::utils::mkConcat(
66
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 4u)));
67
148
    d_five = bv::utils::mkConcat(
68
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 5u)));
69
148
    d_six = bv::utils::mkConcat(
70
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 6u)));
71
148
    d_seven = bv::utils::mkConcat(
72
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 7u)));
73
148
    d_eight = bv::utils::mkConcat(
74
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 8u)));
75
148
    d_nine = bv::utils::mkConcat(
76
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 9u)));
77
148
    d_ten = bv::utils::mkConcat(
78
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 10u)));
79
148
    d_twelve = bv::utils::mkConcat(
80
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 12u)));
81
148
    d_eighteen = bv::utils::mkConcat(
82
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 18u)));
83
148
    d_twentyfour = bv::utils::mkConcat(
84
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 24u)));
85
148
    d_thirty = bv::utils::mkConcat(
86
222
        d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 30u)));
87
88
74
    d_one32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 1u));
89
74
    d_two32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 2u));
90
74
    d_three32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 3u));
91
74
    d_four32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 4u));
92
74
    d_five32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 5u));
93
74
    d_six32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 6u));
94
74
    d_seven32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 7u));
95
74
    d_eight32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 8u));
96
74
    d_nine32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 9u));
97
74
    d_ten32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 10u));
98
99
74
    d_x_mul_one = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_one);
100
74
    d_x_mul_two = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_two);
101
74
    d_x_mul_four = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four);
102
74
    d_y_mul_three = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three);
103
74
    d_y_mul_one = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_one);
104
74
    d_y_mul_four = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_four);
105
74
    d_y_mul_five = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_five);
106
74
    d_y_mul_seven = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven);
107
74
    d_z_mul_one = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_one);
108
74
    d_z_mul_three = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_three);
109
74
    d_z_mul_five = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_five);
110
74
    d_z_mul_six = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_six);
111
74
    d_z_mul_twelve = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_twelve);
112
74
    d_z_mul_nine = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_nine);
113
74
  }
114
115
212
  void print_matrix_dbg(std::vector<Integer>& rhs,
116
                        std::vector<std::vector<Integer>>& lhs)
117
  {
118
832
    for (size_t m = 0, nrows = lhs.size(), ncols = lhs[0].size(); m < nrows;
119
         ++m)
120
    {
121
2508
      for (size_t n = 0; n < ncols; ++n)
122
      {
123
1888
        std::cout << " " << lhs[m][n];
124
      }
125
620
      std::cout << " " << rhs[m];
126
620
      std::cout << std::endl;
127
    }
128
212
  }
129
130
106
  void testGaussElimX(Integer prime,
131
                      std::vector<Integer> rhs,
132
                      std::vector<std::vector<Integer>> lhs,
133
                      BVGauss::Result expected,
134
                      std::vector<Integer>* rrhs = nullptr,
135
                      std::vector<std::vector<Integer>>* rlhs = nullptr)
136
  {
137
106
    size_t nrows = lhs.size();
138
106
    size_t ncols = lhs[0].size();
139
    BVGauss::Result ret;
140
212
    std::vector<Integer> resrhs = std::vector<Integer>(rhs);
141
    std::vector<std::vector<Integer>> reslhs =
142
212
        std::vector<std::vector<Integer>>(lhs);
143
144
106
    std::cout << "Input: " << std::endl;
145
106
    print_matrix_dbg(rhs, lhs);
146
147
106
    ret = BVGauss::gaussElim(prime, resrhs, reslhs);
148
149
    std::cout << "BVGauss::Result: "
150
106
              << (ret == BVGauss::Result::INVALID
151
                      ? "INVALID"
152
94
                      : (ret == BVGauss::Result::UNIQUE
153
124
                             ? "UNIQUE"
154
30
                             : (ret == BVGauss::Result::PARTIAL ? "PARTIAL"
155
306
                                                                : "NONE")))
156
106
              << std::endl;
157
106
    print_matrix_dbg(resrhs, reslhs);
158
159
106
    ASSERT_EQ(expected, ret);
160
161
106
    if (expected == BVGauss::Result::UNIQUE)
162
    {
163
      /* map result value to column index
164
       * e.g.:
165
       * 1 0 0 2  -> res = { 2, 0, 3}
166
       * 0 0 1 3 */
167
128
      std::vector<Integer> res = std::vector<Integer>(ncols, Integer(0));
168
254
      for (size_t i = 0; i < nrows; ++i)
169
768
        for (size_t j = 0; j < ncols; ++j)
170
        {
171
578
          if (reslhs[i][j] == 1)
172
158
            res[j] = resrhs[i];
173
          else
174
420
            ASSERT_EQ(reslhs[i][j], 0);
175
        }
176
177
254
      for (size_t i = 0; i < nrows; ++i)
178
      {
179
380
        Integer tmp = Integer(0);
180
768
        for (size_t j = 0; j < ncols; ++j)
181
578
          tmp = tmp.modAdd(lhs[i][j].modMultiply(res[j], prime), prime);
182
190
        ASSERT_EQ(tmp, rhs[i].euclidianDivideRemainder(prime));
183
      }
184
    }
185
106
    if (rrhs != nullptr && rlhs != nullptr)
186
    {
187
64
      for (size_t i = 0; i < nrows; ++i)
188
      {
189
192
        for (size_t j = 0; j < ncols; ++j)
190
        {
191
144
          ASSERT_EQ(reslhs[i][j], (*rlhs)[i][j]);
192
        }
193
48
        ASSERT_EQ(resrhs[i], (*rrhs)[i]);
194
      }
195
    }
196
  }
197
198
  Node d_p;
199
  Node d_x;
200
  Node d_y;
201
  Node d_z;
202
  Node d_zero;
203
  Node d_one;
204
  Node d_two;
205
  Node d_three;
206
  Node d_four;
207
  Node d_five;
208
  Node d_six;
209
  Node d_seven;
210
  Node d_eight;
211
  Node d_nine;
212
  Node d_ten;
213
  Node d_twelve;
214
  Node d_eighteen;
215
  Node d_twentyfour;
216
  Node d_thirty;
217
  Node d_one32;
218
  Node d_two32;
219
  Node d_three32;
220
  Node d_four32;
221
  Node d_five32;
222
  Node d_six32;
223
  Node d_seven32;
224
  Node d_eight32;
225
  Node d_nine32;
226
  Node d_ten32;
227
  Node d_x_mul_one;
228
  Node d_x_mul_two;
229
  Node d_x_mul_four;
230
  Node d_y_mul_one;
231
  Node d_y_mul_three;
232
  Node d_y_mul_four;
233
  Node d_y_mul_five;
234
  Node d_y_mul_seven;
235
  Node d_z_mul_one;
236
  Node d_z_mul_three;
237
  Node d_z_mul_five;
238
  Node d_z_mul_twelve;
239
  Node d_z_mul_six;
240
  Node d_z_mul_nine;
241
};
242
243
46
TEST_F(TestPPWhiteBVGauss, elim_mod)
244
{
245
4
  std::vector<Integer> rhs;
246
4
  std::vector<std::vector<Integer>> lhs;
247
248
  /* -------------------------------------------------------------------
249
   *   lhs   rhs  modulo { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 }
250
   *  --^--   ^
251
   *  1 1 1   5
252
   *  2 3 5   8
253
   *  4 0 5   2
254
   * ------------------------------------------------------------------- */
255
2
  rhs = {Integer(5), Integer(8), Integer(2)};
256
26
  lhs = {{Integer(1), Integer(1), Integer(1)},
257
         {Integer(2), Integer(3), Integer(5)},
258
24
         {Integer(4), Integer(0), Integer(5)}};
259
2
  std::cout << "matrix 0, modulo 0" << std::endl;  // throws
260
2
  ASSERT_DEATH(BVGauss::gaussElim(Integer(0), rhs, lhs), "prime > 0");
261
2
  std::cout << "matrix 0, modulo 1" << std::endl;
262
2
  testGaussElimX(Integer(1), rhs, lhs, BVGauss::Result::UNIQUE);
263
2
  std::cout << "matrix 0, modulo 2" << std::endl;
264
2
  testGaussElimX(Integer(2), rhs, lhs, BVGauss::Result::UNIQUE);
265
2
  std::cout << "matrix 0, modulo 3" << std::endl;
266
2
  testGaussElimX(Integer(3), rhs, lhs, BVGauss::Result::UNIQUE);
267
2
  std::cout << "matrix 0, modulo 4" << std::endl;  // no inverse
268
2
  testGaussElimX(Integer(4), rhs, lhs, BVGauss::Result::INVALID);
269
2
  std::cout << "matrix 0, modulo 5" << std::endl;
270
2
  testGaussElimX(Integer(5), rhs, lhs, BVGauss::Result::UNIQUE);
271
2
  std::cout << "matrix 0, modulo 6" << std::endl;  // no inverse
272
2
  testGaussElimX(Integer(6), rhs, lhs, BVGauss::Result::INVALID);
273
2
  std::cout << "matrix 0, modulo 7" << std::endl;
274
2
  testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
275
2
  std::cout << "matrix 0, modulo 8" << std::endl;  // no inverse
276
2
  testGaussElimX(Integer(8), rhs, lhs, BVGauss::Result::INVALID);
277
2
  std::cout << "matrix 0, modulo 9" << std::endl;
278
2
  testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::UNIQUE);
279
2
  std::cout << "matrix 0, modulo 10" << std::endl;  // no inverse
280
2
  testGaussElimX(Integer(10), rhs, lhs, BVGauss::Result::INVALID);
281
2
  std::cout << "matrix 0, modulo 11" << std::endl;
282
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
283
}
284
285
46
TEST_F(TestPPWhiteBVGauss, elim_unique_done)
286
{
287
4
  std::vector<Integer> rhs;
288
4
  std::vector<std::vector<Integer>> lhs;
289
290
  /* -------------------------------------------------------------------
291
   *   lhs     rhs        lhs    rhs  modulo 17
292
   *  --^---    ^        --^--    ^
293
   *  1 0 0    4   -->   1 0 0    4
294
   *  0 1 0   15         0 1 0   15
295
   *  0 0 1    3         0 0 1    3
296
   * ------------------------------------------------------------------- */
297
2
  rhs = {Integer(4), Integer(15), Integer(3)};
298
26
  lhs = {{Integer(1), Integer(0), Integer(0)},
299
         {Integer(0), Integer(1), Integer(0)},
300
24
         {Integer(0), Integer(0), Integer(1)}};
301
2
  std::cout << "matrix 1, modulo 17" << std::endl;
302
2
  testGaussElimX(Integer(17), rhs, lhs, BVGauss::Result::UNIQUE);
303
2
}
304
305
46
TEST_F(TestPPWhiteBVGauss, elim_unique)
306
{
307
4
  std::vector<Integer> rhs;
308
4
  std::vector<std::vector<Integer>> lhs;
309
310
  /* -------------------------------------------------------------------
311
   *   lhs     rhs  modulo { 11,17,59 }
312
   *  --^---    ^
313
   *  2 4  6   18
314
   *  4 5  6   24
315
   *  3 1 -2    4
316
   * ------------------------------------------------------------------- */
317
2
  rhs = {Integer(18), Integer(24), Integer(4)};
318
26
  lhs = {{Integer(2), Integer(4), Integer(6)},
319
         {Integer(4), Integer(5), Integer(6)},
320
24
         {Integer(3), Integer(1), Integer(-2)}};
321
2
  std::cout << "matrix 2, modulo 11" << std::endl;
322
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
323
2
  std::cout << "matrix 2, modulo 17" << std::endl;
324
2
  testGaussElimX(Integer(17), rhs, lhs, BVGauss::Result::UNIQUE);
325
2
  std::cout << "matrix 2, modulo 59" << std::endl;
326
2
  testGaussElimX(Integer(59), rhs, lhs, BVGauss::Result::UNIQUE);
327
328
  /* -------------------------------------------------------------------
329
   *      lhs       rhs         lhs     rhs   modulo 11
330
   *  -----^-----    ^        ---^---    ^
331
   *  1  1  2   0    1   -->  1 0 0 0    1
332
   *  2 -1  0   1   -2        0 1 0 0    2
333
   *  1 -1 -1  -2    4        0 0 1 0   -1
334
   *  2 -1  2  -1    0        0 0 0 1   -2
335
   * ------------------------------------------------------------------- */
336
2
  rhs = {Integer(1), Integer(-2), Integer(4), Integer(0)};
337
42
  lhs = {{Integer(1), Integer(1), Integer(2), Integer(0)},
338
         {Integer(2), Integer(-1), Integer(0), Integer(1)},
339
         {Integer(1), Integer(-1), Integer(-1), Integer(-2)},
340
40
         {Integer(2), Integer(-1), Integer(2), Integer(-1)}};
341
2
  std::cout << "matrix 3, modulo 11" << std::endl;
342
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
343
2
}
344
345
46
TEST_F(TestPPWhiteBVGauss, elim_unique_zero1)
346
{
347
4
  std::vector<Integer> rhs;
348
4
  std::vector<std::vector<Integer>> lhs;
349
350
  /* -------------------------------------------------------------------
351
   *   lhs   rhs        lhs   rhs   modulo 11
352
   *  --^--   ^        --^--   ^
353
   *  0 4 5   2   -->  1 0 0   4
354
   *  1 1 1   5        0 1 0   3
355
   *  3 2 5   8        0 0 1   9
356
   * ------------------------------------------------------------------- */
357
2
  rhs = {Integer(2), Integer(5), Integer(8)};
358
26
  lhs = {{Integer(0), Integer(4), Integer(5)},
359
         {Integer(1), Integer(1), Integer(1)},
360
24
         {Integer(3), Integer(2), Integer(5)}};
361
2
  std::cout << "matrix 4, modulo 11" << std::endl;
362
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
363
364
  /* -------------------------------------------------------------------
365
   *   lhs   rhs        lhs   rhs   modulo 11
366
   *  --^--   ^        --^--   ^
367
   *  1 1 1   5   -->  1 0 0   4
368
   *  0 4 5   2        0 1 0   3
369
   *  3 2 5   8        0 0 1   9
370
   * ------------------------------------------------------------------- */
371
2
  rhs = {Integer(5), Integer(2), Integer(8)};
372
26
  lhs = {{Integer(1), Integer(1), Integer(1)},
373
         {Integer(0), Integer(4), Integer(5)},
374
24
         {Integer(3), Integer(2), Integer(5)}};
375
2
  std::cout << "matrix 5, modulo 11" << std::endl;
376
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
377
378
  /* -------------------------------------------------------------------
379
   *   lhs   rhs        lhs   rhs   modulo 11
380
   *  --^--   ^        --^--   ^
381
   *  1 1 1   5   -->  1 0 0   4
382
   *  3 2 5   8        0 1 0   9
383
   *  0 4 5   2        0 0 1   3
384
   * ------------------------------------------------------------------- */
385
2
  rhs = {Integer(5), Integer(8), Integer(2)};
386
26
  lhs = {{Integer(1), Integer(1), Integer(1)},
387
         {Integer(3), Integer(2), Integer(5)},
388
24
         {Integer(0), Integer(4), Integer(5)}};
389
2
  std::cout << "matrix 6, modulo 11" << std::endl;
390
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
391
2
}
392
393
46
TEST_F(TestPPWhiteBVGauss, elim_unique_zero2)
394
{
395
4
  std::vector<Integer> rhs;
396
4
  std::vector<std::vector<Integer>> lhs;
397
398
  /* -------------------------------------------------------------------
399
   *   lhs   rhs        lhs   rhs   modulo 11
400
   *  --^--   ^        --^--   ^
401
   *  0 0 5   2        1 0 0   10
402
   *  1 1 1   5   -->  0 1 0   10
403
   *  3 2 5   8        0 0 1   7
404
   * ------------------------------------------------------------------- */
405
2
  rhs = {Integer(2), Integer(5), Integer(8)};
406
26
  lhs = {{Integer(0), Integer(0), Integer(5)},
407
         {Integer(1), Integer(1), Integer(1)},
408
24
         {Integer(3), Integer(2), Integer(5)}};
409
2
  std::cout << "matrix 7, modulo 11" << std::endl;
410
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
411
412
  /* -------------------------------------------------------------------
413
   *   lhs   rhs        lhs   rhs   modulo 11
414
   *  --^--   ^        --^--   ^
415
   *  1 1 1   5   -->  1 0 0   10
416
   *  0 0 5   2        0 1 0   10
417
   *  3 2 5   8        0 0 1   7
418
   * ------------------------------------------------------------------- */
419
2
  rhs = {Integer(5), Integer(2), Integer(8)};
420
26
  lhs = {{Integer(1), Integer(1), Integer(1)},
421
         {Integer(0), Integer(0), Integer(5)},
422
24
         {Integer(3), Integer(2), Integer(5)}};
423
2
  std::cout << "matrix 8, modulo 11" << std::endl;
424
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
425
426
  /* -------------------------------------------------------------------
427
   *   lhs   rhs        lhs   rhs   modulo 11
428
   *  --^--   ^        --^--   ^
429
   *  1 1 1   5   -->  1 0 0   10
430
   *  3 2 5   8        0 1 0   10
431
   *  0 0 5   2        0 0 1    7
432
   * ------------------------------------------------------------------- */
433
2
  rhs = {Integer(5), Integer(8), Integer(2)};
434
26
  lhs = {{Integer(1), Integer(1), Integer(1)},
435
         {Integer(3), Integer(2), Integer(5)},
436
24
         {Integer(0), Integer(0), Integer(5)}};
437
2
  std::cout << "matrix 9, modulo 11" << std::endl;
438
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
439
2
}
440
441
46
TEST_F(TestPPWhiteBVGauss, elim_unique_zero3)
442
{
443
4
  std::vector<Integer> rhs;
444
4
  std::vector<std::vector<Integer>> lhs;
445
446
  /* -------------------------------------------------------------------
447
   *   lhs   rhs        lhs   rhs   modulo 7
448
   *  --^--   ^        --^--   ^
449
   *  2 0 6   4        1 0 0   3
450
   *  0 0 0   0   -->  0 0 0   0
451
   *  4 0 6   3        0 0 1   2
452
   * ------------------------------------------------------------------- */
453
2
  rhs = {Integer(4), Integer(0), Integer(3)};
454
26
  lhs = {{Integer(2), Integer(0), Integer(6)},
455
         {Integer(0), Integer(0), Integer(0)},
456
24
         {Integer(4), Integer(0), Integer(6)}};
457
2
  std::cout << "matrix 10, modulo 7" << std::endl;
458
2
  testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
459
460
  /* -------------------------------------------------------------------
461
   *   lhs   rhs        lhs   rhs   modulo 7
462
   *  --^--   ^        --^--   ^
463
   *  2 6 0   4        1 0 0   3
464
   *  0 0 0   0   -->  0 0 0   0
465
   *  4 6 0   3        0 0 1   2
466
   * ------------------------------------------------------------------- */
467
2
  rhs = {Integer(4), Integer(0), Integer(3)};
468
26
  lhs = {{Integer(2), Integer(6), Integer(0)},
469
         {Integer(0), Integer(0), Integer(0)},
470
24
         {Integer(4), Integer(6), Integer(0)}};
471
2
  std::cout << "matrix 11, modulo 7" << std::endl;
472
2
  testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
473
2
}
474
475
46
TEST_F(TestPPWhiteBVGauss, elim_unique_zero4)
476
{
477
4
  std::vector<Integer> rhs, resrhs;
478
4
  std::vector<std::vector<Integer>> lhs, reslhs;
479
480
  /* -------------------------------------------------------------------
481
   *   lhs   rhs  modulo 11
482
   *  --^--   ^
483
   *  0 1 1   5
484
   *  0 0 0   0
485
   *  0 0 5   2
486
   * ------------------------------------------------------------------- */
487
2
  rhs = {Integer(5), Integer(0), Integer(2)};
488
26
  lhs = {{Integer(0), Integer(1), Integer(1)},
489
         {Integer(0), Integer(0), Integer(0)},
490
24
         {Integer(0), Integer(0), Integer(5)}};
491
2
  std::cout << "matrix 12, modulo 11" << std::endl;
492
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
493
494
  /* -------------------------------------------------------------------
495
   *   lhs   rhs  modulo 11
496
   *  --^--   ^
497
   *  0 1 1   5
498
   *  0 3 5   8
499
   *  0 0 0   0
500
   * ------------------------------------------------------------------- */
501
2
  rhs = {Integer(5), Integer(8), Integer(0)};
502
26
  lhs = {{Integer(0), Integer(1), Integer(1)},
503
         {Integer(0), Integer(3), Integer(5)},
504
24
         {Integer(0), Integer(0), Integer(0)}};
505
2
  std::cout << "matrix 13, modulo 11" << std::endl;
506
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
507
508
  /* -------------------------------------------------------------------
509
   *   lhs   rhs  modulo 11
510
   *  --^--   ^
511
   *  0 0 0   0
512
   *  0 3 5   8
513
   *  0 0 5   2
514
   * ------------------------------------------------------------------- */
515
2
  rhs = {Integer(0), Integer(8), Integer(2)};
516
26
  lhs = {{Integer(0), Integer(0), Integer(0)},
517
         {Integer(0), Integer(3), Integer(5)},
518
24
         {Integer(0), Integer(0), Integer(5)}};
519
2
  std::cout << "matrix 14, modulo 11" << std::endl;
520
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
521
522
  /* -------------------------------------------------------------------
523
   *   lhs   rhs  modulo 11
524
   *  --^--   ^
525
   *  1 0 1   5
526
   *  0 0 0   0
527
   *  4 0 5   2
528
   * ------------------------------------------------------------------- */
529
2
  rhs = {Integer(5), Integer(0), Integer(2)};
530
26
  lhs = {{Integer(1), Integer(0), Integer(1)},
531
         {Integer(0), Integer(0), Integer(0)},
532
24
         {Integer(4), Integer(0), Integer(5)}};
533
2
  std::cout << "matrix 15, modulo 11" << std::endl;
534
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
535
536
  /* -------------------------------------------------------------------
537
   *   lhs   rhs  modulo 11
538
   *  --^--   ^
539
   *  1 0 1   5
540
   *  2 0 5   8
541
   *  0 0 0   0
542
   * ------------------------------------------------------------------- */
543
2
  rhs = {Integer(5), Integer(8), Integer(0)};
544
26
  lhs = {{Integer(1), Integer(0), Integer(1)},
545
         {Integer(2), Integer(0), Integer(5)},
546
24
         {Integer(0), Integer(0), Integer(0)}};
547
2
  std::cout << "matrix 16, modulo 11" << std::endl;
548
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
549
550
  /* -------------------------------------------------------------------
551
   *   lhs   rhs  modulo 11
552
   *  --^--   ^
553
   *  0 0 0   0
554
   *  2 0 5   8
555
   *  4 0 5   2
556
   * ------------------------------------------------------------------- */
557
2
  rhs = {Integer(0), Integer(8), Integer(2)};
558
26
  lhs = {{Integer(0), Integer(0), Integer(0)},
559
         {Integer(2), Integer(0), Integer(5)},
560
24
         {Integer(4), Integer(0), Integer(5)}};
561
2
  std::cout << "matrix 17, modulo 11" << std::endl;
562
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
563
564
  /* -------------------------------------------------------------------
565
   *   lhs   rhs  modulo 11
566
   *  --^--   ^
567
   *  1 1 0   5
568
   *  0 0 0   0
569
   *  4 0 0   2
570
   * ------------------------------------------------------------------- */
571
2
  rhs = {Integer(5), Integer(0), Integer(2)};
572
26
  lhs = {{Integer(1), Integer(1), Integer(0)},
573
         {Integer(0), Integer(0), Integer(0)},
574
24
         {Integer(4), Integer(0), Integer(0)}};
575
2
  std::cout << "matrix 18, modulo 11" << std::endl;
576
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
577
578
  /* -------------------------------------------------------------------
579
   *   lhs   rhs  modulo 11
580
   *  --^--   ^
581
   *  1 1 0   5
582
   *  2 3 0   8
583
   *  0 0 0   0
584
   * ------------------------------------------------------------------- */
585
2
  rhs = {Integer(5), Integer(8), Integer(0)};
586
26
  lhs = {{Integer(1), Integer(1), Integer(0)},
587
         {Integer(2), Integer(3), Integer(0)},
588
24
         {Integer(0), Integer(0), Integer(0)}};
589
2
  std::cout << "matrix 18, modulo 11" << std::endl;
590
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
591
592
  /* -------------------------------------------------------------------
593
   *   lhs   rhs  modulo 11
594
   *  --^--   ^
595
   *  0 0 0   0
596
   *  2 3 0   8
597
   *  4 0 0   2
598
   * ------------------------------------------------------------------- */
599
2
  rhs = {Integer(0), Integer(8), Integer(2)};
600
26
  lhs = {{Integer(0), Integer(0), Integer(0)},
601
         {Integer(2), Integer(3), Integer(0)},
602
24
         {Integer(4), Integer(0), Integer(0)}};
603
2
  std::cout << "matrix 19, modulo 11" << std::endl;
604
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::UNIQUE);
605
606
  /* -------------------------------------------------------------------
607
   *     lhs    rhs  modulo 2
608
   *  ----^---   ^
609
   *  2  4   6   18     0 0 0   0
610
   *  4  5   6   24  =  0 1 0   0
611
   *  2  7  12   30     0 1 0   0
612
   * ------------------------------------------------------------------- */
613
2
  rhs = {Integer(18), Integer(24), Integer(30)};
614
26
  lhs = {{Integer(2), Integer(4), Integer(6)},
615
         {Integer(4), Integer(5), Integer(6)},
616
24
         {Integer(2), Integer(7), Integer(12)}};
617
2
  std::cout << "matrix 20, modulo 2" << std::endl;
618
2
  resrhs = {Integer(0), Integer(0), Integer(0)};
619
26
  reslhs = {{Integer(0), Integer(1), Integer(0)},
620
            {Integer(0), Integer(0), Integer(0)},
621
24
            {Integer(0), Integer(0), Integer(0)}};
622
6
  testGaussElimX(
623
4
      Integer(2), rhs, lhs, BVGauss::Result::UNIQUE, &resrhs, &reslhs);
624
2
}
625
626
46
TEST_F(TestPPWhiteBVGauss, elim_unique_partial)
627
{
628
4
  std::vector<Integer> rhs;
629
4
  std::vector<std::vector<Integer>> lhs;
630
631
  /* -------------------------------------------------------------------
632
   *   lhs   rhs        lhs   rhs   modulo 7
633
   *  --^--   ^        --^--   ^
634
   *  2 0 6   4        1 0 0   3
635
   *  4 0 6   3        0 0 1   2
636
   * ------------------------------------------------------------------- */
637
2
  rhs = {Integer(4), Integer(3)};
638
18
  lhs = {{Integer(2), Integer(0), Integer(6)},
639
16
         {Integer(4), Integer(0), Integer(6)}};
640
2
  std::cout << "matrix 21, modulo 7" << std::endl;
641
2
  testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
642
643
  /* -------------------------------------------------------------------
644
   *   lhs   rhs        lhs   rhs   modulo 7
645
   *  --^--   ^        --^--   ^
646
   *  2 6 0   4        1 0 0   3
647
   *  4 6 0   3        0 1 0   2
648
   * ------------------------------------------------------------------- */
649
2
  rhs = {Integer(4), Integer(3)};
650
18
  lhs = {{Integer(2), Integer(6), Integer(0)},
651
16
         {Integer(4), Integer(6), Integer(0)}};
652
2
  std::cout << "matrix 22, modulo 7" << std::endl;
653
2
  testGaussElimX(Integer(7), rhs, lhs, BVGauss::Result::UNIQUE);
654
2
}
655
656
46
TEST_F(TestPPWhiteBVGauss, elim_none)
657
{
658
4
  std::vector<Integer> rhs;
659
4
  std::vector<std::vector<Integer>> lhs;
660
661
  /* -------------------------------------------------------------------
662
   *   lhs     rhs       modulo 9
663
   *  --^---    ^
664
   *  2 4  6   18   -->  not coprime (no inverse)
665
   *  4 5  6   24
666
   *  3 1 -2    4
667
   * ------------------------------------------------------------------- */
668
2
  rhs = {Integer(18), Integer(24), Integer(4)};
669
26
  lhs = {{Integer(2), Integer(4), Integer(6)},
670
         {Integer(4), Integer(5), Integer(6)},
671
24
         {Integer(3), Integer(1), Integer(-2)}};
672
2
  std::cout << "matrix 23, modulo 9" << std::endl;
673
2
  testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::INVALID);
674
675
  /* -------------------------------------------------------------------
676
   *     lhs    rhs       modulo 59
677
   *  ----^---   ^
678
   *  1 -2  -6   12   --> no solution
679
   *  2  4  12  -17
680
   *  1 -4 -12   22
681
   * ------------------------------------------------------------------- */
682
2
  rhs = {Integer(12), Integer(-17), Integer(22)};
683
26
  lhs = {{Integer(1), Integer(-2), Integer(-6)},
684
         {Integer(2), Integer(4), Integer(12)},
685
24
         {Integer(1), Integer(-4), Integer(-12)}};
686
2
  std::cout << "matrix 24, modulo 59" << std::endl;
687
2
  testGaussElimX(Integer(59), rhs, lhs, BVGauss::Result::NONE);
688
689
  /* -------------------------------------------------------------------
690
   *     lhs    rhs       modulo 9
691
   *  ----^---   ^
692
   *  2  4   6   18   --> not coprime (no inverse)
693
   *  4  5   6   24
694
   *  2  7  12   30
695
   * ------------------------------------------------------------------- */
696
2
  rhs = {Integer(18), Integer(24), Integer(30)};
697
26
  lhs = {{Integer(2), Integer(4), Integer(6)},
698
         {Integer(4), Integer(5), Integer(6)},
699
24
         {Integer(2), Integer(7), Integer(12)}};
700
2
  std::cout << "matrix 25, modulo 9" << std::endl;
701
2
  testGaussElimX(Integer(9), rhs, lhs, BVGauss::Result::INVALID);
702
2
}
703
704
46
TEST_F(TestPPWhiteBVGauss, elim_none_zero)
705
{
706
4
  std::vector<Integer> rhs;
707
4
  std::vector<std::vector<Integer>> lhs;
708
709
  /* -------------------------------------------------------------------
710
   *   lhs   rhs  modulo 11
711
   *  --^--   ^
712
   *  0 1 1   5
713
   *  0 3 5   8
714
   *  0 0 5   2
715
   * ------------------------------------------------------------------- */
716
2
  rhs = {Integer(5), Integer(8), Integer(2)};
717
26
  lhs = {{Integer(0), Integer(1), Integer(1)},
718
         {Integer(0), Integer(3), Integer(5)},
719
24
         {Integer(0), Integer(0), Integer(5)}};
720
2
  std::cout << "matrix 26, modulo 11" << std::endl;
721
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
722
723
  /* -------------------------------------------------------------------
724
   *   lhs   rhs  modulo 11
725
   *  --^--   ^
726
   *  1 0 1   5
727
   *  2 0 5   8
728
   *  4 0 5   2
729
   * ------------------------------------------------------------------- */
730
2
  rhs = {Integer(5), Integer(8), Integer(2)};
731
26
  lhs = {{Integer(1), Integer(0), Integer(1)},
732
         {Integer(2), Integer(0), Integer(5)},
733
24
         {Integer(4), Integer(0), Integer(5)}};
734
2
  std::cout << "matrix 27, modulo 11" << std::endl;
735
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
736
737
  /* -------------------------------------------------------------------
738
   *   lhs   rhs  modulo 11
739
   *  --^--   ^
740
   *  1 1 0   5
741
   *  2 3 0   8
742
   *  4 0 0   2
743
   * ------------------------------------------------------------------- */
744
2
  rhs = {Integer(5), Integer(8), Integer(2)};
745
26
  lhs = {{Integer(1), Integer(1), Integer(0)},
746
         {Integer(2), Integer(3), Integer(0)},
747
24
         {Integer(4), Integer(0), Integer(0)}};
748
2
  std::cout << "matrix 28, modulo 11" << std::endl;
749
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::NONE);
750
2
}
751
752
46
TEST_F(TestPPWhiteBVGauss, elim_partial1)
753
{
754
4
  std::vector<Integer> rhs, resrhs;
755
4
  std::vector<std::vector<Integer>> lhs, reslhs;
756
757
  /* -------------------------------------------------------------------
758
   *   lhs   rhs        lhs   rhs  modulo 11
759
   *  --^--   ^        --^--   ^
760
   *  1 0 9   7   -->  1 0 9   7
761
   *  0 1 3   9        0 1 3   9
762
   * ------------------------------------------------------------------- */
763
2
  rhs = {Integer(7), Integer(9)};
764
18
  lhs = {{Integer(1), Integer(0), Integer(9)},
765
16
         {Integer(0), Integer(1), Integer(3)}};
766
2
  std::cout << "matrix 29, modulo 11" << std::endl;
767
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
768
769
  /* -------------------------------------------------------------------
770
   *   lhs   rhs        lhs   rhs  modulo 11
771
   *  --^--   ^        --^--   ^
772
   *  1 3 0   7   -->  1 3 0   7
773
   *  0 0 1   9        0 0 1   9
774
   * ------------------------------------------------------------------- */
775
2
  rhs = {Integer(7), Integer(9)};
776
18
  lhs = {{Integer(1), Integer(3), Integer(0)},
777
16
         {Integer(0), Integer(0), Integer(1)}};
778
2
  std::cout << "matrix 30, modulo 11" << std::endl;
779
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
780
781
  /* -------------------------------------------------------------------
782
   *   lhs   rhs        lhs   rhs  modulo 11
783
   *  --^--   ^        --^--   ^
784
   *  1 1 1   5   -->  1 0 9   7
785
   *  2 3 5   8        0 1 3   9
786
   * ------------------------------------------------------------------- */
787
2
  rhs = {Integer(5), Integer(8)};
788
18
  lhs = {{Integer(1), Integer(1), Integer(1)},
789
16
         {Integer(2), Integer(3), Integer(5)}};
790
2
  std::cout << "matrix 31, modulo 11" << std::endl;
791
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
792
793
  /* -------------------------------------------------------------------
794
   *     lhs    rhs  modulo { 3, 5, 7, 11, 17, 31, 59 }
795
   *  ----^---   ^
796
   *  2  4   6   18
797
   *  4  5   6   24
798
   *  2  7  12   30
799
   * ------------------------------------------------------------------- */
800
2
  rhs = {Integer(18), Integer(24), Integer(30)};
801
26
  lhs = {{Integer(2), Integer(4), Integer(6)},
802
         {Integer(4), Integer(5), Integer(6)},
803
24
         {Integer(2), Integer(7), Integer(12)}};
804
2
  std::cout << "matrix 32, modulo 3" << std::endl;
805
2
  resrhs = {Integer(0), Integer(0), Integer(0)};
806
26
  reslhs = {{Integer(1), Integer(2), Integer(0)},
807
            {Integer(0), Integer(0), Integer(0)},
808
24
            {Integer(0), Integer(0), Integer(0)}};
809
6
  testGaussElimX(
810
4
      Integer(3), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
811
2
  resrhs = {Integer(1), Integer(4), Integer(0)};
812
2
  std::cout << "matrix 32, modulo 5" << std::endl;
813
26
  reslhs = {{Integer(1), Integer(0), Integer(4)},
814
            {Integer(0), Integer(1), Integer(2)},
815
24
            {Integer(0), Integer(0), Integer(0)}};
816
6
  testGaussElimX(
817
4
      Integer(5), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
818
2
  std::cout << "matrix 32, modulo 7" << std::endl;
819
26
  reslhs = {{Integer(1), Integer(0), Integer(6)},
820
            {Integer(0), Integer(1), Integer(2)},
821
24
            {Integer(0), Integer(0), Integer(0)}};
822
6
  testGaussElimX(
823
4
      Integer(7), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
824
2
  std::cout << "matrix 32, modulo 11" << std::endl;
825
26
  reslhs = {{Integer(1), Integer(0), Integer(10)},
826
            {Integer(0), Integer(1), Integer(2)},
827
24
            {Integer(0), Integer(0), Integer(0)}};
828
6
  testGaussElimX(
829
4
      Integer(11), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
830
2
  std::cout << "matrix 32, modulo 17" << std::endl;
831
26
  reslhs = {{Integer(1), Integer(0), Integer(16)},
832
            {Integer(0), Integer(1), Integer(2)},
833
24
            {Integer(0), Integer(0), Integer(0)}};
834
6
  testGaussElimX(
835
4
      Integer(17), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
836
2
  std::cout << "matrix 32, modulo 59" << std::endl;
837
26
  reslhs = {{Integer(1), Integer(0), Integer(58)},
838
            {Integer(0), Integer(1), Integer(2)},
839
24
            {Integer(0), Integer(0), Integer(0)}};
840
6
  testGaussElimX(
841
4
      Integer(59), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
842
843
  /* -------------------------------------------------------------------
844
   *     lhs    rhs        lhs   rhs   modulo 3
845
   *  ----^---   ^        --^--   ^
846
   *   4  6 2   18   -->  1 0 2   0
847
   *   5  6 4   24        0 0 0   0
848
   *   7 12 2   30        0 0 0   0
849
   * ------------------------------------------------------------------- */
850
2
  rhs = {Integer(18), Integer(24), Integer(30)};
851
26
  lhs = {{Integer(4), Integer(6), Integer(2)},
852
         {Integer(5), Integer(6), Integer(4)},
853
24
         {Integer(7), Integer(12), Integer(2)}};
854
2
  std::cout << "matrix 33, modulo 3" << std::endl;
855
2
  resrhs = {Integer(0), Integer(0), Integer(0)};
856
26
  reslhs = {{Integer(1), Integer(0), Integer(2)},
857
            {Integer(0), Integer(0), Integer(0)},
858
24
            {Integer(0), Integer(0), Integer(0)}};
859
6
  testGaussElimX(
860
4
      Integer(3), rhs, lhs, BVGauss::Result::PARTIAL, &resrhs, &reslhs);
861
2
}
862
863
46
TEST_F(TestPPWhiteBVGauss, elim_partial2)
864
{
865
4
  std::vector<Integer> rhs;
866
4
  std::vector<std::vector<Integer>> lhs;
867
868
  /* -------------------------------------------------------------------
869
   *    lhs    rhs  -->    lhs    rhs  modulo 11
870
   *  ---^---   ^        ---^---   ^
871
   *  x y z w            x y z w
872
   *  1 2 0 6   2        1 2 0 0   1
873
   *  0 0 2 2   2        0 0 1 0   10
874
   *  0 0 0 1   2        0 0 0 1   2
875
   * ------------------------------------------------------------------- */
876
2
  rhs = {Integer(2), Integer(2), Integer(2)};
877
32
  lhs = {{Integer(1), Integer(2), Integer(6), Integer(0)},
878
         {Integer(0), Integer(0), Integer(2), Integer(2)},
879
30
         {Integer(0), Integer(0), Integer(1), Integer(0)}};
880
2
  std::cout << "matrix 34, modulo 11" << std::endl;
881
2
  testGaussElimX(Integer(11), rhs, lhs, BVGauss::Result::PARTIAL);
882
2
}
883
884
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1)
885
{
886
  /* -------------------------------------------------------------------
887
   *   lhs   rhs  modulo 11
888
   *  --^--   ^
889
   *  1 1 1   5
890
   *  2 3 5   8
891
   *  4 0 5   2
892
   * ------------------------------------------------------------------- */
893
894
  Node eq1 = d_nodeManager->mkNode(
895
      kind::EQUAL,
896
8
      d_nodeManager->mkNode(
897
          kind::BITVECTOR_UREM,
898
8
          d_nodeManager->mkNode(
899
              kind::BITVECTOR_PLUS,
900
4
              d_nodeManager->mkNode(
901
                  kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one),
902
              d_z_mul_one),
903
          d_p),
904
8
      d_five);
905
906
  Node eq2 = d_nodeManager->mkNode(
907
      kind::EQUAL,
908
8
      d_nodeManager->mkNode(
909
          kind::BITVECTOR_UREM,
910
8
          d_nodeManager->mkNode(
911
              kind::BITVECTOR_PLUS,
912
4
              d_nodeManager->mkNode(
913
                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three),
914
              d_z_mul_five),
915
          d_p),
916
8
      d_eight);
917
918
  Node eq3 = d_nodeManager->mkNode(
919
      kind::EQUAL,
920
8
      d_nodeManager->mkNode(
921
          kind::BITVECTOR_UREM,
922
4
          d_nodeManager->mkNode(
923
              kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five),
924
          d_p),
925
8
      d_two);
926
927
4
  std::vector<Node> eqs = {eq1, eq2, eq3};
928
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
929
2
  BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
930
2
  ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
931
2
  ASSERT_EQ(res.size(), 3);
932
2
  ASSERT_EQ(res[d_x], d_three32);
933
2
  ASSERT_EQ(res[d_y], d_four32);
934
2
  ASSERT_EQ(res[d_z], d_nine32);
935
}
936
937
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
938
{
939
  /* -------------------------------------------------------------------
940
   *   lhs   rhs  modulo 11
941
   *  --^--   ^
942
   *  1 1 1   5
943
   *  2 3 5   8
944
   *  4 0 5   2
945
   * ------------------------------------------------------------------- */
946
947
  Node zextop6 =
948
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(6));
949
950
  Node p = d_nodeManager->mkNode(
951
      zextop6,
952
4
      bv::utils::mkConcat(bv::utils::mkZero(6),
953
10
                          d_nodeManager->mkNode(kind::BITVECTOR_PLUS,
954
4
                                                bv::utils::mkConst(20, 7),
955
10
                                                bv::utils::mkConst(20, 4))));
956
957
  Node x_mul_one = d_nodeManager->mkNode(
958
      kind::BITVECTOR_MULT,
959
4
      d_nodeManager->mkNode(kind::BITVECTOR_SUB, d_five, d_four),
960
8
      d_x);
961
  Node y_mul_one = d_nodeManager->mkNode(
962
      kind::BITVECTOR_MULT,
963
4
      d_nodeManager->mkNode(kind::BITVECTOR_UREM, d_one, d_five),
964
8
      d_y);
965
  Node z_mul_one =
966
4
      d_nodeManager->mkNode(kind::BITVECTOR_MULT, bv::utils::mkOne(32), d_z);
967
968
  Node x_mul_two = d_nodeManager->mkNode(
969
      kind::BITVECTOR_MULT,
970
10
      d_nodeManager->mkNode(
971
8
          kind::BITVECTOR_SHL, bv::utils::mkOne(32), bv::utils::mkOne(32)),
972
8
      d_x);
973
  Node y_mul_three =
974
      d_nodeManager->mkNode(kind::BITVECTOR_MULT,
975
10
                            d_nodeManager->mkNode(kind::BITVECTOR_LSHR,
976
4
                                                  bv::utils::mkOnes(32),
977
4
                                                  bv::utils::mkConst(32, 30)),
978
8
                            d_y);
979
  Node z_mul_five = d_nodeManager->mkNode(
980
      kind::BITVECTOR_MULT,
981
4
      bv::utils::mkExtract(
982
6
          d_nodeManager->mkNode(
983
              zextop6,
984
4
              d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_three, d_two)),
985
          31,
986
          0),
987
8
      d_z);
988
989
  Node x_mul_four = d_nodeManager->mkNode(
990
      kind::BITVECTOR_MULT,
991
10
      d_nodeManager->mkNode(
992
          kind::BITVECTOR_UDIV,
993
10
          d_nodeManager->mkNode(
994
              kind::BITVECTOR_PLUS,
995
10
              d_nodeManager->mkNode(kind::BITVECTOR_MULT,
996
4
                                    bv::utils::mkConst(32, 4),
997
4
                                    bv::utils::mkConst(32, 5)),
998
4
              bv::utils::mkConst(32, 4)),
999
4
          bv::utils::mkConst(32, 6)),
1000
8
      d_x);
1001
1002
  Node eq1 = d_nodeManager->mkNode(
1003
      kind::EQUAL,
1004
8
      d_nodeManager->mkNode(
1005
          kind::BITVECTOR_UREM,
1006
8
          d_nodeManager->mkNode(
1007
              kind::BITVECTOR_PLUS,
1008
4
              d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_one, y_mul_one),
1009
              z_mul_one),
1010
          p),
1011
8
      d_five);
1012
1013
  Node eq2 = d_nodeManager->mkNode(
1014
      kind::EQUAL,
1015
8
      d_nodeManager->mkNode(
1016
          kind::BITVECTOR_UREM,
1017
8
          d_nodeManager->mkNode(
1018
              kind::BITVECTOR_PLUS,
1019
4
              d_nodeManager->mkNode(
1020
                  kind::BITVECTOR_PLUS, x_mul_two, y_mul_three),
1021
              z_mul_five),
1022
          p),
1023
8
      d_eight);
1024
1025
  Node eq3 = d_nodeManager->mkNode(
1026
      kind::EQUAL,
1027
8
      d_nodeManager->mkNode(
1028
          kind::BITVECTOR_UREM,
1029
4
          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_four, z_mul_five),
1030
          d_p),
1031
8
      d_two);
1032
1033
4
  std::vector<Node> eqs = {eq1, eq2, eq3};
1034
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1035
2
  BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1036
2
  ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
1037
2
  ASSERT_EQ(res.size(), 3);
1038
2
  ASSERT_EQ(res[d_x], d_three32);
1039
2
  ASSERT_EQ(res[d_y], d_four32);
1040
2
  ASSERT_EQ(res[d_z], d_nine32);
1041
}
1042
1043
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
1044
{
1045
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1046
  BVGauss::Result ret;
1047
1048
  /* -------------------------------------------------------------------
1049
   *   lhs   rhs        lhs   rhs  modulo 11
1050
   *  --^--   ^        --^--   ^
1051
   *  1 0 9   7   -->  1 0 9   7
1052
   *  0 1 3   9        0 1 3   9
1053
   * ------------------------------------------------------------------- */
1054
1055
  Node eq1 = d_nodeManager->mkNode(
1056
      kind::EQUAL,
1057
8
      d_nodeManager->mkNode(
1058
          kind::BITVECTOR_UREM,
1059
4
          d_nodeManager->mkNode(
1060
              kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine),
1061
          d_p),
1062
8
      d_seven);
1063
1064
  Node eq2 = d_nodeManager->mkNode(
1065
      kind::EQUAL,
1066
8
      d_nodeManager->mkNode(
1067
          kind::BITVECTOR_UREM,
1068
4
          d_nodeManager->mkNode(
1069
              kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three),
1070
          d_p),
1071
8
      d_nine);
1072
1073
4
  std::vector<Node> eqs = {eq1, eq2};
1074
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1075
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1076
2
  ASSERT_EQ(res.size(), 2);
1077
1078
  Node x1 = d_nodeManager->mkNode(
1079
      kind::BITVECTOR_UREM,
1080
6
      d_nodeManager->mkNode(
1081
          kind::BITVECTOR_PLUS,
1082
          d_seven32,
1083
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)),
1084
8
      d_p);
1085
  Node y1 = d_nodeManager->mkNode(
1086
      kind::BITVECTOR_UREM,
1087
6
      d_nodeManager->mkNode(
1088
          kind::BITVECTOR_PLUS,
1089
          d_nine32,
1090
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)),
1091
8
      d_p);
1092
1093
  Node x2 = d_nodeManager->mkNode(
1094
      kind::BITVECTOR_UREM,
1095
6
      d_nodeManager->mkNode(
1096
          kind::BITVECTOR_PLUS,
1097
          d_two32,
1098
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)),
1099
8
      d_p);
1100
  Node z2 = d_nodeManager->mkNode(
1101
      kind::BITVECTOR_UREM,
1102
6
      d_nodeManager->mkNode(
1103
          kind::BITVECTOR_PLUS,
1104
          d_three32,
1105
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)),
1106
8
      d_p);
1107
1108
  Node y3 = d_nodeManager->mkNode(
1109
      kind::BITVECTOR_UREM,
1110
6
      d_nodeManager->mkNode(
1111
          kind::BITVECTOR_PLUS,
1112
          d_three32,
1113
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)),
1114
8
      d_p);
1115
  Node z3 = d_nodeManager->mkNode(
1116
      kind::BITVECTOR_UREM,
1117
6
      d_nodeManager->mkNode(
1118
          kind::BITVECTOR_PLUS,
1119
          d_two32,
1120
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)),
1121
8
      d_p);
1122
1123
  /* result depends on order of variables in matrix */
1124
2
  if (res.find(d_x) == res.end())
1125
  {
1126
    /*
1127
     *  y z x           y z x
1128
     *  0 9 1  7   -->  1 0 7  3
1129
     *  1 3 0  9        0 1 5  2
1130
     *
1131
     *  z y x           z y x
1132
     *  9 0 1  7   -->  1 0 5  2
1133
     *  3 1 0  9        0 1 7  3
1134
     */
1135
    ASSERT_EQ(res[d_y], y3);
1136
    ASSERT_EQ(res[d_z], z3);
1137
  }
1138
2
  else if (res.find(d_y) == res.end())
1139
  {
1140
    /*
1141
     *  x z y           x z y
1142
     *  1 9 0  7   -->  1 0 8  2
1143
     *  0 3 1  9        0 1 4  3
1144
     *
1145
     *  z x y           z x y
1146
     *  9 1 0  7   -->  1 0 4  3
1147
     *  3 0 1  9        0 1 8  2
1148
     */
1149
    ASSERT_EQ(res[d_x], x2);
1150
    ASSERT_EQ(res[d_z], z2);
1151
  }
1152
  else
1153
  {
1154
2
    ASSERT_EQ(res.find(d_z), res.end());
1155
    /*
1156
     *  x y z           x y z
1157
     *  1 0 9  7   -->  1 0 9  7
1158
     *  0 1 3  9        0 1 3  9
1159
     *
1160
     *  y x z           y x z
1161
     *  0 1 9  7   -->  1 0 3  9
1162
     *  1 0 3  9        0 1 9  7
1163
     */
1164
2
    ASSERT_EQ(res[d_x], x1);
1165
2
    ASSERT_EQ(res[d_y], y1);
1166
  }
1167
}
1168
1169
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
1170
{
1171
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1172
  BVGauss::Result ret;
1173
1174
  /* -------------------------------------------------------------------
1175
   *   lhs   rhs        lhs   rhs  modulo 11
1176
   *  --^--   ^        --^--   ^
1177
   *  1 0 9   7   -->  1 0 9   7
1178
   *  0 1 3   9        0 1 3   9
1179
   * ------------------------------------------------------------------- */
1180
1181
  Node eq1 = d_nodeManager->mkNode(
1182
      kind::EQUAL,
1183
8
      d_nodeManager->mkNode(
1184
          kind::BITVECTOR_UREM,
1185
4
          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x, d_z_mul_nine),
1186
          d_p),
1187
8
      d_seven);
1188
1189
  Node eq2 = d_nodeManager->mkNode(
1190
      kind::EQUAL,
1191
8
      d_nodeManager->mkNode(
1192
          kind::BITVECTOR_UREM,
1193
4
          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_y, d_z_mul_three),
1194
          d_p),
1195
8
      d_nine);
1196
1197
4
  std::vector<Node> eqs = {eq1, eq2};
1198
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1199
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1200
2
  ASSERT_EQ(res.size(), 2);
1201
1202
  Node x1 = d_nodeManager->mkNode(
1203
      kind::BITVECTOR_UREM,
1204
6
      d_nodeManager->mkNode(
1205
          kind::BITVECTOR_PLUS,
1206
          d_seven32,
1207
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)),
1208
8
      d_p);
1209
  Node y1 = d_nodeManager->mkNode(
1210
      kind::BITVECTOR_UREM,
1211
6
      d_nodeManager->mkNode(
1212
          kind::BITVECTOR_PLUS,
1213
          d_nine32,
1214
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)),
1215
8
      d_p);
1216
1217
  Node x2 = d_nodeManager->mkNode(
1218
      kind::BITVECTOR_UREM,
1219
6
      d_nodeManager->mkNode(
1220
          kind::BITVECTOR_PLUS,
1221
          d_two32,
1222
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)),
1223
8
      d_p);
1224
  Node z2 = d_nodeManager->mkNode(
1225
      kind::BITVECTOR_UREM,
1226
6
      d_nodeManager->mkNode(
1227
          kind::BITVECTOR_PLUS,
1228
          d_three32,
1229
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)),
1230
8
      d_p);
1231
1232
  Node y3 = d_nodeManager->mkNode(
1233
      kind::BITVECTOR_UREM,
1234
6
      d_nodeManager->mkNode(
1235
          kind::BITVECTOR_PLUS,
1236
          d_three32,
1237
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)),
1238
8
      d_p);
1239
  Node z3 = d_nodeManager->mkNode(
1240
      kind::BITVECTOR_UREM,
1241
6
      d_nodeManager->mkNode(
1242
          kind::BITVECTOR_PLUS,
1243
          d_two32,
1244
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)),
1245
8
      d_p);
1246
1247
  /* result depends on order of variables in matrix */
1248
2
  if (res.find(d_x) == res.end())
1249
  {
1250
    /*
1251
     *  y z x           y z x
1252
     *  0 9 1  7   -->  1 0 7  3
1253
     *  1 3 0  9        0 1 5  2
1254
     *
1255
     *  z y x           z y x
1256
     *  9 0 1  7   -->  1 0 5  2
1257
     *  3 1 0  9        0 1 7  3
1258
     */
1259
    ASSERT_EQ(res[d_y], y3);
1260
    ASSERT_EQ(res[d_z], z3);
1261
  }
1262
2
  else if (res.find(d_y) == res.end())
1263
  {
1264
    /*
1265
     *  x z y           x z y
1266
     *  1 9 0  7   -->  1 0 8  2
1267
     *  0 3 1  9        0 1 4  3
1268
     *
1269
     *  z x y           z x y
1270
     *  9 1 0  7   -->  1 0 4  3
1271
     *  3 0 1  9        0 1 8  2
1272
     */
1273
    ASSERT_EQ(res[d_x], x2);
1274
    ASSERT_EQ(res[d_z], z2);
1275
  }
1276
  else
1277
  {
1278
2
    ASSERT_EQ(res.find(d_z), res.end());
1279
    /*
1280
     *  x y z           x y z
1281
     *  1 0 9  7   -->  1 0 9  7
1282
     *  0 1 3  9        0 1 3  9
1283
     *
1284
     *  y x z           y x z
1285
     *  0 1 9  7   -->  1 0 3  9
1286
     *  1 0 3  9        0 1 9  7
1287
     */
1288
2
    ASSERT_EQ(res[d_x], x1);
1289
2
    ASSERT_EQ(res[d_y], y1);
1290
  }
1291
}
1292
1293
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
1294
{
1295
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1296
  BVGauss::Result ret;
1297
1298
  /* -------------------------------------------------------------------
1299
   *   lhs   rhs        lhs   rhs  modulo 11
1300
   *  --^--   ^        --^--   ^
1301
   *  1 3 0   7   -->  1 3 0   7
1302
   *  0 0 1   9        0 0 1   9
1303
   * ------------------------------------------------------------------- */
1304
1305
  Node eq1 = d_nodeManager->mkNode(
1306
      kind::EQUAL,
1307
8
      d_nodeManager->mkNode(
1308
          kind::BITVECTOR_UREM,
1309
4
          d_nodeManager->mkNode(
1310
              kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_three),
1311
          d_p),
1312
8
      d_seven);
1313
1314
  Node eq2 = d_nodeManager->mkNode(
1315
      kind::EQUAL,
1316
4
      d_nodeManager->mkNode(kind::BITVECTOR_UREM, d_z_mul_one, d_p),
1317
8
      d_nine);
1318
1319
4
  std::vector<Node> eqs = {eq1, eq2};
1320
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1321
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1322
2
  ASSERT_EQ(res.size(), 2);
1323
1324
  Node x1 = d_nodeManager->mkNode(
1325
      kind::BITVECTOR_UREM,
1326
6
      d_nodeManager->mkNode(
1327
          kind::BITVECTOR_PLUS,
1328
          d_seven32,
1329
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_eight32)),
1330
8
      d_p);
1331
  Node y2 = d_nodeManager->mkNode(
1332
      kind::BITVECTOR_UREM,
1333
6
      d_nodeManager->mkNode(
1334
          kind::BITVECTOR_PLUS,
1335
          d_six32,
1336
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_seven32)),
1337
8
      d_p);
1338
1339
  /* result depends on order of variables in matrix */
1340
2
  if (res.find(d_x) == res.end())
1341
  {
1342
    /*
1343
     *  x y z           x y z
1344
     *  1 3 0  7   -->  1 3 0  7
1345
     *  0 0 1  9        0 0 1  9
1346
     *
1347
     *  x z y           x z y
1348
     *  1 0 3  7   -->  1 0 3  7
1349
     *  0 1 0  9        0 1 0  9
1350
     *
1351
     *  z x y           z x y
1352
     *  0 1 3  7   -->  1 0 0  9
1353
     *  1 0 0  9        0 1 3  7
1354
     */
1355
    ASSERT_EQ(res[d_y], y2);
1356
    ASSERT_EQ(res[d_z], d_nine32);
1357
  }
1358
2
  else if (res.find(d_y) == res.end())
1359
  {
1360
    /*
1361
     *  z y x           z y x
1362
     *  0 3 1  7   -->  1 0 0  9
1363
     *  1 0 0  9        0 1 4  6
1364
     *
1365
     *  y x z           y x z
1366
     *  3 1 0  7   -->  1 4 0  6
1367
     *  0 0 1  9        0 0 1  9
1368
     *
1369
     *  y z x           y z x
1370
     *  3 0 1  7   -->  1 0 4  6
1371
     *  0 1 0  9        0 1 0  9
1372
     */
1373
2
    ASSERT_EQ(res[d_x], x1);
1374
2
    ASSERT_EQ(res[d_z], d_nine32);
1375
  }
1376
  else
1377
  {
1378
    ASSERT_TRUE(false);
1379
  }
1380
}
1381
1382
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
1383
{
1384
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1385
  BVGauss::Result ret;
1386
1387
  /* -------------------------------------------------------------------
1388
   *   lhs   rhs        lhs   rhs  modulo 11
1389
   *  --^--   ^        --^--   ^
1390
   *  1 1 1   5   -->  1 0 9   7
1391
   *  2 3 5   8        0 1 3   9
1392
   * ------------------------------------------------------------------- */
1393
1394
  Node eq1 = d_nodeManager->mkNode(
1395
      kind::EQUAL,
1396
8
      d_nodeManager->mkNode(
1397
          kind::BITVECTOR_UREM,
1398
8
          d_nodeManager->mkNode(
1399
              kind::BITVECTOR_PLUS,
1400
4
              d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y),
1401
              d_z_mul_one),
1402
          d_p),
1403
8
      d_five);
1404
1405
  Node eq2 = d_nodeManager->mkNode(
1406
      kind::EQUAL,
1407
8
      d_nodeManager->mkNode(
1408
          kind::BITVECTOR_UREM,
1409
8
          d_nodeManager->mkNode(
1410
              kind::BITVECTOR_PLUS,
1411
4
              d_nodeManager->mkNode(
1412
                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three),
1413
              d_z_mul_five),
1414
          d_p),
1415
8
      d_eight);
1416
1417
4
  std::vector<Node> eqs = {eq1, eq2};
1418
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1419
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1420
2
  ASSERT_EQ(res.size(), 2);
1421
1422
  Node x1 = d_nodeManager->mkNode(
1423
      kind::BITVECTOR_UREM,
1424
6
      d_nodeManager->mkNode(
1425
          kind::BITVECTOR_PLUS,
1426
          d_seven32,
1427
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)),
1428
8
      d_p);
1429
  Node y1 = d_nodeManager->mkNode(
1430
      kind::BITVECTOR_UREM,
1431
6
      d_nodeManager->mkNode(
1432
          kind::BITVECTOR_PLUS,
1433
          d_nine32,
1434
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)),
1435
8
      d_p);
1436
  Node x2 = d_nodeManager->mkNode(
1437
      kind::BITVECTOR_UREM,
1438
6
      d_nodeManager->mkNode(
1439
          kind::BITVECTOR_PLUS,
1440
          d_two32,
1441
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)),
1442
8
      d_p);
1443
  Node z2 = d_nodeManager->mkNode(
1444
      kind::BITVECTOR_UREM,
1445
6
      d_nodeManager->mkNode(
1446
          kind::BITVECTOR_PLUS,
1447
          d_three32,
1448
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)),
1449
8
      d_p);
1450
  Node y3 = d_nodeManager->mkNode(
1451
      kind::BITVECTOR_UREM,
1452
6
      d_nodeManager->mkNode(
1453
          kind::BITVECTOR_PLUS,
1454
          d_three32,
1455
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)),
1456
8
      d_p);
1457
  Node z3 = d_nodeManager->mkNode(
1458
      kind::BITVECTOR_UREM,
1459
6
      d_nodeManager->mkNode(
1460
          kind::BITVECTOR_PLUS,
1461
          d_two32,
1462
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)),
1463
8
      d_p);
1464
1465
  /* result depends on order of variables in matrix */
1466
2
  if (res.find(d_x) == res.end())
1467
  {
1468
    /*
1469
     *  y z x           y z x
1470
     *  1 1 1  5   -->  1 0 7  3
1471
     *  3 5 2  8        0 1 5  2
1472
     *
1473
     *  z y x           z y x
1474
     *  1 1 1  5   -->  1 0 5  2
1475
     *  5 3 2  8        0 1 7  3
1476
     */
1477
    ASSERT_EQ(res[d_y], y3);
1478
    ASSERT_EQ(res[d_z], z3);
1479
  }
1480
2
  else if (res.find(d_y) == res.end())
1481
  {
1482
    /*
1483
     *  x z y           x z y
1484
     *  1 1 1  5   -->  1 0 8  2
1485
     *  2 5 3  8        0 1 4  3
1486
     *
1487
     *  z x y           z x y
1488
     *  1 1 1  5   -->  1 0 4  3
1489
     *  5 2 3  9        0 1 8  2
1490
     */
1491
    ASSERT_EQ(res[d_x], x2);
1492
    ASSERT_EQ(res[d_z], z2);
1493
  }
1494
  else
1495
  {
1496
2
    ASSERT_EQ(res.find(d_z), res.end());
1497
    /*
1498
     *  x y z           x y z
1499
     *  1 1 1  5   -->  1 0 9  7
1500
     *  2 3 5  8        0 1 3  9
1501
     *
1502
     *  y x z           y x z
1503
     *  1 1 1  5   -->  1 0 3  9
1504
     *  3 2 5  8        0 1 9  7
1505
     */
1506
2
    ASSERT_EQ(res[d_x], x1);
1507
2
    ASSERT_EQ(res[d_y], y1);
1508
  }
1509
}
1510
1511
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
1512
{
1513
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1514
  BVGauss::Result ret;
1515
1516
  /* -------------------------------------------------------------------
1517
   *     lhs    rhs          lhs    rhs  modulo 11
1518
   *  ----^---   ^         ---^---   ^
1519
   *  2  4   6   18   -->  1 0 10    1
1520
   *  4  5   6   24        0 1  2    4
1521
   *  2  7  12   30        0 0  0    0
1522
   * ------------------------------------------------------------------- */
1523
1524
  Node eq1 = d_nodeManager->mkNode(
1525
      kind::EQUAL,
1526
8
      d_nodeManager->mkNode(
1527
          kind::BITVECTOR_UREM,
1528
8
          d_nodeManager->mkNode(
1529
              kind::BITVECTOR_PLUS,
1530
4
              d_nodeManager->mkNode(
1531
                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four),
1532
              d_z_mul_six),
1533
          d_p),
1534
8
      d_eighteen);
1535
1536
  Node eq2 = d_nodeManager->mkNode(
1537
      kind::EQUAL,
1538
8
      d_nodeManager->mkNode(
1539
          kind::BITVECTOR_UREM,
1540
8
          d_nodeManager->mkNode(
1541
              kind::BITVECTOR_PLUS,
1542
4
              d_nodeManager->mkNode(
1543
                  kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five),
1544
              d_z_mul_six),
1545
          d_p),
1546
8
      d_twentyfour);
1547
1548
  Node eq3 = d_nodeManager->mkNode(
1549
      kind::EQUAL,
1550
8
      d_nodeManager->mkNode(
1551
          kind::BITVECTOR_UREM,
1552
8
          d_nodeManager->mkNode(
1553
              kind::BITVECTOR_PLUS,
1554
4
              d_nodeManager->mkNode(
1555
                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven),
1556
              d_z_mul_twelve),
1557
          d_p),
1558
8
      d_thirty);
1559
1560
4
  std::vector<Node> eqs = {eq1, eq2, eq3};
1561
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1562
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1563
2
  ASSERT_EQ(res.size(), 2);
1564
1565
  Node x1 = d_nodeManager->mkNode(
1566
      kind::BITVECTOR_UREM,
1567
6
      d_nodeManager->mkNode(
1568
          kind::BITVECTOR_PLUS,
1569
          d_one32,
1570
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_one32)),
1571
8
      d_p);
1572
  Node y1 = d_nodeManager->mkNode(
1573
      kind::BITVECTOR_UREM,
1574
6
      d_nodeManager->mkNode(
1575
          kind::BITVECTOR_PLUS,
1576
          d_four32,
1577
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_nine32)),
1578
8
      d_p);
1579
  Node x2 = d_nodeManager->mkNode(
1580
      kind::BITVECTOR_UREM,
1581
6
      d_nodeManager->mkNode(
1582
          kind::BITVECTOR_PLUS,
1583
          d_three32,
1584
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)),
1585
8
      d_p);
1586
  Node z2 = d_nodeManager->mkNode(
1587
      kind::BITVECTOR_UREM,
1588
6
      d_nodeManager->mkNode(
1589
          kind::BITVECTOR_PLUS,
1590
          d_two32,
1591
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)),
1592
8
      d_p);
1593
  Node y3 = d_nodeManager->mkNode(
1594
      kind::BITVECTOR_UREM,
1595
6
      d_nodeManager->mkNode(
1596
          kind::BITVECTOR_PLUS,
1597
          d_six32,
1598
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_nine32)),
1599
8
      d_p);
1600
  Node z3 = d_nodeManager->mkNode(
1601
      kind::BITVECTOR_UREM,
1602
6
      d_nodeManager->mkNode(
1603
          kind::BITVECTOR_PLUS,
1604
          d_ten32,
1605
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_one32)),
1606
8
      d_p);
1607
1608
  /* result depends on order of variables in matrix */
1609
2
  if (res.find(d_x) == res.end())
1610
  {
1611
    /*
1612
     *  y  z x           y z  x
1613
     *  4  6 2  18  -->  1 0  2   6
1614
     *  5  6 4  24       0 1 10  10
1615
     *  7 12 2  30       0 0  0   0
1616
     *
1617
     *  z  y x           z y  x
1618
     *  6  4 2  18  -->  1 0 10  10
1619
     *  6  5 4  24       0 1  2   6
1620
     * 12 12 2  30       0 0  0   0
1621
     *
1622
     */
1623
    ASSERT_EQ(res[d_y], y3);
1624
    ASSERT_EQ(res[d_z], z3);
1625
  }
1626
2
  else if (res.find(d_y) == res.end())
1627
  {
1628
    /*
1629
     *  x  z y           x z y
1630
     *  2  6 4  18  -->  1 0 6  3
1631
     *  4  6 5  24       0 1 6  2
1632
     *  2 12 7  30       0 0 0  0
1633
     *
1634
     *  z x  y           z  x y
1635
     *  6 2  4  18  -->  1  0 6  2
1636
     *  6 4  5  24       0  1 6  3
1637
     * 12 2 12  30       0  0 0  0
1638
     *
1639
     */
1640
    ASSERT_EQ(res[d_x], x2);
1641
    ASSERT_EQ(res[d_z], z2);
1642
  }
1643
  else
1644
  {
1645
2
    ASSERT_EQ(res.find(d_z), res.end());
1646
    /*
1647
     *  x y  z           x y  z
1648
     *  2 4  6  18  -->  1 0 10  1
1649
     *  4 5  6  24       0 1  2  4
1650
     *  2 7 12  30       0 0  0  0
1651
     *
1652
     *  y x  z            y x  z
1653
     *  4 2  6  18   -->  1 0  2 49
1654
     *  5 4  6  24        0 1 10  1
1655
     *  7 2 12  30        0 0  0  0
1656
     */
1657
2
    ASSERT_EQ(res[d_x], x1);
1658
2
    ASSERT_EQ(res[d_y], y1);
1659
  }
1660
}
1661
1662
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
1663
{
1664
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1665
  BVGauss::Result ret;
1666
1667
  /* -------------------------------------------------------------------
1668
   *     lhs    rhs         lhs   rhs  modulo 3
1669
   *  ----^---   ^         --^--   ^
1670
   *  2  4   6   18   -->  1 2 0   0
1671
   *  4  5   6   24        0 0 0   0
1672
   *  2  7  12   30        0 0 0   0
1673
   * ------------------------------------------------------------------- */
1674
1675
  Node eq1 = d_nodeManager->mkNode(
1676
      kind::EQUAL,
1677
8
      d_nodeManager->mkNode(
1678
          kind::BITVECTOR_UREM,
1679
8
          d_nodeManager->mkNode(
1680
              kind::BITVECTOR_PLUS,
1681
4
              d_nodeManager->mkNode(
1682
                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four),
1683
              d_z_mul_six),
1684
          d_three),
1685
8
      d_eighteen);
1686
1687
  Node eq2 = d_nodeManager->mkNode(
1688
      kind::EQUAL,
1689
8
      d_nodeManager->mkNode(
1690
          kind::BITVECTOR_UREM,
1691
8
          d_nodeManager->mkNode(
1692
              kind::BITVECTOR_PLUS,
1693
4
              d_nodeManager->mkNode(
1694
                  kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five),
1695
              d_z_mul_six),
1696
          d_three),
1697
8
      d_twentyfour);
1698
1699
  Node eq3 = d_nodeManager->mkNode(
1700
      kind::EQUAL,
1701
8
      d_nodeManager->mkNode(
1702
          kind::BITVECTOR_UREM,
1703
8
          d_nodeManager->mkNode(
1704
              kind::BITVECTOR_PLUS,
1705
4
              d_nodeManager->mkNode(
1706
                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven),
1707
              d_z_mul_twelve),
1708
          d_three),
1709
8
      d_thirty);
1710
1711
4
  std::vector<Node> eqs = {eq1, eq2, eq3};
1712
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1713
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1714
2
  ASSERT_EQ(res.size(), 1);
1715
1716
  Node x1 = d_nodeManager->mkNode(
1717
      kind::BITVECTOR_UREM,
1718
4
      d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_one32),
1719
8
      d_three);
1720
  Node y2 = d_nodeManager->mkNode(
1721
      kind::BITVECTOR_UREM,
1722
4
      d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_one32),
1723
8
      d_three);
1724
1725
  /* result depends on order of variables in matrix */
1726
2
  if (res.find(d_x) == res.end())
1727
  {
1728
    /*
1729
     *  y x  z           y x z
1730
     *  4 2  6  18  -->  1 2 0 0
1731
     *  5 4  6  24       0 0 0 0
1732
     *  7 2 12  30       0 0 0 0
1733
     *
1734
     *  y  z x            y z x
1735
     *  4  6 2  18  -->  1 0 2  0
1736
     *  5  6 4  24       0 0 0  0
1737
     *  7 12 2  30       0 0 0  0
1738
     *
1739
     *  z  y x           z y x
1740
     *  6  4 2  18  -->  0 1 2  0
1741
     *  6  5 4  24       0 0 0  0
1742
     * 12 12 2  30       0 0 0  0
1743
     *
1744
     */
1745
2
    ASSERT_EQ(res[d_y], y2);
1746
  }
1747
  else if (res.find(d_y) == res.end())
1748
  {
1749
    /*
1750
     *  x y  z           x y z
1751
     *  2 4  6  18  -->  1 2 0  0
1752
     *  4 5  6  24       0 0 0  0
1753
     *  2 7 12  30       0 0 0  0
1754
     *
1755
     *  x  z y           x z y
1756
     *  2  6 4  18  -->  1 0 2  0
1757
     *  4  6 5  24       0 0 0  0
1758
     *  2 12 7  30       0 0 0  0
1759
     *
1760
     *  z x  y           z  x y
1761
     *  6 2  4  18  -->  0  1 2  0
1762
     *  6 4  5  24       0  0 0  0
1763
     * 12 2 12  30       0  0 0  0
1764
     *
1765
     */
1766
    ASSERT_EQ(res[d_x], x1);
1767
  }
1768
  else
1769
  {
1770
    ASSERT_TRUE(false);
1771
  }
1772
}
1773
1774
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
1775
{
1776
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1777
  BVGauss::Result ret;
1778
1779
  /* -------------------------------------------------------------------
1780
   *    lhs    rhs  -->    lhs    rhs  modulo 11
1781
   *  ---^---   ^        ---^---   ^
1782
   *  x y z w            x y z w
1783
   *  1 2 0 6   2        1 2 0 6   2
1784
   *  0 0 2 2   2        0 0 1 1   1
1785
   *  0 0 0 1   2        0 0 0 1   2
1786
   * ------------------------------------------------------------------- */
1787
1788
4
  Node y_mul_two = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_two);
1789
4
  Node z_mul_two = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two);
1790
  Node w = bv::utils::mkConcat(
1791
4
      d_zero, d_nodeManager->mkVar("w", d_nodeManager->mkBitVectorType(16)));
1792
4
  Node w_mul_six = d_nodeManager->mkNode(kind::BITVECTOR_MULT, w, d_six);
1793
4
  Node w_mul_two = d_nodeManager->mkNode(kind::BITVECTOR_MULT, w, d_two);
1794
1795
  Node eq1 = d_nodeManager->mkNode(
1796
      kind::EQUAL,
1797
8
      d_nodeManager->mkNode(
1798
          kind::BITVECTOR_UREM,
1799
8
          d_nodeManager->mkNode(
1800
              kind::BITVECTOR_PLUS,
1801
4
              d_nodeManager->mkNode(
1802
                  kind::BITVECTOR_PLUS, d_x_mul_one, y_mul_two),
1803
              w_mul_six),
1804
          d_p),
1805
8
      d_two);
1806
1807
  Node eq2 = d_nodeManager->mkNode(
1808
      kind::EQUAL,
1809
8
      d_nodeManager->mkNode(
1810
          kind::BITVECTOR_UREM,
1811
4
          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, z_mul_two, w_mul_two),
1812
          d_p),
1813
8
      d_two);
1814
1815
  Node eq3 = d_nodeManager->mkNode(
1816
4
      kind::EQUAL, d_nodeManager->mkNode(kind::BITVECTOR_UREM, w, d_p), d_two);
1817
1818
4
  std::vector<Node> eqs = {eq1, eq2, eq3};
1819
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1820
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1821
2
  ASSERT_EQ(res.size(), 3);
1822
1823
  Node x1 = d_nodeManager->mkNode(
1824
      kind::BITVECTOR_UREM,
1825
6
      d_nodeManager->mkNode(
1826
          kind::BITVECTOR_PLUS,
1827
          d_one32,
1828
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_nine32)),
1829
8
      d_p);
1830
4
  Node z1 = d_ten32;
1831
4
  Node w1 = d_two32;
1832
1833
  Node y2 = d_nodeManager->mkNode(
1834
      kind::BITVECTOR_UREM,
1835
6
      d_nodeManager->mkNode(
1836
          kind::BITVECTOR_PLUS,
1837
          d_six32,
1838
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_five32)),
1839
8
      d_p);
1840
4
  Node z2 = d_ten32;
1841
4
  Node w2 = d_two32;
1842
1843
  /* result depends on order of variables in matrix */
1844
2
  if (res.find(d_x) == res.end())
1845
  {
1846
2
    ASSERT_EQ(res[d_y], y2);
1847
2
    ASSERT_EQ(res[d_z], z2);
1848
2
    ASSERT_EQ(res[w], w2);
1849
  }
1850
  else if (res.find(d_y) == res.end())
1851
  {
1852
    ASSERT_EQ(res[d_x], x1);
1853
    ASSERT_EQ(res[d_z], z1);
1854
    ASSERT_EQ(res[w], w1);
1855
  }
1856
  else
1857
  {
1858
    ASSERT_TRUE(false);
1859
  }
1860
}
1861
1862
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
1863
{
1864
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
1865
  BVGauss::Result ret;
1866
1867
  /* -------------------------------------------------------------------
1868
   *   lhs   rhs        lhs   rhs  modulo 11
1869
   *  --^--   ^        --^--   ^
1870
   *  1 0 9   7   -->  1 0 9   7
1871
   *  0 1 3   9        0 1 3   9
1872
   * ------------------------------------------------------------------- */
1873
1874
4
  Node zero = bv::utils::mkZero(8);
1875
4
  Node xx = d_nodeManager->mkVar("xx", d_nodeManager->mkBitVectorType(8));
1876
4
  Node yy = d_nodeManager->mkVar("yy", d_nodeManager->mkBitVectorType(8));
1877
4
  Node zz = d_nodeManager->mkVar("zz", d_nodeManager->mkBitVectorType(8));
1878
1879
  Node x = bv::utils::mkConcat(
1880
      d_zero,
1881
4
      bv::utils::mkConcat(
1882
8
          zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, xx), 7, 0)));
1883
  Node y = bv::utils::mkConcat(
1884
      d_zero,
1885
4
      bv::utils::mkConcat(
1886
8
          zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, yy), 7, 0)));
1887
  Node z = bv::utils::mkConcat(
1888
      d_zero,
1889
4
      bv::utils::mkConcat(
1890
8
          zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, zz), 7, 0)));
1891
1892
4
  Node x_mul_one = d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, d_one32);
1893
4
  Node nine_mul_z = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_nine32, z);
1894
4
  Node one_mul_y = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_one, y);
1895
4
  Node z_mul_three = d_nodeManager->mkNode(kind::BITVECTOR_MULT, z, d_three);
1896
1897
  Node eq1 = d_nodeManager->mkNode(
1898
      kind::EQUAL,
1899
8
      d_nodeManager->mkNode(
1900
          kind::BITVECTOR_UREM,
1901
4
          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_one, nine_mul_z),
1902
          d_p),
1903
8
      d_seven);
1904
1905
  Node eq2 = d_nodeManager->mkNode(
1906
      kind::EQUAL,
1907
8
      d_nodeManager->mkNode(
1908
          kind::BITVECTOR_UREM,
1909
4
          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, one_mul_y, z_mul_three),
1910
          d_p),
1911
8
      d_nine);
1912
1913
4
  std::vector<Node> eqs = {eq1, eq2};
1914
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
1915
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1916
2
  ASSERT_EQ(res.size(), 2);
1917
1918
2
  x = Rewriter::rewrite(x);
1919
2
  y = Rewriter::rewrite(y);
1920
2
  z = Rewriter::rewrite(z);
1921
1922
  Node x1 = d_nodeManager->mkNode(
1923
      kind::BITVECTOR_UREM,
1924
6
      d_nodeManager->mkNode(
1925
          kind::BITVECTOR_PLUS,
1926
          d_seven32,
1927
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, z, d_two32)),
1928
8
      d_p);
1929
  Node y1 = d_nodeManager->mkNode(
1930
      kind::BITVECTOR_UREM,
1931
6
      d_nodeManager->mkNode(
1932
          kind::BITVECTOR_PLUS,
1933
          d_nine32,
1934
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, z, d_eight32)),
1935
8
      d_p);
1936
1937
  Node x2 = d_nodeManager->mkNode(
1938
      kind::BITVECTOR_UREM,
1939
6
      d_nodeManager->mkNode(
1940
          kind::BITVECTOR_PLUS,
1941
          d_two32,
1942
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, y, d_three32)),
1943
8
      d_p);
1944
  Node z2 = d_nodeManager->mkNode(
1945
      kind::BITVECTOR_UREM,
1946
6
      d_nodeManager->mkNode(
1947
          kind::BITVECTOR_PLUS,
1948
          d_three32,
1949
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, y, d_seven32)),
1950
8
      d_p);
1951
1952
  Node y3 = d_nodeManager->mkNode(
1953
      kind::BITVECTOR_UREM,
1954
6
      d_nodeManager->mkNode(
1955
          kind::BITVECTOR_PLUS,
1956
          d_three32,
1957
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, d_four32)),
1958
8
      d_p);
1959
  Node z3 = d_nodeManager->mkNode(
1960
      kind::BITVECTOR_UREM,
1961
6
      d_nodeManager->mkNode(
1962
          kind::BITVECTOR_PLUS,
1963
          d_two32,
1964
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, d_six32)),
1965
8
      d_p);
1966
1967
  /* result depends on order of variables in matrix */
1968
2
  if (res.find(x) == res.end())
1969
  {
1970
    /*
1971
     *  y z x           y z x
1972
     *  0 9 1  7   -->  1 0 7  3
1973
     *  1 3 0  9        0 1 5  2
1974
     *
1975
     *  z y x           z y x
1976
     *  9 0 1  7   -->  1 0 5  2
1977
     *  3 1 0  9        0 1 7  3
1978
     */
1979
    ASSERT_EQ(res[Rewriter::rewrite(y)], y3);
1980
    ASSERT_EQ(res[Rewriter::rewrite(z)], z3);
1981
  }
1982
2
  else if (res.find(y) == res.end())
1983
  {
1984
    /*
1985
     *  x z y           x z y
1986
     *  1 9 0  7   -->  1 0 8  2
1987
     *  0 3 1  9        0 1 4  3
1988
     *
1989
     *  z x y           z x y
1990
     *  9 1 0  7   -->  1 0 4  3
1991
     *  3 0 1  9        0 1 8  2
1992
     */
1993
    ASSERT_EQ(res[x], x2);
1994
    ASSERT_EQ(res[z], z2);
1995
  }
1996
  else
1997
  {
1998
2
    ASSERT_EQ(res.find(z), res.end());
1999
    /*
2000
     *  x y z           x y z
2001
     *  1 0 9  7   -->  1 0 9  7
2002
     *  0 1 3  9        0 1 3  9
2003
     *
2004
     *  y x z           y x z
2005
     *  0 1 9  7   -->  1 0 3  9
2006
     *  1 0 3  9        0 1 9  7
2007
     */
2008
2
    ASSERT_EQ(res[x], x1);
2009
2
    ASSERT_EQ(res[y], y1);
2010
  }
2011
}
2012
2013
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
2014
{
2015
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
2016
  BVGauss::Result ret;
2017
2018
  /* -------------------------------------------------------------------
2019
   *   lhs   rhs        lhs   rhs  modulo 11
2020
   *  --^--   ^        --^--   ^
2021
   *  1 0 9   7   -->  1 0 9   7
2022
   *  0 1 3   9        0 1 3   9
2023
   * ------------------------------------------------------------------- */
2024
2025
4
  Node zero = bv::utils::mkZero(8);
2026
4
  Node xx = d_nodeManager->mkVar("xx", d_nodeManager->mkBitVectorType(8));
2027
4
  Node yy = d_nodeManager->mkVar("yy", d_nodeManager->mkBitVectorType(8));
2028
4
  Node zz = d_nodeManager->mkVar("zz", d_nodeManager->mkBitVectorType(8));
2029
2030
  Node x = bv::utils::mkConcat(
2031
      d_zero,
2032
4
      bv::utils::mkConcat(
2033
          zero,
2034
4
          bv::utils::mkExtract(
2035
8
              d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, zero, xx), 7, 0)));
2036
  Node y = bv::utils::mkConcat(
2037
      d_zero,
2038
4
      bv::utils::mkConcat(
2039
          zero,
2040
4
          bv::utils::mkExtract(
2041
8
              d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, zero, yy), 7, 0)));
2042
  Node z = bv::utils::mkConcat(
2043
      d_zero,
2044
4
      bv::utils::mkConcat(
2045
          zero,
2046
4
          bv::utils::mkExtract(
2047
8
              d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0)));
2048
2049
4
  NodeBuilder<> nbx(d_nodeManager.get(), kind::BITVECTOR_MULT);
2050
2
  nbx << d_x << d_one << x;
2051
4
  Node x_mul_one_mul_xx = nbx.constructNode();
2052
4
  NodeBuilder<> nby(d_nodeManager.get(), kind::BITVECTOR_MULT);
2053
2
  nby << d_y << y << d_one;
2054
4
  Node y_mul_yy_mul_one = nby.constructNode();
2055
4
  NodeBuilder<> nbz(d_nodeManager.get(), kind::BITVECTOR_MULT);
2056
2
  nbz << d_three << d_z << z;
2057
4
  Node three_mul_z_mul_zz = nbz.constructNode();
2058
4
  NodeBuilder<> nbz2(d_nodeManager.get(), kind::BITVECTOR_MULT);
2059
2
  nbz2 << d_z << d_nine << z;
2060
4
  Node z_mul_nine_mul_zz = nbz2.constructNode();
2061
2062
4
  Node x_mul_xx = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, x);
2063
4
  Node y_mul_yy = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, y);
2064
4
  Node z_mul_zz = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, z);
2065
2066
  Node eq1 = d_nodeManager->mkNode(
2067
      kind::EQUAL,
2068
8
      d_nodeManager->mkNode(
2069
          kind::BITVECTOR_UREM,
2070
4
          d_nodeManager->mkNode(
2071
              kind::BITVECTOR_PLUS, x_mul_one_mul_xx, z_mul_nine_mul_zz),
2072
          d_p),
2073
8
      d_seven);
2074
2075
  Node eq2 = d_nodeManager->mkNode(
2076
      kind::EQUAL,
2077
8
      d_nodeManager->mkNode(
2078
          kind::BITVECTOR_UREM,
2079
4
          d_nodeManager->mkNode(
2080
              kind::BITVECTOR_PLUS, y_mul_yy_mul_one, three_mul_z_mul_zz),
2081
          d_p),
2082
8
      d_nine);
2083
2084
4
  std::vector<Node> eqs = {eq1, eq2};
2085
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
2086
2
  ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
2087
2
  ASSERT_EQ(res.size(), 2);
2088
2089
2
  x_mul_xx = Rewriter::rewrite(x_mul_xx);
2090
2
  y_mul_yy = Rewriter::rewrite(y_mul_yy);
2091
2
  z_mul_zz = Rewriter::rewrite(z_mul_zz);
2092
2093
  Node x1 = d_nodeManager->mkNode(
2094
      kind::BITVECTOR_UREM,
2095
6
      d_nodeManager->mkNode(
2096
          kind::BITVECTOR_PLUS,
2097
          d_seven32,
2098
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_two32)),
2099
8
      d_p);
2100
  Node y1 = d_nodeManager->mkNode(
2101
      kind::BITVECTOR_UREM,
2102
6
      d_nodeManager->mkNode(
2103
          kind::BITVECTOR_PLUS,
2104
          d_nine32,
2105
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_eight32)),
2106
8
      d_p);
2107
2108
  Node x2 = d_nodeManager->mkNode(
2109
      kind::BITVECTOR_UREM,
2110
6
      d_nodeManager->mkNode(
2111
          kind::BITVECTOR_PLUS,
2112
          d_two32,
2113
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_three32)),
2114
8
      d_p);
2115
  Node z2 = d_nodeManager->mkNode(
2116
      kind::BITVECTOR_UREM,
2117
6
      d_nodeManager->mkNode(
2118
          kind::BITVECTOR_PLUS,
2119
          d_three32,
2120
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_seven32)),
2121
8
      d_p);
2122
2123
  Node y3 = d_nodeManager->mkNode(
2124
      kind::BITVECTOR_UREM,
2125
6
      d_nodeManager->mkNode(
2126
          kind::BITVECTOR_PLUS,
2127
          d_three32,
2128
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_four32)),
2129
8
      d_p);
2130
  Node z3 = d_nodeManager->mkNode(
2131
      kind::BITVECTOR_UREM,
2132
6
      d_nodeManager->mkNode(
2133
          kind::BITVECTOR_PLUS,
2134
          d_two32,
2135
4
          d_nodeManager->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_six32)),
2136
8
      d_p);
2137
2138
  /* result depends on order of variables in matrix */
2139
2
  if (res.find(x_mul_xx) == res.end())
2140
  {
2141
    /*
2142
     *  y z x           y z x
2143
     *  0 9 1  7   -->  1 0 7  3
2144
     *  1 3 0  9        0 1 5  2
2145
     *
2146
     *  z y x           z y x
2147
     *  9 0 1  7   -->  1 0 5  2
2148
     *  3 1 0  9        0 1 7  3
2149
     */
2150
    ASSERT_EQ(res[y_mul_yy], y3);
2151
    ASSERT_EQ(res[z_mul_zz], z3);
2152
  }
2153
2
  else if (res.find(y_mul_yy) == res.end())
2154
  {
2155
    /*
2156
     *  x z y           x z y
2157
     *  1 9 0  7   -->  1 0 8  2
2158
     *  0 3 1  9        0 1 4  3
2159
     *
2160
     *  z x y           z x y
2161
     *  9 1 0  7   -->  1 0 4  3
2162
     *  3 0 1  9        0 1 8  2
2163
     */
2164
    ASSERT_EQ(res[x_mul_xx], x2);
2165
    ASSERT_EQ(res[z_mul_zz], z2);
2166
  }
2167
  else
2168
  {
2169
2
    ASSERT_EQ(res.find(z_mul_zz), res.end());
2170
    /*
2171
     *  x y z           x y z
2172
     *  1 0 9  7   -->  1 0 9  7
2173
     *  0 1 3  9        0 1 3  9
2174
     *
2175
     *  y x z           y x z
2176
     *  0 1 9  7   -->  1 0 3  9
2177
     *  1 0 3  9        0 1 9  7
2178
     */
2179
2
    ASSERT_EQ(res[x_mul_xx], x1);
2180
2
    ASSERT_EQ(res[y_mul_yy], y1);
2181
  }
2182
}
2183
2184
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1)
2185
{
2186
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
2187
  BVGauss::Result ret;
2188
2189
  /* -------------------------------------------------------------------
2190
   * 3x / 2z = 4  modulo 11
2191
   * 2x % 5y = 2
2192
   * y O z = 5
2193
   * ------------------------------------------------------------------- */
2194
2195
  Node n1 = d_nodeManager->mkNode(
2196
      kind::BITVECTOR_UDIV,
2197
4
      d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_three, d_x),
2198
8
      d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_two, d_y));
2199
  Node n2 = d_nodeManager->mkNode(
2200
      kind::BITVECTOR_UREM,
2201
4
      d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_two, d_x),
2202
8
      d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_five, d_y));
2203
2204
  Node n3 = bv::utils::mkConcat(
2205
      d_zero,
2206
4
      bv::utils::mkExtract(
2207
8
          d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, d_y, d_z), 15, 0));
2208
2209
  Node eq1 = d_nodeManager->mkNode(
2210
      kind::EQUAL,
2211
4
      d_nodeManager->mkNode(kind::BITVECTOR_UREM, n1, d_p),
2212
8
      d_four);
2213
2214
  Node eq2 = d_nodeManager->mkNode(
2215
4
      kind::EQUAL, d_nodeManager->mkNode(kind::BITVECTOR_UREM, n2, d_p), d_two);
2216
2217
  Node eq3 = d_nodeManager->mkNode(
2218
      kind::EQUAL,
2219
4
      d_nodeManager->mkNode(kind::BITVECTOR_UREM, n3, d_p),
2220
8
      d_five);
2221
2222
4
  std::vector<Node> eqs = {eq1, eq2, eq3};
2223
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
2224
2
  ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
2225
2
  ASSERT_EQ(res.size(), 3);
2226
2227
2
  ASSERT_EQ(res[n1], d_four32);
2228
2
  ASSERT_EQ(res[n2], d_two32);
2229
2
  ASSERT_EQ(res[n3], d_five32);
2230
}
2231
2232
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2)
2233
{
2234
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
2235
  BVGauss::Result ret;
2236
2237
  /* -------------------------------------------------------------------
2238
   * x*y = 4  modulo 11
2239
   * x*y*z = 2
2240
   * 2*x*y + 2*z = 9
2241
   * ------------------------------------------------------------------- */
2242
2243
4
  Node zero32 = bv::utils::mkZero(32);
2244
2245
  Node x = bv::utils::mkConcat(
2246
4
      zero32, d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)));
2247
  Node y = bv::utils::mkConcat(
2248
4
      zero32, d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)));
2249
  Node z = bv::utils::mkConcat(
2250
4
      zero32, d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16)));
2251
2252
4
  Node n1 = d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y);
2253
  Node n2 =
2254
      d_nodeManager->mkNode(kind::BITVECTOR_MULT,
2255
4
                            d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y),
2256
8
                            z);
2257
  Node n3 = d_nodeManager->mkNode(
2258
      kind::BITVECTOR_PLUS,
2259
10
      d_nodeManager->mkNode(kind::BITVECTOR_MULT,
2260
4
                            d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y),
2261
4
                            bv::utils::mkConcat(d_zero, d_two)),
2262
8
      d_nodeManager->mkNode(
2263
14
          kind::BITVECTOR_MULT, bv::utils::mkConcat(d_zero, d_two), z));
2264
2265
  Node eq1 = d_nodeManager->mkNode(
2266
      kind::EQUAL,
2267
6
      d_nodeManager->mkNode(
2268
4
          kind::BITVECTOR_UREM, n1, bv::utils::mkConcat(d_zero, d_p)),
2269
8
      bv::utils::mkConcat(d_zero, d_four));
2270
2271
  Node eq2 = d_nodeManager->mkNode(
2272
      kind::EQUAL,
2273
6
      d_nodeManager->mkNode(
2274
4
          kind::BITVECTOR_UREM, n2, bv::utils::mkConcat(d_zero, d_p)),
2275
8
      bv::utils::mkConcat(d_zero, d_two));
2276
2277
  Node eq3 = d_nodeManager->mkNode(
2278
      kind::EQUAL,
2279
6
      d_nodeManager->mkNode(
2280
4
          kind::BITVECTOR_UREM, n3, bv::utils::mkConcat(d_zero, d_p)),
2281
8
      bv::utils::mkConcat(d_zero, d_nine));
2282
2283
4
  std::vector<Node> eqs = {eq1, eq2, eq3};
2284
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
2285
2
  ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
2286
2
  ASSERT_EQ(res.size(), 3);
2287
2288
2
  n1 = Rewriter::rewrite(n1);
2289
2
  n2 = Rewriter::rewrite(n2);
2290
2
  z = Rewriter::rewrite(z);
2291
2292
2
  ASSERT_EQ(res[n1], bv::utils::mkConst(48, 4));
2293
2
  ASSERT_EQ(res[n2], bv::utils::mkConst(48, 2));
2294
2295
4
  Integer twoxy = (res[n1].getConst<BitVector>().getValue() * Integer(2))
2296
4
                      .euclidianDivideRemainder(Integer(48));
2297
4
  Integer twoz = (res[z].getConst<BitVector>().getValue() * Integer(2))
2298
4
                     .euclidianDivideRemainder(Integer(48));
2299
4
  Integer r = (twoxy + twoz).euclidianDivideRemainder(Integer(11));
2300
2
  ASSERT_EQ(r, Integer(9));
2301
}
2302
2303
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_invalid)
2304
{
2305
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
2306
  BVGauss::Result ret;
2307
2308
  /* -------------------------------------------------------------------
2309
   * x*y = 4  modulo 11
2310
   * x*y*z = 2
2311
   * 2*x*y = 9
2312
   * ------------------------------------------------------------------- */
2313
2314
4
  Node zero32 = bv::utils::mkZero(32);
2315
2316
  Node x = bv::utils::mkConcat(
2317
4
      zero32, d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)));
2318
  Node y = bv::utils::mkConcat(
2319
4
      zero32, d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)));
2320
  Node z = bv::utils::mkConcat(
2321
4
      zero32, d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16)));
2322
2323
4
  Node n1 = d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y);
2324
  Node n2 =
2325
      d_nodeManager->mkNode(kind::BITVECTOR_MULT,
2326
4
                            d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y),
2327
8
                            z);
2328
  Node n3 =
2329
      d_nodeManager->mkNode(kind::BITVECTOR_MULT,
2330
4
                            d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y),
2331
8
                            bv::utils::mkConcat(d_zero, d_two));
2332
2333
  Node eq1 = d_nodeManager->mkNode(
2334
      kind::EQUAL,
2335
6
      d_nodeManager->mkNode(
2336
4
          kind::BITVECTOR_UREM, n1, bv::utils::mkConcat(d_zero, d_p)),
2337
8
      bv::utils::mkConcat(d_zero, d_four));
2338
2339
  Node eq2 = d_nodeManager->mkNode(
2340
      kind::EQUAL,
2341
6
      d_nodeManager->mkNode(
2342
4
          kind::BITVECTOR_UREM, n2, bv::utils::mkConcat(d_zero, d_p)),
2343
8
      bv::utils::mkConcat(d_zero, d_two));
2344
2345
  Node eq3 = d_nodeManager->mkNode(
2346
      kind::EQUAL,
2347
6
      d_nodeManager->mkNode(
2348
4
          kind::BITVECTOR_UREM, n3, bv::utils::mkConcat(d_zero, d_p)),
2349
8
      bv::utils::mkConcat(d_zero, d_nine));
2350
2351
4
  std::vector<Node> eqs = {eq1, eq2, eq3};
2352
2
  ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
2353
2
  ASSERT_EQ(ret, BVGauss::Result::INVALID);
2354
}
2355
2356
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1)
2357
{
2358
  /* -------------------------------------------------------------------
2359
   *   lhs   rhs  modulo 11
2360
   *  --^--   ^
2361
   *  1 1 1   5
2362
   *  2 3 5   8
2363
   *  4 0 5   2
2364
   * ------------------------------------------------------------------- */
2365
2366
  Node eq1 = d_nodeManager->mkNode(
2367
      kind::EQUAL,
2368
8
      d_nodeManager->mkNode(
2369
          kind::BITVECTOR_UREM,
2370
8
          d_nodeManager->mkNode(
2371
              kind::BITVECTOR_PLUS,
2372
4
              d_nodeManager->mkNode(
2373
                  kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one),
2374
              d_z_mul_one),
2375
          d_p),
2376
8
      d_five);
2377
2378
  Node eq2 = d_nodeManager->mkNode(
2379
      kind::EQUAL,
2380
8
      d_nodeManager->mkNode(
2381
          kind::BITVECTOR_UREM,
2382
8
          d_nodeManager->mkNode(
2383
              kind::BITVECTOR_PLUS,
2384
4
              d_nodeManager->mkNode(
2385
                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three),
2386
              d_z_mul_five),
2387
          d_p),
2388
8
      d_eight);
2389
2390
  Node eq3 = d_nodeManager->mkNode(
2391
      kind::EQUAL,
2392
8
      d_nodeManager->mkNode(
2393
          kind::BITVECTOR_UREM,
2394
4
          d_nodeManager->mkNode(
2395
              kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five),
2396
          d_p),
2397
8
      d_two);
2398
2399
  Node a = d_nodeManager->mkNode(
2400
4
      kind::AND, d_nodeManager->mkNode(kind::AND, eq1, eq2), eq3);
2401
2402
4
  AssertionPipeline apipe;
2403
2
  apipe.push_back(a);
2404
4
  passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
2405
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
2406
2
  PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
2407
2
  ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
2408
  Node resx = d_nodeManager->mkNode(
2409
4
      kind::EQUAL, d_x, d_nodeManager->mkConst<BitVector>(BitVector(32, 3u)));
2410
  Node resy = d_nodeManager->mkNode(
2411
4
      kind::EQUAL, d_y, d_nodeManager->mkConst<BitVector>(BitVector(32, 4u)));
2412
  Node resz = d_nodeManager->mkNode(
2413
4
      kind::EQUAL, d_z, d_nodeManager->mkConst<BitVector>(BitVector(32, 9u)));
2414
2
  ASSERT_EQ(apipe.size(), 4);
2415
2
  ASSERT_NE(std::find(apipe.begin(), apipe.end(), resx), apipe.end());
2416
2
  ASSERT_NE(std::find(apipe.begin(), apipe.end(), resy), apipe.end());
2417
2
  ASSERT_NE(std::find(apipe.begin(), apipe.end(), resz), apipe.end());
2418
}
2419
2420
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
2421
{
2422
  /* -------------------------------------------------------------------
2423
   *   lhs   rhs        lhs   rhs   modulo 11
2424
   *  --^--   ^        --^--   ^
2425
   *  1 1 1   5        1 0 0   3
2426
   *  2 3 5   8        0 1 0   4
2427
   *  4 0 5   2        0 0 1   9
2428
   *
2429
   *   lhs   rhs        lhs   rhs   modulo 7
2430
   *  --^--   ^        --^--   ^
2431
   *  2 6 0   4        1 0 0   3
2432
   *  4 6 0   3        0 1 0   2
2433
   * ------------------------------------------------------------------- */
2434
2435
  Node eq1 = d_nodeManager->mkNode(
2436
      kind::EQUAL,
2437
8
      d_nodeManager->mkNode(
2438
          kind::BITVECTOR_UREM,
2439
8
          d_nodeManager->mkNode(
2440
              kind::BITVECTOR_PLUS,
2441
4
              d_nodeManager->mkNode(
2442
                  kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one),
2443
              d_z_mul_one),
2444
          d_p),
2445
8
      d_five);
2446
2447
  Node eq2 = d_nodeManager->mkNode(
2448
      kind::EQUAL,
2449
8
      d_nodeManager->mkNode(
2450
          kind::BITVECTOR_UREM,
2451
8
          d_nodeManager->mkNode(
2452
              kind::BITVECTOR_PLUS,
2453
4
              d_nodeManager->mkNode(
2454
                  kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three),
2455
              d_z_mul_five),
2456
          d_p),
2457
8
      d_eight);
2458
2459
  Node eq3 = d_nodeManager->mkNode(
2460
      kind::EQUAL,
2461
8
      d_nodeManager->mkNode(
2462
          kind::BITVECTOR_UREM,
2463
4
          d_nodeManager->mkNode(
2464
              kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five),
2465
          d_p),
2466
8
      d_two);
2467
2468
4
  Node y_mul_six = d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_six);
2469
2470
  Node eq4 = d_nodeManager->mkNode(
2471
      kind::EQUAL,
2472
8
      d_nodeManager->mkNode(
2473
          kind::BITVECTOR_UREM,
2474
4
          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, y_mul_six),
2475
          d_seven),
2476
8
      d_four);
2477
2478
  Node eq5 = d_nodeManager->mkNode(
2479
      kind::EQUAL,
2480
8
      d_nodeManager->mkNode(
2481
          kind::BITVECTOR_UREM,
2482
4
          d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, y_mul_six),
2483
          d_seven),
2484
8
      d_three);
2485
2486
  Node a = d_nodeManager->mkNode(
2487
4
      kind::AND, d_nodeManager->mkNode(kind::AND, eq1, eq2), eq3);
2488
2489
4
  AssertionPipeline apipe;
2490
2
  apipe.push_back(a);
2491
2
  apipe.push_back(eq4);
2492
2
  apipe.push_back(eq5);
2493
4
  passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
2494
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
2495
2
  PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
2496
2
  ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
2497
  Node resx1 = d_nodeManager->mkNode(
2498
4
      kind::EQUAL, d_x, d_nodeManager->mkConst<BitVector>(BitVector(32, 3u)));
2499
  Node resx2 = d_nodeManager->mkNode(
2500
4
      kind::EQUAL, d_x, d_nodeManager->mkConst<BitVector>(BitVector(32, 3u)));
2501
  Node resy1 = d_nodeManager->mkNode(
2502
4
      kind::EQUAL, d_y, d_nodeManager->mkConst<BitVector>(BitVector(32, 4u)));
2503
  Node resy2 = d_nodeManager->mkNode(
2504
4
      kind::EQUAL, d_y, d_nodeManager->mkConst<BitVector>(BitVector(32, 2u)));
2505
  Node resz = d_nodeManager->mkNode(
2506
4
      kind::EQUAL, d_z, d_nodeManager->mkConst<BitVector>(BitVector(32, 9u)));
2507
2
  ASSERT_EQ(apipe.size(), 8);
2508
2
  ASSERT_NE(std::find(apipe.begin(), apipe.end(), resx1), apipe.end());
2509
2
  ASSERT_NE(std::find(apipe.begin(), apipe.end(), resx2), apipe.end());
2510
2
  ASSERT_NE(std::find(apipe.begin(), apipe.end(), resy1), apipe.end());
2511
2
  ASSERT_NE(std::find(apipe.begin(), apipe.end(), resy2), apipe.end());
2512
2
  ASSERT_NE(std::find(apipe.begin(), apipe.end(), resz), apipe.end());
2513
}
2514
2515
46
TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
2516
{
2517
  /* -------------------------------------------------------------------
2518
   *   lhs   rhs        lhs   rhs  modulo 11
2519
   *  --^--   ^        --^--   ^
2520
   *  1 0 9   7   -->  1 0 9   7
2521
   *  0 1 3   9        0 1 3   9
2522
   * ------------------------------------------------------------------- */
2523
2524
  Node eq1 = d_nodeManager->mkNode(
2525
      kind::EQUAL,
2526
8
      d_nodeManager->mkNode(
2527
          kind::BITVECTOR_UREM,
2528
4
          d_nodeManager->mkNode(
2529
              kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine),
2530
          d_p),
2531
8
      d_seven);
2532
2533
  Node eq2 = d_nodeManager->mkNode(
2534
      kind::EQUAL,
2535
8
      d_nodeManager->mkNode(
2536
          kind::BITVECTOR_UREM,
2537
4
          d_nodeManager->mkNode(
2538
              kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three),
2539
          d_p),
2540
8
      d_nine);
2541
2542
4
  AssertionPipeline apipe;
2543
2
  apipe.push_back(eq1);
2544
2
  apipe.push_back(eq2);
2545
4
  passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
2546
4
  std::unordered_map<Node, Node, NodeHashFunction> res;
2547
2
  PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
2548
2
  ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
2549
2
  ASSERT_EQ(apipe.size(), 4);
2550
2551
  Node resx1 = d_nodeManager->mkNode(
2552
      kind::EQUAL,
2553
      d_x,
2554
8
      d_nodeManager->mkNode(
2555
          kind::BITVECTOR_UREM,
2556
6
          d_nodeManager->mkNode(
2557
              kind::BITVECTOR_PLUS,
2558
              d_seven32,
2559
4
              d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)),
2560
6
          d_p));
2561
  Node resy1 = d_nodeManager->mkNode(
2562
      kind::EQUAL,
2563
      d_y,
2564
8
      d_nodeManager->mkNode(
2565
          kind::BITVECTOR_UREM,
2566
6
          d_nodeManager->mkNode(
2567
              kind::BITVECTOR_PLUS,
2568
              d_nine32,
2569
4
              d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)),
2570
6
          d_p));
2571
2572
  Node resx2 = d_nodeManager->mkNode(
2573
      kind::EQUAL,
2574
      d_x,
2575
8
      d_nodeManager->mkNode(
2576
          kind::BITVECTOR_UREM,
2577
6
          d_nodeManager->mkNode(
2578
              kind::BITVECTOR_PLUS,
2579
              d_two32,
2580
4
              d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)),
2581
6
          d_p));
2582
  Node resz2 = d_nodeManager->mkNode(
2583
      kind::EQUAL,
2584
      d_z,
2585
8
      d_nodeManager->mkNode(
2586
          kind::BITVECTOR_UREM,
2587
6
          d_nodeManager->mkNode(
2588
              kind::BITVECTOR_PLUS,
2589
              d_three32,
2590
4
              d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)),
2591
6
          d_p));
2592
2593
  Node resy3 = d_nodeManager->mkNode(
2594
      kind::EQUAL,
2595
      d_y,
2596
8
      d_nodeManager->mkNode(
2597
          kind::BITVECTOR_UREM,
2598
6
          d_nodeManager->mkNode(
2599
              kind::BITVECTOR_PLUS,
2600
              d_three32,
2601
4
              d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)),
2602
6
          d_p));
2603
  Node resz3 = d_nodeManager->mkNode(
2604
      kind::EQUAL,
2605
      d_z,
2606
8
      d_nodeManager->mkNode(
2607
          kind::BITVECTOR_UREM,
2608
6
          d_nodeManager->mkNode(
2609
              kind::BITVECTOR_PLUS,
2610
              d_two32,
2611
4
              d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)),
2612
6
          d_p));
2613
2614
2
  bool fx1 = std::find(apipe.begin(), apipe.end(), resx1) != apipe.end();
2615
2
  bool fy1 = std::find(apipe.begin(), apipe.end(), resy1) != apipe.end();
2616
2
  bool fx2 = std::find(apipe.begin(), apipe.end(), resx2) != apipe.end();
2617
2
  bool fz2 = std::find(apipe.begin(), apipe.end(), resz2) != apipe.end();
2618
2
  bool fy3 = std::find(apipe.begin(), apipe.end(), resy3) != apipe.end();
2619
2
  bool fz3 = std::find(apipe.begin(), apipe.end(), resz3) != apipe.end();
2620
2621
  /* result depends on order of variables in matrix */
2622
2
  ASSERT_TRUE((fx1 && fy1) || (fx2 && fz2) || (fy3 && fz3));
2623
}
2624
2625
46
TEST_F(TestPPWhiteBVGauss, get_min_bw1)
2626
{
2627
2
  ASSERT_EQ(BVGauss::getMinBwExpr(bv::utils::mkConst(32, 11)), 4);
2628
2629
2
  ASSERT_EQ(BVGauss::getMinBwExpr(d_p), 4);
2630
2
  ASSERT_EQ(BVGauss::getMinBwExpr(d_x), 16);
2631
2632
4
  Node extp = bv::utils::mkExtract(d_p, 4, 0);
2633
2
  ASSERT_EQ(BVGauss::getMinBwExpr(extp), 4);
2634
4
  Node extx = bv::utils::mkExtract(d_x, 4, 0);
2635
2
  ASSERT_EQ(BVGauss::getMinBwExpr(extx), 5);
2636
2637
  Node zextop8 =
2638
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(8));
2639
  Node zextop16 =
2640
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(16));
2641
  Node zextop32 =
2642
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(32));
2643
  Node zextop40 =
2644
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(40));
2645
2646
4
  Node zext40p = d_nodeManager->mkNode(zextop8, d_p);
2647
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext40p), 4);
2648
4
  Node zext40x = d_nodeManager->mkNode(zextop8, d_x);
2649
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext40x), 16);
2650
2651
4
  Node zext48p = d_nodeManager->mkNode(zextop16, d_p);
2652
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext48p), 4);
2653
4
  Node zext48x = d_nodeManager->mkNode(zextop16, d_x);
2654
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext48x), 16);
2655
2656
4
  Node p8 = d_nodeManager->mkConst<BitVector>(BitVector(8, 11u));
2657
4
  Node x8 = d_nodeManager->mkVar("x8", d_nodeManager->mkBitVectorType(8));
2658
2659
4
  Node zext48p8 = d_nodeManager->mkNode(zextop40, p8);
2660
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext48p8), 4);
2661
4
  Node zext48x8 = d_nodeManager->mkNode(zextop40, x8);
2662
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext48x8), 8);
2663
2664
4
  Node mult1p = d_nodeManager->mkNode(kind::BITVECTOR_MULT, extp, extp);
2665
2
  ASSERT_EQ(BVGauss::getMinBwExpr(mult1p), 5);
2666
4
  Node mult1x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, extx, extx);
2667
2
  ASSERT_EQ(BVGauss::getMinBwExpr(mult1x), 0);
2668
2669
4
  Node mult2p = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p);
2670
2
  ASSERT_EQ(BVGauss::getMinBwExpr(mult2p), 7);
2671
4
  Node mult2x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x);
2672
2
  ASSERT_EQ(BVGauss::getMinBwExpr(mult2x), 32);
2673
2674
4
  NodeBuilder<> nbmult3p(kind::BITVECTOR_MULT);
2675
2
  nbmult3p << zext48p << zext48p << zext48p;
2676
4
  Node mult3p = nbmult3p;
2677
2
  ASSERT_EQ(BVGauss::getMinBwExpr(mult3p), 11);
2678
4
  NodeBuilder<> nbmult3x(kind::BITVECTOR_MULT);
2679
2
  nbmult3x << zext48x << zext48x << zext48x;
2680
4
  Node mult3x = nbmult3x;
2681
2
  ASSERT_EQ(BVGauss::getMinBwExpr(mult3x), 48);
2682
2683
4
  NodeBuilder<> nbmult4p(kind::BITVECTOR_MULT);
2684
2
  nbmult4p << zext48p << zext48p8 << zext48p;
2685
4
  Node mult4p = nbmult4p;
2686
2
  ASSERT_EQ(BVGauss::getMinBwExpr(mult4p), 11);
2687
4
  NodeBuilder<> nbmult4x(kind::BITVECTOR_MULT);
2688
2
  nbmult4x << zext48x << zext48x8 << zext48x;
2689
4
  Node mult4x = nbmult4x;
2690
2
  ASSERT_EQ(BVGauss::getMinBwExpr(mult4x), 40);
2691
2692
4
  Node concat1p = bv::utils::mkConcat(d_p, zext48p);
2693
2
  ASSERT_EQ(BVGauss::getMinBwExpr(concat1p), 52);
2694
4
  Node concat1x = bv::utils::mkConcat(d_x, zext48x);
2695
2
  ASSERT_EQ(BVGauss::getMinBwExpr(concat1x), 64);
2696
2697
4
  Node concat2p = bv::utils::mkConcat(bv::utils::mkZero(16), zext48p);
2698
2
  ASSERT_EQ(BVGauss::getMinBwExpr(concat2p), 4);
2699
4
  Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x);
2700
2
  ASSERT_EQ(BVGauss::getMinBwExpr(concat2x), 16);
2701
2702
4
  Node udiv1p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p);
2703
2
  ASSERT_EQ(BVGauss::getMinBwExpr(udiv1p), 1);
2704
4
  Node udiv1x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x);
2705
2
  ASSERT_EQ(BVGauss::getMinBwExpr(udiv1x), 48);
2706
2707
4
  Node udiv2p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p8);
2708
2
  ASSERT_EQ(BVGauss::getMinBwExpr(udiv2p), 1);
2709
4
  Node udiv2x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x8);
2710
2
  ASSERT_EQ(BVGauss::getMinBwExpr(udiv2x), 48);
2711
2712
4
  Node urem1p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p);
2713
2
  ASSERT_EQ(BVGauss::getMinBwExpr(urem1p), 1);
2714
4
  Node urem1x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x);
2715
2
  ASSERT_EQ(BVGauss::getMinBwExpr(urem1x), 1);
2716
2717
4
  Node urem2p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p8);
2718
2
  ASSERT_EQ(BVGauss::getMinBwExpr(urem2p), 1);
2719
4
  Node urem2x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x8);
2720
2
  ASSERT_EQ(BVGauss::getMinBwExpr(urem2x), 16);
2721
2722
4
  Node urem3p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p8, zext48p);
2723
2
  ASSERT_EQ(BVGauss::getMinBwExpr(urem3p), 1);
2724
4
  Node urem3x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x8, zext48x);
2725
2
  ASSERT_EQ(BVGauss::getMinBwExpr(urem3x), 8);
2726
2727
4
  Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, extp, extp);
2728
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add1p), 5);
2729
4
  Node add1x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, extx, extx);
2730
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add1x), 0);
2731
2732
4
  Node add2p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext40p, zext40p);
2733
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add2p), 5);
2734
4
  Node add2x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext40x, zext40x);
2735
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add2x), 17);
2736
2737
4
  Node add3p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext48p8, zext48p);
2738
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add3p), 5);
2739
4
  Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x);
2740
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add3x), 17);
2741
2742
4
  NodeBuilder<> nbadd4p(kind::BITVECTOR_PLUS);
2743
2
  nbadd4p << zext48p << zext48p << zext48p;
2744
4
  Node add4p = nbadd4p;
2745
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add4p), 6);
2746
4
  NodeBuilder<> nbadd4x(kind::BITVECTOR_PLUS);
2747
2
  nbadd4x << zext48x << zext48x << zext48x;
2748
4
  Node add4x = nbadd4x;
2749
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add4x), 18);
2750
2751
4
  NodeBuilder<> nbadd5p(kind::BITVECTOR_PLUS);
2752
2
  nbadd5p << zext48p << zext48p8 << zext48p;
2753
4
  Node add5p = nbadd5p;
2754
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add5p), 6);
2755
4
  NodeBuilder<> nbadd5x(kind::BITVECTOR_PLUS);
2756
2
  nbadd5x << zext48x << zext48x8 << zext48x;
2757
4
  Node add5x = nbadd5x;
2758
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add5x), 18);
2759
2760
4
  NodeBuilder<> nbadd6p(kind::BITVECTOR_PLUS);
2761
2
  nbadd6p << zext48p << zext48p << zext48p << zext48p;
2762
4
  Node add6p = nbadd6p;
2763
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add6p), 6);
2764
4
  NodeBuilder<> nbadd6x(kind::BITVECTOR_PLUS);
2765
2
  nbadd6x << zext48x << zext48x << zext48x << zext48x;
2766
4
  Node add6x = nbadd6x;
2767
2
  ASSERT_EQ(BVGauss::getMinBwExpr(add6x), 18);
2768
2769
4
  Node not1p = d_nodeManager->mkNode(kind::BITVECTOR_NOT, zext40p);
2770
2
  ASSERT_EQ(BVGauss::getMinBwExpr(not1p), 40);
2771
4
  Node not1x = d_nodeManager->mkNode(kind::BITVECTOR_NOT, zext40x);
2772
2
  ASSERT_EQ(BVGauss::getMinBwExpr(not1x), 40);
2773
}
2774
2775
46
TEST_F(TestPPWhiteBVGauss, get_min_bw2)
2776
{
2777
  /* ((_ zero_extend 5)
2778
   *     ((_ extract 7 0) ((_ zero_extend 15) d_p)))  */
2779
  Node zextop5 =
2780
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2781
  Node zextop15 =
2782
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(15));
2783
4
  Node zext1 = d_nodeManager->mkNode(zextop15, d_p);
2784
4
  Node ext = bv::utils::mkExtract(zext1, 7, 0);
2785
4
  Node zext2 = d_nodeManager->mkNode(zextop5, ext);
2786
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 4);
2787
}
2788
2789
46
TEST_F(TestPPWhiteBVGauss, get_min_bw3a)
2790
{
2791
  /* ((_ zero_extend 5)
2792
   *     (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x z)))
2793
   *             ((_ extract 4 0) z)))  */
2794
4
  Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16));
2795
4
  Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16));
2796
4
  Node z = d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16));
2797
  Node zextop5 =
2798
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2799
4
  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, x, y);
2800
4
  Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
2801
4
  Node ext1 = bv::utils::mkExtract(zext1, 4, 0);
2802
4
  Node ext2 = bv::utils::mkExtract(z, 4, 0);
2803
4
  Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2);
2804
4
  Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
2805
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5);
2806
}
2807
2808
46
TEST_F(TestPPWhiteBVGauss, get_min_bw3b)
2809
{
2810
  /* ((_ zero_extend 5)
2811
   *     (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x z)))
2812
   *             ((_ extract 4 0) z)))  */
2813
  Node zextop5 =
2814
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2815
4
  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, d_x, d_y);
2816
4
  Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
2817
4
  Node ext1 = bv::utils::mkExtract(zext1, 4, 0);
2818
4
  Node ext2 = bv::utils::mkExtract(d_z, 4, 0);
2819
4
  Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2);
2820
4
  Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
2821
2
  ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5);
2822
}
2823
2824
46
TEST_F(TestPPWhiteBVGauss, get_min_bw4a)
2825
{
2826
  /* (bvadd
2827
   *     ((_ zero_extend 5)
2828
   *         (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x y)))
2829
   *                 ((_ extract 4 0) z)))
2830
   *     ((_ zero_extend 7)
2831
   *         (bvudiv ((_ extract 2 0) ((_ zero_extend 5) (bvudiv x y)))
2832
   *                 ((_ extract 2 0) z)))  */
2833
4
  Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16));
2834
4
  Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16));
2835
4
  Node z = d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16));
2836
  Node zextop5 =
2837
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2838
  Node zextop7 =
2839
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(7));
2840
2841
4
  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, x, y);
2842
4
  Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
2843
2844
4
  Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0);
2845
4
  Node ext2_1 = bv::utils::mkExtract(z, 4, 0);
2846
4
  Node udiv2_1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_1, ext2_1);
2847
4
  Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1);
2848
2849
4
  Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0);
2850
4
  Node ext2_2 = bv::utils::mkExtract(z, 2, 0);
2851
4
  Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2);
2852
4
  Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2);
2853
2854
4
  Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
2855
2856
2
  ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6);
2857
}
2858
2859
46
TEST_F(TestPPWhiteBVGauss, get_min_bw4b)
2860
{
2861
  /* (bvadd
2862
   *     ((_ zero_extend 5)
2863
   *         (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x y)))
2864
   *                 ((_ extract 4 0) z)))
2865
   *     ((_ zero_extend 7)
2866
   *         (bvudiv ((_ extract 2 0) ((_ zero_extend 5) (bvudiv x y)))
2867
   *                 ((_ extract 2 0) z)))  */
2868
  Node zextop5 =
2869
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2870
  Node zextop7 =
2871
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(7));
2872
2873
4
  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, d_x, d_y);
2874
4
  Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
2875
2876
4
  Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0);
2877
4
  Node ext2_1 = bv::utils::mkExtract(d_z, 4, 0);
2878
4
  Node udiv2_1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_1, ext2_1);
2879
4
  Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1);
2880
2881
4
  Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0);
2882
4
  Node ext2_2 = bv::utils::mkExtract(d_z, 2, 0);
2883
4
  Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2);
2884
4
  Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2);
2885
2886
4
  Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
2887
2888
2
  ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6);
2889
}
2890
2891
46
TEST_F(TestPPWhiteBVGauss, get_min_bw5a)
2892
{
2893
  /* (bvadd
2894
   *   (bvadd
2895
   *     (bvadd
2896
   *       (bvadd
2897
   *         (bvadd
2898
   *           (bvadd
2899
   *             (bvadd (bvmul (_ bv86 13)
2900
   *                           ((_ zero_extend 5)
2901
   *                             ((_ extract 7 0) ((_ zero_extend 15) x))))
2902
   *                    (bvmul (_ bv41 13)
2903
   *                           ((_ zero_extend 5)
2904
   *                             ((_ extract 7 0) ((_ zero_extend 15) y)))))
2905
   *             (bvmul (_ bv37 13)
2906
   *                    ((_ zero_extend 5)
2907
   *                      ((_ extract 7 0) ((_ zero_extend 15) z)))))
2908
   *           (bvmul (_ bv170 13)
2909
   *                  ((_ zero_extend 5)
2910
   *                    ((_ extract 7 0) ((_ zero_extend 15) u)))))
2911
   *         (bvmul (_ bv112 13)
2912
   *                ((_ zero_extend 5)
2913
   *                  ((_ extract 7 0) ((_ zero_extend 15) v)))))
2914
   *       (bvmul (_ bv195 13) ((_ zero_extend 5) ((_ extract 15 8) s))))
2915
   *     (bvmul (_ bv124 13) ((_ zero_extend 5) ((_ extract 7 0) s))))
2916
   *   (bvmul (_ bv83 13)
2917
   *          ((_ zero_extend 5) ((_ extract 7 0) ((_ zero_extend 15) w)))))
2918
   */
2919
4
  Node x = bv::utils::mkVar(1);
2920
4
  Node y = bv::utils::mkVar(1);
2921
4
  Node z = bv::utils::mkVar(1);
2922
4
  Node u = bv::utils::mkVar(1);
2923
4
  Node v = bv::utils::mkVar(1);
2924
4
  Node w = bv::utils::mkVar(1);
2925
4
  Node s = bv::utils::mkVar(16);
2926
2927
  Node zextop5 =
2928
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2929
  Node zextop15 =
2930
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(15));
2931
2932
4
  Node zext15x = d_nodeManager->mkNode(zextop15, x);
2933
4
  Node zext15y = d_nodeManager->mkNode(zextop15, y);
2934
4
  Node zext15z = d_nodeManager->mkNode(zextop15, z);
2935
4
  Node zext15u = d_nodeManager->mkNode(zextop15, u);
2936
4
  Node zext15v = d_nodeManager->mkNode(zextop15, v);
2937
4
  Node zext15w = d_nodeManager->mkNode(zextop15, w);
2938
2939
4
  Node ext7x = bv::utils::mkExtract(zext15x, 7, 0);
2940
4
  Node ext7y = bv::utils::mkExtract(zext15y, 7, 0);
2941
4
  Node ext7z = bv::utils::mkExtract(zext15z, 7, 0);
2942
4
  Node ext7u = bv::utils::mkExtract(zext15u, 7, 0);
2943
4
  Node ext7v = bv::utils::mkExtract(zext15v, 7, 0);
2944
4
  Node ext7w = bv::utils::mkExtract(zext15w, 7, 0);
2945
4
  Node ext7s = bv::utils::mkExtract(s, 7, 0);
2946
4
  Node ext15s = bv::utils::mkExtract(s, 15, 8);
2947
2948
4
  Node xx = bv::utils::mkConcat(bv::utils::mkZero(5), ext7x);
2949
4
  Node yy = bv::utils::mkConcat(bv::utils::mkZero(5), ext7y);
2950
4
  Node zz = bv::utils::mkConcat(bv::utils::mkZero(5), ext7z);
2951
4
  Node uu = bv::utils::mkConcat(bv::utils::mkZero(5), ext7u);
2952
4
  Node vv = bv::utils::mkConcat(bv::utils::mkZero(5), ext7v);
2953
4
  Node ww = bv::utils::mkConcat(bv::utils::mkZero(5), ext7w);
2954
4
  Node s7 = bv::utils::mkConcat(bv::utils::mkZero(5), ext7s);
2955
4
  Node s15 = bv::utils::mkConcat(bv::utils::mkZero(5), ext15s);
2956
2957
  Node plus1 = d_nodeManager->mkNode(
2958
      kind::BITVECTOR_PLUS,
2959
8
      d_nodeManager->mkNode(
2960
4
          kind::BITVECTOR_MULT, bv::utils::mkConst(13, 86), xx),
2961
8
      d_nodeManager->mkNode(
2962
14
          kind::BITVECTOR_MULT, bv::utils::mkConst(13, 41), yy));
2963
  Node plus2 = d_nodeManager->mkNode(
2964
      kind::BITVECTOR_PLUS,
2965
      plus1,
2966
8
      d_nodeManager->mkNode(
2967
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(13, 37), zz));
2968
  Node plus3 = d_nodeManager->mkNode(
2969
      kind::BITVECTOR_PLUS,
2970
      plus2,
2971
8
      d_nodeManager->mkNode(
2972
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(13, 170), uu));
2973
  Node plus4 = d_nodeManager->mkNode(
2974
      kind::BITVECTOR_PLUS,
2975
      plus3,
2976
8
      d_nodeManager->mkNode(
2977
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(13, 112), uu));
2978
  Node plus5 = d_nodeManager->mkNode(
2979
      kind::BITVECTOR_PLUS,
2980
      plus4,
2981
8
      d_nodeManager->mkNode(
2982
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(13, 195), s15));
2983
  Node plus6 = d_nodeManager->mkNode(
2984
      kind::BITVECTOR_PLUS,
2985
      plus5,
2986
8
      d_nodeManager->mkNode(
2987
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(13, 124), s7));
2988
  Node plus7 = d_nodeManager->mkNode(
2989
      kind::BITVECTOR_PLUS,
2990
      plus6,
2991
8
      d_nodeManager->mkNode(
2992
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww));
2993
2994
2
  ASSERT_EQ(BVGauss::getMinBwExpr(plus7), 0);
2995
}
2996
2997
46
TEST_F(TestPPWhiteBVGauss, get_min_bw5b)
2998
{
2999
  /* (bvadd
3000
   *   (bvadd
3001
   *     (bvadd
3002
   *       (bvadd
3003
   *         (bvadd
3004
   *           (bvadd
3005
   *             (bvadd (bvmul (_ bv86 20)
3006
   *                           ((_ zero_extend 12)
3007
   *                             ((_ extract 7 0) ((_ zero_extend 15) x))))
3008
   *                    (bvmul (_ bv41 20)
3009
   *                           ((_ zero_extend 12)
3010
   *                             ((_ extract 7 0) ((_ zero_extend 15) y)))))
3011
   *             (bvmul (_ bv37 20)
3012
   *                    ((_ zero_extend 12)
3013
   *                      ((_ extract 7 0) ((_ zero_extend 15) z)))))
3014
   *           (bvmul (_ bv170 20)
3015
   *                  ((_ zero_extend 12)
3016
   *                    ((_ extract 7 0) ((_ zero_extend 15) u)))))
3017
   *         (bvmul (_ bv112 20)
3018
   *                ((_ zero_extend 12)
3019
   *                  ((_ extract 7 0) ((_ zero_extend 15) v)))))
3020
   *       (bvmul (_ bv195 20) ((_ zero_extend 12) ((_ extract 15 8) s))))
3021
   *     (bvmul (_ bv124 20) ((_ zero_extend 12) ((_ extract 7 0) s))))
3022
   *   (bvmul (_ bv83 20)
3023
   *          ((_ zero_extend 12) ((_ extract 7 0) ((_ zero_extend 15) w)))))
3024
   */
3025
4
  Node x = bv::utils::mkVar(1);
3026
4
  Node y = bv::utils::mkVar(1);
3027
4
  Node z = bv::utils::mkVar(1);
3028
4
  Node u = bv::utils::mkVar(1);
3029
4
  Node v = bv::utils::mkVar(1);
3030
4
  Node w = bv::utils::mkVar(1);
3031
4
  Node s = bv::utils::mkVar(16);
3032
3033
  Node zextop15 =
3034
4
      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(15));
3035
3036
4
  Node zext15x = d_nodeManager->mkNode(zextop15, x);
3037
4
  Node zext15y = d_nodeManager->mkNode(zextop15, y);
3038
4
  Node zext15z = d_nodeManager->mkNode(zextop15, z);
3039
4
  Node zext15u = d_nodeManager->mkNode(zextop15, u);
3040
4
  Node zext15v = d_nodeManager->mkNode(zextop15, v);
3041
4
  Node zext15w = d_nodeManager->mkNode(zextop15, w);
3042
3043
4
  Node ext7x = bv::utils::mkExtract(zext15x, 7, 0);
3044
4
  Node ext7y = bv::utils::mkExtract(zext15y, 7, 0);
3045
4
  Node ext7z = bv::utils::mkExtract(zext15z, 7, 0);
3046
4
  Node ext7u = bv::utils::mkExtract(zext15u, 7, 0);
3047
4
  Node ext7v = bv::utils::mkExtract(zext15v, 7, 0);
3048
4
  Node ext7w = bv::utils::mkExtract(zext15w, 7, 0);
3049
4
  Node ext7s = bv::utils::mkExtract(s, 7, 0);
3050
4
  Node ext15s = bv::utils::mkExtract(s, 15, 8);
3051
3052
4
  Node xx = bv::utils::mkConcat(bv::utils::mkZero(12), ext7x);
3053
4
  Node yy = bv::utils::mkConcat(bv::utils::mkZero(12), ext7y);
3054
4
  Node zz = bv::utils::mkConcat(bv::utils::mkZero(12), ext7z);
3055
4
  Node uu = bv::utils::mkConcat(bv::utils::mkZero(12), ext7u);
3056
4
  Node vv = bv::utils::mkConcat(bv::utils::mkZero(12), ext7v);
3057
4
  Node ww = bv::utils::mkConcat(bv::utils::mkZero(12), ext7w);
3058
4
  Node s7 = bv::utils::mkConcat(bv::utils::mkZero(12), ext7s);
3059
4
  Node s15 = bv::utils::mkConcat(bv::utils::mkZero(12), ext15s);
3060
3061
  Node plus1 = d_nodeManager->mkNode(
3062
      kind::BITVECTOR_PLUS,
3063
8
      d_nodeManager->mkNode(
3064
4
          kind::BITVECTOR_MULT, bv::utils::mkConst(20, 86), xx),
3065
8
      d_nodeManager->mkNode(
3066
14
          kind::BITVECTOR_MULT, bv::utils::mkConst(20, 41), yy));
3067
  Node plus2 = d_nodeManager->mkNode(
3068
      kind::BITVECTOR_PLUS,
3069
      plus1,
3070
8
      d_nodeManager->mkNode(
3071
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(20, 37), zz));
3072
  Node plus3 = d_nodeManager->mkNode(
3073
      kind::BITVECTOR_PLUS,
3074
      plus2,
3075
8
      d_nodeManager->mkNode(
3076
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(20, 170), uu));
3077
  Node plus4 = d_nodeManager->mkNode(
3078
      kind::BITVECTOR_PLUS,
3079
      plus3,
3080
8
      d_nodeManager->mkNode(
3081
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(20, 112), uu));
3082
  Node plus5 = d_nodeManager->mkNode(
3083
      kind::BITVECTOR_PLUS,
3084
      plus4,
3085
8
      d_nodeManager->mkNode(
3086
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(20, 195), s15));
3087
  Node plus6 = d_nodeManager->mkNode(
3088
      kind::BITVECTOR_PLUS,
3089
      plus5,
3090
8
      d_nodeManager->mkNode(
3091
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(20, 124), s7));
3092
  Node plus7 = d_nodeManager->mkNode(
3093
      kind::BITVECTOR_PLUS,
3094
      plus6,
3095
8
      d_nodeManager->mkNode(
3096
10
          kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww));
3097
3098
2
  ASSERT_EQ(BVGauss::getMinBwExpr(plus7), 19);
3099
2
  ASSERT_EQ(BVGauss::getMinBwExpr(Rewriter::rewrite(plus7)), 17);
3100
}
3101
}  // namespace test
3102
1498898
}  // namespace CVC4