google test: theory: Migrate theory_bags_type_rules_white. (#5984)

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index c135c4a943b964501aec41ca745cc4508f8b4854..8e7951f173ae61f2386e544b9c8cabc89b2b830b 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -17,7 +17,7 @@ cvc4_add_unit_test_white(strings_rewriter_white theory)
 cvc4_add_unit_test_white(theory_arith_white theory)
 cvc4_add_unit_test_white(theory_bags_normal_form_white theory)
 cvc4_add_unit_test_white(theory_bags_rewriter_white theory)
-cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory)
+cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
 cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory)
 cvc4_add_cxx_unit_test_white(theory_bv_white theory)
 cvc4_add_unit_test_white(theory_engine_white theory)

diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp
new file mode 100644 (file)
index 0000000..6e2a818
--- /dev/null
+++ b/test/unit/theory/theory_bags_type_rules_white.cpp
@@ -0,0 +1,114 @@
+/*********************                                                        */
+/*! \file theory_bags_type_rules_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of bags typing rules
+ **/
+
+#include "expr/dtype.h"
+#include "test_smt.h"
+#include "theory/bags/theory_bags_type_rules.h"
+#include "theory/strings/type_enumerator.h"
+
+namespace CVC4 {
+
+using namespace smt;
+using namespace theory;
+using namespace kind;
+using namespace theory::bags;
+
+namespace test {
+
+typedef expr::Attribute<Node, Node> attribute;
+
+class TestTheoryWhiteBagsTypeRule : public TestSmt
+{
+ protected:
+  std::vector<Node> getNStrings(size_t n)
+  {
+    std::vector<Node> elements(n);
+    CVC4::theory::strings::StringEnumerator enumerator(
+        d_nodeManager->stringType());
+
+    for (size_t i = 0; i < n; i++)
+    {
+      ++enumerator;
+      elements[i] = *enumerator;
+    }
+
+    return elements;
+  }
+};
+
+TEST_F(TestTheoryWhiteBagsTypeRule, count_operator)
+{
+  std::vector<Node> elements = getNStrings(1);
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                  elements[0],
+                                  d_nodeManager->mkConst(Rational(100)));
+
+  Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag);
+  Node node = d_nodeManager->mkConst(Rational(10));
+
+  // node of type Int is not compatible with bag of type (Bag String)
+  ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true),
+               TypeCheckingExceptionPrivate);
+}
+
+TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator)
+{
+  std::vector<Node> elements = getNStrings(1);
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                  elements[0],
+                                  d_nodeManager->mkConst(Rational(10)));
+  ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag));
+  ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(),
+            bag.getType());
+}
+
+TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator)
+{
+  std::vector<Node> elements = getNStrings(1);
+  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       elements[0],
+                                       d_nodeManager->mkConst(Rational(-1)));
+  Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                   elements[0],
+                                   d_nodeManager->mkConst(Rational(0)));
+  Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       elements[0],
+                                       d_nodeManager->mkConst(Rational(1)));
+
+  // only positive multiplicity are constants
+  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), negative));
+  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), zero));
+  ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), positive));
+}
+
+TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator)
+{
+  std::vector<Node> elements = getNStrings(1);
+  Node set =
+      d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]);
+  ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_FROM_SET, set));
+  ASSERT_TRUE(d_nodeManager->mkNode(BAG_FROM_SET, set).getType().isBag());
+}
+
+TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator)
+{
+  std::vector<Node> elements = getNStrings(1);
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                  elements[0],
+                                  d_nodeManager->mkConst(Rational(10)));
+  ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag));
+  ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet());
+}
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h
deleted file mode 100644 (file)
index 825e526..0000000
--- a/test/unit/theory/theory_bags_type_rules_white.h
+++ /dev/null
@@ -1,123 +0,0 @@
-/*********************                                                        */
-/*! \file theory_bags_type_rules_white.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mudathir Mohamed, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of bags typing rules
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "expr/dtype.h"
-#include "smt/smt_engine.h"
-#include "theory/bags/theory_bags_type_rules.h"
-#include "theory/strings/type_enumerator.h"
-
-using namespace CVC4;
-using namespace CVC4::smt;
-using namespace CVC4::theory;
-using namespace CVC4::kind;
-using namespace CVC4::theory::bags;
-using namespace std;
-
-typedef expr::Attribute<Node, Node> attribute;
-
-class BagsTypeRuleWhite : public CxxTest::TestSuite
-{
- public:
-  void setUp() override
-  {
-    d_em.reset(new ExprManager());
-    d_nm.reset(NodeManager::fromExprManager(d_em.get()));
-    d_smt.reset(new SmtEngine(d_nm.get()));
-    d_smt->finishInit();
-  }
-
-  void tearDown() override
-  {
-    d_smt.reset();
-    d_nm.release();
-    d_em.reset();
-  }
-
-  std::vector<Node> getNStrings(size_t n)
-  {
-    std::vector<Node> elements(n);
-    CVC4::theory::strings::StringEnumerator enumerator(d_nm->stringType());
-
-    for (size_t i = 0; i < n; i++)
-    {
-      ++enumerator;
-      elements[i] = *enumerator;
-    }
-
-    return elements;
-  }
-
-  void testCountOperator()
-  {
-    vector<Node> elements = getNStrings(1);
-    Node bag = d_nm->mkBag(
-        d_nm->stringType(), elements[0], d_nm->mkConst(Rational(100)));
-
-    Node count = d_nm->mkNode(BAG_COUNT, elements[0], bag);
-    Node node = d_nm->mkConst(Rational(10));
-
-    // node of type Int is not compatible with bag of type (Bag String)
-    TS_ASSERT_THROWS(d_nm->mkNode(BAG_COUNT, node, bag).getType(true),
-                     TypeCheckingExceptionPrivate&);
-  }
-
-  void testDuplicateRemovalOperator()
-  {
-    vector<Node> elements = getNStrings(1);
-    Node bag = d_nm->mkBag(
-        d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10)));
-    TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(DUPLICATE_REMOVAL, bag));
-    TS_ASSERT(d_nm->mkNode(DUPLICATE_REMOVAL, bag).getType() == bag.getType());
-  }
-
-  void testMkBagOperator()
-  {
-    vector<Node> elements = getNStrings(1);
-    Node negative = d_nm->mkBag(
-        d_nm->stringType(), elements[0], d_nm->mkConst(Rational(-1)));
-    Node zero = d_nm->mkBag(
-        d_nm->stringType(), elements[0], d_nm->mkConst(Rational(0)));
-    Node positive = d_nm->mkBag(
-        d_nm->stringType(), elements[0], d_nm->mkConst(Rational(1)));
-
-    // only positive multiplicity are constants
-    TS_ASSERT(!MkBagTypeRule::computeIsConst(d_nm.get(), negative));
-    TS_ASSERT(!MkBagTypeRule::computeIsConst(d_nm.get(), zero));
-    TS_ASSERT(MkBagTypeRule::computeIsConst(d_nm.get(), positive));
-  }
-
-  void testFromSetOperator()
-  {
-    vector<Node> elements = getNStrings(1);
-    Node set = d_nm->mkSingleton(d_nm->stringType(), elements[0]);
-    TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(BAG_FROM_SET, set));
-    TS_ASSERT(d_nm->mkNode(BAG_FROM_SET, set).getType().isBag());
-  }
-
-  void testToSetOperator()
-  {
-    vector<Node> elements = getNStrings(1);
-    Node bag = d_nm->mkBag(
-        d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10)));
-    TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(BAG_TO_SET, bag));
-    TS_ASSERT(d_nm->mkNode(BAG_TO_SET, bag).getType().isSet());
-  }
-
- private:
-  std::unique_ptr<ExprManager> d_em;
-  std::unique_ptr<SmtEngine> d_smt;
-  std::unique_ptr<NodeManager> d_nm;
-}; /* class BagsTypeRuleBlack */