GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_bags_rewriter_white.cpp Lines: 432 432 100.0 %
Date: 2021-03-22 Branches: 1347 3250 41.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bags_rewriter_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Mudathir Mohamed
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 White box testing of bags rewriter
13
 **/
14
15
#include "expr/dtype.h"
16
#include "test_smt.h"
17
#include "theory/bags/bags_rewriter.h"
18
#include "theory/strings/type_enumerator.h"
19
20
namespace CVC4 {
21
22
using namespace theory;
23
using namespace kind;
24
using namespace theory::bags;
25
26
namespace test {
27
28
typedef expr::Attribute<Node, Node> attribute;
29
30
64
class TestTheoryWhiteBagsRewriter : public TestSmt
31
{
32
 protected:
33
32
  void SetUp() override
34
  {
35
32
    TestSmt::SetUp();
36
32
    d_rewriter.reset(new BagsRewriter(nullptr));
37
32
  }
38
39
16
  std::vector<Node> getNStrings(size_t n)
40
  {
41
16
    std::vector<Node> elements(n);
42
48
    for (size_t i = 0; i < n; i++)
43
    {
44
32
      elements[i] = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
45
    }
46
16
    return elements;
47
  }
48
49
  std::unique_ptr<BagsRewriter> d_rewriter;
50
};
51
52
25
TEST_F(TestTheoryWhiteBagsRewriter, empty_bag_normal_form)
53
{
54
4
  Node emptybag = d_nodeManager->mkConst(EmptyBag(d_nodeManager->stringType()));
55
  // empty bags are in normal form
56
2
  ASSERT_TRUE(emptybag.isConst());
57
4
  RewriteResponse response = d_rewriter->postRewrite(emptybag);
58
2
  ASSERT_TRUE(emptybag == response.d_node && response.d_status == REWRITE_DONE);
59
}
60
61
25
TEST_F(TestTheoryWhiteBagsRewriter, bag_equality)
62
{
63
4
  std::vector<Node> elements = getNStrings(2);
64
4
  Node x = elements[0];
65
4
  Node y = elements[1];
66
4
  Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType());
67
4
  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->integerType());
68
4
  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
69
4
  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), y, d);
70
  Node emptyBag = d_nodeManager->mkConst(
71
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
72
4
  Node emptyString = d_nodeManager->mkConst(String(""));
73
4
  Node constantBag = d_nodeManager->mkBag(d_nodeManager->stringType(),
74
                                          emptyString,
75
8
                                          d_nodeManager->mkConst(Rational(1)));
76
77
  // (= A A) = true where A is a bag
78
4
  Node n1 = A.eqNode(A);
79
4
  RewriteResponse response1 = d_rewriter->preRewrite(n1);
80
2
  ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(true)
81
2
              && response1.d_status == REWRITE_AGAIN_FULL);
82
83
  // (= A B) = false if A and B are different bag constants
84
4
  Node n2 = constantBag.eqNode(emptyBag);
85
4
  RewriteResponse response2 = d_rewriter->postRewrite(n2);
86
2
  ASSERT_TRUE(response2.d_node == d_nodeManager->mkConst(false)
87
2
              && response2.d_status == REWRITE_AGAIN_FULL);
88
89
  // (= B A) = (= A B) if A < B and at least one of A or B is not a constant
90
4
  Node n3 = B.eqNode(A);
91
4
  RewriteResponse response3 = d_rewriter->postRewrite(n3);
92
2
  ASSERT_TRUE(response3.d_node == A.eqNode(B)
93
2
              && response3.d_status == REWRITE_AGAIN_FULL);
94
95
  // (= A B) = (= A B) no rewrite
96
4
  Node n4 = A.eqNode(B);
97
4
  RewriteResponse response4 = d_rewriter->postRewrite(n4);
98
2
  ASSERT_TRUE(response4.d_node == n4 && response4.d_status == REWRITE_DONE);
99
}
100
101
25
TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element)
102
{
103
4
  std::vector<Node> elements = getNStrings(1);
104
4
  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
105
2
                                       elements[0],
106
10
                                       d_nodeManager->mkConst(Rational(-1)));
107
4
  Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
108
2
                                   elements[0],
