GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_bags_normal_form_white.cpp Lines: 283 283 100.0 %
Date: 2021-03-23 Branches: 1079 2564 42.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bags_normal_form_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 normal form
13
 **/
14
15
#include "expr/dtype.h"
16
#include "test_smt.h"
17
#include "theory/bags/bags_rewriter.h"
18
#include "theory/bags/normal_form.h"
19
#include "theory/strings/type_enumerator.h"
20
21
namespace CVC4 {
22
23
using namespace theory;
24
using namespace kind;
25
using namespace theory::bags;
26
27
namespace test {
28
29
typedef expr::Attribute<Node, Node> attribute;
30
31
60
class TestTheoryWhiteBagsNormalForm : public TestSmt
32
{
33
 protected:
34
30
  void SetUp() override
35
  {
36
30
    TestSmt::SetUp();
37
30
    d_rewriter.reset(new BagsRewriter(nullptr));
38
30
  }
39
40
4
  std::vector<Node> getNStrings(size_t n)
41
  {
42
4
    std::vector<Node> elements(n);
43
    CVC4::theory::strings::StringEnumerator enumerator(
44
8
        d_nodeManager->stringType());
45
46
12
    for (size_t i = 0; i < n; i++)
47
    {
48
8
      ++enumerator;
49
8
      elements[i] = *enumerator;
50
    }
51
52
8
    return elements;
53
  }
54
55
  std::unique_ptr<BagsRewriter> d_rewriter;
56
};
57
58
24
TEST_F(TestTheoryWhiteBagsNormalForm, empty_bag_normal_form)
59
{
60
4
  Node emptybag = d_nodeManager->mkConst(EmptyBag(d_nodeManager->stringType()));
61
  // empty bags are in normal form
62
2
  ASSERT_TRUE(emptybag.isConst());
63
4
  Node n = NormalForm::evaluate(emptybag);
64
2
  ASSERT_EQ(emptybag, n);
65
}
66
67
24
TEST_F(TestTheoryWhiteBagsNormalForm, mkBag_constant_element)
68
{
69
4
  std::vector<Node> elements = getNStrings(1);
70
4
  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
71
2
                                       elements[0],
72
10
                                       d_nodeManager->mkConst(Rational(-1)));
73
4
  Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
74
2
                                   elements[0],
75
10
                                   d_nodeManager->mkConst(Rational(0)));
76
4
  Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
77
2
                                       elements[0],
78
10
                                       d_nodeManager->mkConst(Rational(1)));
79
  Node emptybag = d_nodeManager->mkConst(
80
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
81
82
2
  ASSERT_FALSE(negative.isConst());
83
2
  ASSERT_FALSE(zero.isConst());
84
2
  ASSERT_EQ(emptybag, NormalForm::evaluate(negative));
85
2
  ASSERT_EQ(emptybag, NormalForm::evaluate(zero));
86
2
  ASSERT_EQ(positive, NormalForm::evaluate(positive));
87
}
88
89
24
TEST_F(TestTheoryWhiteBagsNormalForm, bag_count)
90
{
91
  // Examples
92
  // -------
93
  // (bag.count "x" (emptybag String)) = 0
94
  // (bag.count "x" (mkBag "y" 5)) = 0
95
  // (bag.count "x" (mkBag "x" 4)) = 4
96
  // (bag.count "x" (union_disjoint (mkBag "x" 4) (mkBag "y" 5)) = 4
97
  // (bag.count "x" (union_disjoint (mkBag "y" 5) (mkBag "z" 5)) = 0
98
99
4
  Node zero = d_nodeManager->mkConst(Rational(0));
100
4
  Node four = d_nodeManager->mkConst(Rational(4));
101
  Node empty = d_nodeManager->mkConst(
102
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
103
4
  Node x = d_nodeManager->mkConst(String("x"));
104
4
  Node y = d_nodeManager->mkConst(String("y"));
105
4
  Node z = d_nodeManager->mkConst(String("z"));
106
  Node x_4 = d_nodeManager->mkBag(
107
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
108
  Node y_5 = d_nodeManager->mkBag(
109
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5)));
110
  Node z_5 = d_nodeManager->mkBag(
111
4
      d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(5)));
