GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_bags_type_rules_white.cpp Lines: 52 52 100.0 %
Date: 2021-03-23 Branches: 136 352 38.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bags_type_rules_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Mudathir Mohamed
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Black box testing of bags typing rules
13
 **/
14
15
#include "expr/dtype.h"
16
#include "test_smt.h"
17
#include "theory/bags/theory_bags_type_rules.h"
18
#include "theory/strings/type_enumerator.h"
19
20
namespace CVC4 {
21
22
using namespace theory;
23
using namespace kind;
24
using namespace theory::bags;
25
26
namespace test {
27
28
typedef expr::Attribute<Node, Node> attribute;
29
30
20
class TestTheoryWhiteBagsTypeRule : public TestSmt
31
{
32
 protected:
33
10
  std::vector<Node> getNStrings(size_t n)
34
  {
35
10
    std::vector<Node> elements(n);
36
    CVC4::theory::strings::StringEnumerator enumerator(
37
20
        d_nodeManager->stringType());
38
39
20
    for (size_t i = 0; i < n; i++)
40
    {
41
10
      ++enumerator;
42
10
      elements[i] = *enumerator;
43
    }
44
45
20
    return elements;
46
  }
47
};
48
49
14
TEST_F(TestTheoryWhiteBagsTypeRule, count_operator)
50
{
51
4
  std::vector<Node> elements = getNStrings(1);
52
4
  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
53
2
                                  elements[0],
54
10
                                  d_nodeManager->mkConst(Rational(100)));
55
56
4
  Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag);
57
4
  Node node = d_nodeManager->mkConst(Rational(10));
58
59
  // node of type Int is not compatible with bag of type (Bag String)
60
2
  ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true),
61
2
               TypeCheckingExceptionPrivate);
62
}
63
64
14
TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator)
65
{
66
4
  std::vector<Node> elements = getNStrings(1);
67
4
  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
68
2
                                  elements[0],
69
10
                                  d_nodeManager->mkConst(Rational(10)));
70
2
  ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag));
71
2
  ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(),
72
2
            bag.getType());
73
}
74
75
14
TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator)
76
{
77
4
  std::vector<Node> elements = getNStrings(1);
78
4
  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
79
2
                                       elements[0],
80
10
                                       d_nodeManager->mkConst(Rational(-1)));
81
4
  Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
82
2
                                   elements[0],
83
10
                                   d_nodeManager->mkConst(Rational(0)));
84
4
  Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
85
2
                                       elements[0],
86
10
                                       d_nodeManager->mkConst(Rational(1)));
87
88
  // only positive multiplicity are constants
89
2
  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), negative));
90
2
  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), zero));
91
2
  ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), positive));
92
}
93
94
14
TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator)
95
{
96
4
  std::vector<Node> elements = getNStrings(1);
97
  Node set =
98
4
      d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]);
99
2
  ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_FROM_SET, set));
100
2
  ASSERT_TRUE(d_nodeManager->mkNode(BAG_FROM_SET, set).getType().isBag());
101
}
102
103
14
TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator)
104
{
105
4
  std::vector<Node> elements = getNStrings(1);
106
4
  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
107
2
                                  elements[0],
108
10
                                  d_nodeManager->mkConst(Rational(10)));
109
2
  ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag));
110
2
  ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet());
111
}
112
}  // namespace test
113
69200
}  // namespace CVC4