109
10
                                   d_nodeManager->mkConst(Rational(0)));
110
4
  Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
111
2
                                       elements[0],
112
10
                                       d_nodeManager->mkConst(Rational(1)));
113
  Node emptybag = d_nodeManager->mkConst(
114
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
115
4
  RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
116
4
  RewriteResponse zeroResponse = d_rewriter->postRewrite(zero);
117
4
  RewriteResponse positiveResponse = d_rewriter->postRewrite(positive);
118
119
  // bags with non-positive multiplicity are rewritten as empty bags
120
2
  ASSERT_TRUE(negativeResponse.d_status == REWRITE_AGAIN_FULL
121
2
              && negativeResponse.d_node == emptybag);
122
2
  ASSERT_TRUE(zeroResponse.d_status == REWRITE_AGAIN_FULL
123
2
              && zeroResponse.d_node == emptybag);
124
125
  // no change for positive
126
2
  ASSERT_TRUE(positiveResponse.d_status == REWRITE_DONE
127
2
              && positive == positiveResponse.d_node);
128
}
129
130
25
TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element)
131
{
132
4
  Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
133
4
  Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(),
134
                                       skolem,
135
8
                                       d_nodeManager->mkConst(Rational(-1)));
136
4
  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
137
                                       skolem,
138
8
                                       d_nodeManager->mkConst(Rational(-1)));
139
  Node zero = d_nodeManager->mkBag(
140
4
      d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(0)));
141
  Node positive = d_nodeManager->mkBag(
142
4
      d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(1)));
143
  Node emptybag = d_nodeManager->mkConst(
144
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
145
4
  RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
146
4
  RewriteResponse zeroResponse = d_rewriter->postRewrite(zero);
147
4
  RewriteResponse positiveResponse = d_rewriter->postRewrite(positive);
148
149
  // bags with non-positive multiplicity are rewritten as empty bags
150
2
  ASSERT_TRUE(negativeResponse.d_status == REWRITE_AGAIN_FULL
151
2
              && negativeResponse.d_node == emptybag);
152
2
  ASSERT_TRUE(zeroResponse.d_status == REWRITE_AGAIN_FULL
153
2
              && zeroResponse.d_node == emptybag);
154
155
  // no change for positive
156
2
  ASSERT_TRUE(positiveResponse.d_status == REWRITE_DONE
157
2
              && positive == positiveResponse.d_node);
158
}
159
160
25
TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
161
{
162
2
  int n = 3;
163
4
  Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
164
  Node emptyBag = d_nodeManager->mkConst(
165
4
      EmptyBag(d_nodeManager->mkBagType(skolem.getType())));
166
  Node bag = d_nodeManager->mkBag(
167
4
      d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(n)));
168
169
  // (bag.count x emptybag) = 0
170
4
  Node n1 = d_nodeManager->mkNode(BAG_COUNT, skolem, emptyBag);
171
4
  RewriteResponse response1 = d_rewriter->postRewrite(n1);
172
2
  ASSERT_TRUE(response1.d_status == REWRITE_AGAIN_FULL
173
2
              && response1.d_node == d_nodeManager->mkConst(Rational(0)));
174
175
  // (bag.count x (mkBag x c) = c where c > 0 is a constant
176
4
  Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag);
177
4
  RewriteResponse response2 = d_rewriter->postRewrite(n2);
178
2
  ASSERT_TRUE(response2.d_status == REWRITE_AGAIN_FULL
179
2
              && response2.d_node == d_nodeManager->mkConst(Rational(n)));
