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 |
|
|
21 |
|
namespace cvc5 { |
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 |
20 |
class TestTheoryWhiteBagsTypeRule : public TestSmt |
32 |
|
{ |
33 |
|
protected: |
34 |
10 |
std::vector<Node> getNStrings(size_t n) |
35 |
|
{ |
36 |
10 |
std::vector<Node> elements(n); |
37 |
|
cvc5::theory::strings::StringEnumerator enumerator( |
38 |
20 |
d_nodeManager->stringType()); |
39 |
|
|
40 |
20 |
for (size_t i = 0; i < n; i++) |
41 |
|
{ |
42 |
10 |
++enumerator; |
43 |
10 |
elements[i] = *enumerator; |
44 |
|
} |
45 |
|
|
46 |
20 |
return elements; |
47 |
|
} |
48 |
|
}; |
49 |
|
|
50 |
14 |
TEST_F(TestTheoryWhiteBagsTypeRule, count_operator) |
51 |
|
{ |
52 |
4 |
std::vector<Node> elements = getNStrings(1); |
53 |
4 |
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), |
54 |
2 |
elements[0], |
55 |
10 |
d_nodeManager->mkConst(Rational(100))); |
56 |
|
|
57 |
4 |
Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag); |
58 |
4 |
Node node = d_nodeManager->mkConst(Rational(10)); |
59 |
|
|
60 |
|
// node of type Int is not compatible with bag of type (Bag String) |
61 |
2 |
ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true), |
62 |
2 |
TypeCheckingExceptionPrivate); |
63 |
|
} |
64 |
|
|
65 |
14 |
TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) |
66 |
|
{ |
67 |
4 |
std::vector<Node> elements = getNStrings(1); |
68 |
4 |
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), |
69 |
2 |
elements[0], |
70 |
10 |
d_nodeManager->mkConst(Rational(10))); |
71 |
2 |
ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag)); |
72 |
2 |
ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(), |
73 |
2 |
bag.getType()); |
74 |
|
} |
75 |
|
|
76 |
14 |
TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) |
77 |
|
{ |
78 |
4 |
std::vector<Node> elements = getNStrings(1); |
79 |
4 |
Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), |
80 |
2 |
elements[0], |
81 |
10 |
d_nodeManager->mkConst(Rational(-1))); |
82 |
4 |
Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), |
83 |
2 |
elements[0], |
84 |
10 |
d_nodeManager->mkConst(Rational(0))); |
85 |
4 |
Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), |
86 |
2 |
elements[0], |
87 |
10 |
d_nodeManager->mkConst(Rational(1))); |
88 |
|
|
89 |
|
// only positive multiplicity are constants |
90 |
2 |
ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), negative)); |
91 |
2 |
ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), zero)); |
92 |
2 |
ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), positive)); |
93 |
|
} |
94 |
|
|
95 |
14 |
TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) |
96 |
|
{ |
97 |
4 |
std::vector<Node> elements = getNStrings(1); |
98 |
|
Node set = |
99 |
4 |
d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]); |
100 |
2 |
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_FROM_SET, set)); |
101 |
2 |
ASSERT_TRUE(d_nodeManager->mkNode(BAG_FROM_SET, set).getType().isBag()); |
102 |
|
} |
103 |
|
|
104 |
14 |
TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) |
105 |
|
{ |
106 |
4 |
std::vector<Node> elements = getNStrings(1); |
107 |
4 |
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), |
108 |
2 |
elements[0], |
109 |
10 |
d_nodeManager->mkConst(Rational(10))); |
110 |
2 |
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag)); |
111 |
2 |
ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet()); |
112 |
|
} |
113 |
|
} // namespace test |
114 |
68386 |
} // namespace cvc5 |