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 |
20 |
class TestTheoryWhiteBagsTypeRule : public TestSmt |
33 |
|
{ |
34 |
|
protected: |
35 |
10 |
std::vector<Node> getNStrings(size_t n) |
36 |
|
{ |
37 |
10 |
std::vector<Node> elements(n); |
38 |
|
cvc5::theory::strings::StringEnumerator enumerator( |
39 |
20 |
d_nodeManager->stringType()); |
40 |
|
|
41 |
20 |
for (size_t i = 0; i < n; i++) |
42 |
|
{ |
43 |
10 |
++enumerator; |
44 |
10 |
elements[i] = *enumerator; |
45 |
|
} |
46 |
|
|
47 |
20 |
return elements; |
48 |
|
} |
49 |
|
}; |
50 |
|
|
51 |
14 |
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 |
14 |
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 |
14 |
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 |
14 |
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 |
14 |
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 |
|
} // namespace test |
115 |
69576 |
} // namespace cvc5 |