1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Mathias Preiner, Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Unit tests for BvInstantiator. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <iostream> |
17 |
|
#include <vector> |
18 |
|
|
19 |
|
#include "expr/node.h" |
20 |
|
#include "test_smt.h" |
21 |
|
#include "theory/bv/theory_bv_utils.h" |
22 |
|
#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h" |
23 |
|
#include "theory/rewriter.h" |
24 |
|
#include "util/bitvector.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
|
28 |
|
using namespace theory; |
29 |
|
using namespace theory::bv; |
30 |
|
using namespace theory::bv::utils; |
31 |
|
using namespace theory::quantifiers; |
32 |
|
using namespace theory::quantifiers::utils; |
33 |
|
|
34 |
|
namespace test { |
35 |
|
|
36 |
16 |
class TestTheoryWhiteyQuantifiersBvInstantiator : public TestSmt |
37 |
|
{ |
38 |
|
protected: |
39 |
62 |
Node mkNeg(TNode n) { return d_nodeManager->mkNode(kind::BITVECTOR_NEG, n); } |
40 |
|
|
41 |
12 |
Node mkMult(TNode a, TNode b) |
42 |
|
{ |
43 |
12 |
return d_nodeManager->mkNode(kind::BITVECTOR_MULT, a, b); |
44 |
|
} |
45 |
|
|
46 |
4 |
Node mkMult(const std::vector<Node>& children) |
47 |
|
{ |
48 |
4 |
return d_nodeManager->mkNode(kind::BITVECTOR_MULT, children); |
49 |
|
} |
50 |
|
|
51 |
20 |
Node mkPlus(TNode a, TNode b) |
52 |
|
{ |
53 |
20 |
return d_nodeManager->mkNode(kind::BITVECTOR_ADD, a, b); |
54 |
|
} |
55 |
|
|
56 |
4 |
Node mkPlus(const std::vector<Node>& children) |
57 |
|
{ |
58 |
4 |
return d_nodeManager->mkNode(kind::BITVECTOR_ADD, children); |
59 |
|
} |
60 |
|
}; |
61 |
|
|
62 |
|
/** |
63 |
|
* getPvCoeff(x, n) should return |
64 |
|
* |
65 |
|
* 1 if n == x |
66 |
|
* -1 if n == -x |
67 |
|
* a if n == x * a |
68 |
|
* -a if n == x * -a |
69 |
|
* Node::null() otherwise. |
70 |
|
* |
71 |
|
* Note that x * a and x * -a have to be normalized. |
72 |
|
*/ |
73 |
13 |
TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, getPvCoeff) |
74 |
|
{ |
75 |
4 |
Node x = mkVar(32); |
76 |
4 |
Node a = mkVar(32); |
77 |
4 |
Node one = mkOne(32); |
78 |
|
BvLinearAttribute is_linear; |
79 |
|
|
80 |
|
/* x -> 1 */ |
81 |
4 |
Node coeff_x = getPvCoeff(x, x); |
82 |
2 |
ASSERT_EQ(coeff_x, one); |
83 |
|
|
84 |
|
/* -x -> -1 */ |
85 |
4 |
Node coeff_neg_x = getPvCoeff(x, mkNeg(x)); |
86 |
2 |
ASSERT_EQ(coeff_neg_x, mkNeg(one)); |
87 |
|
|
88 |
|
/* x * a -> null (since x * a not a normalized) */ |
89 |
4 |
Node x_mult_a = mkMult(x, a); |
90 |
4 |
Node coeff_x_mult_a = getPvCoeff(x, x_mult_a); |
91 |
2 |
ASSERT_TRUE(coeff_x_mult_a.isNull()); |
92 |
|
|
93 |
|
/* x * a -> a */ |
94 |
2 |
x_mult_a.setAttribute(is_linear, true); |
95 |
2 |
coeff_x_mult_a = getPvCoeff(x, x_mult_a); |
96 |
2 |
ASSERT_EQ(coeff_x_mult_a, a); |
97 |
|
|
98 |
|
/* x * -a -> -a */ |
99 |
4 |
Node x_mult_neg_a = mkMult(x, mkNeg(a)); |
100 |
2 |
x_mult_neg_a.setAttribute(is_linear, true); |
101 |
4 |
Node coeff_x_mult_neg_a = getPvCoeff(x, x_mult_neg_a); |
102 |
2 |
ASSERT_EQ(coeff_x_mult_neg_a, mkNeg(a)); |
103 |
|
} |
104 |
|
|
105 |
13 |
TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult) |
106 |
|
{ |
107 |
4 |
Node x = mkVar(32); |
108 |
4 |
Node neg_x = mkNeg(x); |
109 |
4 |
Node a = mkVar(32); |
110 |
4 |
Node b = mkVar(32); |
111 |
4 |
Node c = mkVar(32); |
112 |
4 |
Node d = mkVar(32); |
113 |
4 |
Node zero = mkZero(32); |
114 |
4 |
Node one = mkOne(32); |
115 |
|
BvLinearAttribute is_linear; |
116 |
4 |
std::unordered_map<Node, bool> contains_x; |
117 |
|
|
118 |
2 |
contains_x[x] = true; |
119 |
2 |
contains_x[neg_x] = true; |
120 |
|
|
121 |
|
/* x * -x -> null (since non linear) */ |
122 |
4 |
Node norm_xx = normalizePvMult(x, {x, neg_x}, contains_x); |
123 |
2 |
ASSERT_TRUE(norm_xx.isNull()); |
124 |
|
|
125 |
|
/* nothing to normalize -> create a * a */ |
126 |
4 |
Node norm_aa = normalizePvMult(x, {a, a}, contains_x); |
127 |
2 |
ASSERT_EQ(norm_aa, Rewriter::rewrite(mkMult(a, a))); |
128 |
|
|
129 |
|
/* normalize x * a -> x * a */ |
130 |
4 |
Node norm_xa = normalizePvMult(x, {x, a}, contains_x); |
131 |
2 |
ASSERT_TRUE(contains_x[norm_xa]); |
132 |
2 |
ASSERT_TRUE(norm_xa.getAttribute(is_linear)); |
133 |
2 |
ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_MULT); |
134 |
2 |
ASSERT_EQ(norm_xa.getNumChildren(), 2); |
135 |
2 |
ASSERT_EQ(norm_xa[0], x); |
136 |
2 |
ASSERT_EQ(norm_xa[1], a); |
137 |
|
|
138 |
|
/* normalize a * x -> x * a */ |
139 |
4 |
Node norm_ax = normalizePvMult(x, {a, x}, contains_x); |
140 |
2 |
ASSERT_TRUE(contains_x[norm_ax]); |
141 |
2 |
ASSERT_TRUE(norm_ax.getAttribute(is_linear)); |
142 |
2 |
ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_MULT); |
143 |
2 |
ASSERT_EQ(norm_ax.getNumChildren(), 2); |
144 |
2 |
ASSERT_EQ(norm_ax[0], x); |
145 |
2 |
ASSERT_EQ(norm_ax[1], a); |
146 |
|
|
147 |
|
/* normalize a * -x -> x * -a */ |
148 |
4 |
Node norm_neg_ax = normalizePvMult(x, {a, neg_x}, contains_x); |
149 |
2 |
ASSERT_TRUE(contains_x[norm_neg_ax]); |
150 |
2 |
ASSERT_TRUE(norm_neg_ax.getAttribute(is_linear)); |
151 |
2 |
ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_MULT); |
152 |
2 |
ASSERT_EQ(norm_neg_ax.getNumChildren(), 2); |
153 |
2 |
ASSERT_EQ(norm_neg_ax[0], x); |
154 |
2 |
ASSERT_EQ(norm_neg_ax[1], mkNeg(a)); |
155 |
|
|
156 |
|
/* normalize 0 * x -> 0 */ |
157 |
4 |
Node norm_zx = normalizePvMult(x, {zero, x}, contains_x); |
158 |
2 |
ASSERT_EQ(norm_zx, zero); |
159 |
|
|
160 |
|
/* normalize 1 * x -> x */ |
161 |
4 |
Node norm_ox = normalizePvMult(x, {one, x}, contains_x); |
162 |
2 |
ASSERT_EQ(norm_ox, x); |
163 |
|
|
164 |
|
/* normalize a * b * c * x * d -> x * (a * b * c * d) */ |
165 |
4 |
Node norm_abcxd = normalizePvMult(x, {a, b, c, x, d}, contains_x); |
166 |
2 |
ASSERT_TRUE(contains_x[norm_abcxd]); |
167 |
2 |
ASSERT_TRUE(norm_abcxd.getAttribute(is_linear)); |
168 |
2 |
ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_MULT); |
169 |
2 |
ASSERT_EQ(norm_abcxd.getNumChildren(), 2); |
170 |
2 |
ASSERT_EQ(norm_abcxd[0], x); |
171 |
2 |
ASSERT_EQ(norm_abcxd[1], Rewriter::rewrite(mkMult({a, b, c, d}))); |
172 |
|
|
173 |
|
/* normalize a * b * c * -x * d -> x * -(a * b * c * d) */ |
174 |
4 |
Node norm_neg_abcxd = normalizePvMult(x, {a, b, c, neg_x, d}, contains_x); |
175 |
2 |
ASSERT_TRUE(contains_x[norm_neg_abcxd]); |
176 |
2 |
ASSERT_TRUE(norm_neg_abcxd.getAttribute(is_linear)); |
177 |
2 |
ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_MULT); |
178 |
2 |
ASSERT_EQ(norm_neg_abcxd.getNumChildren(), 2); |
179 |
2 |
ASSERT_EQ(norm_neg_abcxd[0], x); |
180 |
2 |
ASSERT_TRUE(norm_neg_abcxd[1] |
181 |
2 |
== mkNeg(Rewriter::rewrite(mkMult({a, b, c, d})))); |
182 |
|
|
183 |
|
/* normalize b * (x * a) -> x * (b * a) */ |
184 |
4 |
Node norm_bxa = normalizePvMult(x, {b, norm_ax}, contains_x); |
185 |
2 |
ASSERT_TRUE(contains_x[norm_bxa]); |
186 |
2 |
ASSERT_TRUE(norm_bxa.getAttribute(is_linear)); |
187 |
2 |
ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_MULT); |
188 |
2 |
ASSERT_EQ(norm_bxa.getNumChildren(), 2); |
189 |
2 |
ASSERT_EQ(norm_bxa[0], x); |
190 |
2 |
ASSERT_EQ(norm_bxa[1], Rewriter::rewrite(mkMult(b, a))); |
191 |
|
|
192 |
|
/* normalize b * -(x * a) -> x * -(a * b) */ |
193 |
4 |
Node neg_norm_ax = mkNeg(norm_ax); |
194 |
2 |
contains_x[neg_norm_ax] = true; |
195 |
4 |
Node norm_neg_bxa = normalizePvMult(x, {b, neg_norm_ax}, contains_x); |
196 |
2 |
ASSERT_TRUE(contains_x[norm_neg_bxa]); |
197 |
2 |
ASSERT_TRUE(norm_neg_bxa.getAttribute(is_linear)); |
198 |
2 |
ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_MULT); |
199 |
2 |
ASSERT_EQ(norm_neg_bxa.getNumChildren(), 2); |
200 |
2 |
ASSERT_EQ(norm_neg_bxa[0], x); |
201 |
2 |
ASSERT_EQ(norm_neg_bxa[1], mkNeg(Rewriter::rewrite(mkMult(b, a)))); |
202 |
|
} |
203 |
|
|
204 |
13 |
TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) |
205 |
|
{ |
206 |
4 |
Node one = mkOne(32); |
207 |
4 |
Node x = mkVar(32); |
208 |
4 |
Node neg_x = mkNeg(x); |
209 |
4 |
Node a = mkVar(32); |
210 |
4 |
Node b = mkVar(32); |
211 |
4 |
Node c = mkVar(32); |
212 |
4 |
Node d = mkVar(32); |
213 |
|
BvLinearAttribute is_linear; |
214 |
4 |
std::unordered_map<Node, bool> contains_x; |
215 |
|
|
216 |
2 |
contains_x[x] = true; |
217 |
2 |
contains_x[neg_x] = true; |
218 |
|
|
219 |
|
/* a + b * x -> null (since b * x not normalized) */ |
220 |
4 |
Node mult_bx = mkMult(b, x); |
221 |
2 |
contains_x[mult_bx] = true; |
222 |
4 |
Node norm_abx = normalizePvPlus(x, {a, mult_bx}, contains_x); |
223 |
2 |
ASSERT_TRUE(norm_abx.isNull()); |
224 |
|
|
225 |
|
/* nothing to normalize -> create a + a */ |
226 |
4 |
Node norm_aa = normalizePvPlus(x, {a, a}, contains_x); |
227 |
2 |
ASSERT_EQ(norm_aa, Rewriter::rewrite(mkPlus(a, a))); |
228 |
|
|
229 |
|
/* x + a -> x + a */ |
230 |
4 |
Node norm_xa = normalizePvPlus(x, {x, a}, contains_x); |
231 |
2 |
ASSERT_TRUE(contains_x[norm_xa]); |
232 |
2 |
ASSERT_TRUE(norm_xa.getAttribute(is_linear)); |
233 |
2 |
ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_ADD); |
234 |
2 |
ASSERT_EQ(norm_xa.getNumChildren(), 2); |
235 |
2 |
ASSERT_EQ(norm_xa[0], x); |
236 |
2 |
ASSERT_EQ(norm_xa[1], a); |
237 |
|
|
238 |
|
/* a * x -> x * a */ |
239 |
4 |
Node norm_ax = normalizePvPlus(x, {a, x}, contains_x); |
240 |
2 |
ASSERT_TRUE(contains_x[norm_ax]); |
241 |
2 |
ASSERT_TRUE(norm_ax.getAttribute(is_linear)); |
242 |
2 |
ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_ADD); |
243 |
2 |
ASSERT_EQ(norm_ax.getNumChildren(), 2); |
244 |
2 |
ASSERT_EQ(norm_ax[0], x); |
245 |
2 |
ASSERT_EQ(norm_ax[1], a); |
246 |
|
|
247 |
|
/* a + -x -> (x * -1) + a */ |
248 |
4 |
Node norm_neg_ax = normalizePvPlus(x, {a, neg_x}, contains_x); |
249 |
2 |
ASSERT_TRUE(contains_x[norm_neg_ax]); |
250 |
2 |
ASSERT_TRUE(norm_neg_ax.getAttribute(is_linear)); |
251 |
2 |
ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_ADD); |
252 |
2 |
ASSERT_EQ(norm_neg_ax.getNumChildren(), 2); |
253 |
2 |
ASSERT_EQ(norm_neg_ax[0].getKind(), kind::BITVECTOR_MULT); |
254 |
2 |
ASSERT_EQ(norm_neg_ax[0].getNumChildren(), 2); |
255 |
2 |
ASSERT_TRUE(norm_neg_ax[0].getAttribute(is_linear)); |
256 |
2 |
ASSERT_TRUE(contains_x[norm_neg_ax[0]]); |
257 |
2 |
ASSERT_EQ(norm_neg_ax[0][0], x); |
258 |
2 |
ASSERT_EQ(norm_neg_ax[0][1], Rewriter::rewrite(mkNeg(one))); |
259 |
2 |
ASSERT_EQ(norm_neg_ax[1], a); |
260 |
|
|
261 |
|
/* -x + -a * x -> x * (-1 - a) */ |
262 |
|
Node norm_xax = normalizePvPlus( |
263 |
4 |
x, {mkNeg(x), normalizePvMult(x, {mkNeg(a), x}, contains_x)}, contains_x); |
264 |
2 |
ASSERT_TRUE(contains_x[norm_xax]); |
265 |
2 |
ASSERT_TRUE(norm_xax.getAttribute(is_linear)); |
266 |
2 |
ASSERT_EQ(norm_xax.getKind(), kind::BITVECTOR_MULT); |
267 |
2 |
ASSERT_EQ(norm_xax.getNumChildren(), 2); |
268 |
2 |
ASSERT_EQ(norm_xax[0], x); |
269 |
2 |
ASSERT_EQ(norm_xax[1], Rewriter::rewrite(mkPlus(mkNeg(one), mkNeg(a)))); |
270 |
|
|
271 |
|
/* a + b + c + x + d -> x + (a + b + c + d) */ |
272 |
4 |
Node norm_abcxd = normalizePvPlus(x, {a, b, c, x, d}, contains_x); |
273 |
2 |
ASSERT_TRUE(contains_x[norm_abcxd]); |
274 |
2 |
ASSERT_TRUE(norm_abcxd.getAttribute(is_linear)); |
275 |
2 |
ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_ADD); |
276 |
2 |
ASSERT_EQ(norm_abcxd.getNumChildren(), 2); |
277 |
2 |
ASSERT_EQ(norm_abcxd[0], x); |
278 |
2 |
ASSERT_EQ(norm_abcxd[1], Rewriter::rewrite(mkPlus({a, b, c, d}))); |
279 |
|
|
280 |
|
/* a + b + c + -x + d -> (x * -1) + (a + b + c + d) */ |
281 |
4 |
Node norm_neg_abcxd = normalizePvPlus(x, {a, b, c, neg_x, d}, contains_x); |
282 |
2 |
ASSERT_TRUE(contains_x[norm_neg_abcxd]); |
283 |
2 |
ASSERT_TRUE(norm_neg_abcxd.getAttribute(is_linear)); |
284 |
2 |
ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_ADD); |
285 |
2 |
ASSERT_EQ(norm_neg_abcxd.getNumChildren(), 2); |
286 |
2 |
ASSERT_EQ(norm_neg_abcxd[0].getKind(), kind::BITVECTOR_MULT); |
287 |
2 |
ASSERT_EQ(norm_neg_abcxd[0].getNumChildren(), 2); |
288 |
2 |
ASSERT_TRUE(norm_neg_abcxd[0].getAttribute(is_linear)); |
289 |
2 |
ASSERT_TRUE(contains_x[norm_neg_abcxd[0]]); |
290 |
2 |
ASSERT_EQ(norm_neg_abcxd[0][0], x); |
291 |
2 |
ASSERT_EQ(norm_neg_abcxd[0][1], Rewriter::rewrite(mkNeg(one))); |
292 |
2 |
ASSERT_EQ(norm_neg_abcxd[1], Rewriter::rewrite(mkPlus({a, b, c, d}))); |
293 |
|
|
294 |
|
/* b + (x + a) -> x + (b + a) */ |
295 |
4 |
Node norm_bxa = normalizePvPlus(x, {b, norm_ax}, contains_x); |
296 |
2 |
ASSERT_TRUE(contains_x[norm_bxa]); |
297 |
2 |
ASSERT_TRUE(norm_bxa.getAttribute(is_linear)); |
298 |
2 |
ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_ADD); |
299 |
2 |
ASSERT_EQ(norm_bxa.getNumChildren(), 2); |
300 |
2 |
ASSERT_EQ(norm_bxa[0], x); |
301 |
2 |
ASSERT_EQ(norm_bxa[1], Rewriter::rewrite(mkPlus(b, a))); |
302 |
|
|
303 |
|
/* b + -(x + a) -> (x * -1) + b - a */ |
304 |
4 |
Node neg_norm_ax = mkNeg(norm_ax); |
305 |
2 |
contains_x[neg_norm_ax] = true; |
306 |
4 |
Node norm_neg_bxa = normalizePvPlus(x, {b, neg_norm_ax}, contains_x); |
307 |
2 |
ASSERT_TRUE(contains_x[norm_neg_bxa]); |
308 |
2 |
ASSERT_TRUE(norm_neg_bxa.getAttribute(is_linear)); |
309 |
2 |
ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_ADD); |
310 |
2 |
ASSERT_EQ(norm_neg_bxa.getNumChildren(), 2); |
311 |
2 |
ASSERT_EQ(norm_neg_abcxd[0].getKind(), kind::BITVECTOR_MULT); |
312 |
2 |
ASSERT_EQ(norm_neg_abcxd[0].getNumChildren(), 2); |
313 |
2 |
ASSERT_TRUE(norm_neg_abcxd[0].getAttribute(is_linear)); |
314 |
2 |
ASSERT_TRUE(contains_x[norm_neg_abcxd[0]]); |
315 |
2 |
ASSERT_EQ(norm_neg_abcxd[0][0], x); |
316 |
2 |
ASSERT_EQ(norm_neg_abcxd[0][1], Rewriter::rewrite(mkNeg(one))); |
317 |
2 |
ASSERT_EQ(norm_neg_bxa[1], Rewriter::rewrite((mkPlus(b, mkNeg(a))))); |
318 |
|
|
319 |
|
/* -x + x + a -> a */ |
320 |
4 |
Node norm_neg_xxa = normalizePvPlus(x, {neg_x, x, a}, contains_x); |
321 |
2 |
ASSERT_FALSE(contains_x[norm_neg_xxa]); |
322 |
2 |
ASSERT_EQ(norm_neg_xxa, a); |
323 |
|
} |
324 |
|
|
325 |
13 |
TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual) |
326 |
|
{ |
327 |
4 |
Node x = mkVar(32); |
328 |
4 |
Node neg_x = mkNeg(x); |
329 |
4 |
Node a = mkVar(32); |
330 |
4 |
Node b = mkVar(32); |
331 |
4 |
Node c = mkVar(32); |
332 |
4 |
Node d = mkVar(32); |
333 |
4 |
Node zero = mkZero(32); |
334 |
4 |
Node one = mkOne(32); |
335 |
4 |
Node ntrue = mkTrue(); |
336 |
|
BvLinearAttribute is_linear; |
337 |
4 |
std::unordered_map<Node, bool> contains_x; |
338 |
|
|
339 |
2 |
contains_x[x] = true; |
340 |
2 |
contains_x[neg_x] = true; |
341 |
|
|
342 |
|
/* x = a -> null (nothing to normalize) */ |
343 |
4 |
Node norm_xa = normalizePvEqual(x, {x, a}, contains_x); |
344 |
2 |
ASSERT_TRUE(norm_xa.isNull()); |
345 |
|
|
346 |
|
/* x = x -> true */ |
347 |
4 |
Node norm_xx = normalizePvEqual(x, {x, x}, contains_x); |
348 |
2 |
ASSERT_EQ(norm_xx, ntrue); |
349 |
|
|
350 |
|
/* x = -x -> x * 2 = 0 */ |
351 |
4 |
Node norm_neg_xx = normalizePvEqual(x, {x, neg_x}, contains_x); |
352 |
2 |
ASSERT_EQ(norm_neg_xx.getKind(), kind::EQUAL); |
353 |
2 |
ASSERT_EQ(norm_neg_xx[0].getKind(), kind::BITVECTOR_MULT); |
354 |
2 |
ASSERT_EQ(norm_neg_xx[0].getNumChildren(), 2); |
355 |
2 |
ASSERT_TRUE(norm_neg_xx[0].getAttribute(is_linear)); |
356 |
2 |
ASSERT_TRUE(contains_x[norm_neg_xx[0]]); |
357 |
2 |
ASSERT_EQ(norm_neg_xx[0][0], x); |
358 |
2 |
ASSERT_EQ(norm_neg_xx[0][1], Rewriter::rewrite(mkConst(32, 2))); |
359 |
2 |
ASSERT_EQ(norm_neg_xx[1], zero); |
360 |
|
|
361 |
|
/* a + x = x -> 0 = -a */ |
362 |
|
Node norm_axx = normalizePvEqual( |
363 |
4 |
x, {normalizePvPlus(x, {a, x}, contains_x), x}, contains_x); |
364 |
2 |
ASSERT_EQ(norm_axx.getKind(), kind::EQUAL); |
365 |
2 |
ASSERT_EQ(norm_axx[0], zero); |
366 |
2 |
ASSERT_EQ(norm_axx[1], mkNeg(a)); |
367 |
|
|
368 |
|
/* a + -x = x -> x * -2 = a */ |
369 |
|
Node norm_neg_axx = normalizePvEqual( |
370 |
4 |
x, {normalizePvPlus(x, {a, neg_x}, contains_x), x}, contains_x); |
371 |
2 |
ASSERT_EQ(norm_neg_axx.getKind(), kind::EQUAL); |
372 |
2 |
ASSERT_EQ(norm_neg_axx[0].getKind(), kind::BITVECTOR_MULT); |
373 |
2 |
ASSERT_EQ(norm_neg_axx[0].getNumChildren(), 2); |
374 |
2 |
ASSERT_TRUE(norm_neg_axx[0].getAttribute(is_linear)); |
375 |
2 |
ASSERT_TRUE(contains_x[norm_neg_axx[0]]); |
376 |
2 |
ASSERT_EQ(norm_neg_axx[0][0], x); |
377 |
2 |
ASSERT_EQ(norm_neg_axx[0][1], Rewriter::rewrite(mkNeg(mkConst(32, 2)))); |
378 |
2 |
ASSERT_EQ(norm_neg_axx[1], mkNeg(a)); |
379 |
|
|
380 |
|
/* a * x = x -> x * (a - 1) = 0 */ |
381 |
|
Node norm_mult_axx = normalizePvEqual( |
382 |
4 |
x, {normalizePvMult(x, {a, x}, contains_x), x}, contains_x); |
383 |
2 |
ASSERT_EQ(norm_mult_axx.getKind(), kind::EQUAL); |
384 |
2 |
ASSERT_EQ(norm_mult_axx[0].getKind(), kind::BITVECTOR_MULT); |
385 |
2 |
ASSERT_EQ(norm_mult_axx[0].getNumChildren(), 2); |
386 |
2 |
ASSERT_TRUE(norm_mult_axx[0].getAttribute(is_linear)); |
387 |
2 |
ASSERT_TRUE(contains_x[norm_mult_axx[0]]); |
388 |
2 |
ASSERT_EQ(norm_mult_axx[0][0], x); |
389 |
2 |
ASSERT_EQ(norm_mult_axx[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one)))); |
390 |
2 |
ASSERT_EQ(norm_mult_axx[1], zero); |
391 |
|
|
392 |
|
/* a * x = x + b -> x * (a - 1) = b */ |
393 |
|
Node norm_axxb = normalizePvEqual(x, |
394 |
4 |
{normalizePvMult(x, {a, x}, contains_x), |
395 |
4 |
normalizePvPlus(x, {b, x}, contains_x)}, |
396 |
8 |
contains_x); |
397 |
2 |
ASSERT_EQ(norm_axxb.getKind(), kind::EQUAL); |
398 |
2 |
ASSERT_EQ(norm_axxb[0].getKind(), kind::BITVECTOR_MULT); |
399 |
2 |
ASSERT_EQ(norm_axxb[0].getNumChildren(), 2); |
400 |
2 |
ASSERT_TRUE(norm_axxb[0].getAttribute(is_linear)); |
401 |
2 |
ASSERT_TRUE(contains_x[norm_axxb[0]]); |
402 |
2 |
ASSERT_EQ(norm_axxb[0][0], x); |
403 |
2 |
ASSERT_EQ(norm_axxb[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one)))); |
404 |
2 |
ASSERT_EQ(norm_axxb[1], b); |
405 |
|
|
406 |
|
/* a * x + c = x -> x * (a - 1) = -c */ |
407 |
|
Node norm_axcx = normalizePvEqual( |
408 |
|
x, |
409 |
|
{normalizePvPlus( |
410 |
8 |
x, {normalizePvMult(x, {a, x}, contains_x), c}, contains_x), |
411 |
|
x}, |
412 |
8 |
contains_x); |
413 |
2 |
ASSERT_EQ(norm_axcx.getKind(), kind::EQUAL); |
414 |
2 |
ASSERT_EQ(norm_axcx[0].getKind(), kind::BITVECTOR_MULT); |
415 |
2 |
ASSERT_EQ(norm_axcx[0].getNumChildren(), 2); |
416 |
2 |
ASSERT_TRUE(norm_axcx[0].getAttribute(is_linear)); |
417 |
2 |
ASSERT_TRUE(contains_x[norm_axcx[0]]); |
418 |
2 |
ASSERT_EQ(norm_axcx[0][0], x); |
419 |
2 |
ASSERT_EQ(norm_axcx[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one)))); |
420 |
2 |
ASSERT_EQ(norm_axcx[1], mkNeg(c)); |
421 |
|
|
422 |
|
/* a * x + c = x + b -> x * (a - 1) = b - c*/ |
423 |
|
Node norm_axcxb = normalizePvEqual( |
424 |
|
x, |
425 |
|
{normalizePvPlus( |
426 |
8 |
x, {normalizePvMult(x, {a, x}, contains_x), c}, contains_x), |
427 |
4 |
normalizePvPlus(x, {b, x}, contains_x)}, |
428 |
10 |
contains_x); |
429 |
2 |
ASSERT_EQ(norm_axcxb.getKind(), kind::EQUAL); |
430 |
2 |
ASSERT_EQ(norm_axcxb[0].getKind(), kind::BITVECTOR_MULT); |
431 |
2 |
ASSERT_EQ(norm_axcxb[0].getNumChildren(), 2); |
432 |
2 |
ASSERT_TRUE(norm_axcxb[0].getAttribute(is_linear)); |
433 |
2 |
ASSERT_TRUE(contains_x[norm_axcxb[0]]); |
434 |
2 |
ASSERT_EQ(norm_axcxb[0][0], x); |
435 |
2 |
ASSERT_EQ(norm_axcxb[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one)))); |
436 |
2 |
ASSERT_EQ(norm_axcxb[1], Rewriter::rewrite(mkPlus(b, mkNeg(c)))); |
437 |
|
|
438 |
|
/* -(a + -x) = a * x -> x * (1 - a) = a */ |
439 |
|
Node norm_axax = |
440 |
|
normalizePvEqual(x, |
441 |
4 |
{mkNeg(normalizePvPlus(x, {a, neg_x}, contains_x)), |
442 |
4 |
normalizePvMult(x, {a, x}, contains_x)}, |
443 |
8 |
contains_x); |
444 |
2 |
ASSERT_EQ(norm_axax.getKind(), kind::EQUAL); |
445 |
2 |
ASSERT_EQ(norm_axax[0].getKind(), kind::BITVECTOR_MULT); |
446 |
2 |
ASSERT_EQ(norm_axax[0].getNumChildren(), 2); |
447 |
2 |
ASSERT_TRUE(norm_axax[0].getAttribute(is_linear)); |
448 |
2 |
ASSERT_TRUE(contains_x[norm_axax[0]]); |
449 |
2 |
ASSERT_EQ(norm_axax[0][0], x); |
450 |
2 |
ASSERT_EQ(norm_axax[0][1], Rewriter::rewrite(mkPlus(one, mkNeg(a)))); |
451 |
2 |
ASSERT_EQ(norm_axax[1], a); |
452 |
|
} |
453 |
|
} // namespace test |
454 |
89701 |
} // namespace cvc5 |