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