GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp Lines: 285 285 100.0 %
Date: 2021-03-22 Branches: 1398 4228 33.1 %

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