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