google test: theory: Migrate type_enumerator_white. (#6007)

3 files changed, 336 insertions, 305 deletions

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 90155518e..32219e232 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -28,4 +28,4 @@ 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)
-cvc4_add_cxx_unit_test_white(type_enumerator_white theory)
+cvc4_add_unit_test_white(type_enumerator_white theory)
diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp
new file mode 100644
index 000000000..0693d7d35
--- /dev/null
+++ b/test/unit/theory/type_enumerator_white.cpp
@@ -0,0 +1,335 @@
+/*********************                                                        */
+/*! \file type_enumerator_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds, Morgan Deters
+ ** 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::TypeEnumerator
+ **
+ ** White box testing of CVC4::theory::TypeEnumerator.  (These tests depends
+ ** on the ordering that the TypeEnumerators use, so it's a white-box test.)
+ **/
+
+#include <unordered_set>
+
+#include "expr/array_store_all.h"
+#include "expr/dtype.h"
+#include "expr/kind.h"
+#include "expr/type_node.h"
+#include "options/language.h"
+#include "test_smt.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+
+using namespace theory;
+using namespace kind;
+
+namespace test {
+
+class TestTheoryWhiteTypeEnumerator : public TestSmt
+{
+};
+
+TEST_F(TestTheoryWhiteTypeEnumerator, booleans)
+{
+  TypeEnumerator te(d_nodeManager->booleanType());
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*te, d_nodeManager->mkConst(false));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(true));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_THROW(*++te, NoMoreValuesException);
+  ASSERT_TRUE(te.isFinished());
+  ASSERT_THROW(*++te, NoMoreValuesException);
+  ASSERT_TRUE(te.isFinished());
+  ASSERT_THROW(*++te, NoMoreValuesException);
+  ASSERT_TRUE(te.isFinished());
+}
+
+TEST_F(TestTheoryWhiteTypeEnumerator, uf)
+{
+  TypeNode sort = d_nodeManager->mkSort("T");
+  TypeNode sort2 = d_nodeManager->mkSort("U");
+  TypeEnumerator te(sort);
+  ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, 0)));
+  for (size_t i = 1; i < 100; ++i)
+  {
+    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i)));
+    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort2, i)));
+    ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedConstant(sort, i)));
+    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i + 2)));
+  }
+}
+
+TEST_F(TestTheoryWhiteTypeEnumerator, arith)
+{
+  TypeEnumerator te(d_nodeManager->integerType());
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0)));
+  for (int i = 1; i <= 100; ++i)
+  {
+    ASSERT_FALSE(te.isFinished());
+    ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(i)));
+    ASSERT_FALSE(te.isFinished());
+    ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-i)));
+  }
+  ASSERT_FALSE(te.isFinished());
+
+  te = TypeEnumerator(d_nodeManager->realType());
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 3)));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 4)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 4)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 1)));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(6, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-6, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 4)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 4)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 6)));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 6)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(7, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-7, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 7)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 7)));
+  ASSERT_FALSE(te.isFinished());
+}
+
+TEST_F(TestTheoryWhiteTypeEnumerator, dtypes_finite)
+{
+  DType dt("Colors");
+  dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
+  dt.addConstructor(std::make_shared<DTypeConstructor>("orange"));
+  dt.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
+  dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
+  dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+  dt.addConstructor(std::make_shared<DTypeConstructor>("violet"));
+  TypeNode datatype = d_nodeManager->mkDatatypeType(dt);
+  const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
+      datatype.getDType().getConstructors();
+  TypeEnumerator te(datatype);
+  ASSERT_EQ(
+      *te,
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor()));
+  ASSERT_EQ(
+      *++te,
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor()));
+  ASSERT_EQ(
+      *++te,
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor()));
+  ASSERT_EQ(
+      *++te,
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor()));
+  ASSERT_EQ(
+      *++te,
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor()));
+  ASSERT_EQ(
+      *++te,
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor()));
+  ASSERT_THROW(*++te, NoMoreValuesException);
+  ASSERT_THROW(*++te, NoMoreValuesException);
+  ASSERT_THROW(*++te, NoMoreValuesException);
+}
+
+TEST_F(TestTheoryWhiteTypeEnumerator, dtypes_infinite)
+{
+  DType colors("Colors");
+  colors.addConstructor(std::make_shared<DTypeConstructor>("red"));
+  colors.addConstructor(std::make_shared<DTypeConstructor>("orange"));
+  colors.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
+  colors.addConstructor(std::make_shared<DTypeConstructor>("green"));
+  colors.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+  colors.addConstructor(std::make_shared<DTypeConstructor>("violet"));
+  TypeNode colorsType = d_nodeManager->mkDatatypeType(colors);
+  const std::vector<std::shared_ptr<DTypeConstructor> >& ctCons =
+      colorsType.getDType().getConstructors();
+  DType listColors("ListColors");
+  std::shared_ptr<DTypeConstructor> consC =
+      std::make_shared<DTypeConstructor>("cons");
+  consC->addArg("car", colorsType);
+  consC->addArgSelf("cdr");
+  listColors.addConstructor(consC);
+  listColors.addConstructor(std::make_shared<DTypeConstructor>("nil"));
+  TypeNode listColorsType = d_nodeManager->mkDatatypeType(listColors);
+  const std::vector<std::shared_ptr<DTypeConstructor> >& lctCons =
+      listColorsType.getDType().getConstructors();
+
+  TypeEnumerator te(listColorsType);
+  ASSERT_FALSE(te.isFinished());
+  Node cons = lctCons[0]->getConstructor();
+  Node nil =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor());
+  Node red =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor());
+  Node orange =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor());
+  Node yellow =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor());
+  ASSERT_EQ(*te, nil);
+  ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te,
+            d_nodeManager->mkNode(
+                APPLY_CONSTRUCTOR,
+                cons,
+                red,
+                d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te,
+            d_nodeManager->mkNode(
+                APPLY_CONSTRUCTOR,
+                cons,
+                red,
+                d_nodeManager->mkNode(
+                    APPLY_CONSTRUCTOR,
+                    cons,
+                    red,
+                    d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te,
+            d_nodeManager->mkNode(
+                APPLY_CONSTRUCTOR,
+                cons,
+                orange,
+                d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil));
+  ASSERT_FALSE(te.isFinished());
+  ASSERT_EQ(*++te,
+            d_nodeManager->mkNode(
+                APPLY_CONSTRUCTOR,
+                cons,
+                red,
+                d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)));
+  ASSERT_FALSE(te.isFinished());
+}
+
+TEST_F(TestTheoryWhiteTypeEnumerator, arrays_infinite)
+{
+  TypeEnumerator te(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                               d_nodeManager->integerType()));
+  std::unordered_set<Node, NodeHashFunction> elts;
+  for (uint32_t i = 0; i < 1000; ++i)
+  {
+    ASSERT_FALSE(te.isFinished());
+    Node elt = *te++;
+    // ensure no duplicates
+    ASSERT_TRUE(elts.find(elt) == elts.end());
+    elts.insert(elt);
+  }
+  ASSERT_FALSE(te.isFinished());
+
+  // ensure that certain items were found
+  TypeNode arrayType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                  d_nodeManager->integerType());
+  Node zeroes = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(0))));
+  Node ones = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(1))));
+  Node twos = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(2))));
+  Node threes = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(3))));
+  Node fours = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(4))));
+  Node tens = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(10))));
+
+  Node zero = d_nodeManager->mkConst(Rational(0));
+  Node one = d_nodeManager->mkConst(Rational(1));
+  Node two = d_nodeManager->mkConst(Rational(2));
+  Node three = d_nodeManager->mkConst(Rational(3));
+  Node four = d_nodeManager->mkConst(Rational(4));
+  Node five = d_nodeManager->mkConst(Rational(5));
+  Node eleven = d_nodeManager->mkConst(Rational(11));
+
+  ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, ones, zero, zero)),
+            elts.end());
+
+  // the arrays enumerator is currently not a fair enumerator -- when it is,
+  // these should be flipped
+  ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, tens, four, five)),
+            elts.end());
+  ASSERT_EQ(elts.find(d_nodeManager->mkNode(
+                STORE,
+                d_nodeManager->mkNode(
+                    STORE,
+                    d_nodeManager->mkNode(STORE, fours, eleven, two),
+                    two,
+                    one),
+                zero,
+                two)),
+            elts.end());
+  ASSERT_EQ(elts.find(threes), elts.end());
+  ASSERT_EQ(elts.find(d_nodeManager->mkNode(
+                STORE,
+                d_nodeManager->mkNode(
+                    STORE,
+                    d_nodeManager->mkNode(
+                        STORE,
+                        d_nodeManager->mkNode(STORE, twos, three, zero),
+                        two,
+                        zero),
+                    one,
+                    zero),
+                zero,
+                zero)),
+            elts.end());
+}
+
+TEST_F(TestTheoryWhiteTypeEnumerator, bv)
+{
+  TypeEnumerator te(d_nodeManager->mkBitVectorType(3));
+  ASSERT_EQ(*te, d_nodeManager->mkConst(BitVector(3u, 0u)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 1u)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 2u)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 3u)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 4u)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 5u)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 6u)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 7u)));
+  ASSERT_THROW(*++te, NoMoreValuesException);
+  ASSERT_THROW(*++te, NoMoreValuesException);
+  ASSERT_THROW(*++te, NoMoreValuesException);
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
deleted file mode 100644
index 24bf9922e..000000000
--- a/test/unit/theory/type_enumerator_white.h
+++ /dev/null
@@ -1,304 +0,0 @@
-/*********************                                                        */
-/*! \file type_enumerator_white.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, 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::TypeEnumerator
- **
- ** White box testing of CVC4::theory::TypeEnumerator.  (These tests depends
- ** on the ordering that the TypeEnumerators use, so it's a white-box test.)
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <unordered_set>
-
-#include "expr/array_store_all.h"
-#include "expr/dtype.h"
-#include "expr/expr_manager.h"
-#include "expr/kind.h"
-#include "expr/node_manager.h"
-#include "expr/type_node.h"
-#include "options/language.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/type_enumerator.h"
-
-using namespace CVC4;
-using namespace CVC4::smt;
-using namespace CVC4::theory;
-using namespace CVC4::kind;
-
-using namespace std;
-
-class TypeEnumeratorWhite : 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 testBooleans() {
-    TypeEnumerator te(d_nm->booleanType());
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*te, d_nm->mkConst(false));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(true));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-    TS_ASSERT( te.isFinished() );
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-    TS_ASSERT( te.isFinished() );
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-    TS_ASSERT( te.isFinished() );
-  }
-
-  void testUF() {
-    TypeNode sort = d_nm->mkSort("T");
-    TypeNode sort2 = d_nm->mkSort("U");
-    TypeEnumerator te(sort);
-    TS_ASSERT_EQUALS(*te, d_nm->mkConst(UninterpretedConstant(sort, 0)));
-    for(size_t i = 1; i < 100; ++i) {
-      TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i)));
-      TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort2, i)));
-      TS_ASSERT_EQUALS(*++te, d_nm->mkConst(UninterpretedConstant(sort, i)));
-      TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i + 2)));
-    }
-  }
-
-  void testArith() {
-    TypeEnumerator te(d_nm->integerType());
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0)));
-    for(int i = 1; i <= 100; ++i) {
-      TS_ASSERT( ! te.isFinished() );
-      TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(i)));
-      TS_ASSERT( ! te.isFinished() );
-      TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-i)));
-    }
-    TS_ASSERT( ! te.isFinished() );
-
-    te = TypeEnumerator(d_nm->realType());
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 2)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 2)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 3)));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 3)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 2)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 2)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 3)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 3)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 4)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 4)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 1)));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 5)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 5)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(6, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-6, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 2)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 2)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 3)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 3)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 4)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 4)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 5)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 5)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 6)));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 6)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(7, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-7, 1)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 3)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 3)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 5)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 5)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7)));
-    TS_ASSERT( ! te.isFinished() );
-  }
-
-  void testDTypesFinite()
-  {
-    DType dt("Colors");
-    dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
-    dt.addConstructor(std::make_shared<DTypeConstructor>("orange"));
-    dt.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
-    dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
-    dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
-    dt.addConstructor(std::make_shared<DTypeConstructor>("violet"));
-    TypeNode datatype = d_nm->mkDatatypeType(dt);
-    const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
-        datatype.getDType().getConstructors();
-    TypeEnumerator te(datatype);
-    TS_ASSERT_EQUALS(
-        *te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor()));
-    TS_ASSERT_EQUALS(
-        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor()));
-    TS_ASSERT_EQUALS(
-        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor()));
-    TS_ASSERT_EQUALS(
-        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor()));
-    TS_ASSERT_EQUALS(
-        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor()));
-    TS_ASSERT_EQUALS(
-        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor()));
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-  }
-
-  void testDTypesInfinite1()
-  {
-    DType colors("Colors");
-    colors.addConstructor(std::make_shared<DTypeConstructor>("red"));
-    colors.addConstructor(std::make_shared<DTypeConstructor>("orange"));
-    colors.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
-    colors.addConstructor(std::make_shared<DTypeConstructor>("green"));
-    colors.addConstructor(std::make_shared<DTypeConstructor>("blue"));
-    colors.addConstructor(std::make_shared<DTypeConstructor>("violet"));
-    TypeNode colorsType = d_nm->mkDatatypeType(colors);
-    const std::vector<std::shared_ptr<DTypeConstructor> >& ctCons =
-        colorsType.getDType().getConstructors();
-    DType listColors("ListColors");
-    std::shared_ptr<DTypeConstructor> consC =
-        std::make_shared<DTypeConstructor>("cons");
-    consC->addArg("car", colorsType);
-    consC->addArgSelf("cdr");
-    listColors.addConstructor(consC);
-    listColors.addConstructor(std::make_shared<DTypeConstructor>("nil"));
-    TypeNode listColorsType = d_nm->mkDatatypeType(listColors);
-    const std::vector<std::shared_ptr<DTypeConstructor> >& lctCons =
-        listColorsType.getDType().getConstructors();
-
-    TypeEnumerator te(listColorsType);
-    TS_ASSERT( ! te.isFinished() );
-    Node cons = lctCons[0]->getConstructor();
-    Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor());
-    Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor());
-    Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor());
-    Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor());
-    TS_ASSERT_EQUALS(*te, nil);
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil));
-    TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)));
-    TS_ASSERT( ! te.isFinished() );
-  }
-
-  void NOTYETtestDTypesInfinite2()
-  {
-    //TypeNode datatype;
-    //TypeEnumerator te(datatype);
-    //TS_ASSERT( ! te.isFinished() );
-    TS_FAIL("unimplemented");
-  }
-
-  void testArraysInfinite() {
-    TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()));
-    unordered_set<Node, NodeHashFunction> elts;
-    for(size_t i = 0; i < 1000; ++i) {
-      TS_ASSERT( ! te.isFinished() );
-      Node elt = *te++;
-      // ensure no duplicates
-      TS_ASSERT( elts.find(elt) == elts.end() );
-      elts.insert(elt);
-    }
-    TS_ASSERT( ! te.isFinished() );
-
-    // ensure that certain items were found
-    TypeNode arrayType =
-        d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType());
-    Node zeroes =
-        d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(0))));
-    Node ones =
-        d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(1))));
-    Node twos =
-        d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(2))));
-    Node threes =
-        d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(3))));
-    Node fours =
-        d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(4))));
-    Node tens =
-        d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(10))));
-
-    Node zero = d_nm->mkConst(Rational(0));
-    Node one = d_nm->mkConst(Rational(1));
-    Node two = d_nm->mkConst(Rational(2));
-    Node three = d_nm->mkConst(Rational(3));
-    Node four = d_nm->mkConst(Rational(4));
-    Node five = d_nm->mkConst(Rational(5));
-    Node eleven = d_nm->mkConst(Rational(11));
-
-    // FIXME: the arrays enumerator isn't currently a fair enumerator,
-    // so these will fail; disable them for now
-    //TS_ASSERT( elts.find( d_nm->mkNode(STORE, ones, zero, zero) ) != elts.end() );
-    //TS_ASSERT( elts.find( d_nm->mkNode(STORE, tens, four, five) ) != elts.end() );
-    //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, fours, eleven, two), two, one), zero, two) ) != elts.end() );
-    //TS_ASSERT( elts.find( threes ) != elts.end() );
-    //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, twos, three, zero), two, zero), one, zero), zero, zero) ) != elts.end() );
-  }
-
-  void testBV() {
-    TypeEnumerator te(d_nm->mkBitVectorType(3));
-    TS_ASSERT_EQUALS(*te, d_nm->mkConst(BitVector(3u, 0u)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 1u)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 2u)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 3u)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 4u)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 5u)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 6u)));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 7u)));
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
-  }
-
- private:
-  ExprManager* d_em;
-  SmtEngine* d_smt;
-  NodeManager* d_nm;
-  SmtScope* d_scope;
-};/* class TypeEnumeratorWhite */