180
}
181
182
25
TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)
183
{
184
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
185
  Node bag = d_nodeManager->mkBag(
186
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
187
188
  // (duplicate_removal (mkBag x n)) = (mkBag x 1)
189
4
  Node n = d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag);
190
4
  RewriteResponse response = d_rewriter->postRewrite(n);
191
  Node noDuplicate = d_nodeManager->mkBag(
192
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
193
2
  ASSERT_TRUE(response.d_node == noDuplicate
194
2
              && response.d_status == REWRITE_AGAIN_FULL);
195
}
196
197
25
TEST_F(TestTheoryWhiteBagsRewriter, union_max)
198
{
199
2
  int n = 3;
200
4
  std::vector<Node> elements = getNStrings(2);
201
  Node emptyBag = d_nodeManager->mkConst(
202
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
203
4
  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
204
2
                                elements[0],
205
10
                                d_nodeManager->mkConst(Rational(n)));
206
4
  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
207
2
                                elements[1],
208
10
                                d_nodeManager->mkConst(Rational(n + 1)));
209
4
  Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
210
4
  Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
211
4
  Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
212
4
  Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
213
214
  // (union_max A emptybag) = A
215
4
  Node unionMax1 = d_nodeManager->mkNode(UNION_MAX, A, emptyBag);
216
4
  RewriteResponse response1 = d_rewriter->postRewrite(unionMax1);
217
2
  ASSERT_TRUE(response1.d_node == A
218
2
              && response1.d_status == REWRITE_AGAIN_FULL);
219
220
  // (union_max emptybag A) = A
221
4
  Node unionMax2 = d_nodeManager->mkNode(UNION_MAX, emptyBag, A);
222
4
  RewriteResponse response2 = d_rewriter->postRewrite(unionMax2);
223
2
  ASSERT_TRUE(response2.d_node == A
224
2
              && response2.d_status == REWRITE_AGAIN_FULL);
225
226
  // (union_max A A) = A
227
4
  Node unionMax3 = d_nodeManager->mkNode(UNION_MAX, A, A);
228
4
  RewriteResponse response3 = d_rewriter->postRewrite(unionMax3);
229
2
  ASSERT_TRUE(response3.d_node == A
230
2
              && response3.d_status == REWRITE_AGAIN_FULL);
231
232
  // (union_max A (union_max A B)) = (union_max A B)
233
4
  Node unionMax4 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxAB);
234
4
  RewriteResponse response4 = d_rewriter->postRewrite(unionMax4);
235
2
  ASSERT_TRUE(response4.d_node == unionMaxAB
236
2
              && response4.d_status == REWRITE_AGAIN_FULL);
237
238
  // (union_max A (union_max B A)) = (union_max B A)
239
4
  Node unionMax5 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxBA);
240
4
  RewriteResponse response5 = d_rewriter->postRewrite(unionMax5);
241
2
  ASSERT_TRUE(response5.d_node == unionMaxBA
242
2
              && response4.d_status == REWRITE_AGAIN_FULL);
243
244
  // (union_max (union_max A B) A) = (union_max A B)
245
4
  Node unionMax6 = d_nodeManager->mkNode(UNION_MAX, unionMaxAB, A);
246
4
  RewriteResponse response6 = d_rewriter->postRewrite(unionMax6);
247
2
  ASSERT_TRUE(response6.d_node == unionMaxAB
248
2
              && response6.d_status == REWRITE_AGAIN_FULL);
249
250
  // (union_max (union_max B A) A) = (union_max B A)
251
4
  Node unionMax7 = d_nodeManager->mkNode(UNION_MAX, unionMaxBA, A);
252
4
  RewriteResponse response7 = d_rewriter->postRewrite(unionMax7);
253
2
  ASSERT_TRUE(response7.d_node == unionMaxBA
254
2
              && response7.d_status == REWRITE_AGAIN_FULL);
255
256
  // (union_max A (union_disjoint A B)) = (union_disjoint A B)
257
4
  Node unionMax8 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointAB);
258
4
  RewriteResponse response8 = d_rewriter->postRewrite(unionMax8);
259
2
  ASSERT_TRUE(response8.d_node == unionDisjointAB
260
2
              && response8.d_status == REWRITE_AGAIN_FULL);
261
262
  // (union_max A (union_disjoint B A)) = (union_disjoint B A)
263
4
  Node unionMax9 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointBA);
264
4
  RewriteResponse response9 = d_rewriter->postRewrite(unionMax9);
265
2
  ASSERT_TRUE(response9.d_node == unionDisjointBA
266
2
              && response9.d_status == REWRITE_AGAIN_FULL);
267
268
  // (union_max (union_disjoint A B) A) = (union_disjoint A B)
269
4
  Node unionMax10 = d_nodeManager->mkNode(UNION_MAX, unionDisjointAB, A);
270
4
  RewriteResponse response10 = d_rewriter->postRewrite(unionMax10);
