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