112
113
4
  Node input1 = d_nodeManager->mkNode(BAG_COUNT, x, empty);
114
4
  Node output1 = zero;
115
2
  ASSERT_EQ(output1, NormalForm::evaluate(input1));
116
117
4
  Node input2 = d_nodeManager->mkNode(BAG_COUNT, x, y_5);
118
4
  Node output2 = zero;
119
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
120
121
4
  Node input3 = d_nodeManager->mkNode(BAG_COUNT, x, x_4);
122
4
  Node output3 = four;
123
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
124
125
4
  Node unionDisjointXY = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5);
126
4
  Node input4 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointXY);
127
4
  Node output4 = four;
128
2
  ASSERT_EQ(output3, NormalForm::evaluate(input3));
129
130
4
  Node unionDisjointYZ = d_nodeManager->mkNode(UNION_DISJOINT, y_5, z_5);
131
4
  Node input5 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointYZ);
132
4
  Node output5 = zero;
133
2
  ASSERT_EQ(output4, NormalForm::evaluate(input4));
134
}
135
136
24
TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal)
137
{
138
  // Examples
139
  // --------
140
  //  - (duplicate_removal (emptybag String)) = (emptybag String)
141
  //  - (duplicate_removal (mkBag "x" 4)) = (emptybag "x" 1)
142
  //  - (duplicate_removal (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) =
143
  //     (disjoint_union (mkBag "x" 1) (mkBag "y" 1)
144
145
  Node emptybag = d_nodeManager->mkConst(
146
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
147
4
  Node input1 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, emptybag);
148
4
  Node output1 = emptybag;
149
2
  ASSERT_EQ(output1, NormalForm::evaluate(input1));
150
151
4
  Node x = d_nodeManager->mkConst(String("x"));
152
4
  Node y = d_nodeManager->mkConst(String("y"));
153
154
  Node x_1 = d_nodeManager->mkBag(
155
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
156
  Node y_1 = d_nodeManager->mkBag(
157
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
158
159
  Node x_4 = d_nodeManager->mkBag(
160
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
161
  Node y_5 = d_nodeManager->mkBag(
162
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5)));
163
164
4
  Node input2 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, x_4);
165
4
  Node output2 = x_1;
166
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
167
168
4
  Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5);
169
4
  Node input3 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, normalBag);
170
4
  Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1);
171
2
  ASSERT_EQ(output3, NormalForm::evaluate(input3));
172
}
173
174
24
TEST_F(TestTheoryWhiteBagsNormalForm, union_max)
175
{
176
  // Example
177
  // -------
178
  // input: (union_max A B)
179
  //    where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
180
  //          B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
181
  // output:
182
  //    (union_disjoint A B)
183
  //        where A = (MK_BAG "x" 4)
184
  //              B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2)))
185
186
4
  Node x = d_nodeManager->mkConst(String("x"));
187
4
  Node y = d_nodeManager->mkConst(String("y"));
188
4
  Node z = d_nodeManager->mkConst(String("z"));
189
  Node x_4 = d_nodeManager->mkBag(
190
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
191
  Node x_3 = d_nodeManager->mkBag(
192
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
193
  Node x_7 = d_nodeManager->mkBag(
194
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
195
  Node z_2 = d_nodeManager->mkBag(
196
4
      d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
197
  Node y_1 = d_nodeManager->mkBag(
198
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
199
200
4
  Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
201
4
  Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
202
4
  Node input = d_nodeManager->mkNode(UNION_MAX, A, B);
203
204
  // output
205
  Node output = d_nodeManager->mkNode(
206
4
      UNION_DISJOINT, x_4, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2));
207
208
2
  ASSERT_TRUE(output.isConst());
209
2
  ASSERT_EQ(output, NormalForm::evaluate(input));
210
}
211
212
24
TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1)
213
{
214
4
  std::vector<Node> elements = getNStrings(3);
215
  Node emptybag = d_nodeManager->mkConst(
216
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
217
4
  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
218
2
                                elements[0],
219
10
                                d_nodeManager->mkConst(Rational(2)));
220
4
  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
221
2
                                elements[1],
222
10
                                d_nodeManager->mkConst(Rational(3)));
223
4
  Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
224
2
                                elements[2],
225
10
                                d_nodeManager->mkConst(Rational(4)));
226
227
4
  Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
228
  // unionDisjointAB is already in a normal form
229
2
  ASSERT_TRUE(unionDisjointAB.isConst());
230
2
  ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointAB));