271
2
  ASSERT_TRUE(response10.d_node == unionDisjointAB
272
2
              && response10.d_status == REWRITE_AGAIN_FULL);
273
274
  // (union_max (union_disjoint B A) A) = (union_disjoint B A)
275
4
  Node unionMax11 = d_nodeManager->mkNode(UNION_MAX, unionDisjointBA, A);
276
4
  RewriteResponse response11 = d_rewriter->postRewrite(unionMax11);
277
2
  ASSERT_TRUE(response11.d_node == unionDisjointBA
278
2
              && response11.d_status == REWRITE_AGAIN_FULL);
279
}
280
281
25
TEST_F(TestTheoryWhiteBagsRewriter, union_disjoint)
282
{
283
2
  int n = 3;
284
4
  std::vector<Node> elements = getNStrings(3);
285
  Node emptyBag = d_nodeManager->mkConst(
286
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
287
4
  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
288
2
                                elements[0],
289
10
                                d_nodeManager->mkConst(Rational(n)));
290
4
  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
291
2
                                elements[1],
292
10
                                d_nodeManager->mkConst(Rational(n + 1)));
293
4
  Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
294
2
                                elements[2],
295
10
                                d_nodeManager->mkConst(Rational(n + 2)));
296
297
4
  Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
298
4
  Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
299
4
  Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
300
4
  Node unionMaxAC = d_nodeManager->mkNode(UNION_MAX, A, C);
301
4
  Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
302
4
  Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
303
4
  Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
304
305
  // (union_disjoint A emptybag) = A
306
4
  Node unionDisjoint1 = d_nodeManager->mkNode(UNION_DISJOINT, A, emptyBag);
307
4
  RewriteResponse response1 = d_rewriter->postRewrite(unionDisjoint1);
308
2
  ASSERT_TRUE(response1.d_node == A
309
2
              && response1.d_status == REWRITE_AGAIN_FULL);
310
311
  // (union_disjoint emptybag A) = A
312
4
  Node unionDisjoint2 = d_nodeManager->mkNode(UNION_DISJOINT, emptyBag, A);
313
4
  RewriteResponse response2 = d_rewriter->postRewrite(unionDisjoint2);
314
2
  ASSERT_TRUE(response2.d_node == A
315
2
              && response2.d_status == REWRITE_AGAIN_FULL);
316
317
  // (union_disjoint (union_max A B) (intersection_min B A)) =
318
  //          (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b)
319
  Node unionDisjoint3 =
320
4
      d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAB, intersectionBA);
321
4
  RewriteResponse response3 = d_rewriter->postRewrite(unionDisjoint3);
322
2
  ASSERT_TRUE(response3.d_node == unionDisjointAB
323
2
              && response3.d_status == REWRITE_AGAIN_FULL);
324
325
  // (union_disjoint (intersection_min B A)) (union_max A B) =
326
  //          (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b)
327
  Node unionDisjoint4 =
328
4
      d_nodeManager->mkNode(UNION_DISJOINT, unionMaxBA, intersectionBA);
329
4
  RewriteResponse response4 = d_rewriter->postRewrite(unionDisjoint4);
330
2
  ASSERT_TRUE(response4.d_node == unionDisjointBA
331
2
              && response4.d_status == REWRITE_AGAIN_FULL);
332
333
  // (union_disjoint (intersection_min B A)) (union_max A B) =
334
  //          (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b)
335
  Node unionDisjoint5 =
336
4
      d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAC, intersectionAB);
337
4
  RewriteResponse response5 = d_rewriter->postRewrite(unionDisjoint5);
338
2
  ASSERT_TRUE(response5.d_node == unionDisjoint5
339
2
              && response5.d_status == REWRITE_DONE);
340
}
341
342
25
TEST_F(TestTheoryWhiteBagsRewriter, intersection_min)
343
{
344
2
  int n = 3;
345
4
  std::vector<Node> elements = getNStrings(2);
346
  Node emptyBag = d_nodeManager->mkConst(
347
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
348
4
  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
349
2
                                elements[0],
350
10
                                d_nodeManager->mkConst(Rational(n)));
351
4
  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
352
2
                                elements[1],
353
10
                                d_nodeManager->mkConst(Rational(n + 1)));
