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 |
|
* Black box testing of bags typing rules |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "expr/dtype.h" |
17 |
|
#include "test_smt.h" |
18 |
|
#include "theory/bags/theory_bags_type_rules.h" |
19 |
|
#include "theory/strings/type_enumerator.h" |
20 |
|
#include "util/rational.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 |
24 |
class TestTheoryWhiteBagsTypeRule : public TestSmt |
33 |
|
{ |
34 |
|
protected: |
35 |
12 |
std::vector<Node> getNStrings(size_t n) |
36 |
|
{ |
37 |
12 |
std::vector<Node> elements(n); |
38 |
|
cvc5::theory::strings::StringEnumerator enumerator( |
39 |
24 |
d_nodeManager->stringType()); |
40 |
|
|
41 |
24 |
for (size_t i = 0; i < n; i++) |
42 |
|
{ |
43 |
12 |
++enumerator; |
44 |
12 |
elements[i] = *enumerator; |
45 |
|
} |
46 |
|
|
47 |
24 |
return elements; |
48 |
|
} |
49 |
|
}; |
50 |
|
|
51 |
15 |
TEST_F(TestTheoryWhiteBagsTypeRule, count_operator) |
52 |
|
{ |
53 |
4 |
std::vector<Node> elements = getNStrings(1); |
54 |
4 |
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), |
55 |
2 |
elements[0], |
56 |
10 |
d_nodeManager->mkConst(Rational(100))); |
57 |
|
|
58 |
4 |
Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag); |
59 |
4 |
Node node = d_nodeManager->mkConst(Rational(10)); |
60 |
|
|
61 |
|
// node of type Int is not compatible with bag of type (Bag String) |
62 |
2 |
ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true), |
63 |
2 |
TypeCheckingExceptionPrivate); |
64 |
|
} |
65 |
|
|
66 |
15 |
TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) |
67 |
|
{ |
68 |
4 |
std::vector<Node> elements = getNStrings(1); |
69 |
4 |
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), |
70 |
2 |
elements[0], |
71 |
10 |
d_nodeManager->mkConst(Rational(10))); |
72 |
2 |
ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag)); |
73 |
2 |
ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(), |
74 |
2 |
bag.getType()); |
75 |
|
} |
76 |
|
|
77 |
15 |
TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) |
78 |
|
{ |
79 |
4 |
std::vector<Node> elements = getNStrings(1); |
80 |
4 |
Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), |
81 |
2 |
elements[0], |
82 |
10 |
d_nodeManager->mkConst(Rational(-1))); |
83 |
4 |
Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), |
84 |
2 |
elements[0], |
85 |
10 |
d_nodeManager->mkConst(Rational(0))); |
86 |
4 |
Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), |
87 |
2 |
elements[0], |
88 |
10 |
d_nodeManager->mkConst(Rational(1))); |
89 |
|
|
90 |
|
// only positive multiplicity are constants |
91 |
2 |
ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), negative)); |
92 |
2 |
ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), zero)); |
93 |
2 |
ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), positive)); |
94 |
|
} |
95 |
|
|
96 |
15 |
TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) |
97 |
|
{ |
98 |
4 |
std::vector<Node> elements = getNStrings(1); |
99 |
|
Node set = |
100 |
4 |
d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]); |
101 |
2 |
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_FROM_SET, set)); |
102 |
2 |
ASSERT_TRUE(d_nodeManager->mkNode(BAG_FROM_SET, set).getType().isBag()); |
103 |
|
} |
104 |
|
|
105 |
15 |
TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) |
106 |
|
{ |
107 |
4 |
std::vector<Node> elements = getNStrings(1); |
108 |
4 |
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), |
109 |
2 |
elements[0], |
110 |
10 |
d_nodeManager->mkConst(Rational(10))); |
111 |
2 |
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag)); |
112 |
2 |
ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet()); |
113 |
|
} |
114 |
|
|
115 |
15 |
TEST_F(TestTheoryWhiteBagsTypeRule, map_operator) |
116 |
|
{ |
117 |
4 |
std::vector<Node> elements = getNStrings(1); |
118 |
4 |
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), |
119 |
2 |
elements[0], |
120 |
10 |
d_nodeManager->mkConst(Rational(10))); |
121 |
|
Node set = |
122 |
4 |
d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]); |
123 |
|
|
124 |
4 |
Node x1 = d_nodeManager->mkBoundVar("x", d_nodeManager->stringType()); |
125 |
4 |
Node length = d_nodeManager->mkNode(STRING_LENGTH, x1); |
126 |
4 |
std::vector<Node> args1; |
127 |
2 |
args1.push_back(x1); |
128 |
4 |
Node bound1 = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, args1); |
129 |
4 |
Node lambda1 = d_nodeManager->mkNode(LAMBDA, bound1, length); |
130 |
|
|
131 |
2 |
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_MAP, lambda1, bag)); |
132 |
4 |
Node mappedBag = d_nodeManager->mkNode(BAG_MAP, lambda1, bag); |
133 |
2 |
ASSERT_TRUE(mappedBag.getType().isBag()); |
134 |
2 |
ASSERT_EQ(d_nodeManager->integerType(), |
135 |
2 |
mappedBag.getType().getBagElementType()); |
136 |
|
|
137 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
138 |
4 |
Node x2 = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType()); |
139 |
4 |
std::vector<Node> args2; |
140 |
2 |
args2.push_back(x2); |
141 |
4 |
Node bound2 = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, args2); |
142 |
4 |
Node lambda2 = d_nodeManager->mkNode(LAMBDA, bound2, one); |
143 |
2 |
ASSERT_THROW(d_nodeManager->mkNode(BAG_MAP, lambda2, bag).getType(true), |
144 |
2 |
TypeCheckingExceptionPrivate); |
145 |
2 |
ASSERT_THROW(d_nodeManager->mkNode(BAG_MAP, lambda2, set).getType(true), |
146 |
2 |
TypeCheckingExceptionPrivate); |
147 |
|
} |
148 |
|
|
149 |
|
} // namespace test |
150 |
84607 |
} // namespace cvc5 |