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 : 37 : void SetUp() override
42 : : {
43 : 37 : TestSmt::SetUp();
44 : :
45 : 37 : d_preprocContext.reset(new preprocessing::PreprocessingPassContext(
46 : 37 : d_slvEngine->getEnv(),
47 : 37 : d_slvEngine->d_smtSolver->getTheoryEngine(),
48 : 37 : d_slvEngine->d_smtSolver->getPropEngine(),
49 : 37 : nullptr));
50 : :
51 : 37 : d_bv_gauss.reset(new BVGauss(d_preprocContext.get()));
52 : :
53 : 37 : d_zero = bv::utils::mkZero(d_nodeManager.get(), 16);
54 : :
55 : 111 : d_p = bv::utils::mkConcat(
56 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 11u)));
57 : 111 : d_x = bv::utils::mkConcat(
58 : 148 : d_zero, d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)));
59 : 111 : d_y = bv::utils::mkConcat(
60 : 148 : d_zero, d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)));
61 : 111 : d_z = bv::utils::mkConcat(
62 : 148 : d_zero, d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16)));
63 : :
64 : 111 : d_one = bv::utils::mkConcat(
65 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 1u)));
66 : 111 : d_two = bv::utils::mkConcat(
67 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 2u)));
68 : 111 : d_three = bv::utils::mkConcat(
69 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 3u)));
70 : 111 : d_four = bv::utils::mkConcat(
71 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 4u)));
72 : 111 : d_five = bv::utils::mkConcat(
73 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 5u)));
74 : 111 : d_six = bv::utils::mkConcat(
75 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 6u)));
76 : 111 : d_seven = bv::utils::mkConcat(
77 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 7u)));
78 : 111 : d_eight = bv::utils::mkConcat(
79 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 8u)));
80 : 111 : d_nine = bv::utils::mkConcat(
81 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 9u)));
82 : 111 : d_ten = bv::utils::mkConcat(
83 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 10u)));
84 : 111 : d_twelve = bv::utils::mkConcat(
85 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 12u)));
86 : 111 : d_eighteen = bv::utils::mkConcat(
87 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 18u)));
88 : 111 : d_twentyfour = bv::utils::mkConcat(
89 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 24u)));
90 : 111 : d_thirty = bv::utils::mkConcat(
91 : 148 : d_zero, d_nodeManager->mkConst<BitVector>(BitVector(16, 30u)));
92 : :
93 : 37 : d_one32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 1u));
94 : 37 : d_two32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 2u));
95 : 37 : d_three32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 3u));
96 : 37 : d_four32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 4u));
97 : 37 : d_five32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 5u));
98 : 37 : d_six32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 6u));
99 : 37 : d_seven32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 7u));
100 : 37 : d_eight32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 8u));
101 : 37 : d_nine32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 9u));
102 : 37 : d_ten32 = d_nodeManager->mkConst<BitVector>(BitVector(32, 10u));
103 : :
104 : 37 : d_x_mul_one = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_one);
105 : 37 : d_x_mul_two = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_two);
106 : 37 : d_x_mul_four = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_four);
107 : 37 : d_y_mul_three = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_three);
108 : 37 : d_y_mul_one = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_one);
109 : 37 : d_y_mul_four = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_four);
110 : 37 : d_y_mul_five = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_five);
111 : 37 : d_y_mul_seven = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_seven);
112 : 37 : d_z_mul_one = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_one);
113 : 37 : d_z_mul_three = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_three);
114 : 37 : d_z_mul_five = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_five);
115 : 37 : d_z_mul_six = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_six);
116 : 37 : d_z_mul_twelve = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_twelve);
117 : 37 : d_z_mul_nine = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_nine);
118 : 37 : }
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_unique2)
946 : : {
947 : : /* -------------------------------------------------------------------
948 : : * lhs rhs modulo 11
949 : : * --^-- ^
950 : : * 1 1 1 5
951 : : * 2 3 5 8
952 : : * 4 0 5 2
953 : : * ------------------------------------------------------------------- */
954 : :
955 : : Node zextop6 =
956 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(6));
957 : :
958 : 1 : Node p = d_nodeManager->mkNode(
959 : : zextop6,
960 : 4 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 6),
961 : 1 : d_nodeManager->mkNode(
962 : : Kind::BITVECTOR_ADD,
963 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 7),
964 : 3 : bv::utils::mkConst(d_nodeManager.get(), 20, 4))));
965 : :
966 : 1 : Node x_mul_one = d_nodeManager->mkNode(
967 : : Kind::BITVECTOR_MULT,
968 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_SUB, d_five, d_four),
969 : 3 : d_x);
970 : 1 : Node y_mul_one = d_nodeManager->mkNode(
971 : : Kind::BITVECTOR_MULT,
972 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_UREM, d_one, d_five),
973 : 3 : d_y);
974 : 1 : Node z_mul_one = d_nodeManager->mkNode(
975 : 2 : Kind::BITVECTOR_MULT, bv::utils::mkOne(d_nodeManager.get(), 32), d_z);
976 : :
977 : 1 : Node x_mul_two = d_nodeManager->mkNode(
978 : : Kind::BITVECTOR_MULT,
979 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_SHL,
980 : 2 : bv::utils::mkOne(d_nodeManager.get(), 32),
981 : 2 : bv::utils::mkOne(d_nodeManager.get(), 32)),
982 : 5 : d_x);
983 : 1 : Node y_mul_three = d_nodeManager->mkNode(
984 : : Kind::BITVECTOR_MULT,
985 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_LSHR,
986 : 2 : bv::utils::mkOnes(d_nodeManager.get(), 32),
987 : 2 : bv::utils::mkConst(d_nodeManager.get(), 32, 30)),
988 : 5 : d_y);
989 : 1 : Node z_mul_five = d_nodeManager->mkNode(
990 : : Kind::BITVECTOR_MULT,
991 : 2 : bv::utils::mkExtract(
992 : 1 : d_nodeManager->mkNode(
993 : : zextop6,
994 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, d_three, d_two)),
995 : : 31,
996 : : 0),
997 : 3 : d_z);
998 : :
999 : 1 : Node x_mul_four = d_nodeManager->mkNode(
1000 : : Kind::BITVECTOR_MULT,
1001 : 1 : d_nodeManager->mkNode(
1002 : : Kind::BITVECTOR_UDIV,
1003 : 1 : d_nodeManager->mkNode(
1004 : : Kind::BITVECTOR_ADD,
1005 : 1 : d_nodeManager->mkNode(
1006 : : Kind::BITVECTOR_MULT,
1007 : 2 : bv::utils::mkConst(d_nodeManager.get(), 32, 4),
1008 : 2 : bv::utils::mkConst(d_nodeManager.get(), 32, 5)),
1009 : 2 : bv::utils::mkConst(d_nodeManager.get(), 32, 4)),
1010 : 2 : bv::utils::mkConst(d_nodeManager.get(), 32, 6)),
1011 : 9 : d_x);
1012 : :
1013 : 1 : Node eq1 = d_nodeManager->mkNode(
1014 : : Kind::EQUAL,
1015 : 1 : d_nodeManager->mkNode(
1016 : : Kind::BITVECTOR_UREM,
1017 : 1 : d_nodeManager->mkNode(
1018 : : Kind::BITVECTOR_ADD,
1019 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, x_mul_one, y_mul_one),
1020 : : z_mul_one),
1021 : : p),
1022 : 5 : d_five);
1023 : :
1024 : 1 : Node eq2 = d_nodeManager->mkNode(
1025 : : Kind::EQUAL,
1026 : 1 : d_nodeManager->mkNode(
1027 : : Kind::BITVECTOR_UREM,
1028 : 1 : d_nodeManager->mkNode(
1029 : : Kind::BITVECTOR_ADD,
1030 : 1 : d_nodeManager->mkNode(
1031 : : Kind::BITVECTOR_ADD, x_mul_two, y_mul_three),
1032 : : z_mul_five),
1033 : : p),
1034 : 5 : d_eight);
1035 : :
1036 : 1 : Node eq3 = d_nodeManager->mkNode(
1037 : : Kind::EQUAL,
1038 : 1 : d_nodeManager->mkNode(
1039 : : Kind::BITVECTOR_UREM,
1040 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, x_mul_four, z_mul_five),
1041 : 1 : d_p),
1042 : 4 : d_two);
1043 : :
1044 : 5 : std::vector<Node> eqs = {eq1, eq2, eq3};
1045 : 1 : std::unordered_map<Node, Node> res;
1046 : 1 : BVGauss::Result ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1047 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
1048 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 3);
1049 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_x], d_three32);
1050 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_y], d_four32);
1051 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_z], d_nine32);
1052 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
1053 : :
1054 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
1055 : : {
1056 : 1 : std::unordered_map<Node, Node> res;
1057 : : BVGauss::Result ret;
1058 : :
1059 : : /* -------------------------------------------------------------------
1060 : : * lhs rhs lhs rhs modulo 11
1061 : : * --^-- ^ --^-- ^
1062 : : * 1 0 9 7 --> 1 0 9 7
1063 : : * 0 1 3 9 0 1 3 9
1064 : : * ------------------------------------------------------------------- */
1065 : :
1066 : 1 : Node eq1 = d_nodeManager->mkNode(
1067 : : Kind::EQUAL,
1068 : 1 : d_nodeManager->mkNode(
1069 : : Kind::BITVECTOR_UREM,
1070 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, d_x_mul_one, d_z_mul_nine),
1071 : 1 : d_p),
1072 : 4 : d_seven);
1073 : :
1074 : 1 : Node eq2 = d_nodeManager->mkNode(
1075 : : Kind::EQUAL,
1076 : 1 : d_nodeManager->mkNode(
1077 : : Kind::BITVECTOR_UREM,
1078 : 1 : d_nodeManager->mkNode(
1079 : 2 : Kind::BITVECTOR_ADD, d_y_mul_one, d_z_mul_three),
1080 : 1 : d_p),
1081 : 4 : d_nine);
1082 : :
1083 : 4 : std::vector<Node> eqs = {eq1, eq2};
1084 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1085 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1086 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 2);
1087 : :
1088 : 1 : Node x1 = d_nodeManager->mkNode(
1089 : : Kind::BITVECTOR_UREM,
1090 : 1 : d_nodeManager->mkNode(
1091 : : Kind::BITVECTOR_ADD,
1092 : 1 : d_seven32,
1093 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_two32)),
1094 : 3 : d_p);
1095 : 1 : Node y1 = d_nodeManager->mkNode(
1096 : : Kind::BITVECTOR_UREM,
1097 : 1 : d_nodeManager->mkNode(
1098 : : Kind::BITVECTOR_ADD,
1099 : 1 : d_nine32,
1100 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_eight32)),
1101 : 3 : d_p);
1102 : :
1103 : 1 : Node x2 = d_nodeManager->mkNode(
1104 : : Kind::BITVECTOR_UREM,
1105 : 1 : d_nodeManager->mkNode(
1106 : : Kind::BITVECTOR_ADD,
1107 : 1 : d_two32,
1108 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_three32)),
1109 : 3 : d_p);
1110 : 1 : Node z2 = d_nodeManager->mkNode(
1111 : : Kind::BITVECTOR_UREM,
1112 : 1 : d_nodeManager->mkNode(
1113 : : Kind::BITVECTOR_ADD,
1114 : 1 : d_three32,
1115 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_seven32)),
1116 : 3 : d_p);
1117 : :
1118 : 1 : Node y3 = d_nodeManager->mkNode(
1119 : : Kind::BITVECTOR_UREM,
1120 : 1 : d_nodeManager->mkNode(
1121 : : Kind::BITVECTOR_ADD,
1122 : 1 : d_three32,
1123 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_four32)),
1124 : 3 : d_p);
1125 : 1 : Node z3 = d_nodeManager->mkNode(
1126 : : Kind::BITVECTOR_UREM,
1127 : 1 : d_nodeManager->mkNode(
1128 : : Kind::BITVECTOR_ADD,
1129 : 1 : d_two32,
1130 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_six32)),
1131 : 3 : d_p);
1132 : :
1133 : : /* result depends on order of variables in matrix */
1134 [ + - ]: 1 : if (res.find(d_x) == res.end())
1135 : : {
1136 : : /*
1137 : : * y z x y z x
1138 : : * 0 9 1 7 --> 1 0 7 3
1139 : : * 1 3 0 9 0 1 5 2
1140 : : *
1141 : : * z y x z y x
1142 : : * 9 0 1 7 --> 1 0 5 2
1143 : : * 3 1 0 9 0 1 7 3
1144 : : */
1145 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_y], y3);
1146 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_z], z3);
1147 : : }
1148 [ - - ]: 0 : else if (res.find(d_y) == res.end())
1149 : : {
1150 : : /*
1151 : : * x z y x z y
1152 : : * 1 9 0 7 --> 1 0 8 2
1153 : : * 0 3 1 9 0 1 4 3
1154 : : *
1155 : : * z x y z x y
1156 : : * 9 1 0 7 --> 1 0 4 3
1157 : : * 3 0 1 9 0 1 8 2
1158 : : */
1159 : 0 : ASSERT_EQ(res[d_x], x2);
1160 : 0 : ASSERT_EQ(res[d_z], z2);
1161 : : }
1162 : : else
1163 : : {
1164 : 0 : ASSERT_EQ(res.find(d_z), res.end());
1165 : : /*
1166 : : * x y z x y z
1167 : : * 1 0 9 7 --> 1 0 9 7
1168 : : * 0 1 3 9 0 1 3 9
1169 : : *
1170 : : * y x z y x z
1171 : : * 0 1 9 7 --> 1 0 3 9
1172 : : * 1 0 3 9 0 1 9 7
1173 : : */
1174 : 0 : ASSERT_EQ(res[d_x], x1);
1175 : 0 : ASSERT_EQ(res[d_y], y1);
1176 : : }
1177 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
1178 : :
1179 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
1180 : : {
1181 : 1 : std::unordered_map<Node, Node> res;
1182 : : BVGauss::Result ret;
1183 : :
1184 : : /* -------------------------------------------------------------------
1185 : : * lhs rhs lhs rhs modulo 11
1186 : : * --^-- ^ --^-- ^
1187 : : * 1 0 9 7 --> 1 0 9 7
1188 : : * 0 1 3 9 0 1 3 9
1189 : : * ------------------------------------------------------------------- */
1190 : :
1191 : 1 : Node eq1 = d_nodeManager->mkNode(
1192 : : Kind::EQUAL,
1193 : 1 : d_nodeManager->mkNode(
1194 : : Kind::BITVECTOR_UREM,
1195 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, d_x, d_z_mul_nine),
1196 : 1 : d_p),
1197 : 4 : d_seven);
1198 : :
1199 : 1 : Node eq2 = d_nodeManager->mkNode(
1200 : : Kind::EQUAL,
1201 : 1 : d_nodeManager->mkNode(
1202 : : Kind::BITVECTOR_UREM,
1203 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, d_y, d_z_mul_three),
1204 : 1 : d_p),
1205 : 4 : d_nine);
1206 : :
1207 : 4 : std::vector<Node> eqs = {eq1, eq2};
1208 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1209 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1210 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 2);
1211 : :
1212 : 1 : Node x1 = d_nodeManager->mkNode(
1213 : : Kind::BITVECTOR_UREM,
1214 : 1 : d_nodeManager->mkNode(
1215 : : Kind::BITVECTOR_ADD,
1216 : 1 : d_seven32,
1217 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_two32)),
1218 : 3 : d_p);
1219 : 1 : Node y1 = d_nodeManager->mkNode(
1220 : : Kind::BITVECTOR_UREM,
1221 : 1 : d_nodeManager->mkNode(
1222 : : Kind::BITVECTOR_ADD,
1223 : 1 : d_nine32,
1224 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_eight32)),
1225 : 3 : d_p);
1226 : :
1227 : 1 : Node x2 = d_nodeManager->mkNode(
1228 : : Kind::BITVECTOR_UREM,
1229 : 1 : d_nodeManager->mkNode(
1230 : : Kind::BITVECTOR_ADD,
1231 : 1 : d_two32,
1232 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_three32)),
1233 : 3 : d_p);
1234 : 1 : Node z2 = d_nodeManager->mkNode(
1235 : : Kind::BITVECTOR_UREM,
1236 : 1 : d_nodeManager->mkNode(
1237 : : Kind::BITVECTOR_ADD,
1238 : 1 : d_three32,
1239 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_seven32)),
1240 : 3 : d_p);
1241 : :
1242 : 1 : Node y3 = d_nodeManager->mkNode(
1243 : : Kind::BITVECTOR_UREM,
1244 : 1 : d_nodeManager->mkNode(
1245 : : Kind::BITVECTOR_ADD,
1246 : 1 : d_three32,
1247 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_four32)),
1248 : 3 : d_p);
1249 : 1 : Node z3 = d_nodeManager->mkNode(
1250 : : Kind::BITVECTOR_UREM,
1251 : 1 : d_nodeManager->mkNode(
1252 : : Kind::BITVECTOR_ADD,
1253 : 1 : d_two32,
1254 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_six32)),
1255 : 3 : d_p);
1256 : :
1257 : : /* result depends on order of variables in matrix */
1258 [ + - ]: 1 : if (res.find(d_x) == res.end())
1259 : : {
1260 : : /*
1261 : : * y z x y z x
1262 : : * 0 9 1 7 --> 1 0 7 3
1263 : : * 1 3 0 9 0 1 5 2
1264 : : *
1265 : : * z y x z y x
1266 : : * 9 0 1 7 --> 1 0 5 2
1267 : : * 3 1 0 9 0 1 7 3
1268 : : */
1269 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_y], y3);
1270 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_z], z3);
1271 : : }
1272 [ - - ]: 0 : else if (res.find(d_y) == res.end())
1273 : : {
1274 : : /*
1275 : : * x z y x z y
1276 : : * 1 9 0 7 --> 1 0 8 2
1277 : : * 0 3 1 9 0 1 4 3
1278 : : *
1279 : : * z x y z x y
1280 : : * 9 1 0 7 --> 1 0 4 3
1281 : : * 3 0 1 9 0 1 8 2
1282 : : */
1283 : 0 : ASSERT_EQ(res[d_x], x2);
1284 : 0 : ASSERT_EQ(res[d_z], z2);
1285 : : }
1286 : : else
1287 : : {
1288 : 0 : ASSERT_EQ(res.find(d_z), res.end());
1289 : : /*
1290 : : * x y z x y z
1291 : : * 1 0 9 7 --> 1 0 9 7
1292 : : * 0 1 3 9 0 1 3 9
1293 : : *
1294 : : * y x z y x z
1295 : : * 0 1 9 7 --> 1 0 3 9
1296 : : * 1 0 3 9 0 1 9 7
1297 : : */
1298 : 0 : ASSERT_EQ(res[d_x], x1);
1299 : 0 : ASSERT_EQ(res[d_y], y1);
1300 : : }
1301 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
1302 : :
1303 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
1304 : : {
1305 : 1 : std::unordered_map<Node, Node> res;
1306 : : BVGauss::Result ret;
1307 : :
1308 : : /* -------------------------------------------------------------------
1309 : : * lhs rhs lhs rhs modulo 11
1310 : : * --^-- ^ --^-- ^
1311 : : * 1 3 0 7 --> 1 3 0 7
1312 : : * 0 0 1 9 0 0 1 9
1313 : : * ------------------------------------------------------------------- */
1314 : :
1315 : 1 : Node eq1 = d_nodeManager->mkNode(
1316 : : Kind::EQUAL,
1317 : 1 : d_nodeManager->mkNode(
1318 : : Kind::BITVECTOR_UREM,
1319 : 1 : d_nodeManager->mkNode(
1320 : 2 : Kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_three),
1321 : 1 : d_p),
1322 : 4 : d_seven);
1323 : :
1324 : 1 : Node eq2 = d_nodeManager->mkNode(
1325 : : Kind::EQUAL,
1326 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_UREM, d_z_mul_one, d_p),
1327 : 3 : d_nine);
1328 : :
1329 : 4 : std::vector<Node> eqs = {eq1, eq2};
1330 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1331 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1332 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 2);
1333 : :
1334 : 1 : Node x1 = d_nodeManager->mkNode(
1335 : : Kind::BITVECTOR_UREM,
1336 : 1 : d_nodeManager->mkNode(
1337 : : Kind::BITVECTOR_ADD,
1338 : 1 : d_seven32,
1339 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_eight32)),
1340 : 3 : d_p);
1341 : 1 : Node y2 = d_nodeManager->mkNode(
1342 : : Kind::BITVECTOR_UREM,
1343 : 1 : d_nodeManager->mkNode(
1344 : : Kind::BITVECTOR_ADD,
1345 : 1 : d_six32,
1346 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_seven32)),
1347 : 3 : d_p);
1348 : :
1349 : : /* result depends on order of variables in matrix */
1350 [ + - ]: 1 : if (res.find(d_x) == res.end())
1351 : : {
1352 : : /*
1353 : : * x y z x y z
1354 : : * 1 3 0 7 --> 1 3 0 7
1355 : : * 0 0 1 9 0 0 1 9
1356 : : *
1357 : : * x z y x z y
1358 : : * 1 0 3 7 --> 1 0 3 7
1359 : : * 0 1 0 9 0 1 0 9
1360 : : *
1361 : : * z x y z x y
1362 : : * 0 1 3 7 --> 1 0 0 9
1363 : : * 1 0 0 9 0 1 3 7
1364 : : */
1365 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_y], y2);
1366 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_z], d_nine32);
1367 : : }
1368 [ - - ]: 0 : else if (res.find(d_y) == res.end())
1369 : : {
1370 : : /*
1371 : : * z y x z y x
1372 : : * 0 3 1 7 --> 1 0 0 9
1373 : : * 1 0 0 9 0 1 4 6
1374 : : *
1375 : : * y x z y x z
1376 : : * 3 1 0 7 --> 1 4 0 6
1377 : : * 0 0 1 9 0 0 1 9
1378 : : *
1379 : : * y z x y z x
1380 : : * 3 0 1 7 --> 1 0 4 6
1381 : : * 0 1 0 9 0 1 0 9
1382 : : */
1383 : 0 : ASSERT_EQ(res[d_x], x1);
1384 : 0 : ASSERT_EQ(res[d_z], d_nine32);
1385 : : }
1386 : : else
1387 : : {
1388 : 0 : ASSERT_TRUE(false);
1389 : : }
1390 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
1391 : :
1392 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
1393 : : {
1394 : 1 : std::unordered_map<Node, Node> res;
1395 : : BVGauss::Result ret;
1396 : :
1397 : : /* -------------------------------------------------------------------
1398 : : * lhs rhs lhs rhs modulo 11
1399 : : * --^-- ^ --^-- ^
1400 : : * 1 1 1 5 --> 1 0 9 7
1401 : : * 2 3 5 8 0 1 3 9
1402 : : * ------------------------------------------------------------------- */
1403 : :
1404 : 1 : Node eq1 = d_nodeManager->mkNode(
1405 : : Kind::EQUAL,
1406 : 1 : d_nodeManager->mkNode(
1407 : : Kind::BITVECTOR_UREM,
1408 : 1 : d_nodeManager->mkNode(
1409 : : Kind::BITVECTOR_ADD,
1410 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, d_x_mul_one, d_y),
1411 : 1 : d_z_mul_one),
1412 : 1 : d_p),
1413 : 5 : d_five);
1414 : :
1415 : 1 : Node eq2 = d_nodeManager->mkNode(
1416 : : Kind::EQUAL,
1417 : 1 : d_nodeManager->mkNode(
1418 : : Kind::BITVECTOR_UREM,
1419 : 1 : d_nodeManager->mkNode(
1420 : : Kind::BITVECTOR_ADD,
1421 : 1 : d_nodeManager->mkNode(
1422 : 2 : Kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three),
1423 : 1 : d_z_mul_five),
1424 : 1 : d_p),
1425 : 5 : d_eight);
1426 : :
1427 : 4 : std::vector<Node> eqs = {eq1, eq2};
1428 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1429 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1430 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 2);
1431 : :
1432 : 1 : Node x1 = d_nodeManager->mkNode(
1433 : : Kind::BITVECTOR_UREM,
1434 : 1 : d_nodeManager->mkNode(
1435 : : Kind::BITVECTOR_ADD,
1436 : 1 : d_seven32,
1437 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_two32)),
1438 : 3 : d_p);
1439 : 1 : Node y1 = d_nodeManager->mkNode(
1440 : : Kind::BITVECTOR_UREM,
1441 : 1 : d_nodeManager->mkNode(
1442 : : Kind::BITVECTOR_ADD,
1443 : 1 : d_nine32,
1444 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_eight32)),
1445 : 3 : d_p);
1446 : 1 : Node x2 = d_nodeManager->mkNode(
1447 : : Kind::BITVECTOR_UREM,
1448 : 1 : d_nodeManager->mkNode(
1449 : : Kind::BITVECTOR_ADD,
1450 : 1 : d_two32,
1451 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_three32)),
1452 : 3 : d_p);
1453 : 1 : Node z2 = d_nodeManager->mkNode(
1454 : : Kind::BITVECTOR_UREM,
1455 : 1 : d_nodeManager->mkNode(
1456 : : Kind::BITVECTOR_ADD,
1457 : 1 : d_three32,
1458 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_seven32)),
1459 : 3 : d_p);
1460 : 1 : Node y3 = d_nodeManager->mkNode(
1461 : : Kind::BITVECTOR_UREM,
1462 : 1 : d_nodeManager->mkNode(
1463 : : Kind::BITVECTOR_ADD,
1464 : 1 : d_three32,
1465 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_four32)),
1466 : 3 : d_p);
1467 : 1 : Node z3 = d_nodeManager->mkNode(
1468 : : Kind::BITVECTOR_UREM,
1469 : 1 : d_nodeManager->mkNode(
1470 : : Kind::BITVECTOR_ADD,
1471 : 1 : d_two32,
1472 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_six32)),
1473 : 3 : d_p);
1474 : :
1475 : : /* result depends on order of variables in matrix */
1476 [ + - ]: 1 : if (res.find(d_x) == res.end())
1477 : : {
1478 : : /*
1479 : : * y z x y z x
1480 : : * 1 1 1 5 --> 1 0 7 3
1481 : : * 3 5 2 8 0 1 5 2
1482 : : *
1483 : : * z y x z y x
1484 : : * 1 1 1 5 --> 1 0 5 2
1485 : : * 5 3 2 8 0 1 7 3
1486 : : */
1487 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_y], y3);
1488 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_z], z3);
1489 : : }
1490 [ - - ]: 0 : else if (res.find(d_y) == res.end())
1491 : : {
1492 : : /*
1493 : : * x z y x z y
1494 : : * 1 1 1 5 --> 1 0 8 2
1495 : : * 2 5 3 8 0 1 4 3
1496 : : *
1497 : : * z x y z x y
1498 : : * 1 1 1 5 --> 1 0 4 3
1499 : : * 5 2 3 9 0 1 8 2
1500 : : */
1501 : 0 : ASSERT_EQ(res[d_x], x2);
1502 : 0 : ASSERT_EQ(res[d_z], z2);
1503 : : }
1504 : : else
1505 : : {
1506 : 0 : ASSERT_EQ(res.find(d_z), res.end());
1507 : : /*
1508 : : * x y z x y z
1509 : : * 1 1 1 5 --> 1 0 9 7
1510 : : * 2 3 5 8 0 1 3 9
1511 : : *
1512 : : * y x z y x z
1513 : : * 1 1 1 5 --> 1 0 3 9
1514 : : * 3 2 5 8 0 1 9 7
1515 : : */
1516 : 0 : ASSERT_EQ(res[d_x], x1);
1517 : 0 : ASSERT_EQ(res[d_y], y1);
1518 : : }
1519 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
1520 : :
1521 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
1522 : : {
1523 : 1 : std::unordered_map<Node, Node> res;
1524 : : BVGauss::Result ret;
1525 : :
1526 : : /* -------------------------------------------------------------------
1527 : : * lhs rhs lhs rhs modulo 11
1528 : : * ----^--- ^ ---^--- ^
1529 : : * 2 4 6 18 --> 1 0 10 1
1530 : : * 4 5 6 24 0 1 2 4
1531 : : * 2 7 12 30 0 0 0 0
1532 : : * ------------------------------------------------------------------- */
1533 : :
1534 : 1 : Node eq1 = d_nodeManager->mkNode(
1535 : : Kind::EQUAL,
1536 : 1 : d_nodeManager->mkNode(
1537 : : Kind::BITVECTOR_UREM,
1538 : 1 : d_nodeManager->mkNode(
1539 : : Kind::BITVECTOR_ADD,
1540 : 1 : d_nodeManager->mkNode(
1541 : 2 : Kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_four),
1542 : 1 : d_z_mul_six),
1543 : 1 : d_p),
1544 : 5 : d_eighteen);
1545 : :
1546 : 1 : Node eq2 = d_nodeManager->mkNode(
1547 : : Kind::EQUAL,
1548 : 1 : d_nodeManager->mkNode(
1549 : : Kind::BITVECTOR_UREM,
1550 : 1 : d_nodeManager->mkNode(
1551 : : Kind::BITVECTOR_ADD,
1552 : 1 : d_nodeManager->mkNode(
1553 : 2 : Kind::BITVECTOR_ADD, d_x_mul_four, d_y_mul_five),
1554 : 1 : d_z_mul_six),
1555 : 1 : d_p),
1556 : 5 : d_twentyfour);
1557 : :
1558 : 1 : Node eq3 = d_nodeManager->mkNode(
1559 : : Kind::EQUAL,
1560 : 1 : d_nodeManager->mkNode(
1561 : : Kind::BITVECTOR_UREM,
1562 : 1 : d_nodeManager->mkNode(
1563 : : Kind::BITVECTOR_ADD,
1564 : 1 : d_nodeManager->mkNode(
1565 : 2 : Kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_seven),
1566 : 1 : d_z_mul_twelve),
1567 : 1 : d_p),
1568 : 5 : d_thirty);
1569 : :
1570 : 5 : std::vector<Node> eqs = {eq1, eq2, eq3};
1571 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1572 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1573 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 2);
1574 : :
1575 : 1 : Node x1 = d_nodeManager->mkNode(
1576 : : Kind::BITVECTOR_UREM,
1577 : 1 : d_nodeManager->mkNode(
1578 : : Kind::BITVECTOR_ADD,
1579 : 1 : d_one32,
1580 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_one32)),
1581 : 3 : d_p);
1582 : 1 : Node y1 = d_nodeManager->mkNode(
1583 : : Kind::BITVECTOR_UREM,
1584 : 1 : d_nodeManager->mkNode(
1585 : : Kind::BITVECTOR_ADD,
1586 : 1 : d_four32,
1587 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_nine32)),
1588 : 3 : d_p);
1589 : 1 : Node x2 = d_nodeManager->mkNode(
1590 : : Kind::BITVECTOR_UREM,
1591 : 1 : d_nodeManager->mkNode(
1592 : : Kind::BITVECTOR_ADD,
1593 : 1 : d_three32,
1594 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_five32)),
1595 : 3 : d_p);
1596 : 1 : Node z2 = d_nodeManager->mkNode(
1597 : : Kind::BITVECTOR_UREM,
1598 : 1 : d_nodeManager->mkNode(
1599 : : Kind::BITVECTOR_ADD,
1600 : 1 : d_two32,
1601 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_five32)),
1602 : 3 : d_p);
1603 : 1 : Node y3 = d_nodeManager->mkNode(
1604 : : Kind::BITVECTOR_UREM,
1605 : 1 : d_nodeManager->mkNode(
1606 : : Kind::BITVECTOR_ADD,
1607 : 1 : d_six32,
1608 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_nine32)),
1609 : 3 : d_p);
1610 : 1 : Node z3 = d_nodeManager->mkNode(
1611 : : Kind::BITVECTOR_UREM,
1612 : 1 : d_nodeManager->mkNode(
1613 : : Kind::BITVECTOR_ADD,
1614 : 1 : d_ten32,
1615 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_one32)),
1616 : 3 : d_p);
1617 : :
1618 : : /* result depends on order of variables in matrix */
1619 [ + - ]: 1 : if (res.find(d_x) == res.end())
1620 : : {
1621 : : /*
1622 : : * y z x y z x
1623 : : * 4 6 2 18 --> 1 0 2 6
1624 : : * 5 6 4 24 0 1 10 10
1625 : : * 7 12 2 30 0 0 0 0
1626 : : *
1627 : : * z y x z y x
1628 : : * 6 4 2 18 --> 1 0 10 10
1629 : : * 6 5 4 24 0 1 2 6
1630 : : * 12 12 2 30 0 0 0 0
1631 : : *
1632 : : */
1633 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_y], y3);
1634 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_z], z3);
1635 : : }
1636 [ - - ]: 0 : else if (res.find(d_y) == res.end())
1637 : : {
1638 : : /*
1639 : : * x z y x z y
1640 : : * 2 6 4 18 --> 1 0 6 3
1641 : : * 4 6 5 24 0 1 6 2
1642 : : * 2 12 7 30 0 0 0 0
1643 : : *
1644 : : * z x y z x y
1645 : : * 6 2 4 18 --> 1 0 6 2
1646 : : * 6 4 5 24 0 1 6 3
1647 : : * 12 2 12 30 0 0 0 0
1648 : : *
1649 : : */
1650 : 0 : ASSERT_EQ(res[d_x], x2);
1651 : 0 : ASSERT_EQ(res[d_z], z2);
1652 : : }
1653 : : else
1654 : : {
1655 : 0 : ASSERT_EQ(res.find(d_z), res.end());
1656 : : /*
1657 : : * x y z x y z
1658 : : * 2 4 6 18 --> 1 0 10 1
1659 : : * 4 5 6 24 0 1 2 4
1660 : : * 2 7 12 30 0 0 0 0
1661 : : *
1662 : : * y x z y x z
1663 : : * 4 2 6 18 --> 1 0 2 49
1664 : : * 5 4 6 24 0 1 10 1
1665 : : * 7 2 12 30 0 0 0 0
1666 : : */
1667 : 0 : ASSERT_EQ(res[d_x], x1);
1668 : 0 : ASSERT_EQ(res[d_y], y1);
1669 : : }
1670 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
1671 : :
1672 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
1673 : : {
1674 : 1 : std::unordered_map<Node, Node> res;
1675 : : BVGauss::Result ret;
1676 : :
1677 : : /* -------------------------------------------------------------------
1678 : : * lhs rhs lhs rhs modulo 3
1679 : : * ----^--- ^ --^-- ^
1680 : : * 2 4 6 18 --> 1 2 0 0
1681 : : * 4 5 6 24 0 0 0 0
1682 : : * 2 7 12 30 0 0 0 0
1683 : : * ------------------------------------------------------------------- */
1684 : :
1685 : 1 : Node eq1 = d_nodeManager->mkNode(
1686 : : Kind::EQUAL,
1687 : 1 : d_nodeManager->mkNode(
1688 : : Kind::BITVECTOR_UREM,
1689 : 1 : d_nodeManager->mkNode(
1690 : : Kind::BITVECTOR_ADD,
1691 : 1 : d_nodeManager->mkNode(
1692 : 2 : Kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_four),
1693 : 1 : d_z_mul_six),
1694 : 1 : d_three),
1695 : 5 : d_eighteen);
1696 : :
1697 : 1 : Node eq2 = d_nodeManager->mkNode(
1698 : : Kind::EQUAL,
1699 : 1 : d_nodeManager->mkNode(
1700 : : Kind::BITVECTOR_UREM,
1701 : 1 : d_nodeManager->mkNode(
1702 : : Kind::BITVECTOR_ADD,
1703 : 1 : d_nodeManager->mkNode(
1704 : 2 : Kind::BITVECTOR_ADD, d_x_mul_four, d_y_mul_five),
1705 : 1 : d_z_mul_six),
1706 : 1 : d_three),
1707 : 5 : d_twentyfour);
1708 : :
1709 : 1 : Node eq3 = d_nodeManager->mkNode(
1710 : : Kind::EQUAL,
1711 : 1 : d_nodeManager->mkNode(
1712 : : Kind::BITVECTOR_UREM,
1713 : 1 : d_nodeManager->mkNode(
1714 : : Kind::BITVECTOR_ADD,
1715 : 1 : d_nodeManager->mkNode(
1716 : 2 : Kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_seven),
1717 : 1 : d_z_mul_twelve),
1718 : 1 : d_three),
1719 : 5 : d_thirty);
1720 : :
1721 : 5 : std::vector<Node> eqs = {eq1, eq2, eq3};
1722 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1723 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1724 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 1);
1725 : :
1726 : 1 : Node x1 = d_nodeManager->mkNode(
1727 : : Kind::BITVECTOR_UREM,
1728 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_one32),
1729 : 3 : d_three);
1730 : 1 : Node y2 = d_nodeManager->mkNode(
1731 : : Kind::BITVECTOR_UREM,
1732 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_one32),
1733 : 3 : d_three);
1734 : :
1735 : : /* result depends on order of variables in matrix */
1736 [ + - ]: 1 : if (res.find(d_x) == res.end())
1737 : : {
1738 : : /*
1739 : : * y x z y x z
1740 : : * 4 2 6 18 --> 1 2 0 0
1741 : : * 5 4 6 24 0 0 0 0
1742 : : * 7 2 12 30 0 0 0 0
1743 : : *
1744 : : * y z x y z x
1745 : : * 4 6 2 18 --> 1 0 2 0
1746 : : * 5 6 4 24 0 0 0 0
1747 : : * 7 12 2 30 0 0 0 0
1748 : : *
1749 : : * z y x z y x
1750 : : * 6 4 2 18 --> 0 1 2 0
1751 : : * 6 5 4 24 0 0 0 0
1752 : : * 12 12 2 30 0 0 0 0
1753 : : *
1754 : : */
1755 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_y], y2);
1756 : : }
1757 [ - - ]: 0 : else if (res.find(d_y) == res.end())
1758 : : {
1759 : : /*
1760 : : * x y z x y z
1761 : : * 2 4 6 18 --> 1 2 0 0
1762 : : * 4 5 6 24 0 0 0 0
1763 : : * 2 7 12 30 0 0 0 0
1764 : : *
1765 : : * x z y x z y
1766 : : * 2 6 4 18 --> 1 0 2 0
1767 : : * 4 6 5 24 0 0 0 0
1768 : : * 2 12 7 30 0 0 0 0
1769 : : *
1770 : : * z x y z x y
1771 : : * 6 2 4 18 --> 0 1 2 0
1772 : : * 6 4 5 24 0 0 0 0
1773 : : * 12 2 12 30 0 0 0 0
1774 : : *
1775 : : */
1776 : 0 : ASSERT_EQ(res[d_x], x1);
1777 : : }
1778 : : else
1779 : : {
1780 : 0 : ASSERT_TRUE(false);
1781 : : }
1782 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
1783 : :
1784 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
1785 : : {
1786 : 1 : std::unordered_map<Node, Node> res;
1787 : : BVGauss::Result ret;
1788 : :
1789 : : /* -------------------------------------------------------------------
1790 : : * lhs rhs --> lhs rhs modulo 11
1791 : : * ---^--- ^ ---^--- ^
1792 : : * x y z w x y z w
1793 : : * 1 2 0 6 2 1 2 0 6 2
1794 : : * 0 0 2 2 2 0 0 1 1 1
1795 : : * 0 0 0 1 2 0 0 0 1 2
1796 : : * ------------------------------------------------------------------- */
1797 : :
1798 : 2 : Node y_mul_two = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_two);
1799 : 2 : Node z_mul_two = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_two);
1800 : : Node w = bv::utils::mkConcat(
1801 : 2 : d_zero, d_nodeManager->mkVar("w", d_nodeManager->mkBitVectorType(16)));
1802 : 2 : Node w_mul_six = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, w, d_six);
1803 : 2 : Node w_mul_two = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, w, d_two);
1804 : :
1805 : 1 : Node eq1 = d_nodeManager->mkNode(
1806 : : Kind::EQUAL,
1807 : 1 : d_nodeManager->mkNode(
1808 : : Kind::BITVECTOR_UREM,
1809 : 1 : d_nodeManager->mkNode(
1810 : : Kind::BITVECTOR_ADD,
1811 : 1 : d_nodeManager->mkNode(
1812 : 1 : Kind::BITVECTOR_ADD, d_x_mul_one, y_mul_two),
1813 : : w_mul_six),
1814 : 1 : d_p),
1815 : 5 : d_two);
1816 : :
1817 : 1 : Node eq2 = d_nodeManager->mkNode(
1818 : : Kind::EQUAL,
1819 : 1 : d_nodeManager->mkNode(
1820 : : Kind::BITVECTOR_UREM,
1821 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, z_mul_two, w_mul_two),
1822 : 1 : d_p),
1823 : 4 : d_two);
1824 : :
1825 : 1 : Node eq3 = d_nodeManager->mkNode(
1826 : 2 : Kind::EQUAL, d_nodeManager->mkNode(Kind::BITVECTOR_UREM, w, d_p), d_two);
1827 : :
1828 : 5 : std::vector<Node> eqs = {eq1, eq2, eq3};
1829 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1830 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1831 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 3);
1832 : :
1833 : 1 : Node x1 = d_nodeManager->mkNode(
1834 : : Kind::BITVECTOR_UREM,
1835 : 1 : d_nodeManager->mkNode(
1836 : : Kind::BITVECTOR_ADD,
1837 : 1 : d_one32,
1838 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_nine32)),
1839 : 3 : d_p);
1840 : 1 : Node z1 = d_ten32;
1841 : 1 : Node w1 = d_two32;
1842 : :
1843 : 1 : Node y2 = d_nodeManager->mkNode(
1844 : : Kind::BITVECTOR_UREM,
1845 : 1 : d_nodeManager->mkNode(
1846 : : Kind::BITVECTOR_ADD,
1847 : 1 : d_six32,
1848 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_five32)),
1849 : 3 : d_p);
1850 : 1 : Node z2 = d_ten32;
1851 : 1 : Node w2 = d_two32;
1852 : :
1853 : : /* result depends on order of variables in matrix */
1854 [ + - ]: 1 : if (res.find(d_x) == res.end())
1855 : : {
1856 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_y], y2);
1857 [ - + ][ + - ]: 1 : ASSERT_EQ(res[d_z], z2);
1858 [ - + ][ + - ]: 1 : ASSERT_EQ(res[w], w2);
1859 : : }
1860 [ - - ]: 0 : else if (res.find(d_y) == res.end())
1861 : : {
1862 : 0 : ASSERT_EQ(res[d_x], x1);
1863 : 0 : ASSERT_EQ(res[d_z], z1);
1864 : 0 : ASSERT_EQ(res[w], w1);
1865 : : }
1866 : : else
1867 : : {
1868 : 0 : ASSERT_TRUE(false);
1869 : : }
1870 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
1871 : :
1872 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
1873 : : {
1874 : 1 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
1875 : 1 : std::unordered_map<Node, Node> res;
1876 : : BVGauss::Result ret;
1877 : :
1878 : : /* -------------------------------------------------------------------
1879 : : * lhs rhs lhs rhs modulo 11
1880 : : * --^-- ^ --^-- ^
1881 : : * 1 0 9 7 --> 1 0 9 7
1882 : : * 0 1 3 9 0 1 3 9
1883 : : * ------------------------------------------------------------------- */
1884 : :
1885 : 1 : Node zero = bv::utils::mkZero(d_nodeManager.get(), 8);
1886 : 2 : Node xx = d_nodeManager->mkVar("xx", d_nodeManager->mkBitVectorType(8));
1887 : 2 : Node yy = d_nodeManager->mkVar("yy", d_nodeManager->mkBitVectorType(8));
1888 : 2 : Node zz = d_nodeManager->mkVar("zz", d_nodeManager->mkBitVectorType(8));
1889 : :
1890 : : Node x = bv::utils::mkConcat(
1891 : 1 : d_zero,
1892 : 2 : bv::utils::mkConcat(
1893 : 4 : zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, xx), 7, 0)));
1894 : : Node y = bv::utils::mkConcat(
1895 : 1 : d_zero,
1896 : 2 : bv::utils::mkConcat(
1897 : 4 : zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, yy), 7, 0)));
1898 : : Node z = bv::utils::mkConcat(
1899 : 1 : d_zero,
1900 : 2 : bv::utils::mkConcat(
1901 : 4 : zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, zz), 7, 0)));
1902 : :
1903 : 2 : Node x_mul_one = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, d_one32);
1904 : 2 : Node nine_mul_z = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_nine32, z);
1905 : 2 : Node one_mul_y = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_one, y);
1906 : 2 : Node z_mul_three = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, z, d_three);
1907 : :
1908 : 1 : Node eq1 = d_nodeManager->mkNode(
1909 : : Kind::EQUAL,
1910 : 1 : d_nodeManager->mkNode(
1911 : : Kind::BITVECTOR_UREM,
1912 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, x_mul_one, nine_mul_z),
1913 : 1 : d_p),
1914 : 4 : d_seven);
1915 : :
1916 : 1 : Node eq2 = d_nodeManager->mkNode(
1917 : : Kind::EQUAL,
1918 : 1 : d_nodeManager->mkNode(
1919 : : Kind::BITVECTOR_UREM,
1920 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, one_mul_y, z_mul_three),
1921 : 1 : d_p),
1922 : 4 : d_nine);
1923 : :
1924 : 4 : std::vector<Node> eqs = {eq1, eq2};
1925 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
1926 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
1927 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 2);
1928 : :
1929 : 1 : x = rr->rewrite(x);
1930 : 1 : y = rr->rewrite(y);
1931 : 1 : z = rr->rewrite(z);
1932 : :
1933 : 1 : Node x1 = d_nodeManager->mkNode(
1934 : : Kind::BITVECTOR_UREM,
1935 : 1 : d_nodeManager->mkNode(
1936 : : Kind::BITVECTOR_ADD,
1937 : 1 : d_seven32,
1938 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, z, d_two32)),
1939 : 3 : d_p);
1940 : 1 : Node y1 = d_nodeManager->mkNode(
1941 : : Kind::BITVECTOR_UREM,
1942 : 1 : d_nodeManager->mkNode(
1943 : : Kind::BITVECTOR_ADD,
1944 : 1 : d_nine32,
1945 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, z, d_eight32)),
1946 : 3 : d_p);
1947 : :
1948 : 1 : Node x2 = d_nodeManager->mkNode(
1949 : : Kind::BITVECTOR_UREM,
1950 : 1 : d_nodeManager->mkNode(
1951 : : Kind::BITVECTOR_ADD,
1952 : 1 : d_two32,
1953 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, y, d_three32)),
1954 : 3 : d_p);
1955 : 1 : Node z2 = d_nodeManager->mkNode(
1956 : : Kind::BITVECTOR_UREM,
1957 : 1 : d_nodeManager->mkNode(
1958 : : Kind::BITVECTOR_ADD,
1959 : 1 : d_three32,
1960 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, y, d_seven32)),
1961 : 3 : d_p);
1962 : :
1963 : 1 : Node y3 = d_nodeManager->mkNode(
1964 : : Kind::BITVECTOR_UREM,
1965 : 1 : d_nodeManager->mkNode(
1966 : : Kind::BITVECTOR_ADD,
1967 : 1 : d_three32,
1968 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, d_four32)),
1969 : 3 : d_p);
1970 : 1 : Node z3 = d_nodeManager->mkNode(
1971 : : Kind::BITVECTOR_UREM,
1972 : 1 : d_nodeManager->mkNode(
1973 : : Kind::BITVECTOR_ADD,
1974 : 1 : d_two32,
1975 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, d_six32)),
1976 : 3 : d_p);
1977 : :
1978 : : /* result depends on order of variables in matrix */
1979 [ + - ]: 1 : if (res.find(x) == res.end())
1980 : : {
1981 : : /*
1982 : : * y z x y z x
1983 : : * 0 9 1 7 --> 1 0 7 3
1984 : : * 1 3 0 9 0 1 5 2
1985 : : *
1986 : : * z y x z y x
1987 : : * 9 0 1 7 --> 1 0 5 2
1988 : : * 3 1 0 9 0 1 7 3
1989 : : */
1990 [ - + ][ + - ]: 2 : ASSERT_EQ(res[rr->rewrite(y)], y3);
1991 [ - + ][ + - ]: 2 : ASSERT_EQ(res[rr->rewrite(z)], z3);
1992 : : }
1993 [ - - ]: 0 : else if (res.find(y) == res.end())
1994 : : {
1995 : : /*
1996 : : * x z y x z y
1997 : : * 1 9 0 7 --> 1 0 8 2
1998 : : * 0 3 1 9 0 1 4 3
1999 : : *
2000 : : * z x y z x y
2001 : : * 9 1 0 7 --> 1 0 4 3
2002 : : * 3 0 1 9 0 1 8 2
2003 : : */
2004 : 0 : ASSERT_EQ(res[x], x2);
2005 : 0 : ASSERT_EQ(res[z], z2);
2006 : : }
2007 : : else
2008 : : {
2009 : 0 : ASSERT_EQ(res.find(z), res.end());
2010 : : /*
2011 : : * x y z x y z
2012 : : * 1 0 9 7 --> 1 0 9 7
2013 : : * 0 1 3 9 0 1 3 9
2014 : : *
2015 : : * y x z y x z
2016 : : * 0 1 9 7 --> 1 0 3 9
2017 : : * 1 0 3 9 0 1 9 7
2018 : : */
2019 : 0 : ASSERT_EQ(res[x], x1);
2020 : 0 : ASSERT_EQ(res[y], y1);
2021 : : }
2022 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
2023 : :
2024 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
2025 : : {
2026 : 1 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
2027 : 1 : std::unordered_map<Node, Node> res;
2028 : : BVGauss::Result ret;
2029 : :
2030 : : /* -------------------------------------------------------------------
2031 : : * lhs rhs lhs rhs modulo 11
2032 : : * --^-- ^ --^-- ^
2033 : : * 1 0 9 7 --> 1 0 9 7
2034 : : * 0 1 3 9 0 1 3 9
2035 : : * ------------------------------------------------------------------- */
2036 : :
2037 : 1 : Node zero = bv::utils::mkZero(d_nodeManager.get(), 8);
2038 : 2 : Node xx = d_nodeManager->mkVar("xx", d_nodeManager->mkBitVectorType(8));
2039 : 2 : Node yy = d_nodeManager->mkVar("yy", d_nodeManager->mkBitVectorType(8));
2040 : 2 : Node zz = d_nodeManager->mkVar("zz", d_nodeManager->mkBitVectorType(8));
2041 : :
2042 : : Node x = bv::utils::mkConcat(
2043 : 1 : d_zero,
2044 : 2 : bv::utils::mkConcat(
2045 : : zero,
2046 : 2 : bv::utils::mkExtract(
2047 : 3 : d_nodeManager->mkNode(Kind::BITVECTOR_CONCAT, zero, xx), 7, 0)));
2048 : : Node y = bv::utils::mkConcat(
2049 : 1 : d_zero,
2050 : 2 : bv::utils::mkConcat(
2051 : : zero,
2052 : 2 : bv::utils::mkExtract(
2053 : 3 : d_nodeManager->mkNode(Kind::BITVECTOR_CONCAT, zero, yy), 7, 0)));
2054 : : Node z = bv::utils::mkConcat(
2055 : 1 : d_zero,
2056 : 2 : bv::utils::mkConcat(
2057 : : zero,
2058 : 2 : bv::utils::mkExtract(
2059 : 3 : d_nodeManager->mkNode(Kind::BITVECTOR_CONCAT, zero, zz), 7, 0)));
2060 : :
2061 : 1 : NodeBuilder nbx(d_nodeManager.get(), Kind::BITVECTOR_MULT);
2062 : 1 : nbx << d_x << d_one << x;
2063 : 1 : Node x_mul_one_mul_xx = nbx.constructNode();
2064 : 1 : NodeBuilder nby(d_nodeManager.get(), Kind::BITVECTOR_MULT);
2065 : 1 : nby << d_y << y << d_one;
2066 : 1 : Node y_mul_yy_mul_one = nby.constructNode();
2067 : 1 : NodeBuilder nbz(d_nodeManager.get(), Kind::BITVECTOR_MULT);
2068 : 1 : nbz << d_three << d_z << z;
2069 : 1 : Node three_mul_z_mul_zz = nbz.constructNode();
2070 : 1 : NodeBuilder nbz2(d_nodeManager.get(), Kind::BITVECTOR_MULT);
2071 : 1 : nbz2 << d_z << d_nine << z;
2072 : 1 : Node z_mul_nine_mul_zz = nbz2.constructNode();
2073 : :
2074 : 2 : Node x_mul_xx = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, x);
2075 : 2 : Node y_mul_yy = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, y);
2076 : 2 : Node z_mul_zz = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, z);
2077 : :
2078 : 1 : Node eq1 = d_nodeManager->mkNode(
2079 : : Kind::EQUAL,
2080 : 1 : d_nodeManager->mkNode(
2081 : : Kind::BITVECTOR_UREM,
2082 : 1 : d_nodeManager->mkNode(
2083 : : Kind::BITVECTOR_ADD, x_mul_one_mul_xx, z_mul_nine_mul_zz),
2084 : 1 : d_p),
2085 : 4 : d_seven);
2086 : :
2087 : 1 : Node eq2 = d_nodeManager->mkNode(
2088 : : Kind::EQUAL,
2089 : 1 : d_nodeManager->mkNode(
2090 : : Kind::BITVECTOR_UREM,
2091 : 1 : d_nodeManager->mkNode(
2092 : : Kind::BITVECTOR_ADD, y_mul_yy_mul_one, three_mul_z_mul_zz),
2093 : 1 : d_p),
2094 : 4 : d_nine);
2095 : :
2096 : 4 : std::vector<Node> eqs = {eq1, eq2};
2097 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
2098 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::PARTIAL);
2099 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 2);
2100 : :
2101 : 1 : x_mul_xx = rr->rewrite(x_mul_xx);
2102 : 1 : y_mul_yy = rr->rewrite(y_mul_yy);
2103 : 1 : z_mul_zz = rr->rewrite(z_mul_zz);
2104 : :
2105 : 1 : Node x1 = d_nodeManager->mkNode(
2106 : : Kind::BITVECTOR_UREM,
2107 : 1 : d_nodeManager->mkNode(
2108 : : Kind::BITVECTOR_ADD,
2109 : 1 : d_seven32,
2110 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, z_mul_zz, d_two32)),
2111 : 3 : d_p);
2112 : 1 : Node y1 = d_nodeManager->mkNode(
2113 : : Kind::BITVECTOR_UREM,
2114 : 1 : d_nodeManager->mkNode(
2115 : : Kind::BITVECTOR_ADD,
2116 : 1 : d_nine32,
2117 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, z_mul_zz, d_eight32)),
2118 : 3 : d_p);
2119 : :
2120 : 1 : Node x2 = d_nodeManager->mkNode(
2121 : : Kind::BITVECTOR_UREM,
2122 : 1 : d_nodeManager->mkNode(
2123 : : Kind::BITVECTOR_ADD,
2124 : 1 : d_two32,
2125 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, y_mul_yy, d_three32)),
2126 : 3 : d_p);
2127 : 1 : Node z2 = d_nodeManager->mkNode(
2128 : : Kind::BITVECTOR_UREM,
2129 : 1 : d_nodeManager->mkNode(
2130 : : Kind::BITVECTOR_ADD,
2131 : 1 : d_three32,
2132 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, y_mul_yy, d_seven32)),
2133 : 3 : d_p);
2134 : :
2135 : 1 : Node y3 = d_nodeManager->mkNode(
2136 : : Kind::BITVECTOR_UREM,
2137 : 1 : d_nodeManager->mkNode(
2138 : : Kind::BITVECTOR_ADD,
2139 : 1 : d_three32,
2140 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x_mul_xx, d_four32)),
2141 : 3 : d_p);
2142 : 1 : Node z3 = d_nodeManager->mkNode(
2143 : : Kind::BITVECTOR_UREM,
2144 : 1 : d_nodeManager->mkNode(
2145 : : Kind::BITVECTOR_ADD,
2146 : 1 : d_two32,
2147 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x_mul_xx, d_six32)),
2148 : 3 : d_p);
2149 : :
2150 : : /* result depends on order of variables in matrix */
2151 [ + - ]: 1 : if (res.find(x_mul_xx) == res.end())
2152 : : {
2153 : : /*
2154 : : * y z x y z x
2155 : : * 0 9 1 7 --> 1 0 7 3
2156 : : * 1 3 0 9 0 1 5 2
2157 : : *
2158 : : * z y x z y x
2159 : : * 9 0 1 7 --> 1 0 5 2
2160 : : * 3 1 0 9 0 1 7 3
2161 : : */
2162 [ - + ][ + - ]: 1 : ASSERT_EQ(res[y_mul_yy], y3);
2163 [ - + ][ + - ]: 1 : ASSERT_EQ(res[z_mul_zz], z3);
2164 : : }
2165 [ - - ]: 0 : else if (res.find(y_mul_yy) == res.end())
2166 : : {
2167 : : /*
2168 : : * x z y x z y
2169 : : * 1 9 0 7 --> 1 0 8 2
2170 : : * 0 3 1 9 0 1 4 3
2171 : : *
2172 : : * z x y z x y
2173 : : * 9 1 0 7 --> 1 0 4 3
2174 : : * 3 0 1 9 0 1 8 2
2175 : : */
2176 : 0 : ASSERT_EQ(res[x_mul_xx], x2);
2177 : 0 : ASSERT_EQ(res[z_mul_zz], z2);
2178 : : }
2179 : : else
2180 : : {
2181 : 0 : ASSERT_EQ(res.find(z_mul_zz), res.end());
2182 : : /*
2183 : : * x y z x y z
2184 : : * 1 0 9 7 --> 1 0 9 7
2185 : : * 0 1 3 9 0 1 3 9
2186 : : *
2187 : : * y x z y x z
2188 : : * 0 1 9 7 --> 1 0 3 9
2189 : : * 1 0 3 9 0 1 9 7
2190 : : */
2191 : 0 : ASSERT_EQ(res[x_mul_xx], x1);
2192 : 0 : ASSERT_EQ(res[y_mul_yy], y1);
2193 : : }
2194 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2195 : :
2196 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1)
2197 : : {
2198 : 1 : std::unordered_map<Node, Node> res;
2199 : : BVGauss::Result ret;
2200 : :
2201 : : /* -------------------------------------------------------------------
2202 : : * 3x / 2z = 4 modulo 11
2203 : : * 2x % 5y = 2
2204 : : * y O z = 5
2205 : : * ------------------------------------------------------------------- */
2206 : :
2207 : 1 : Node n1 = d_nodeManager->mkNode(
2208 : : Kind::BITVECTOR_UDIV,
2209 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_three, d_x),
2210 : 3 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_two, d_y));
2211 : 1 : Node n2 = d_nodeManager->mkNode(
2212 : : Kind::BITVECTOR_UREM,
2213 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_two, d_x),
2214 : 3 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_five, d_y));
2215 : :
2216 : : Node n3 = bv::utils::mkConcat(
2217 : 1 : d_zero,
2218 : 2 : bv::utils::mkExtract(
2219 : 3 : d_nodeManager->mkNode(Kind::BITVECTOR_CONCAT, d_y, d_z), 15, 0));
2220 : :
2221 : 1 : Node eq1 = d_nodeManager->mkNode(
2222 : : Kind::EQUAL,
2223 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_UREM, n1, d_p),
2224 : 3 : d_four);
2225 : :
2226 : 1 : Node eq2 = d_nodeManager->mkNode(
2227 : 2 : Kind::EQUAL, d_nodeManager->mkNode(Kind::BITVECTOR_UREM, n2, d_p), d_two);
2228 : :
2229 : 1 : Node eq3 = d_nodeManager->mkNode(
2230 : : Kind::EQUAL,
2231 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_UREM, n3, d_p),
2232 : 3 : d_five);
2233 : :
2234 : 5 : std::vector<Node> eqs = {eq1, eq2, eq3};
2235 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
2236 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
2237 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 3);
2238 : :
2239 [ - + ][ + - ]: 1 : ASSERT_EQ(res[n1], d_four32);
2240 [ - + ][ + - ]: 1 : ASSERT_EQ(res[n2], d_two32);
2241 [ - + ][ + - ]: 1 : ASSERT_EQ(res[n3], d_five32);
2242 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2243 : :
2244 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2)
2245 : : {
2246 : 1 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
2247 : 1 : std::unordered_map<Node, Node> res;
2248 : : BVGauss::Result ret;
2249 : :
2250 : : /* -------------------------------------------------------------------
2251 : : * x*y = 4 modulo 11
2252 : : * x*y*z = 2
2253 : : * 2*x*y + 2*z = 9
2254 : : * ------------------------------------------------------------------- */
2255 : :
2256 : 1 : Node zero32 = bv::utils::mkZero(d_nodeManager.get(), 32);
2257 : :
2258 : : Node x = bv::utils::mkConcat(
2259 : 2 : zero32, d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)));
2260 : : Node y = bv::utils::mkConcat(
2261 : 2 : zero32, d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)));
2262 : : Node z = bv::utils::mkConcat(
2263 : 2 : zero32, d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16)));
2264 : :
2265 : 2 : Node n1 = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, y);
2266 : : Node n2 =
2267 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
2268 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, y),
2269 : 3 : z);
2270 : 1 : Node n3 = d_nodeManager->mkNode(
2271 : : Kind::BITVECTOR_ADD,
2272 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
2273 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, y),
2274 : 2 : bv::utils::mkConcat(d_zero, d_two)),
2275 : 1 : d_nodeManager->mkNode(
2276 : 5 : Kind::BITVECTOR_MULT, bv::utils::mkConcat(d_zero, d_two), z));
2277 : :
2278 : 1 : Node eq1 = d_nodeManager->mkNode(
2279 : : Kind::EQUAL,
2280 : 1 : d_nodeManager->mkNode(
2281 : 2 : Kind::BITVECTOR_UREM, n1, bv::utils::mkConcat(d_zero, d_p)),
2282 : 4 : bv::utils::mkConcat(d_zero, d_four));
2283 : :
2284 : 1 : Node eq2 = d_nodeManager->mkNode(
2285 : : Kind::EQUAL,
2286 : 1 : d_nodeManager->mkNode(
2287 : 2 : Kind::BITVECTOR_UREM, n2, bv::utils::mkConcat(d_zero, d_p)),
2288 : 4 : bv::utils::mkConcat(d_zero, d_two));
2289 : :
2290 : 1 : Node eq3 = d_nodeManager->mkNode(
2291 : : Kind::EQUAL,
2292 : 1 : d_nodeManager->mkNode(
2293 : 2 : Kind::BITVECTOR_UREM, n3, bv::utils::mkConcat(d_zero, d_p)),
2294 : 4 : bv::utils::mkConcat(d_zero, d_nine));
2295 : :
2296 : 5 : std::vector<Node> eqs = {eq1, eq2, eq3};
2297 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
2298 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
2299 [ - + ][ + - ]: 1 : ASSERT_EQ(res.size(), 3);
2300 : :
2301 : 1 : n1 = rr->rewrite(n1);
2302 : 1 : n2 = rr->rewrite(n2);
2303 : 1 : z = rr->rewrite(z);
2304 : :
2305 [ - + ][ + - ]: 2 : ASSERT_EQ(res[n1], bv::utils::mkConst(d_nodeManager.get(), 48, 4));
2306 [ - + ][ + - ]: 2 : ASSERT_EQ(res[n2], bv::utils::mkConst(d_nodeManager.get(), 48, 2));
2307 : :
2308 : 2 : Integer twoxy = (res[n1].getConst<BitVector>().getValue() * Integer(2))
2309 : 2 : .euclidianDivideRemainder(Integer(48));
2310 : 2 : Integer twoz = (res[z].getConst<BitVector>().getValue() * Integer(2))
2311 : 2 : .euclidianDivideRemainder(Integer(48));
2312 : 2 : Integer r = (twoxy + twoz).euclidianDivideRemainder(Integer(11));
2313 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(9));
2314 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2315 : :
2316 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_invalid)
2317 : : {
2318 : 1 : std::unordered_map<Node, Node> res;
2319 : : BVGauss::Result ret;
2320 : :
2321 : : /* -------------------------------------------------------------------
2322 : : * x*y = 4 modulo 11
2323 : : * x*y*z = 2
2324 : : * 2*x*y = 9
2325 : : * ------------------------------------------------------------------- */
2326 : :
2327 : 1 : Node zero32 = bv::utils::mkZero(d_nodeManager.get(), 32);
2328 : :
2329 : : Node x = bv::utils::mkConcat(
2330 : 2 : zero32, d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)));
2331 : : Node y = bv::utils::mkConcat(
2332 : 2 : zero32, d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)));
2333 : : Node z = bv::utils::mkConcat(
2334 : 2 : zero32, d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16)));
2335 : :
2336 : 2 : Node n1 = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, y);
2337 : : Node n2 =
2338 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
2339 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, y),
2340 : 3 : z);
2341 : : Node n3 =
2342 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
2343 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, x, y),
2344 : 3 : bv::utils::mkConcat(d_zero, d_two));
2345 : :
2346 : 1 : Node eq1 = d_nodeManager->mkNode(
2347 : : Kind::EQUAL,
2348 : 1 : d_nodeManager->mkNode(
2349 : 2 : Kind::BITVECTOR_UREM, n1, bv::utils::mkConcat(d_zero, d_p)),
2350 : 4 : bv::utils::mkConcat(d_zero, d_four));
2351 : :
2352 : 1 : Node eq2 = d_nodeManager->mkNode(
2353 : : Kind::EQUAL,
2354 : 1 : d_nodeManager->mkNode(
2355 : 2 : Kind::BITVECTOR_UREM, n2, bv::utils::mkConcat(d_zero, d_p)),
2356 : 4 : bv::utils::mkConcat(d_zero, d_two));
2357 : :
2358 : 1 : Node eq3 = d_nodeManager->mkNode(
2359 : : Kind::EQUAL,
2360 : 1 : d_nodeManager->mkNode(
2361 : 2 : Kind::BITVECTOR_UREM, n3, bv::utils::mkConcat(d_zero, d_p)),
2362 : 4 : bv::utils::mkConcat(d_zero, d_nine));
2363 : :
2364 : 5 : std::vector<Node> eqs = {eq1, eq2, eq3};
2365 : 1 : ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res);
2366 [ - + ][ + - ]: 1 : ASSERT_EQ(ret, BVGauss::Result::INVALID);
2367 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2368 : :
2369 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1)
2370 : : {
2371 : : /* -------------------------------------------------------------------
2372 : : * lhs rhs modulo 11
2373 : : * --^-- ^
2374 : : * 1 1 1 5
2375 : : * 2 3 5 8
2376 : : * 4 0 5 2
2377 : : * ------------------------------------------------------------------- */
2378 : :
2379 : 1 : Node eq1 = d_nodeManager->mkNode(
2380 : : Kind::EQUAL,
2381 : 1 : d_nodeManager->mkNode(
2382 : : Kind::BITVECTOR_UREM,
2383 : 1 : d_nodeManager->mkNode(
2384 : : Kind::BITVECTOR_ADD,
2385 : 1 : d_nodeManager->mkNode(
2386 : 2 : Kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_one),
2387 : 1 : d_z_mul_one),
2388 : 1 : d_p),
2389 : 5 : d_five);
2390 : :
2391 : 1 : Node eq2 = d_nodeManager->mkNode(
2392 : : Kind::EQUAL,
2393 : 1 : d_nodeManager->mkNode(
2394 : : Kind::BITVECTOR_UREM,
2395 : 1 : d_nodeManager->mkNode(
2396 : : Kind::BITVECTOR_ADD,
2397 : 1 : d_nodeManager->mkNode(
2398 : 2 : Kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three),
2399 : 1 : d_z_mul_five),
2400 : 1 : d_p),
2401 : 5 : d_eight);
2402 : :
2403 : 1 : Node eq3 = d_nodeManager->mkNode(
2404 : : Kind::EQUAL,
2405 : 1 : d_nodeManager->mkNode(
2406 : : Kind::BITVECTOR_UREM,
2407 : 1 : d_nodeManager->mkNode(
2408 : 2 : Kind::BITVECTOR_ADD, d_x_mul_four, d_z_mul_five),
2409 : 1 : d_p),
2410 : 4 : d_two);
2411 : :
2412 : 1 : Node a = d_nodeManager->mkNode(
2413 : 2 : Kind::AND, d_nodeManager->mkNode(Kind::AND, eq1, eq2), eq3);
2414 : :
2415 : 1 : AssertionPipeline apipe(d_slvEngine->getEnv());
2416 : 1 : apipe.push_back(a);
2417 : 2 : passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit");
2418 : 1 : std::unordered_map<Node, Node> res;
2419 : 1 : PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
2420 [ - + ][ + - ]: 1 : ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
2421 : 1 : Node resx = d_nodeManager->mkNode(
2422 : 2 : Kind::EQUAL, d_x, d_nodeManager->mkConst<BitVector>(BitVector(32, 3u)));
2423 : 1 : Node resy = d_nodeManager->mkNode(
2424 : 2 : Kind::EQUAL, d_y, d_nodeManager->mkConst<BitVector>(BitVector(32, 4u)));
2425 : 1 : Node resz = d_nodeManager->mkNode(
2426 : 2 : Kind::EQUAL, d_z, d_nodeManager->mkConst<BitVector>(BitVector(32, 9u)));
2427 [ - + ][ + - ]: 1 : ASSERT_EQ(apipe.size(), 6);
2428 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(apipe.begin(), apipe.end(), resx), apipe.end());
2429 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(apipe.begin(), apipe.end(), resy), apipe.end());
2430 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(apipe.begin(), apipe.end(), resz), apipe.end());
2431 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
2432 : :
2433 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
2434 : : {
2435 : : /* -------------------------------------------------------------------
2436 : : * lhs rhs lhs rhs modulo 11
2437 : : * --^-- ^ --^-- ^
2438 : : * 1 1 1 5 1 0 0 3
2439 : : * 2 3 5 8 0 1 0 4
2440 : : * 4 0 5 2 0 0 1 9
2441 : : *
2442 : : * lhs rhs lhs rhs modulo 7
2443 : : * --^-- ^ --^-- ^
2444 : : * 2 6 0 4 1 0 0 3
2445 : : * 4 6 0 3 0 1 0 2
2446 : : * ------------------------------------------------------------------- */
2447 : :
2448 : 1 : Node eq1 = d_nodeManager->mkNode(
2449 : : Kind::EQUAL,
2450 : 1 : d_nodeManager->mkNode(
2451 : : Kind::BITVECTOR_UREM,
2452 : 1 : d_nodeManager->mkNode(
2453 : : Kind::BITVECTOR_ADD,
2454 : 1 : d_nodeManager->mkNode(
2455 : 2 : Kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_one),
2456 : 1 : d_z_mul_one),
2457 : 1 : d_p),
2458 : 5 : d_five);
2459 : :
2460 : 1 : Node eq2 = d_nodeManager->mkNode(
2461 : : Kind::EQUAL,
2462 : 1 : d_nodeManager->mkNode(
2463 : : Kind::BITVECTOR_UREM,
2464 : 1 : d_nodeManager->mkNode(
2465 : : Kind::BITVECTOR_ADD,
2466 : 1 : d_nodeManager->mkNode(
2467 : 2 : Kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three),
2468 : 1 : d_z_mul_five),
2469 : 1 : d_p),
2470 : 5 : d_eight);
2471 : :
2472 : 1 : Node eq3 = d_nodeManager->mkNode(
2473 : : Kind::EQUAL,
2474 : 1 : d_nodeManager->mkNode(
2475 : : Kind::BITVECTOR_UREM,
2476 : 1 : d_nodeManager->mkNode(
2477 : 2 : Kind::BITVECTOR_ADD, d_x_mul_four, d_z_mul_five),
2478 : 1 : d_p),
2479 : 4 : d_two);
2480 : :
2481 : 2 : Node y_mul_six = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_six);
2482 : :
2483 : 1 : Node eq4 = d_nodeManager->mkNode(
2484 : : Kind::EQUAL,
2485 : 1 : d_nodeManager->mkNode(
2486 : : Kind::BITVECTOR_UREM,
2487 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, d_x_mul_two, y_mul_six),
2488 : 1 : d_seven),
2489 : 4 : d_four);
2490 : :
2491 : 1 : Node eq5 = d_nodeManager->mkNode(
2492 : : Kind::EQUAL,
2493 : 1 : d_nodeManager->mkNode(
2494 : : Kind::BITVECTOR_UREM,
2495 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, d_x_mul_four, y_mul_six),
2496 : 1 : d_seven),
2497 : 4 : d_three);
2498 : :
2499 : 1 : Node a = d_nodeManager->mkNode(
2500 : 2 : Kind::AND, d_nodeManager->mkNode(Kind::AND, eq1, eq2), eq3);
2501 : :
2502 : 1 : AssertionPipeline apipe(d_slvEngine->getEnv());
2503 : 1 : apipe.push_back(a);
2504 : 1 : apipe.push_back(eq4);
2505 : 1 : apipe.push_back(eq5);
2506 : 2 : passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit");
2507 : 1 : std::unordered_map<Node, Node> res;
2508 : 1 : PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
2509 [ - + ][ + - ]: 1 : ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
2510 : 1 : Node resx1 = d_nodeManager->mkNode(
2511 : 2 : Kind::EQUAL, d_x, d_nodeManager->mkConst<BitVector>(BitVector(32, 3u)));
2512 : 1 : Node resx2 = d_nodeManager->mkNode(
2513 : 2 : Kind::EQUAL, d_x, d_nodeManager->mkConst<BitVector>(BitVector(32, 3u)));
2514 : 1 : Node resy1 = d_nodeManager->mkNode(
2515 : 2 : Kind::EQUAL, d_y, d_nodeManager->mkConst<BitVector>(BitVector(32, 4u)));
2516 : 1 : Node resy2 = d_nodeManager->mkNode(
2517 : 2 : Kind::EQUAL, d_y, d_nodeManager->mkConst<BitVector>(BitVector(32, 2u)));
2518 : 1 : Node resz = d_nodeManager->mkNode(
2519 : 2 : Kind::EQUAL, d_z, d_nodeManager->mkConst<BitVector>(BitVector(32, 9u)));
2520 [ - + ][ + - ]: 1 : ASSERT_EQ(apipe.size(), 10);
2521 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(apipe.begin(), apipe.end(), resx1), apipe.end());
2522 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(apipe.begin(), apipe.end(), resx2), apipe.end());
2523 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(apipe.begin(), apipe.end(), resy1), apipe.end());
2524 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(apipe.begin(), apipe.end(), resy2), apipe.end());
2525 [ - + ][ + - ]: 1 : ASSERT_NE(std::find(apipe.begin(), apipe.end(), resz), apipe.end());
2526 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2527 : :
2528 : 4 : TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
2529 : : {
2530 : : /* -------------------------------------------------------------------
2531 : : * lhs rhs lhs rhs modulo 11
2532 : : * --^-- ^ --^-- ^
2533 : : * 1 0 9 7 --> 1 0 9 7
2534 : : * 0 1 3 9 0 1 3 9
2535 : : * ------------------------------------------------------------------- */
2536 : :
2537 : 1 : Node eq1 = d_nodeManager->mkNode(
2538 : : Kind::EQUAL,
2539 : 1 : d_nodeManager->mkNode(
2540 : : Kind::BITVECTOR_UREM,
2541 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_ADD, d_x_mul_one, d_z_mul_nine),
2542 : 1 : d_p),
2543 : 4 : d_seven);
2544 : :
2545 : 1 : Node eq2 = d_nodeManager->mkNode(
2546 : : Kind::EQUAL,
2547 : 1 : d_nodeManager->mkNode(
2548 : : Kind::BITVECTOR_UREM,
2549 : 1 : d_nodeManager->mkNode(
2550 : 2 : Kind::BITVECTOR_ADD, d_y_mul_one, d_z_mul_three),
2551 : 1 : d_p),
2552 : 4 : d_nine);
2553 : :
2554 : 1 : AssertionPipeline apipe(d_slvEngine->getEnv());
2555 : 1 : apipe.push_back(eq1);
2556 : 1 : apipe.push_back(eq2);
2557 : 2 : passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit");
2558 : 1 : std::unordered_map<Node, Node> res;
2559 : 1 : PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
2560 [ - + ][ + - ]: 1 : ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
2561 [ - + ][ + - ]: 1 : ASSERT_EQ(apipe.size(), 4);
2562 : :
2563 : 1 : Node resx1 = d_nodeManager->mkNode(
2564 : : Kind::EQUAL,
2565 : 1 : d_x,
2566 : 1 : d_nodeManager->mkNode(
2567 : : Kind::BITVECTOR_UREM,
2568 : 1 : d_nodeManager->mkNode(
2569 : : Kind::BITVECTOR_ADD,
2570 : 1 : d_seven32,
2571 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_two32)),
2572 : 3 : d_p));
2573 : 1 : Node resy1 = d_nodeManager->mkNode(
2574 : : Kind::EQUAL,
2575 : 1 : d_y,
2576 : 1 : d_nodeManager->mkNode(
2577 : : Kind::BITVECTOR_UREM,
2578 : 1 : d_nodeManager->mkNode(
2579 : : Kind::BITVECTOR_ADD,
2580 : 1 : d_nine32,
2581 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_z, d_eight32)),
2582 : 3 : d_p));
2583 : :
2584 : 1 : Node resx2 = d_nodeManager->mkNode(
2585 : : Kind::EQUAL,
2586 : 1 : d_x,
2587 : 1 : d_nodeManager->mkNode(
2588 : : Kind::BITVECTOR_UREM,
2589 : 1 : d_nodeManager->mkNode(
2590 : : Kind::BITVECTOR_ADD,
2591 : 1 : d_two32,
2592 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_three32)),
2593 : 3 : d_p));
2594 : 1 : Node resz2 = d_nodeManager->mkNode(
2595 : : Kind::EQUAL,
2596 : 1 : d_z,
2597 : 1 : d_nodeManager->mkNode(
2598 : : Kind::BITVECTOR_UREM,
2599 : 1 : d_nodeManager->mkNode(
2600 : : Kind::BITVECTOR_ADD,
2601 : 1 : d_three32,
2602 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_y, d_seven32)),
2603 : 3 : d_p));
2604 : :
2605 : 1 : Node resy3 = d_nodeManager->mkNode(
2606 : : Kind::EQUAL,
2607 : 1 : d_y,
2608 : 1 : d_nodeManager->mkNode(
2609 : : Kind::BITVECTOR_UREM,
2610 : 1 : d_nodeManager->mkNode(
2611 : : Kind::BITVECTOR_ADD,
2612 : 1 : d_three32,
2613 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_four32)),
2614 : 3 : d_p));
2615 : 1 : Node resz3 = d_nodeManager->mkNode(
2616 : : Kind::EQUAL,
2617 : 1 : d_z,
2618 : 1 : d_nodeManager->mkNode(
2619 : : Kind::BITVECTOR_UREM,
2620 : 1 : d_nodeManager->mkNode(
2621 : : Kind::BITVECTOR_ADD,
2622 : 1 : d_two32,
2623 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT, d_x, d_six32)),
2624 : 3 : d_p));
2625 : :
2626 : 1 : bool fx1 = std::find(apipe.begin(), apipe.end(), resx1) != apipe.end();
2627 : 1 : bool fy1 = std::find(apipe.begin(), apipe.end(), resy1) != apipe.end();
2628 : 1 : bool fx2 = std::find(apipe.begin(), apipe.end(), resx2) != apipe.end();
2629 : 1 : bool fz2 = std::find(apipe.begin(), apipe.end(), resz2) != apipe.end();
2630 : 1 : bool fy3 = std::find(apipe.begin(), apipe.end(), resy3) != apipe.end();
2631 : 1 : bool fz3 = std::find(apipe.begin(), apipe.end(), resz3) != apipe.end();
2632 : :
2633 : : /* result depends on order of variables in matrix */
2634 [ - + ][ - - ]: 1 : ASSERT_TRUE((fx1 && fy1) || (fx2 && fz2) || (fy3 && fz3));
[ + - ][ - + ]
[ - - ][ - - ]
[ - + ][ + - ]
2635 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
2636 : :
2637 : 4 : TEST_F(TestPPWhiteBVGauss, get_min_bw1)
2638 : : {
2639 [ - + ]: 1 : ASSERT_EQ(
2640 : : d_bv_gauss->getMinBwExpr(bv::utils::mkConst(d_nodeManager.get(), 32, 11)),
2641 [ + - ]: 1 : 4);
2642 : :
2643 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(d_p), 4);
2644 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(d_x), 16);
2645 : :
2646 : 1 : Node extp = bv::utils::mkExtract(d_p, 4, 0);
2647 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(extp), 4);
2648 : 1 : Node extx = bv::utils::mkExtract(d_x, 4, 0);
2649 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(extx), 5);
2650 : :
2651 : : Node zextop8 =
2652 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(8));
2653 : : Node zextop16 =
2654 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(16));
2655 : : Node zextop32 =
2656 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(32));
2657 : : Node zextop40 =
2658 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(40));
2659 : :
2660 : 2 : Node zext40p = d_nodeManager->mkNode(zextop8, d_p);
2661 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext40p), 4);
2662 : 2 : Node zext40x = d_nodeManager->mkNode(zextop8, d_x);
2663 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext40x), 16);
2664 : :
2665 : 2 : Node zext48p = d_nodeManager->mkNode(zextop16, d_p);
2666 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48p), 4);
2667 : 2 : Node zext48x = d_nodeManager->mkNode(zextop16, d_x);
2668 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48x), 16);
2669 : :
2670 : 1 : Node p8 = d_nodeManager->mkConst<BitVector>(BitVector(8, 11u));
2671 : 2 : Node x8 = d_nodeManager->mkVar("x8", d_nodeManager->mkBitVectorType(8));
2672 : :
2673 : 2 : Node zext48p8 = d_nodeManager->mkNode(zextop40, p8);
2674 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48p8), 4);
2675 : 2 : Node zext48x8 = d_nodeManager->mkNode(zextop40, x8);
2676 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48x8), 8);
2677 : :
2678 : 2 : Node mult1p = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, extp, extp);
2679 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult1p), 5);
2680 : 2 : Node mult1x = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, extx, extx);
2681 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult1x), 0);
2682 : :
2683 : 2 : Node mult2p = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, zext40p, zext40p);
2684 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult2p), 7);
2685 : 2 : Node mult2x = d_nodeManager->mkNode(Kind::BITVECTOR_MULT, zext40x, zext40x);
2686 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult2x), 32);
2687 : :
2688 : 1 : NodeBuilder nbmult3p(d_nodeManager.get(), Kind::BITVECTOR_MULT);
2689 : 1 : nbmult3p << zext48p << zext48p << zext48p;
2690 : 1 : Node mult3p = nbmult3p;
2691 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult3p), 11);
2692 : 1 : NodeBuilder nbmult3x(d_nodeManager.get(), Kind::BITVECTOR_MULT);
2693 : 1 : nbmult3x << zext48x << zext48x << zext48x;
2694 : 1 : Node mult3x = nbmult3x;
2695 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult3x), 48);
2696 : :
2697 : 1 : NodeBuilder nbmult4p(d_nodeManager.get(), Kind::BITVECTOR_MULT);
2698 : 1 : nbmult4p << zext48p << zext48p8 << zext48p;
2699 : 1 : Node mult4p = nbmult4p;
2700 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult4p), 11);
2701 : 1 : NodeBuilder nbmult4x(d_nodeManager.get(), Kind::BITVECTOR_MULT);
2702 : 1 : nbmult4x << zext48x << zext48x8 << zext48x;
2703 : 1 : Node mult4x = nbmult4x;
2704 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult4x), 40);
2705 : :
2706 : 2 : Node concat1p = bv::utils::mkConcat(d_p, zext48p);
2707 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat1p), 52);
2708 : 2 : Node concat1x = bv::utils::mkConcat(d_x, zext48x);
2709 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat1x), 64);
2710 : :
2711 : : Node concat2p =
2712 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 16), zext48p);
2713 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat2p), 4);
2714 : : Node concat2x =
2715 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 16), zext48x);
2716 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat2x), 16);
2717 : :
2718 : 2 : Node udiv1p = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, zext48p, zext48p);
2719 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv1p), 1);
2720 : 2 : Node udiv1x = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, zext48x, zext48x);
2721 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv1x), 48);
2722 : :
2723 : 2 : Node udiv2p = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, zext48p, zext48p8);
2724 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv2p), 1);
2725 : 2 : Node udiv2x = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, zext48x, zext48x8);
2726 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv2x), 48);
2727 : :
2728 : 2 : Node urem1p = d_nodeManager->mkNode(Kind::BITVECTOR_UREM, zext48p, zext48p);
2729 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem1p), 1);
2730 : 2 : Node urem1x = d_nodeManager->mkNode(Kind::BITVECTOR_UREM, zext48x, zext48x);
2731 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem1x), 1);
2732 : :
2733 : 2 : Node urem2p = d_nodeManager->mkNode(Kind::BITVECTOR_UREM, zext48p, zext48p8);
2734 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem2p), 1);
2735 : 2 : Node urem2x = d_nodeManager->mkNode(Kind::BITVECTOR_UREM, zext48x, zext48x8);
2736 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem2x), 16);
2737 : :
2738 : 2 : Node urem3p = d_nodeManager->mkNode(Kind::BITVECTOR_UREM, zext48p8, zext48p);
2739 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem3p), 1);
2740 : 2 : Node urem3x = d_nodeManager->mkNode(Kind::BITVECTOR_UREM, zext48x8, zext48x);
2741 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem3x), 8);
2742 : :
2743 : 2 : Node add1p = d_nodeManager->mkNode(Kind::BITVECTOR_ADD, extp, extp);
2744 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add1p), 5);
2745 : 2 : Node add1x = d_nodeManager->mkNode(Kind::BITVECTOR_ADD, extx, extx);
2746 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add1x), 0);
2747 : :
2748 : 2 : Node add2p = d_nodeManager->mkNode(Kind::BITVECTOR_ADD, zext40p, zext40p);
2749 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add2p), 5);
2750 : 2 : Node add2x = d_nodeManager->mkNode(Kind::BITVECTOR_ADD, zext40x, zext40x);
2751 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add2x), 17);
2752 : :
2753 : 2 : Node add3p = d_nodeManager->mkNode(Kind::BITVECTOR_ADD, zext48p8, zext48p);
2754 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add3p), 5);
2755 : 2 : Node add3x = d_nodeManager->mkNode(Kind::BITVECTOR_ADD, zext48x8, zext48x);
2756 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add3x), 17);
2757 : :
2758 : 1 : NodeBuilder nbadd4p(d_nodeManager.get(), Kind::BITVECTOR_ADD);
2759 : 1 : nbadd4p << zext48p << zext48p << zext48p;
2760 : 1 : Node add4p = nbadd4p;
2761 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add4p), 6);
2762 : 1 : NodeBuilder nbadd4x(d_nodeManager.get(), Kind::BITVECTOR_ADD);
2763 : 1 : nbadd4x << zext48x << zext48x << zext48x;
2764 : 1 : Node add4x = nbadd4x;
2765 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add4x), 18);
2766 : :
2767 : 1 : NodeBuilder nbadd5p(d_nodeManager.get(), Kind::BITVECTOR_ADD);
2768 : 1 : nbadd5p << zext48p << zext48p8 << zext48p;
2769 : 1 : Node add5p = nbadd5p;
2770 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add5p), 6);
2771 : 1 : NodeBuilder nbadd5x(d_nodeManager.get(), Kind::BITVECTOR_ADD);
2772 : 1 : nbadd5x << zext48x << zext48x8 << zext48x;
2773 : 1 : Node add5x = nbadd5x;
2774 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add5x), 18);
2775 : :
2776 : 1 : NodeBuilder nbadd6p(d_nodeManager.get(), Kind::BITVECTOR_ADD);
2777 : 1 : nbadd6p << zext48p << zext48p << zext48p << zext48p;
2778 : 1 : Node add6p = nbadd6p;
2779 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add6p), 6);
2780 : 1 : NodeBuilder nbadd6x(d_nodeManager.get(), Kind::BITVECTOR_ADD);
2781 : 1 : nbadd6x << zext48x << zext48x << zext48x << zext48x;
2782 : 1 : Node add6x = nbadd6x;
2783 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(add6x), 18);
2784 : :
2785 : 1 : Node not1p = d_nodeManager->mkNode(Kind::BITVECTOR_NOT, zext40p);
2786 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(not1p), 40);
2787 : 1 : Node not1x = d_nodeManager->mkNode(Kind::BITVECTOR_NOT, zext40x);
2788 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(not1x), 40);
2789 : : }
2790 : :
2791 : 4 : TEST_F(TestPPWhiteBVGauss, get_min_bw2)
2792 : : {
2793 : : /* ((_ zero_extend 5)
2794 : : * ((_ extract 7 0) ((_ zero_extend 15) d_p))) */
2795 : : Node zextop5 =
2796 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2797 : : Node zextop15 =
2798 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(15));
2799 : 2 : Node zext1 = d_nodeManager->mkNode(zextop15, d_p);
2800 : 1 : Node ext = bv::utils::mkExtract(zext1, 7, 0);
2801 : 2 : Node zext2 = d_nodeManager->mkNode(zextop5, ext);
2802 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 4);
2803 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
2804 : :
2805 : 4 : TEST_F(TestPPWhiteBVGauss, get_min_bw3a)
2806 : : {
2807 : : /* ((_ zero_extend 5)
2808 : : * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x z)))
2809 : : * ((_ extract 4 0) z))) */
2810 : 2 : Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16));
2811 : 2 : Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16));
2812 : 2 : Node z = d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16));
2813 : : Node zextop5 =
2814 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2815 : 2 : Node udiv1 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, x, y);
2816 : 2 : Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
2817 : 1 : Node ext1 = bv::utils::mkExtract(zext1, 4, 0);
2818 : 1 : Node ext2 = bv::utils::mkExtract(z, 4, 0);
2819 : 2 : Node udiv2 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, ext1, ext2);
2820 : : Node zext2 =
2821 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), udiv2);
2822 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 5);
2823 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2824 : :
2825 : 4 : TEST_F(TestPPWhiteBVGauss, get_min_bw3b)
2826 : : {
2827 : : /* ((_ zero_extend 5)
2828 : : * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x z)))
2829 : : * ((_ extract 4 0) z))) */
2830 : : Node zextop5 =
2831 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2832 : 2 : Node udiv1 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, d_x, d_y);
2833 : 2 : Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
2834 : 1 : Node ext1 = bv::utils::mkExtract(zext1, 4, 0);
2835 : 1 : Node ext2 = bv::utils::mkExtract(d_z, 4, 0);
2836 : 2 : Node udiv2 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, ext1, ext2);
2837 : : Node zext2 =
2838 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), udiv2);
2839 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 5);
2840 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
2841 : :
2842 : 4 : TEST_F(TestPPWhiteBVGauss, get_min_bw4a)
2843 : : {
2844 : : /* (bvadd
2845 : : * ((_ zero_extend 5)
2846 : : * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x y)))
2847 : : * ((_ extract 4 0) z)))
2848 : : * ((_ zero_extend 7)
2849 : : * (bvudiv ((_ extract 2 0) ((_ zero_extend 5) (bvudiv x y)))
2850 : : * ((_ extract 2 0) z))) */
2851 : 2 : Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16));
2852 : 2 : Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16));
2853 : 2 : Node z = d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16));
2854 : : Node zextop5 =
2855 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2856 : : Node zextop7 =
2857 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(7));
2858 : :
2859 : 2 : Node udiv1 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, x, y);
2860 : 2 : Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
2861 : :
2862 : 1 : Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0);
2863 : 1 : Node ext2_1 = bv::utils::mkExtract(z, 4, 0);
2864 : 2 : Node udiv2_1 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, ext1_1, ext2_1);
2865 : : Node zext2_1 =
2866 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), udiv2_1);
2867 : :
2868 : 1 : Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0);
2869 : 1 : Node ext2_2 = bv::utils::mkExtract(z, 2, 0);
2870 : 2 : Node udiv2_2 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, ext1_2, ext2_2);
2871 : 2 : Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2);
2872 : :
2873 : 2 : Node plus = d_nodeManager->mkNode(Kind::BITVECTOR_ADD, zext2_1, zext2_2);
2874 : :
2875 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus), 6);
2876 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
2877 : :
2878 : 4 : TEST_F(TestPPWhiteBVGauss, get_min_bw4b)
2879 : : {
2880 : : /* (bvadd
2881 : : * ((_ zero_extend 5)
2882 : : * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x y)))
2883 : : * ((_ extract 4 0) z)))
2884 : : * ((_ zero_extend 7)
2885 : : * (bvudiv ((_ extract 2 0) ((_ zero_extend 5) (bvudiv x y)))
2886 : : * ((_ extract 2 0) z))) */
2887 : : Node zextop5 =
2888 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2889 : : Node zextop7 =
2890 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(7));
2891 : :
2892 : 2 : Node udiv1 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, d_x, d_y);
2893 : 2 : Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
2894 : :
2895 : 1 : Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0);
2896 : 1 : Node ext2_1 = bv::utils::mkExtract(d_z, 4, 0);
2897 : 2 : Node udiv2_1 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, ext1_1, ext2_1);
2898 : : Node zext2_1 =
2899 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), udiv2_1);
2900 : :
2901 : 1 : Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0);
2902 : 1 : Node ext2_2 = bv::utils::mkExtract(d_z, 2, 0);
2903 : 2 : Node udiv2_2 = d_nodeManager->mkNode(Kind::BITVECTOR_UDIV, ext1_2, ext2_2);
2904 : 2 : Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2);
2905 : :
2906 : 2 : Node plus = d_nodeManager->mkNode(Kind::BITVECTOR_ADD, zext2_1, zext2_2);
2907 : :
2908 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus), 6);
2909 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
2910 : :
2911 : 4 : TEST_F(TestPPWhiteBVGauss, get_min_bw5a)
2912 : : {
2913 : : /* (bvadd
2914 : : * (bvadd
2915 : : * (bvadd
2916 : : * (bvadd
2917 : : * (bvadd
2918 : : * (bvadd
2919 : : * (bvadd (bvmul (_ bv86 13)
2920 : : * ((_ zero_extend 5)
2921 : : * ((_ extract 7 0) ((_ zero_extend 15) x))))
2922 : : * (bvmul (_ bv41 13)
2923 : : * ((_ zero_extend 5)
2924 : : * ((_ extract 7 0) ((_ zero_extend 15) y)))))
2925 : : * (bvmul (_ bv37 13)
2926 : : * ((_ zero_extend 5)
2927 : : * ((_ extract 7 0) ((_ zero_extend 15) z)))))
2928 : : * (bvmul (_ bv170 13)
2929 : : * ((_ zero_extend 5)
2930 : : * ((_ extract 7 0) ((_ zero_extend 15) u)))))
2931 : : * (bvmul (_ bv112 13)
2932 : : * ((_ zero_extend 5)
2933 : : * ((_ extract 7 0) ((_ zero_extend 15) v)))))
2934 : : * (bvmul (_ bv195 13) ((_ zero_extend 5) ((_ extract 15 8) s))))
2935 : : * (bvmul (_ bv124 13) ((_ zero_extend 5) ((_ extract 7 0) s))))
2936 : : * (bvmul (_ bv83 13)
2937 : : * ((_ zero_extend 5) ((_ extract 7 0) ((_ zero_extend 15) w)))))
2938 : : */
2939 : 1 : Node x = bv::utils::mkVar(d_nodeManager.get(), 1);
2940 : 1 : Node y = bv::utils::mkVar(d_nodeManager.get(), 1);
2941 : 1 : Node z = bv::utils::mkVar(d_nodeManager.get(), 1);
2942 : 1 : Node u = bv::utils::mkVar(d_nodeManager.get(), 1);
2943 : 1 : Node v = bv::utils::mkVar(d_nodeManager.get(), 1);
2944 : 1 : Node w = bv::utils::mkVar(d_nodeManager.get(), 1);
2945 : 1 : Node s = bv::utils::mkVar(d_nodeManager.get(), 16);
2946 : :
2947 : : Node zextop5 =
2948 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
2949 : : Node zextop15 =
2950 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(15));
2951 : :
2952 : 2 : Node zext15x = d_nodeManager->mkNode(zextop15, x);
2953 : 2 : Node zext15y = d_nodeManager->mkNode(zextop15, y);
2954 : 2 : Node zext15z = d_nodeManager->mkNode(zextop15, z);
2955 : 2 : Node zext15u = d_nodeManager->mkNode(zextop15, u);
2956 : 2 : Node zext15v = d_nodeManager->mkNode(zextop15, v);
2957 : 2 : Node zext15w = d_nodeManager->mkNode(zextop15, w);
2958 : :
2959 : 1 : Node ext7x = bv::utils::mkExtract(zext15x, 7, 0);
2960 : 1 : Node ext7y = bv::utils::mkExtract(zext15y, 7, 0);
2961 : 1 : Node ext7z = bv::utils::mkExtract(zext15z, 7, 0);
2962 : 1 : Node ext7u = bv::utils::mkExtract(zext15u, 7, 0);
2963 : 1 : Node ext7v = bv::utils::mkExtract(zext15v, 7, 0);
2964 : 1 : Node ext7w = bv::utils::mkExtract(zext15w, 7, 0);
2965 : 1 : Node ext7s = bv::utils::mkExtract(s, 7, 0);
2966 : 1 : Node ext15s = bv::utils::mkExtract(s, 15, 8);
2967 : :
2968 : : Node xx =
2969 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), ext7x);
2970 : : Node yy =
2971 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), ext7y);
2972 : : Node zz =
2973 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), ext7z);
2974 : : Node uu =
2975 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), ext7u);
2976 : : Node vv =
2977 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), ext7v);
2978 : : Node ww =
2979 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), ext7w);
2980 : : Node s7 =
2981 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), ext7s);
2982 : : Node s15 =
2983 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 5), ext15s);
2984 : :
2985 : 1 : Node plus1 = d_nodeManager->mkNode(
2986 : : Kind::BITVECTOR_ADD,
2987 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
2988 : 2 : bv::utils::mkConst(d_nodeManager.get(), 13, 86),
2989 : : xx),
2990 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
2991 : 2 : bv::utils::mkConst(d_nodeManager.get(), 13, 41),
2992 : 6 : yy));
2993 : 1 : Node plus2 = d_nodeManager->mkNode(
2994 : : Kind::BITVECTOR_ADD,
2995 : : plus1,
2996 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
2997 : 2 : bv::utils::mkConst(d_nodeManager.get(), 13, 37),
2998 : 3 : zz));
2999 : 1 : Node plus3 = d_nodeManager->mkNode(
3000 : : Kind::BITVECTOR_ADD,
3001 : : plus2,
3002 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3003 : 2 : bv::utils::mkConst(d_nodeManager.get(), 13, 170),
3004 : 3 : uu));
3005 : 1 : Node plus4 = d_nodeManager->mkNode(
3006 : : Kind::BITVECTOR_ADD,
3007 : : plus3,
3008 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3009 : 2 : bv::utils::mkConst(d_nodeManager.get(), 13, 112),
3010 : 3 : uu));
3011 : 1 : Node plus5 = d_nodeManager->mkNode(
3012 : : Kind::BITVECTOR_ADD,
3013 : : plus4,
3014 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3015 : 2 : bv::utils::mkConst(d_nodeManager.get(), 13, 195),
3016 : 3 : s15));
3017 : 1 : Node plus6 = d_nodeManager->mkNode(
3018 : : Kind::BITVECTOR_ADD,
3019 : : plus5,
3020 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3021 : 2 : bv::utils::mkConst(d_nodeManager.get(), 13, 124),
3022 : 3 : s7));
3023 : 1 : Node plus7 = d_nodeManager->mkNode(
3024 : : Kind::BITVECTOR_ADD,
3025 : : plus6,
3026 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3027 : 2 : bv::utils::mkConst(d_nodeManager.get(), 13, 83),
3028 : 3 : ww));
3029 : :
3030 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 0);
3031 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
3032 : :
3033 : 4 : TEST_F(TestPPWhiteBVGauss, get_min_bw5b)
3034 : : {
3035 : 1 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
3036 : : /* (bvadd
3037 : : * (bvadd
3038 : : * (bvadd
3039 : : * (bvadd
3040 : : * (bvadd
3041 : : * (bvadd
3042 : : * (bvadd (bvmul (_ bv86 20)
3043 : : * ((_ zero_extend 12)
3044 : : * ((_ extract 7 0) ((_ zero_extend 15) x))))
3045 : : * (bvmul (_ bv41 20)
3046 : : * ((_ zero_extend 12)
3047 : : * ((_ extract 7 0) ((_ zero_extend 15) y)))))
3048 : : * (bvmul (_ bv37 20)
3049 : : * ((_ zero_extend 12)
3050 : : * ((_ extract 7 0) ((_ zero_extend 15) z)))))
3051 : : * (bvmul (_ bv170 20)
3052 : : * ((_ zero_extend 12)
3053 : : * ((_ extract 7 0) ((_ zero_extend 15) u)))))
3054 : : * (bvmul (_ bv112 20)
3055 : : * ((_ zero_extend 12)
3056 : : * ((_ extract 7 0) ((_ zero_extend 15) v)))))
3057 : : * (bvmul (_ bv195 20) ((_ zero_extend 12) ((_ extract 15 8) s))))
3058 : : * (bvmul (_ bv124 20) ((_ zero_extend 12) ((_ extract 7 0) s))))
3059 : : * (bvmul (_ bv83 20)
3060 : : * ((_ zero_extend 12) ((_ extract 7 0) ((_ zero_extend 15) w)))))
3061 : : */
3062 : 1 : Node x = bv::utils::mkVar(d_nodeManager.get(), 1);
3063 : 1 : Node y = bv::utils::mkVar(d_nodeManager.get(), 1);
3064 : 1 : Node z = bv::utils::mkVar(d_nodeManager.get(), 1);
3065 : 1 : Node u = bv::utils::mkVar(d_nodeManager.get(), 1);
3066 : 1 : Node v = bv::utils::mkVar(d_nodeManager.get(), 1);
3067 : 1 : Node w = bv::utils::mkVar(d_nodeManager.get(), 1);
3068 : 1 : Node s = bv::utils::mkVar(d_nodeManager.get(), 16);
3069 : :
3070 : : Node zextop15 =
3071 : 1 : d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(15));
3072 : :
3073 : 2 : Node zext15x = d_nodeManager->mkNode(zextop15, x);
3074 : 2 : Node zext15y = d_nodeManager->mkNode(zextop15, y);
3075 : 2 : Node zext15z = d_nodeManager->mkNode(zextop15, z);
3076 : 2 : Node zext15u = d_nodeManager->mkNode(zextop15, u);
3077 : 2 : Node zext15v = d_nodeManager->mkNode(zextop15, v);
3078 : 2 : Node zext15w = d_nodeManager->mkNode(zextop15, w);
3079 : :
3080 : 1 : Node ext7x = bv::utils::mkExtract(zext15x, 7, 0);
3081 : 1 : Node ext7y = bv::utils::mkExtract(zext15y, 7, 0);
3082 : 1 : Node ext7z = bv::utils::mkExtract(zext15z, 7, 0);
3083 : 1 : Node ext7u = bv::utils::mkExtract(zext15u, 7, 0);
3084 : 1 : Node ext7v = bv::utils::mkExtract(zext15v, 7, 0);
3085 : 1 : Node ext7w = bv::utils::mkExtract(zext15w, 7, 0);
3086 : 1 : Node ext7s = bv::utils::mkExtract(s, 7, 0);
3087 : 1 : Node ext15s = bv::utils::mkExtract(s, 15, 8);
3088 : :
3089 : : Node xx =
3090 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 12), ext7x);
3091 : : Node yy =
3092 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 12), ext7y);
3093 : : Node zz =
3094 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 12), ext7z);
3095 : : Node uu =
3096 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 12), ext7u);
3097 : : Node vv =
3098 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 12), ext7v);
3099 : : Node ww =
3100 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 12), ext7w);
3101 : : Node s7 =
3102 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 12), ext7s);
3103 : : Node s15 =
3104 : 2 : bv::utils::mkConcat(bv::utils::mkZero(d_nodeManager.get(), 12), ext15s);
3105 : :
3106 : 1 : Node plus1 = d_nodeManager->mkNode(
3107 : : Kind::BITVECTOR_ADD,
3108 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3109 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 86),
3110 : : xx),
3111 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3112 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 41),
3113 : 6 : yy));
3114 : 1 : Node plus2 = d_nodeManager->mkNode(
3115 : : Kind::BITVECTOR_ADD,
3116 : : plus1,
3117 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3118 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 37),
3119 : 3 : zz));
3120 : 1 : Node plus3 = d_nodeManager->mkNode(
3121 : : Kind::BITVECTOR_ADD,
3122 : : plus2,
3123 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3124 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 170),
3125 : 3 : uu));
3126 : 1 : Node plus4 = d_nodeManager->mkNode(
3127 : : Kind::BITVECTOR_ADD,
3128 : : plus3,
3129 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3130 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 112),
3131 : 3 : uu));
3132 : 1 : Node plus5 = d_nodeManager->mkNode(
3133 : : Kind::BITVECTOR_ADD,
3134 : : plus4,
3135 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3136 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 195),
3137 : 3 : s15));
3138 : 1 : Node plus6 = d_nodeManager->mkNode(
3139 : : Kind::BITVECTOR_ADD,
3140 : : plus5,
3141 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3142 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 124),
3143 : 3 : s7));
3144 : 1 : Node plus7 = d_nodeManager->mkNode(
3145 : : Kind::BITVECTOR_ADD,
3146 : : plus6,
3147 : 1 : d_nodeManager->mkNode(Kind::BITVECTOR_MULT,
3148 : 2 : bv::utils::mkConst(d_nodeManager.get(), 20, 83),
3149 : 3 : ww));
3150 : :
3151 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 19);
3152 [ - + ][ + - ]: 1 : ASSERT_EQ(d_bv_gauss->getMinBwExpr(rr->rewrite(plus7)), 17);
3153 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
3154 : : } // namespace test
3155 : : } // namespace cvc5::internal
|