354
4
  Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
355
4
  Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
356
4
  Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
357
4
  Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
358
359
  // (intersection_min A emptybag) = emptyBag
360
4
  Node n1 = d_nodeManager->mkNode(INTERSECTION_MIN, A, emptyBag);
361
4
  RewriteResponse response1 = d_rewriter->postRewrite(n1);
362
2
  ASSERT_TRUE(response1.d_node == emptyBag
363
2
              && response1.d_status == REWRITE_AGAIN_FULL);
364
365
  // (intersection_min emptybag A) = emptyBag
366
4
  Node n2 = d_nodeManager->mkNode(INTERSECTION_MIN, emptyBag, A);
367
4
  RewriteResponse response2 = d_rewriter->postRewrite(n2);
368
2
  ASSERT_TRUE(response2.d_node == emptyBag
369
2
              && response2.d_status == REWRITE_AGAIN_FULL);
370
371
  // (intersection_min A A) = A
372
4
  Node n3 = d_nodeManager->mkNode(INTERSECTION_MIN, A, A);
373
4
  RewriteResponse response3 = d_rewriter->postRewrite(n3);
374
2
  ASSERT_TRUE(response3.d_node == A
375
2
              && response3.d_status == REWRITE_AGAIN_FULL);
376
377
  // (intersection_min A (union_max A B) = A
378
4
  Node n4 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxAB);
379
4
  RewriteResponse response4 = d_rewriter->postRewrite(n4);
380
2
  ASSERT_TRUE(response4.d_node == A
381
2
              && response4.d_status == REWRITE_AGAIN_FULL);
382
383
  // (intersection_min A (union_max B A) = A
384
4
  Node n5 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxBA);
385
4
  RewriteResponse response5 = d_rewriter->postRewrite(n5);
386
2
  ASSERT_TRUE(response5.d_node == A
387
2
              && response4.d_status == REWRITE_AGAIN_FULL);
388
389
  // (intersection_min (union_max A B) A) = A
390
4
  Node n6 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxAB, A);
391
4
  RewriteResponse response6 = d_rewriter->postRewrite(n6);
392
2
  ASSERT_TRUE(response6.d_node == A
393
2
              && response6.d_status == REWRITE_AGAIN_FULL);
394
395
  // (intersection_min (union_max B A) A) = A
396
4
  Node n7 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxBA, A);
397
4
  RewriteResponse response7 = d_rewriter->postRewrite(n7);
398
2
  ASSERT_TRUE(response7.d_node == A
399
2
              && response7.d_status == REWRITE_AGAIN_FULL);
400
401
  // (intersection_min A (union_disjoint A B) = A
402
4
  Node n8 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointAB);
403
4
  RewriteResponse response8 = d_rewriter->postRewrite(n8);
404
2
  ASSERT_TRUE(response8.d_node == A
405
2
              && response8.d_status == REWRITE_AGAIN_FULL);
406
407
  // (intersection_min A (union_disjoint B A) = A
408
4
  Node n9 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointBA);
409
4
  RewriteResponse response9 = d_rewriter->postRewrite(n9);
410
2
  ASSERT_TRUE(response9.d_node == A
411
2
              && response9.d_status == REWRITE_AGAIN_FULL);
412
413
  // (intersection_min (union_disjoint A B) A) = A
414
4
  Node n10 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointAB, A);
415
4
  RewriteResponse response10 = d_rewriter->postRewrite(n10);
416
2
  ASSERT_TRUE(response10.d_node == A
417
2
              && response10.d_status == REWRITE_AGAIN_FULL);
418
419
  // (intersection_min (union_disjoint B A) A) = A
420
4
  Node n11 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointBA, A);
421
4
  RewriteResponse response11 = d_rewriter->postRewrite(n11);
422
2
  ASSERT_TRUE(response11.d_node == A
423
2
              && response11.d_status == REWRITE_AGAIN_FULL);
424
}
425
426
25
TEST_F(TestTheoryWhiteBagsRewriter, difference_subtract)
427
{
428
2
  int n = 3;
429
4
  std::vector<Node> elements = getNStrings(2);
430
  Node emptyBag = d_nodeManager->mkConst(
431
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
432
4
  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
433
2
                                elements[0],
434
10
                                d_nodeManager->mkConst(Rational(n)));
435
4
  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
436
2
                                elements[1],
437
10
                                d_nodeManager->mkConst(Rational(n + 1)));