231
232
4
  Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
233
  // unionDisjointAB is is the normal form of unionDisjointBA
234
2
  ASSERT_FALSE(unionDisjointBA.isConst());
235
2
  ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointBA));
236
237
  Node unionDisjointAB_C =
238
4
      d_nodeManager->mkNode(UNION_DISJOINT, unionDisjointAB, C);
239
4
  Node unionDisjointBC = d_nodeManager->mkNode(UNION_DISJOINT, B, C);
240
  Node unionDisjointA_BC =
241
4
      d_nodeManager->mkNode(UNION_DISJOINT, A, unionDisjointBC);
242
  // unionDisjointA_BC is the normal form of unionDisjointAB_C
243
2
  ASSERT_FALSE(unionDisjointAB_C.isConst());
244
2
  ASSERT_TRUE(unionDisjointA_BC.isConst());
245
2
  ASSERT_EQ(unionDisjointA_BC, NormalForm::evaluate(unionDisjointAB_C));
246
247
4
  Node unionDisjointAA = d_nodeManager->mkNode(UNION_DISJOINT, A, A);
248
4
  Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(),
249
2
                                 elements[0],
250
10
                                 d_nodeManager->mkConst(Rational(4)));
251
2
  ASSERT_FALSE(unionDisjointAA.isConst());
252
2
  ASSERT_TRUE(AA.isConst());
253
2
  ASSERT_EQ(AA, NormalForm::evaluate(unionDisjointAA));
