Refactoring and cleaning the type enumerator for sets (#3908)

* Miscellaneous changes

* Removed unnecessary vector of enumerators

* cleanup

* cleanup

* cleanup

* refactoring

* cleanup

* refactoring

* used binary numbers for sets

* isFinished for enumerator

* format

* added theory_sets_type_enumerator_white.h

* format

* Used BitVector class

* Tracing

* Documentation

* moved implementation to theory_sets_type_enumerator.cpp

* minor changes

2 files changed, 305 insertions, 0 deletions

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index f20088ad1..35f2f7bfa 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -8,6 +8,7 @@ cvc4_add_unit_test_white(theory_bv_white theory)
 cvc4_add_unit_test_white(theory_engine_white theory)
 cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
 cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
+cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
 cvc4_add_unit_test_white(theory_strings_rewriter_white theory)
 cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory)
 cvc4_add_unit_test_white(theory_strings_word_white theory)
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
new file mode 100644
index 000000000..3b5016fad
--- /dev/null
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -0,0 +1,304 @@
+/*********************                                                        */
+/*! \file theory_sets_type_enumerator_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mudathir Mahgoub
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 "theory/sets/theory_sets_type_enumerator.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+using namespace CVC4::theory::sets;
+using namespace std;
+
+class SetEnumeratorWhite : public CxxTest::TestSuite
+{
+  ExprManager* d_em;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
+
+ public:
+  void setUp() override
+  {
+    d_em = new ExprManager();
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_scope = new NodeManagerScope(d_nm);
+  }
+
+  void tearDown() override
+  {
+    delete d_scope;
+    delete d_em;
+  }
+
+  void testSetOfBooleans()
+  {
+    TypeNode boolType = d_nm->booleanType();
+    SetEnumerator setEnumerator(d_nm->mkSetType(boolType));
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual0 = *setEnumerator;
+    Node expected0 =
+        d_nm->mkConst(EmptySet(d_nm->mkSetType(boolType).toType()));
+    TS_ASSERT_EQUALS(expected0, actual0);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual1 = *++setEnumerator;
+    Node expected1 = d_nm->mkNode(Kind::SINGLETON, d_nm->mkConst(false));
+    TS_ASSERT_EQUALS(expected1, actual1);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual2 = *++setEnumerator;
+    Node expected2 = d_nm->mkNode(Kind::SINGLETON, d_nm->mkConst(true));
+    TS_ASSERT_EQUALS(expected2, actual2);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual3 = *++setEnumerator;
+    Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
+    TS_ASSERT_EQUALS(expected3, actual3);
+    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 typeNode = d_nm->mkSort("Atom");
+    Type sort = typeNode.toType();
+    SetEnumerator setEnumerator(d_nm->mkSetType(typeNode));
+
+    Node actual0 = *setEnumerator;
+    Node expected0 =
+        d_nm->mkConst(EmptySet(d_nm->mkSetType(typeNode).toType()));
+    TS_ASSERT_EQUALS(expected0, actual0);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual1 = *++setEnumerator;
+    Node expected1 = d_nm->mkNode(
+        Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 0)));
+    TS_ASSERT_EQUALS(expected1, actual1);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual2 = *++setEnumerator;
+    Node expected2 = d_nm->mkNode(
+        Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 1)));
+    TS_ASSERT_EQUALS(expected2, actual2);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual3 = *++setEnumerator;
+    Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
+    TS_ASSERT_EQUALS(expected3, actual3);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual4 = *++setEnumerator;
+    Node expected4 = d_nm->mkNode(
+        Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 2)));
+    TS_ASSERT_EQUALS(expected4, actual4);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual5 = *++setEnumerator;
+    Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4);
+    TS_ASSERT_EQUALS(expected5, actual5);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual6 = *++setEnumerator;
+    Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4);
+    TS_ASSERT_EQUALS(expected6, actual6);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual7 = *++setEnumerator;
+    Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4);
+    TS_ASSERT_EQUALS(expected7, actual7);
+    TS_ASSERT(!setEnumerator.isFinished());
+  }
+
+  void testSetOfFiniteDatatype()
+  {
+    Datatype dt(d_em, "Colors");
+    dt.addConstructor(DatatypeConstructor("red"));
+    dt.addConstructor(DatatypeConstructor("green"));
+    dt.addConstructor(DatatypeConstructor("blue"));
+    TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt));
+    SetEnumerator setEnumerator(d_nm->mkSetType(datatype));
+
+    Node red = d_nm->mkNode(
+        APPLY_CONSTRUCTOR,
+        DatatypeType(datatype.toType()).getDatatype().getConstructor("red"));
+
+    Node green = d_nm->mkNode(
+        APPLY_CONSTRUCTOR,
+        DatatypeType(datatype.toType()).getDatatype().getConstructor("green"));
+
+    Node blue = d_nm->mkNode(
+        APPLY_CONSTRUCTOR,
+        DatatypeType(datatype.toType()).getDatatype().getConstructor("blue"));
+
+    Node actual0 = *setEnumerator;
+    Node expected0 =
+        d_nm->mkConst(EmptySet(d_nm->mkSetType(datatype).toType()));
+    TS_ASSERT_EQUALS(expected0, actual0);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual1 = *++setEnumerator;
+    Node expected1 = d_nm->mkNode(Kind::SINGLETON, red);
+    TS_ASSERT_EQUALS(expected1, actual1);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual2 = *++setEnumerator;
+    Node expected2 = d_nm->mkNode(Kind::SINGLETON, green);
+    TS_ASSERT_EQUALS(expected2, actual2);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual3 = *++setEnumerator;
+    Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
+    TS_ASSERT_EQUALS(expected3, actual3);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual4 = *++setEnumerator;
+    Node expected4 = d_nm->mkNode(Kind::SINGLETON, blue);
+    TS_ASSERT_EQUALS(expected4, actual4);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual5 = *++setEnumerator;
+    Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4);
+    TS_ASSERT_EQUALS(expected5, actual5);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual6 = *++setEnumerator;
+    Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4);
+    TS_ASSERT_EQUALS(expected6, actual6);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual7 = *++setEnumerator;
+    Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4);
+    TS_ASSERT_EQUALS(expected7, actual7);
+    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 testBV()
+  {
+    TypeNode bitVector2 = d_nm->mkBitVectorType(2);
+    SetEnumerator setEnumerator(d_nm->mkSetType(bitVector2));
+    Node zero = d_nm->mkConst(BitVector(2u, 0u));
+    Node one = d_nm->mkConst(BitVector(2u, 1u));
+    Node two = d_nm->mkConst(BitVector(2u, 2u));
+    Node three = d_nm->mkConst(BitVector(2u, 3u));
+    Node four = d_nm->mkConst(BitVector(2u, 4u));
+
+    Node actual0 = *setEnumerator;
+    Node expected0 =
+        d_nm->mkConst(EmptySet(d_nm->mkSetType(bitVector2).toType()));
+    TS_ASSERT_EQUALS(expected0, actual0);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual1 = *++setEnumerator;
+    Node expected1 = d_nm->mkNode(Kind::SINGLETON, zero);
+    TS_ASSERT_EQUALS(expected1, actual1);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual2 = *++setEnumerator;
+    Node expected2 = d_nm->mkNode(Kind::SINGLETON, one);
+    TS_ASSERT_EQUALS(expected2, actual2);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual3 = *++setEnumerator;
+    Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
+    TS_ASSERT_EQUALS(expected3, actual3);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual4 = *++setEnumerator;
+    Node expected4 = d_nm->mkNode(Kind::SINGLETON, two);
+    TS_ASSERT_EQUALS(expected4, actual4);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual5 = *++setEnumerator;
+    Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4);
+    TS_ASSERT_EQUALS(expected5, actual5);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual6 = *++setEnumerator;
+    Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4);
+    TS_ASSERT_EQUALS(expected6, actual6);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual7 = *++setEnumerator;
+    Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4);
+    TS_ASSERT_EQUALS(expected7, actual7);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual8 = *++setEnumerator;
+    Node expected8 = d_nm->mkNode(Kind::SINGLETON, three);
+    TS_ASSERT_EQUALS(expected8, actual8);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual9 = *++setEnumerator;
+    Node expected9 = d_nm->mkNode(Kind::UNION, expected1, expected8);
+    TS_ASSERT_EQUALS(expected9, actual9);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual10 = *++setEnumerator;
+    Node expected10 = d_nm->mkNode(Kind::UNION, expected2, expected8);
+    TS_ASSERT_EQUALS(expected10, actual10);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual11 = *++setEnumerator;
+    Node expected11 = d_nm->mkNode(Kind::UNION, expected3, expected8);
+    TS_ASSERT_EQUALS(expected11, actual11);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual12 = *++setEnumerator;
+    Node expected12 = d_nm->mkNode(Kind::UNION, expected4, expected8);
+    TS_ASSERT_EQUALS(expected12, actual12);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual13 = *++setEnumerator;
+    Node expected13 = d_nm->mkNode(Kind::UNION, expected5, expected8);
+    TS_ASSERT_EQUALS(expected13, actual13);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual14 = *++setEnumerator;
+    Node expected14 = d_nm->mkNode(Kind::UNION, expected6, expected8);
+    TS_ASSERT_EQUALS(expected14, actual14);
+    TS_ASSERT(!setEnumerator.isFinished());
+
+    Node actual15 = *++setEnumerator;
+    Node expected15 = d_nm->mkNode(Kind::UNION, expected7, expected8);
+    TS_ASSERT_EQUALS(expected15, actual15);
+    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());
+  }
+
+}; /* class SetEnumeratorWhite */