438
4
  Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
439
4
  Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
440
4
  Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
441
4
  Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
442
4
  Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
443
4
  Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
444
445
  // (difference_subtract A emptybag) = A
446
4
  Node n1 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, emptyBag);
447
4
  RewriteResponse response1 = d_rewriter->postRewrite(n1);
448
2
  ASSERT_TRUE(response1.d_node == A
449
2
              && response1.d_status == REWRITE_AGAIN_FULL);
450
451
  // (difference_subtract emptybag A) = emptyBag
452
4
  Node n2 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, emptyBag, A);
453
4
  RewriteResponse response2 = d_rewriter->postRewrite(n2);
454
2
  ASSERT_TRUE(response2.d_node == emptyBag
455
2
              && response2.d_status == REWRITE_AGAIN_FULL);
456
457
  // (difference_subtract A A) = emptybag
458
4
  Node n3 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, A);
459
4
  RewriteResponse response3 = d_rewriter->postRewrite(n3);
460
2
  ASSERT_TRUE(response3.d_node == emptyBag
461
2
              && response3.d_status == REWRITE_AGAIN_FULL);
462
463
  // (difference_subtract (union_disjoint A B) A) = B
464
4
  Node n4 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointAB, A);
465
4
  RewriteResponse response4 = d_rewriter->postRewrite(n4);
466
2
  ASSERT_TRUE(response4.d_node == B
467
2
              && response4.d_status == REWRITE_AGAIN_FULL);
468
469
  // (difference_subtract (union_disjoint B A) A) = B
470
4
  Node n5 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointBA, A);
471
4
  RewriteResponse response5 = d_rewriter->postRewrite(n5);
472
2
  ASSERT_TRUE(response5.d_node == B
473
2
              && response4.d_status == REWRITE_AGAIN_FULL);
474
475
  // (difference_subtract A (union_disjoint A B)) = emptybag
476
4
  Node n6 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointAB);
477
4
  RewriteResponse response6 = d_rewriter->postRewrite(n6);
478
2
  ASSERT_TRUE(response6.d_node == emptyBag
479
2
              && response6.d_status == REWRITE_AGAIN_FULL);
480
481
  // (difference_subtract A (union_disjoint B A)) = emptybag
482
4
  Node n7 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointBA);
483
4
  RewriteResponse response7 = d_rewriter->postRewrite(n7);
484
2
  ASSERT_TRUE(response7.d_node == emptyBag
485
2
              && response7.d_status == REWRITE_AGAIN_FULL);
486
487
  // (difference_subtract A (union_max A B)) = emptybag
488
4
  Node n8 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxAB);
489
4
  RewriteResponse response8 = d_rewriter->postRewrite(n8);
490
2
  ASSERT_TRUE(response8.d_node == emptyBag
491
2
              && response8.d_status == REWRITE_AGAIN_FULL);
492
493
  // (difference_subtract A (union_max B A)) = emptybag
494
4
  Node n9 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxBA);
495
4
  RewriteResponse response9 = d_rewriter->postRewrite(n9);
496
2
  ASSERT_TRUE(response9.d_node == emptyBag
497
2
              && response9.d_status == REWRITE_AGAIN_FULL);
498
499
  // (difference_subtract (intersection_min A B) A) = emptybag
500
4
  Node n10 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionAB, A);
501
4
  RewriteResponse response10 = d_rewriter->postRewrite(n10);
502
2
  ASSERT_TRUE(response10.d_node == emptyBag
503
2
              && response10.d_status == REWRITE_AGAIN_FULL);
504
505
  // (difference_subtract (intersection_min B A) A) = emptybag
506
4
  Node n11 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionBA, A);
507
4
  RewriteResponse response11 = d_rewriter->postRewrite(n11);
508
2
  ASSERT_TRUE(response11.d_node == emptyBag
509
2
              && response11.d_status == REWRITE_AGAIN_FULL);
