google test: theory: Migrate theory_sets_type_enumerator_white. (#6000)

14 files changed, 156 insertions, 186 deletions

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 14ae782e4..d2e9b2e92 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -23,7 +23,7 @@ cvc4_add_unit_test_white(theory_bv_white theory)
 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_cxx_unit_test_white(theory_sets_type_enumerator_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_cxx_unit_test_white(theory_strings_skolem_cache_black theory)
 cvc4_add_cxx_unit_test_white(theory_strings_word_white theory)
diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp
index 039a5f12f..1ced4a584 100644
--- a/test/unit/theory/evaluator_white.cpp
+++ b/test/unit/theory/evaluator_white.cpp
@@ -27,7 +27,6 @@
 
 namespace CVC4 {
 
-using namespace smt;
 using namespace theory;
 
 namespace test {
diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp
index 9c419a28d..59f2cadb2 100644
--- a/test/unit/theory/regexp_operation_black.cpp
+++ b/test/unit/theory/regexp_operation_black.cpp
@@ -30,7 +30,6 @@
 namespace CVC4 {
 
 using namespace kind;
-using namespace smt;
 using namespace theory;
 using namespace theory::strings;
 
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index 590fa2ace..14c04c69c 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -30,7 +30,6 @@
 
 namespace CVC4 {
 
-using namespace smt;
 using namespace theory;
 using namespace theory::quantifiers;
 using namespace theory::strings;
diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp
index c7ed3e97d..80cbce88d 100644
--- a/test/unit/theory/strings_rewriter_white.cpp
+++ b/test/unit/theory/strings_rewriter_white.cpp
@@ -20,8 +20,6 @@
 
 #include "expr/node.h"
 #include "expr/node_manager.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "test_smt.h"
 #include "theory/rewriter.h"
 #include "theory/strings/strings_rewriter.h"
@@ -29,7 +27,6 @@
 namespace CVC4 {
 
 using namespace kind;
-using namespace smt;
 using namespace theory;
 using namespace theory::strings;
 
diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp
index 658571b00..2c6e00a11 100644
--- a/test/unit/theory/theory_bags_normal_form_white.cpp
+++ b/test/unit/theory/theory_bags_normal_form_white.cpp
@@ -20,7 +20,6 @@
 
 namespace CVC4 {
 
-using namespace smt;
 using namespace theory;
 using namespace kind;
 using namespace theory::bags;
diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index db8e430f3..110ab5a64 100644
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -19,7 +19,6 @@
 
 namespace CVC4 {
 
-using namespace smt;
 using namespace theory;
 using namespace kind;
 using namespace theory::bags;
diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp
index 6e2a818e0..2c28d5b2c 100644
--- a/test/unit/theory/theory_bags_type_rules_white.cpp
+++ b/test/unit/theory/theory_bags_type_rules_white.cpp
@@ -19,7 +19,6 @@
 
 namespace CVC4 {
 
-using namespace smt;
 using namespace theory;
 using namespace kind;
 using namespace theory::bags;
diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp
index 0aba243b5..9864e60af 100644
--- a/test/unit/theory/theory_black.cpp
+++ b/test/unit/theory/theory_black.cpp
@@ -28,7 +28,6 @@ namespace CVC4 {
 using namespace kind;
 using namespace context;
 using namespace theory;
-using namespace smt;
 
 namespace test {
 
diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp
index e2e4d1ddb..9a5e7bf8f 100644
--- a/test/unit/theory/theory_bv_rewriter_white.cpp
+++ b/test/unit/theory/theory_bv_rewriter_white.cpp
@@ -26,7 +26,6 @@
 namespace CVC4 {
 
 using namespace kind;
-using namespace smt;
 using namespace theory;
 
 namespace test {
diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index 0f304bfcf..92e359c8f 100644
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -33,7 +33,6 @@ using namespace theory::bv;
 using namespace theory::bv::utils;
 using namespace expr;
 using namespace context;
-using namespace smt;
 
 namespace test {
 
diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp
index c888fbf0d..baf8f4d9c 100644
--- a/test/unit/theory/theory_engine_white.cpp
+++ b/test/unit/theory/theory_engine_white.cpp
@@ -43,7 +43,6 @@ using namespace theory;
 using namespace expr;
 using namespace context;
 using namespace kind;
-using namespace smt;
 using namespace theory::bv;
 
 namespace test {
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp
new file mode 100644
index 000000000..4338e9fa2
--- /dev/null
+++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp
@@ -0,0 +1,155 @@
+/*********************                                                        */
+/*! \file theory_sets_type_enumerator_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds, 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 CVC4::theory::sets::SetsTypeEnumerator
+ **
+ ** White box testing of CVC4::theory::sets::SetsTypeEnumerator.  (These tests
+ ** depends  on the ordering that the SetsTypeEnumerator use, so it's a
+ *white-box
+ ** test.)
+ **/
+
+#include "expr/dtype.h"
+#include "test_smt.h"
+#include "theory/sets/theory_sets_type_enumerator.h"
+
+namespace CVC4 {
+
+using namespace theory;
+using namespace kind;
+using namespace theory::sets;
+
+namespace test {
+
+class TestTheoryWhiteSetsTypeEnumerator : public TestSmt
+{
+ protected:
+  void addAndCheckUnique(Node n, std::vector<Node>& elems)
+  {
+    ASSERT_TRUE(n.isConst());
+    ASSERT_TRUE(std::find(elems.begin(), elems.end(), n) == elems.end());
+    elems.push_back(n);
+  }
+};
+
+TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_booleans)
+{
+  TypeNode boolType = d_nodeManager->booleanType();
+  SetEnumerator setEnumerator(d_nodeManager->mkSetType(boolType));
+  ASSERT_FALSE(setEnumerator.isFinished());
+
+  std::vector<Node> elems;
+
+  Node actual0 = *setEnumerator;
+  addAndCheckUnique(actual0, elems);
+  ASSERT_FALSE(setEnumerator.isFinished());
+
+  Node actual1 = *++setEnumerator;
+  addAndCheckUnique(actual1, elems);
+  ASSERT_FALSE(setEnumerator.isFinished());
+
+  Node actual2 = *++setEnumerator;
+  addAndCheckUnique(actual2, elems);
+  ASSERT_FALSE(setEnumerator.isFinished());
+
+  Node actual3 = Rewriter::rewrite(*++setEnumerator);
+  addAndCheckUnique(actual3, elems);
+  ASSERT_FALSE(setEnumerator.isFinished());
+
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+}
+
+TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_UF)
+{
+  TypeNode sort = d_nodeManager->mkSort("Atom");
+  SetEnumerator setEnumerator(d_nodeManager->mkSetType(sort));
+
+  Node actual0 = *setEnumerator;
+  Node expected0 =
+      d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(sort)));
+  ASSERT_EQ(expected0, actual0);
+  ASSERT_FALSE(setEnumerator.isFinished());
+
+  std::vector<Node> elems;
+  for (unsigned i = 0; i < 7; i++)
+  {
+    Node actual = *setEnumerator;
+    addAndCheckUnique(actual, elems);
+    ASSERT_FALSE(setEnumerator.isFinished());
+    ++setEnumerator;
+  }
+}
+
+TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_finite_dataype)
+{
+  DType dt("Colors");
+  dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
+  dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
+  dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+  TypeNode datatype = d_nodeManager->mkDatatypeType(dt);
+  const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
+      datatype.getDType().getConstructors();
+  SetEnumerator setEnumerator(d_nodeManager->mkSetType(datatype));
+
+  Node red =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor());
+
+  Node green =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor());
+
+  Node blue =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor());
+
+  std::vector<Node> elems;
+  for (unsigned i = 0; i < 8; i++)
+  {
+    Node actual = *setEnumerator;
+    addAndCheckUnique(actual, elems);
+    ASSERT_FALSE(setEnumerator.isFinished());
+    ++setEnumerator;
+  }
+
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+}
+
+TEST_F(TestTheoryWhiteSetsTypeEnumerator, bv)
+{
+  TypeNode bitVector2 = d_nodeManager->mkBitVectorType(2);
+  SetEnumerator setEnumerator(d_nodeManager->mkSetType(bitVector2));
+
+  std::vector<Node> elems;
+  for (unsigned i = 0; i < 16; i++)
+  {
+    Node actual = *setEnumerator;
+    addAndCheckUnique(actual, elems);
+    ASSERT_FALSE(setEnumerator.isFinished());
+    ++setEnumerator;
+  }
+
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
+  ASSERT_TRUE(setEnumerator.isFinished());
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
deleted file mode 100644
index a100984ba..000000000
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ /dev/null
@@ -1,172 +0,0 @@
-/*********************                                                        */
-/*! \file theory_sets_type_enumerator_white.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mudathir Mohamed, Andrew Reynolds, Andres Noetzli
- ** 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 CVC4::theory::sets::SetEnumerator
- **
- ** White box testing of CVC4::theory::sets::SetEnumerator.  (These tests
- ** depends  on the ordering that the SetEnumerator use, so it's a white-box
- *  test.)
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "expr/dtype.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/sets/theory_sets_type_enumerator.h"
-
-using namespace CVC4;
-using namespace CVC4::smt;
-using namespace CVC4::theory;
-using namespace CVC4::kind;
-using namespace CVC4::theory::sets;
-using namespace std;
-
-class SetEnumeratorWhite : public CxxTest::TestSuite
-{
- public:
-  void setUp() override
-  {
-    d_em = new ExprManager();
-    d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_nm);
-    d_scope = new SmtScope(d_smt);
-    d_smt->finishInit();
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_smt;
-    delete d_em;
-  }
-
-  void addAndCheckUnique(Node n, std::vector<Node>& elems)
-  {
-    TS_ASSERT(n.isConst());
-    TS_ASSERT(std::find(elems.begin(), elems.end(), n) == elems.end());
-    elems.push_back(n);
-  }
-
-  void testSetOfBooleans()
-  {
-    TypeNode boolType = d_nm->booleanType();
-    SetEnumerator setEnumerator(d_nm->mkSetType(boolType));
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    std::vector<Node> elems;
-
-    Node actual0 = *setEnumerator;
-    addAndCheckUnique(actual0, elems);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual1 = *++setEnumerator;
-    addAndCheckUnique(actual1, elems);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual2 = *++setEnumerator;
-    addAndCheckUnique(actual2, elems);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual3 = Rewriter::rewrite(*++setEnumerator);
-    addAndCheckUnique(actual3, elems);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-  }
-
-  void testSetOfUF()
-  {
-    TypeNode sort = d_nm->mkSort("Atom");
-    SetEnumerator setEnumerator(d_nm->mkSetType(sort));
-
-    Node actual0 = *setEnumerator;
-    Node expected0 = d_nm->mkConst(EmptySet(d_nm->mkSetType(sort)));
-    TS_ASSERT_EQUALS(expected0, actual0);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    std::vector<Node> elems;
-    for (unsigned i = 0; i < 7; i++)
-    {
-      Node actual = *setEnumerator;
-      addAndCheckUnique(actual, elems);
-      TS_ASSERT(!setEnumerator.isFinished());
-      ++setEnumerator;
-    }
-  }
-
-  void testSetOfFiniteDatatype()
-  {
-    DType dt("Colors");
-    dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
-    dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
-    dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
-    TypeNode datatype = d_nm->mkDatatypeType(dt);
-    const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
-        datatype.getDType().getConstructors();
-    SetEnumerator setEnumerator(d_nm->mkSetType(datatype));
-
-    Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor());
-
-    Node green = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor());
-
-    Node blue = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor());
-
-    std::vector<Node> elems;
-    for (unsigned i = 0; i < 8; i++)
-    {
-      Node actual = *setEnumerator;
-      addAndCheckUnique(actual, elems);
-      TS_ASSERT(!setEnumerator.isFinished());
-      ++setEnumerator;
-    }
-
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-  }
-
-  void testBV()
-  {
-    TypeNode bitVector2 = d_nm->mkBitVectorType(2);
-    SetEnumerator setEnumerator(d_nm->mkSetType(bitVector2));
-
-    std::vector<Node> elems;
-    for (unsigned i = 0; i < 16; i++)
-    {
-      Node actual = *setEnumerator;
-      addAndCheckUnique(actual, elems);
-      TS_ASSERT(!setEnumerator.isFinished());
-      ++setEnumerator;
-    }
-
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-    TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
-    TS_ASSERT(setEnumerator.isFinished());
-  }
-
- private:
-  ExprManager* d_em;
-  SmtEngine* d_smt;
-  NodeManager* d_nm;
-  SmtScope* d_scope;
-}; /* class SetEnumeratorWhite */