google test: theory: Migrate theory_sets_type_rules_white. (#6001)

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index d2e9b2e92b4215cd592f4cbebdbbfe2bf6a35c76..90155518ef43949dc18a9babd76ccfe34c5a9590 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -24,7 +24,7 @@ cvc4_add_unit_test_white(theory_engine_white theory)
 cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
 cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory)
 cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
-cvc4_add_cxx_unit_test_white(theory_sets_type_rules_white theory)
+cvc4_add_unit_test_white(theory_sets_type_rules_white theory)
 cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory)
 cvc4_add_cxx_unit_test_white(theory_strings_word_white theory)
 cvc4_add_cxx_unit_test_white(theory_white theory)

diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp
new file mode 100644 (file)
index 0000000..3c1d64b
--- /dev/null
+++ b/test/unit/theory/theory_sets_type_rules_white.cpp
@@ -0,0 +1,86 @@
+/*********************                                                        */
+/*! \file theory_sets_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 White box testing of sets typing rules
+ **/
+
+#include "expr/dtype.h"
+#include "test_api.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace CVC4::api;
+
+namespace test {
+
+class TestTheoryWhiteSetsTypeRuleApi : public TestApi
+{
+};
+class TestTheoryWhiteSetsTypeRuleInternal : public TestNode
+{
+};
+
+TEST_F(TestTheoryWhiteSetsTypeRuleInternal, is_comparable_to)
+{
+  TypeNode setRealType = d_nodeManager->mkSetType(d_nodeManager->realType());
+  TypeNode setIntType = d_nodeManager->mkSetType(d_nodeManager->integerType());
+  ASSERT_FALSE(setIntType.isComparableTo(setRealType));
+  ASSERT_FALSE(setIntType.isSubtypeOf(setRealType));
+  ASSERT_FALSE(setRealType.isComparableTo(setIntType));
+  ASSERT_FALSE(setRealType.isComparableTo(setIntType));
+}
+
+TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term)
+{
+  Sort realSort = d_solver.getRealSort();
+  Sort intSort = d_solver.getIntegerSort();
+  Term emptyReal = d_solver.mkEmptySet(d_solver.mkSetSort(realSort));
+  Term integerOne = d_solver.mkInteger(1);
+  Term realOne = d_solver.mkReal(1);
+  Term singletonInt = d_solver.mkTerm(api::SINGLETON, integerOne);
+  Term singletonReal = d_solver.mkTerm(api::SINGLETON, realOne);
+  // (union
+  //    (singleton (singleton_op Int) 1)
+  //    (as emptyset (Set Real)))
+  ASSERT_THROW(d_solver.mkTerm(UNION, singletonInt, emptyReal),
+               CVC4ApiException);
+  // (union
+  //    (singleton (singleton_op Real) 1)
+  //    (as emptyset (Set Real)))
+  ASSERT_NO_THROW(d_solver.mkTerm(UNION, singletonReal, emptyReal));
+}
+
+TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node)
+{
+  Node singletonInt =
+      d_nodeManager->mkConst(SingletonOp(d_nodeManager->integerType()));
+  Node singletonReal =
+      d_nodeManager->mkConst(SingletonOp(d_nodeManager->realType()));
+  Node intConstant = d_nodeManager->mkConst(Rational(1));
+  Node realConstant = d_nodeManager->mkConst(Rational(1, 5));
+  // (singleton (singleton_op Real) 1)
+  ASSERT_NO_THROW(
+      d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant));
+  // (singleton (singleton_op Int) (/ 1 5))
+  ASSERT_DEATH(
+      d_nodeManager->mkSingleton(d_nodeManager->integerType(), realConstant),
+      "Invalid operands for mkSingleton");
+
+  Node n = d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant);
+  // the type of (singleton (singleton_op Real) 1) is (Set Real)
+  ASSERT_TRUE(n.getType()
+              == d_nodeManager->mkSetType(d_nodeManager->realType()));
+  // (singleton (singleton_op Real) 1) is a constant in normal form
+  ASSERT_TRUE(n.isConst());
+}
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
deleted file mode 100644 (file)
index 4d60dea..0000000
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ /dev/null
@@ -1,100 +0,0 @@
-/*********************                                                        */
-/*! \file theory_sets_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 White box testing of sets typing rules
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-#include "expr/dtype.h"
-#include "smt/smt_engine.h"
-
-using namespace CVC4;
-using namespace CVC4::api;
-
-class SetsTypeRuleWhite : public CxxTest::TestSuite
-{
- public:
-  void setUp() override
-  {
-    d_slv.reset(new Solver());
-    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_slv.reset();
-    d_smt.reset();
-    d_nm.release();
-    d_em.reset();
-  }
-
-  void testIsisComparableTo()
-  {
-    TypeNode setRealType = d_nm->mkSetType(d_nm->realType());
-    TypeNode setIntType = d_nm->mkSetType(d_nm->integerType());
-    TS_ASSERT(!setIntType.isComparableTo(setRealType));
-    TS_ASSERT(!setIntType.isSubtypeOf(setRealType));
-    TS_ASSERT(!setRealType.isComparableTo(setIntType));
-    TS_ASSERT(!setRealType.isComparableTo(setIntType));
-  }
-
-  void testSingletonTerm()
-  {
-    Sort realSort = d_slv->getRealSort();
-    Sort intSort = d_slv->getIntegerSort();
-    Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort));
-    Term integerOne = d_slv->mkInteger(1);
-    Term realOne = d_slv->mkReal(1);
-    Term singletonInt = d_slv->mkTerm(api::SINGLETON, integerOne);
-    Term singletonReal = d_slv->mkTerm(api::SINGLETON, realOne);
-    // (union
-    //    (singleton (singleton_op Int) 1)
-    //    (as emptyset (Set Real)))
-    TS_ASSERT_THROWS(d_slv->mkTerm(UNION, singletonInt, emptyReal),
-                     CVC4ApiException&);
-    // (union
-    //    (singleton (singleton_op Real) 1)
-    //    (as emptyset (Set Real)))
-    TS_ASSERT_THROWS_NOTHING(d_slv->mkTerm(UNION, singletonReal, emptyReal));
-  }
-
-  void testSingletonNode()
-  {
-    Node singletonInt = d_nm->mkConst(SingletonOp(d_nm->integerType()));
-    Node singletonReal = d_nm->mkConst(SingletonOp(d_nm->realType()));
-    Node intConstant = d_nm->mkConst(Rational(1));
-    Node realConstant = d_nm->mkConst(Rational(1, 5));
-    // (singleton (singleton_op Real) 1)
-    TS_ASSERT_THROWS_NOTHING(
-        d_nm->mkSingleton(d_nm->realType(), intConstant));
-    // (singleton (singleton_op Int) (/ 1 5))
-    // This fails now with the assertions. cxxtest does not catch that.
-    // TS_ASSERT_THROWS(d_nm->mkSingleton(d_nm->integerType(), realConstant),
-    //                 Exception);
-
-    Node n = d_nm->mkSingleton(d_nm->realType(), intConstant);
-    // the type of (singleton (singleton_op Real) 1) is (Set Real)
-    TS_ASSERT(n.getType() == d_nm->mkSetType(d_nm->realType()));
-    // (singleton (singleton_op Real) 1) is a constant in normal form
-    TS_ASSERT(n.isConst());
-  }
-
- private:
-  std::unique_ptr<Solver> d_slv;
-  std::unique_ptr<ExprManager> d_em;
-  std::unique_ptr<SmtEngine> d_smt;
-  std::unique_ptr<NodeManager> d_nm;
-}; /* class SetsTypeRuleWhite */