510
}
511
512
25
TEST_F(TestTheoryWhiteBagsRewriter, difference_remove)
513
{
514
2
  int n = 3;
515
4
  std::vector<Node> elements = getNStrings(2);
516
  Node emptyBag = d_nodeManager->mkConst(
517
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
518
4
  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
519
2
                                elements[0],
520
10
                                d_nodeManager->mkConst(Rational(n)));
521
4
  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
522
2
                                elements[1],
523
10
                                d_nodeManager->mkConst(Rational(n + 1)));
524
4
  Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
525
4
  Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
526
4
  Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
527
4
  Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
528
4
  Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
529
4
  Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
530
531
  // (difference_remove A emptybag) = A
532
4
  Node n1 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, emptyBag);
533
4
  RewriteResponse response1 = d_rewriter->postRewrite(n1);
534
2
  ASSERT_TRUE(response1.d_node == A
535
2
              && response1.d_status == REWRITE_AGAIN_FULL);
536
537
  // (difference_remove emptybag A) = emptyBag
538
4
  Node n2 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, emptyBag, A);
539
4
  RewriteResponse response2 = d_rewriter->postRewrite(n2);
540
2
  ASSERT_TRUE(response2.d_node == emptyBag
541
2
              && response2.d_status == REWRITE_AGAIN_FULL);
542
543
  // (difference_remove A A) = emptybag
544
4
  Node n3 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, A);
545
4
  RewriteResponse response3 = d_rewriter->postRewrite(n3);
546
2
  ASSERT_TRUE(response3.d_node == emptyBag
547
2
              && response3.d_status == REWRITE_AGAIN_FULL);
548
549
  // (difference_remove A (union_disjoint A B)) = emptybag
550
4
  Node n6 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointAB);
551
4
  RewriteResponse response6 = d_rewriter->postRewrite(n6);
552
2
  ASSERT_TRUE(response6.d_node == emptyBag
553
2
              && response6.d_status == REWRITE_AGAIN_FULL);
554
555
  // (difference_remove A (union_disjoint B A)) = emptybag
556
4
  Node n7 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointBA);
557
4
  RewriteResponse response7 = d_rewriter->postRewrite(n7);
558
2
  ASSERT_TRUE(response7.d_node == emptyBag
559
2
              && response7.d_status == REWRITE_AGAIN_FULL);
560
561
  // (difference_remove A (union_max A B)) = emptybag
562
4
  Node n8 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxAB);
563
4
  RewriteResponse response8 = d_rewriter->postRewrite(n8);
564
2
  ASSERT_TRUE(response8.d_node == emptyBag
565
2
              && response8.d_status == REWRITE_AGAIN_FULL);
566
567
  // (difference_remove A (union_max B A)) = emptybag
568
4
  Node n9 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxBA);
569
4
  RewriteResponse response9 = d_rewriter->postRewrite(n9);
570
2
  ASSERT_TRUE(response9.d_node == emptyBag
571
2
              && response9.d_status == REWRITE_AGAIN_FULL);
572
573
  // (difference_remove (intersection_min A B) A) = emptybag
574
4
  Node n10 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionAB, A);
575
4
  RewriteResponse response10 = d_rewriter->postRewrite(n10);
576
2
  ASSERT_TRUE(response10.d_node == emptyBag
577
2
              && response10.d_status == REWRITE_AGAIN_FULL);
578
579
  // (difference_remove (intersection_min B A) A) = emptybag
580
4
  Node n11 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionBA, A);
581
4
  RewriteResponse response11 = d_rewriter->postRewrite(n11);
582
2
  ASSERT_TRUE(response11.d_node == emptyBag
583
2
              && response11.d_status == REWRITE_AGAIN_FULL);