254
}
255
256
24
TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint2)
257
{
258
  // Example
259
  // -------
260
  // input: (union_disjoint A B)
261
  //    where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
262
  //          B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
263
  // output:
264
  //    (union_disjoint A B)
265
  //        where A = (MK_BAG "x" 7)
266
  //              B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2)))
267
268
4
  Node x = d_nodeManager->mkConst(String("x"));
269
4
  Node y = d_nodeManager->mkConst(String("y"));
270
4
  Node z = d_nodeManager->mkConst(String("z"));
271
  Node x_4 = d_nodeManager->mkBag(
272
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
273
  Node x_3 = d_nodeManager->mkBag(
274
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
275
  Node x_7 = d_nodeManager->mkBag(
276
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
277
  Node z_2 = d_nodeManager->mkBag(
278
4
      d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
279
  Node y_1 = d_nodeManager->mkBag(
280
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
281
282
4
  Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
283
4
  Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
284
4
  Node input = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
285
286
  // output
287
  Node output = d_nodeManager->mkNode(
288
4
      UNION_DISJOINT, x_7, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2));
289
290
2
  ASSERT_TRUE(output.isConst());
291
2
  ASSERT_EQ(output, NormalForm::evaluate(input));
292
}
293
294
24
TEST_F(TestTheoryWhiteBagsNormalForm, intersection_min)
295
{
296
  // Example
297
  // -------
298
  // input: (intersection_min A B)
299
  //    where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
300
  //          B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
301
  // output:
302
  //    (MK_BAG "x" 3)
303
304
4
  Node x = d_nodeManager->mkConst(String("x"));
305
4
  Node y = d_nodeManager->mkConst(String("y"));
306
4
  Node z = d_nodeManager->mkConst(String("z"));
307
  Node x_4 = d_nodeManager->mkBag(
308
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
309
  Node x_3 = d_nodeManager->mkBag(
310
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
311
  Node x_7 = d_nodeManager->mkBag(
312
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
313
  Node z_2 = d_nodeManager->mkBag(
314
4
      d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
315
  Node y_1 = d_nodeManager->mkBag(
316
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
317
318
4
  Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
319
4
  Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
320
4
  Node input = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
321
322
  // output
323
4
  Node output = x_3;
324
325
2
  ASSERT_TRUE(output.isConst());
326
2
  ASSERT_EQ(output, NormalForm::evaluate(input));
327
}
328
329
24
TEST_F(TestTheoryWhiteBagsNormalForm, difference_subtract)
330
{
331
  // Example
332
  // -------
333
  // input: (difference_subtract A B)
334
  //    where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
335
  //          B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
336
  // output:
337
  //    (union_disjoint (MK_BAG "x" 1) (MK_BAG "z" 2))
338
339
4
  Node x = d_nodeManager->mkConst(String("x"));
340
4
  Node y = d_nodeManager->mkConst(String("y"));
341
4
  Node z = d_nodeManager->mkConst(String("z"));
342
  Node x_1 = d_nodeManager->mkBag(
343
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
344
  Node x_4 = d_nodeManager->mkBag(
345
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
346
  Node x_3 = d_nodeManager->mkBag(
347
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
348
  Node x_7 = d_nodeManager->mkBag(
349
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
350
  Node z_2 = d_nodeManager->mkBag(
351
4
      d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
352
  Node y_1 = d_nodeManager->mkBag(
353
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
354
355
4
  Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
356
4
  Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
357
4
  Node input = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, B);
358
359
  // output
360
4
  Node output = d_nodeManager->mkNode(UNION_DISJOINT, x_1, z_2);
361
362
2
  ASSERT_TRUE(output.isConst());
363
2
  ASSERT_EQ(output, NormalForm::evaluate(input));
364
}
365
366
24
TEST_F(TestTheoryWhiteBagsNormalForm, difference_remove)
367
{
368
  // Example
369
  // -------
370
  // input: (difference_remove A B)
371
  //    where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
372
  //          B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
373
  // output:
374
  //    (MK_BAG "z" 2)
375
376
4
  Node x = d_nodeManager->mkConst(String("x"));
377
4
  Node y = d_nodeManager->mkConst(String("y"));
378
4
  Node z = d_nodeManager->mkConst(String("z"));
379
  Node x_1 = d_nodeManager->mkBag(
380
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
381
  Node x_4 = d_nodeManager->mkBag(
382
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
383
  Node x_3 = d_nodeManager->mkBag(
384
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
385
  Node x_7 = d_nodeManager->mkBag(
386
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
387
  Node z_2 = d_nodeManager->mkBag(
388
4
      d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
389
  Node y_1 = d_nodeManager->mkBag(
390
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
391
392
4
  Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
393
4
  Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
394
4
  Node input = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, B);
395
396
  // output
397
4
  Node output = z_2;
398
399
2
  ASSERT_TRUE(output.isConst());
400
2
  ASSERT_EQ(output, NormalForm::evaluate(input));
401
}
402
403
24
TEST_F(TestTheoryWhiteBagsNormalForm, choose)
404
{
405
  // Example
406
  // -------
407
  // input:  (choose (emptybag String))
408
  // output: "A"; the first element returned by the type enumerator
409
  // input:  (choose (MK_BAG "x" 4))
410
  // output: "x"
411
  // input:  (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1)))
412
  // output: "x"; deterministically return the first element
413
  Node empty = d_nodeManager->mkConst(
414
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
415
4
  Node x = d_nodeManager->mkConst(String("x"));
416
4
  Node y = d_nodeManager->mkConst(String("y"));
417
4
  Node z = d_nodeManager->mkConst(String("z"));
418
  Node x_4 = d_nodeManager->mkBag(
419
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
420
  Node y_1 = d_nodeManager->mkBag(
421
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
422
423
4
  Node input1 = d_nodeManager->mkNode(BAG_CHOOSE, empty);
424
4
  Node output1 = d_nodeManager->mkConst(String(""));
425
426
2
  ASSERT_EQ(output1, NormalForm::evaluate(input1));
427
428
4
  Node input2 = d_nodeManager->mkNode(BAG_CHOOSE, x_4);
429
4
  Node output2 = x;
430
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
431
432
4
  Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_1);
433
4
  Node input3 = d_nodeManager->mkNode(BAG_CHOOSE, union_disjoint);
434
4
  Node output3 = x;
435
2
  ASSERT_EQ(output3, NormalForm::evaluate(input3));
436
}
437
438
24
TEST_F(TestTheoryWhiteBagsNormalForm, bag_card)
439
{
440
  // Examples
441
  // --------
442
  //  - (card (emptybag String)) = 0
443
  //  - (choose (MK_BAG "x" 4)) = 4
444
  //  - (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1))) = 5
445
  Node empty = d_nodeManager->mkConst(
446
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
447
4
  Node x = d_nodeManager->mkConst(String("x"));
448
4
  Node y = d_nodeManager->mkConst(String("y"));
449
4
  Node z = d_nodeManager->mkConst(String("z"));
450
  Node x_4 = d_nodeManager->mkBag(
451
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
452
  Node y_1 = d_nodeManager->mkBag(
453
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
454
455
4
  Node input1 = d_nodeManager->mkNode(BAG_CARD, empty);
456
4
  Node output1 = d_nodeManager->mkConst(Rational(0));
457
458
2
  ASSERT_EQ(output1, NormalForm::evaluate(input1));
459
460
4
  Node input2 = d_nodeManager->mkNode(BAG_CARD, x_4);
461
4
  Node output2 = d_nodeManager->mkConst(Rational(4));
462
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
463
464
4
  Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_1);
465
4
  Node input3 = d_nodeManager->mkNode(BAG_CARD, union_disjoint);
466
4
  Node output3 = d_nodeManager->mkConst(Rational(5));
467
2
  ASSERT_EQ(output3, NormalForm::evaluate(input3));
468
}
469
470
24
TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton)
471
{
472
  // Examples
473
  // --------
474
  //  - (bag.is_singleton (emptybag String)) = false
475
  //  - (bag.is_singleton (MK_BAG "x" 1)) = true
476
  //  - (bag.is_singleton (MK_BAG "x" 4)) = false
477
  //  - (bag.is_singleton (union_disjoint (MK_BAG "x" 1) (MK_BAG "y" 1))) =
478
  //     false
479
4
  Node falseNode = d_nodeManager->mkConst(false);
480
4
  Node trueNode = d_nodeManager->mkConst(true);
481
  Node empty = d_nodeManager->mkConst(
482
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
483
4
  Node x = d_nodeManager->mkConst(String("x"));
484
4
  Node y = d_nodeManager->mkConst(String("y"));
485
4
  Node z = d_nodeManager->mkConst(String("z"));
486
  Node x_1 = d_nodeManager->mkBag(
487
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
488
  Node x_4 = d_nodeManager->mkBag(
489
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
490
  Node y_1 = d_nodeManager->mkBag(
491
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
492
493
4
  Node input1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, empty);
494
4
  Node output1 = falseNode;
495
2
  ASSERT_EQ(output1, NormalForm::evaluate(input1));
496
497
4
  Node input2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, x_1);
498
4
  Node output2 = trueNode;
499
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
500
501
4
  Node input3 = d_nodeManager->mkNode(BAG_IS_SINGLETON, x_4);
502
4
  Node output3 = falseNode;
503
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
504
505
4
  Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1);
506
4
  Node input4 = d_nodeManager->mkNode(BAG_IS_SINGLETON, union_disjoint);
507
4
  Node output4 = falseNode;
508
2
  ASSERT_EQ(output3, NormalForm::evaluate(input3));
509
}
510
511
24
TEST_F(TestTheoryWhiteBagsNormalForm, from_set)
512
{
513
  // Examples
514
  // --------
515
  //  - (bag.from_set (emptyset String)) = (emptybag String)
516
  //  - (bag.from_set (singleton "x")) = (mkBag "x" 1)
517
  //  - (bag.to_set (union (singleton "x") (singleton "y"))) =
518
  //     (disjoint_union (mkBag "x" 1) (mkBag "y" 1))
519
520
  Node emptyset = d_nodeManager->mkConst(
521
4
      EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType())));
522
  Node emptybag = d_nodeManager->mkConst(
523
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
524
4
  Node input1 = d_nodeManager->mkNode(BAG_FROM_SET, emptyset);
525
4
  Node output1 = emptybag;
526
2
  ASSERT_EQ(output1, NormalForm::evaluate(input1));
527
528
4
  Node x = d_nodeManager->mkConst(String("x"));
529
4
  Node y = d_nodeManager->mkConst(String("y"));
530
531
4
  Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
532
4
  Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y);
533
534
  Node x_1 = d_nodeManager->mkBag(
535
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
536
  Node y_1 = d_nodeManager->mkBag(
537
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
538
539
4
  Node input2 = d_nodeManager->mkNode(BAG_FROM_SET, xSingleton);
540
4
  Node output2 = x_1;
541
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
542
543
  // for normal sets, the first node is the largest, not smallest
544
4
  Node normalSet = d_nodeManager->mkNode(UNION, ySingleton, xSingleton);
545
4
  Node input3 = d_nodeManager->mkNode(BAG_FROM_SET, normalSet);
546
4
  Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1);
547
2
  ASSERT_EQ(output3, NormalForm::evaluate(input3));
548
}
549
550
24
TEST_F(TestTheoryWhiteBagsNormalForm, to_set)
551
{
552
  // Examples
553
  // --------
554
  //  - (bag.to_set (emptybag String)) = (emptyset String)
555
  //  - (bag.to_set (mkBag "x" 4)) = (singleton "x")
556
  //  - (bag.to_set (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) =
557
  //     (union (singleton "x") (singleton "y")))
558
559
  Node emptyset = d_nodeManager->mkConst(
560
4
      EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType())));
561
  Node emptybag = d_nodeManager->mkConst(
562
4
      EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
563
4
  Node input1 = d_nodeManager->mkNode(BAG_TO_SET, emptybag);
564
4
  Node output1 = emptyset;
565
2
  ASSERT_EQ(output1, NormalForm::evaluate(input1));
566
567
4
  Node x = d_nodeManager->mkConst(String("x"));
568
4
  Node y = d_nodeManager->mkConst(String("y"));
569
570
4
  Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
571
4
  Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y);
572
573
  Node x_4 = d_nodeManager->mkBag(
574
4
      d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
575
  Node y_5 = d_nodeManager->mkBag(
576
4
      d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5)));
577
578
4
  Node input2 = d_nodeManager->mkNode(BAG_TO_SET, x_4);
579
4
  Node output2 = xSingleton;
580
2
  ASSERT_EQ(output2, NormalForm::evaluate(input2));
581
582
  // for normal sets, the first node is the largest, not smallest
583
4
  Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5);
584
4
  Node input3 = d_nodeManager->mkNode(BAG_TO_SET, normalBag);
585
4
  Node output3 = d_nodeManager->mkNode(UNION, ySingleton, xSingleton);
586
2
  ASSERT_EQ(output3, NormalForm::evaluate(input3));
587
}
588
}  // namespace test
589
225954
}  // namespace CVC4