584
}
585
586
25
TEST_F(TestTheoryWhiteBagsRewriter, choose)
587
{
588
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
589
4
  Node c = d_nodeManager->mkConst(Rational(3));
590
4
  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
591
592
  // (bag.choose (mkBag x c)) = x where c is a constant > 0
593
4
  Node n1 = d_nodeManager->mkNode(BAG_CHOOSE, bag);
594
4
  RewriteResponse response1 = d_rewriter->postRewrite(n1);
595
2
  ASSERT_TRUE(response1.d_node == x
596
2
              && response1.d_status == REWRITE_AGAIN_FULL);
597
}
598
599
25
TEST_F(TestTheoryWhiteBagsRewriter, bag_card)
600
{
601
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
602
  Node emptyBag = d_nodeManager->mkConst(
603
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
604
4
  Node zero = d_nodeManager->mkConst(Rational(0));
605
4
  Node c = d_nodeManager->mkConst(Rational(3));
606
4
  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
607
4
  std::vector<Node> elements = getNStrings(2);
608
4
  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
609
2
                                elements[0],
610
10
                                d_nodeManager->mkConst(Rational(4)));
611
4
  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
612
2
                                elements[1],
613
10
                                d_nodeManager->mkConst(Rational(5)));
614
4
  Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
615
616
  // TODO(projects#223): enable this test after implementing bags normal form
617
  //    // (bag.card emptybag) = 0
618
  //    Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag);
619
  //    RewriteResponse response1 = d_rewriter->postRewrite(n1);
620
  //    ASSERT_TRUE(response1.d_node == zero && response1.d_status ==
621
  //    REWRITE_AGAIN_FULL);
622
623
  // (bag.card (mkBag x c)) = c where c is a constant > 0
624
4
  Node n2 = d_nodeManager->mkNode(BAG_CARD, bag);
625
4
  RewriteResponse response2 = d_rewriter->postRewrite(n2);
626
2
  ASSERT_TRUE(response2.d_node == c
627
2
              && response2.d_status == REWRITE_AGAIN_FULL);
628
629
  // (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B))
630
4
  Node n3 = d_nodeManager->mkNode(BAG_CARD, unionDisjointAB);
631
4
  Node cardA = d_nodeManager->mkNode(BAG_CARD, A);
632
4
  Node cardB = d_nodeManager->mkNode(BAG_CARD, B);
633
4
  Node plus = d_nodeManager->mkNode(PLUS, cardA, cardB);
634
4
  RewriteResponse response3 = d_rewriter->postRewrite(n3);
635
2
  ASSERT_TRUE(response3.d_node == plus
636
2
              && response3.d_status == REWRITE_AGAIN_FULL);
637
}
638
639
25
TEST_F(TestTheoryWhiteBagsRewriter, is_singleton)
640
{
641
  Node emptybag = d_nodeManager->mkConst(
642
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
643
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
644
4
  Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType());
645
4
  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
646
647
  // TODO(projects#223): complete this function
648
  // (bag.is_singleton emptybag) = false
649
  //    Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag);
650
  //    RewriteResponse response1 = d_rewriter->postRewrite(n1);
651
  //    ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false)
652
  //              && response1.d_status == REWRITE_AGAIN_FULL);
653
654
  // (bag.is_singleton (mkBag x c) = (c == 1)
655
4
  Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag);
656
4
  RewriteResponse response2 = d_rewriter->postRewrite(n2);
657
4
  Node one = d_nodeManager->mkConst(Rational(1));
658
4
  Node equal = c.eqNode(one);
659
2
  ASSERT_TRUE(response2.d_node == equal
660
2
              && response2.d_status == REWRITE_AGAIN_FULL);
661
}
662
663
25
TEST_F(TestTheoryWhiteBagsRewriter, from_set)
664
{
665
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
666
4
  Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
667
668
  // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1)
669
4
  Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton);
670
4
  RewriteResponse response = d_rewriter->postRewrite(n);
671
4
  Node one = d_nodeManager->mkConst(Rational(1));
672
4
  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, one);
673
2
  ASSERT_TRUE(response.d_node == bag
674
2
              && response.d_status == REWRITE_AGAIN_FULL);
675
}
676
677
25
TEST_F(TestTheoryWhiteBagsRewriter, to_set)
678
{
679
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
680
  Node bag = d_nodeManager->mkBag(
681
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
682
683
  // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x)
684
4
  Node n = d_nodeManager->mkNode(BAG_TO_SET, bag);
685
4
  RewriteResponse response = d_rewriter->postRewrite(n);
686
4
  Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
687
2
  ASSERT_TRUE(response.d_node == singleton
688
2
              && response.d_status == REWRITE_AGAIN_FULL);
689
}
690
}  // namespace test
691
234457
}  // namespace CVC4