Refactoring the rewriter of sets (#4856)

Changes it so that we don't flatten unions if at least one child is non-constant, since this may lead to children that are non-constant by mixing constant/non-constant elements and is generally expensive for large unions of singleton elements.

The previous rewriting policy was causing an incorrect model in a separation logic benchmark reported by Andrew Jones, due to unions of constant elements that were unsorted (and hence not considered constants). We now have the invariant that all subterms that are unions of constant elements are set constants.

Note this PR changes the normal form of set constants to be (union (singleton c1) ... (union (singleton cn-1) (singleton cn) ... ) not (union ... (union (singleton c1) (singleton c2)) ... (singleton cn)).

It changes a unit test which was impacted by this change which was failing due to hardcoding the enumeration order in the unit test. The test is now agnostic to the order of elements.

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index c9b6a9d892c3e8f8107e01a51b7f223618255a0b..57344928745b4a9144441ddd9a656ab13fc8ff19 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1646,9 +1646,9 @@ void TheorySep::computeLabelModel( Node lbl ) {
     Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl;
     if( v_val.getKind()!=kind::EMPTYSET ){
       while( v_val.getKind()==kind::UNION ){
-        Assert(v_val[1].getKind() == kind::SINGLETON);
-        d_label_model[lbl].d_heap_locs_model.push_back( v_val[1] );
-        v_val = v_val[0];
+        Assert(v_val[0].getKind() == kind::SINGLETON);
+        d_label_model[lbl].d_heap_locs_model.push_back(v_val[0]);
+        v_val = v_val[1];
       }
       if( v_val.getKind()==kind::SINGLETON ){
         d_label_model[lbl].d_heap_locs_model.push_back( v_val );
@@ -1916,15 +1916,13 @@ Node TheorySep::HeapInfo::getValue( TypeNode tn ) {
   Assert(d_heap_locs.size() == d_heap_locs_model.size());
   if( d_heap_locs.empty() ){
     return NodeManager::currentNM()->mkConst(EmptySet(tn));
-  }else if( d_heap_locs.size()==1 ){
-    return d_heap_locs[0];
-  }else{
-    Node curr = NodeManager::currentNM()->mkNode( kind::UNION, d_heap_locs[0], d_heap_locs[1] );
-    for( unsigned j=2; j<d_heap_locs.size(); j++ ){
-      curr = NodeManager::currentNM()->mkNode( kind::UNION, curr, d_heap_locs[j] );
-    }
-    return curr;
   }
+  Node curr = d_heap_locs[0];
+  for (unsigned j = 1; j < d_heap_locs.size(); j++)
+  {
+    curr = NodeManager::currentNM()->mkNode(kind::UNION, d_heap_locs[j], curr);
+  }
+  return curr;
 }
 
 }/* CVC4::theory::sep namespace */

diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 0607a0e6c715b2e8aaabb82f6ce7612491706ddd..b53a1c03d93637e7e5632f2ee6caac82700ed02d 100644 (file)
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -25,6 +25,12 @@ namespace sets {
 
 class NormalForm {
  public:
+  /**
+   * Constructs a set of the form:
+   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * from the set { c1 ... cn }, also handles empty set case, which is why
+   * setType is passed to this method.
+   */
   template <bool ref_count>
   static Node elementsToSet(const std::set<NodeTemplate<ref_count> >& elements,
                             TypeNode setType)
@@ -42,12 +48,21 @@ class NormalForm {
       Node cur = nm->mkNode(kind::SINGLETON, *it);
       while (++it != elements.end())
       {
-        cur = nm->mkNode(kind::UNION, cur, nm->mkNode(kind::SINGLETON, *it));
+        cur = nm->mkNode(kind::UNION, nm->mkNode(kind::SINGLETON, *it), cur);
       }
       return cur;
     }
   }
 
+  /**
+   * Returns true if n is considered a to be a (canonical) constant set value.
+   * A canonical set value is one whose AST is:
+   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * where c1 ... cn are constants and the node identifier of these constants
+   * are such that:
+   *   c1 > ... > cn.
+   * Also handles the corner cases of empty set and singleton set.
+   */
   static bool checkNormalConstant(TNode n) {
     Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :"
                               << std::endl;
@@ -56,46 +71,62 @@ class NormalForm {
     } else if (n.getKind() == kind::SINGLETON) {
       return n[0].isConst();
     } else if (n.getKind() == kind::UNION) {
-      // assuming (union ... (union {SmallestNodeID} {BiggerNodeId}) ...
-      // {BiggestNodeId})
-
-      // store BiggestNodeId in prvs
-      if (n[1].getKind() != kind::SINGLETON) return false;
-      if (!n[1][0].isConst()) return false;
-      Debug("sets-checknormal")
-          << "[sets-checknormal]              frst element = " << n[1][0] << " "
-          << n[1][0].getId() << std::endl;
-      TNode prvs = n[1][0];
-      n = n[0];
+      // assuming (union {SmallestNodeID} ... (union {BiggerNodeId} ...
 
+      Node orig = n;
+      TNode prvs;
       // check intermediate nodes
-      while (n.getKind() == kind::UNION) {
-        if (n[1].getKind() != kind::SINGLETON) return false;
-        if (!n[1].isConst()) return false;
+      while (n.getKind() == kind::UNION)
+      {
+        if (n[0].getKind() != kind::SINGLETON || !n[0][0].isConst())
+        {
+          // not a constant
+          Trace("sets-isconst") << "sets::isConst: " << orig << " not due to "
+                                << n[0] << std::endl;
+          return false;
+        }
         Debug("sets-checknormal")
-            << "[sets-checknormal]              element = " << n[1][0] << " "
-            << n[1][0].getId() << std::endl;
-        if (n[1][0] >= prvs) return false;
-        prvs = n[1][0];
-        n = n[0];
+            << "[sets-checknormal]              element = " << n[0][0] << " "
+            << n[0][0].getId() << std::endl;
+        if (!prvs.isNull() && n[0][0] >= prvs)
+        {
+          Trace("sets-isconst")
+              << "sets::isConst: " << orig << " not due to compare " << n[0][0]
+              << std::endl;
+          return false;
+        }
+        prvs = n[0][0];
+        n = n[1];
       }
 
       // check SmallestNodeID is smallest
-      if (n.getKind() != kind::SINGLETON) return false;
-      if (!n[0].isConst()) return false;
+      if (n.getKind() != kind::SINGLETON || !n[0].isConst())
+      {
+        Trace("sets-isconst") << "sets::isConst: " << orig
+                              << " not due to final " << n << std::endl;
+        return false;
+      }
       Debug("sets-checknormal")
           << "[sets-checknormal]              lst element = " << n[0] << " "
           << n[0].getId() << std::endl;
-      if (n[0] >= prvs) return false;
-
-      // we made it
-      return true;
-
-    } else {
-      return false;
+      // compare last ID
+      if (n[0] < prvs)
+      {
+        return true;
+      }
+      Trace("sets-isconst")
+          << "sets::isConst: " << orig << " not due to compare final " << n[0]
+          << std::endl;
     }
+    return false;
   }
 
+  /**
+   * Converts a set term to a std::set of its elements. This expects a set of
+   * the form:
+   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * Also handles the corner cases of empty set and singleton set.
+   */
   static std::set<Node> getElementsFromNormalConstant(TNode n) {
     Assert(n.isConst());
     std::set<Node> ret;
@@ -103,29 +134,15 @@ class NormalForm {
       return ret;
     }
     while (n.getKind() == kind::UNION) {
-      Assert(n[1].getKind() == kind::SINGLETON);
-      ret.insert(ret.begin(), n[1][0]);
-      n = n[0];
+      Assert(n[0].getKind() == kind::SINGLETON);
+      ret.insert(ret.begin(), n[0][0]);
+      n = n[1];
     }
     Assert(n.getKind() == kind::SINGLETON);
     ret.insert(n[0]);
     return ret;
   }
   
-  
-  //AJR
-  
-  static void getElementsFromBop( Kind k, Node n, std::vector< Node >& els ){
-    if( n.getKind()==k ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        getElementsFromBop( k, n[i], els );
-      }
-    }else{
-      if( std::find( els.begin(), els.end(), n )==els.end() ){
-        els.push_back( n );
-      }
-    }
-  }
   static Node mkBop( Kind k, std::vector< Node >& els, TypeNode tn, unsigned index = 0 ){
     if( index>=els.size() ){
       return NodeManager::currentNM()->mkConst(EmptySet(tn));

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 741f45dd84d3c9c815f4fdd87826cad3aaa7812c..b1831f26199e49844442dcbf43e10c23b48568b2 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -320,7 +320,7 @@ void TheorySetsPrivate::fullEffortCheck()
         Node n = (*eqc_i);
         if (n != eqc)
         {
-          Trace("sets-eqc") << n << " ";
+          Trace("sets-eqc") << n << " (" << n.isConst() << ") ";
         }
         TypeNode tnn = n.getType();
         if (isSet)

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index eb168c6ed17c725a9fb26fa054b3b667686e2ddd..50aa89cc83bfe5feb6ff4fec21cde8c9dc0f6462 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -27,7 +27,7 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-bool checkConstantMembership(TNode elementTerm, TNode setTerm)
+bool TheorySetsRewriter::checkConstantMembership(TNode elementTerm, TNode setTerm)
 {
   if(setTerm.getKind() == kind::EMPTYSET) {
     return false;
@@ -38,12 +38,11 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
   }
 
   Assert(setTerm.getKind() == kind::UNION
-         && setTerm[1].getKind() == kind::SINGLETON)
+         && setTerm[0].getKind() == kind::SINGLETON)
       << "kind was " << setTerm.getKind() << ", term: " << setTerm;
 
-  return
-    elementTerm == setTerm[1][0] ||
-    checkConstantMembership(elementTerm, setTerm[0]);
+  return elementTerm == setTerm[0][0]
+         || checkConstantMembership(elementTerm, setTerm[1]);
 }
 
 // static
@@ -53,6 +52,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   Trace("sets-postrewrite") << "Process: " << node << std::endl;
 
   if(node.isConst()) {
+    Trace("sets-rewrite-nf")
+        << "Sets::rewrite: no rewrite (constant) " << node << std::endl;
     // Dare you touch the const and mangle it to something else.
     return RewriteResponse(REWRITE_DONE, node);
   }
@@ -163,23 +164,13 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       Assert(newNode.isConst());
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
-    } else {
-      std::vector< Node > els;
-      NormalForm::getElementsFromBop( kind::INTERSECTION, node, els );
-      std::sort( els.begin(), els.end() );
-      Node rew = NormalForm::mkBop( kind::INTERSECTION, els, node.getType() );
-      if( rew!=node ){
-        Trace("sets-rewrite") << "Sets::rewrite " << node << " -> " << rew << std::endl;
-      }
-      return RewriteResponse(REWRITE_DONE, rew);
     }
-    /*
-    } else if (node[0] > node[1]) {
+    else if (node[0] > node[1])
+    {
       Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
-      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
     }
-    */
+    // we don't merge non-constant intersections
     break;
   }//kind::INTERSECION
 
@@ -200,19 +191,16 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
                           std::inserter(newSet, newSet.begin()));
       Node newNode = NormalForm::elementsToSet(newSet, node.getType());
       Assert(newNode.isConst());
-      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      Trace("sets-rewrite")
+          << "Sets::rewrite: UNION_CONSTANT_MERGE: " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
-    } else {
-      std::vector< Node > els;
-      NormalForm::getElementsFromBop( kind::UNION, node, els );
-      std::sort( els.begin(), els.end() );
-      Node rew = NormalForm::mkBop( kind::UNION, els, node.getType() );
-      if( rew!=node ){
-        Trace("sets-rewrite") << "Sets::rewrite " << node << " -> " << rew << std::endl;
-      }
-      Trace("sets-rewrite") << "...no rewrite." << std::endl;
-      return RewriteResponse(REWRITE_DONE, rew);
     }
+    else if (node[0] > node[1])
+    {
+      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
+    // we don't merge non-constant unions
     break;
   }//kind::UNION
   case kind::COMPLEMENT: {
@@ -491,16 +479,15 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
 // static
 RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
   NodeManager* nm = NodeManager::currentNM();
-
-  if(node.getKind() == kind::EQUAL) {
-
+  Kind k = node.getKind();
+  if (k == kind::EQUAL)
+  {
     if(node[0] == node[1]) {
       return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
     }
-
-  }//kind::EQUAL
-  else if(node.getKind() == kind::INSERT) {
-
+  }
+  else if (k == kind::INSERT)
+  {
     Node insertedElements = nm->mkNode(kind::SINGLETON, node[0]);
     size_t setNodeIndex =  node.getNumChildren()-1;
     for(size_t i = 1; i < setNodeIndex; ++i) {
@@ -512,17 +499,16 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
                            nm->mkNode(kind::UNION,
                                       insertedElements,
                                       node[setNodeIndex]));
-
-  }//kind::INSERT
-  else if(node.getKind() == kind::SUBSET) {
-
+  }
+  else if (k == kind::SUBSET)
+  {
     // rewrite (A subset-or-equal B) as (A union B = B)
     return RewriteResponse(REWRITE_AGAIN,
                            nm->mkNode(kind::EQUAL,
                                       nm->mkNode(kind::UNION, node[0], node[1]),
                                       node[1]) );
-
-  }//kind::SUBSET
+  }
+  // could have an efficient normalizer for union here
 
   return RewriteResponse(REWRITE_DONE, node);
 }

diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index 7d1a6c18892b53010d5a1d4bf335270ede4d3f18..fdc9caefbabc8ba904033f07f8c645ca118c9c34 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -70,7 +70,11 @@ class TheorySetsRewriter : public TheoryRewriter
     // often this will suffice
     return postRewrite(equality).d_node;
   }
-
+private:
+  /**
+   * Returns true if elementTerm is in setTerm, where both terms are constants.
+   */
+  bool checkConstantMembership(TNode elementTerm, TNode setTerm);
 }; /* class TheorySetsRewriter */
 
 }/* CVC4::theory::sets namespace */

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ed07c74749f96572aed43491e2bd230c9bb9963a..d784a1ced6f8613f20fede57ae74a0a0fcc49d37 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -858,6 +858,7 @@ set(regress_0_tests
   regress0/sep/sep-01.smt2
   regress0/sep/sep-plus1.smt2
   regress0/sep/sep-simp-unsat-emp.smt2
+  regress0/sep/simple-080420-const-sets.smt2
   regress0/sep/skolem_emp.smt2
   regress0/sep/trees-1.smt2
   regress0/sep/wand-crash.smt2

diff --git a/test/regress/regress0/sep/simple-080420-const-sets.smt2 b/test/regress/regress0/sep/simple-080420-const-sets.smt2
new file mode 100644 (file)
index 0000000..1d85fb1
--- /dev/null
+++ b/test/regress/regress0/sep/simple-080420-const-sets.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-option :produce-models true)
+(set-info :status sat)
+(declare-fun x () Int)
+
+; works
+;(assert (sep (pto 1 2) (pto 5 6) (pto x 8)))
+
+; didn't work due to sets rewriter
+(assert (sep (pto 1 2) (pto 5 6) (pto 7 8)))
+
+(check-sat)

diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index dff4b2e9880882149442e10ca42466adbda93809..ec02938762d8fa8732f0a40c211b45610cecac84 100644 (file)
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -49,32 +49,35 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
     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;
-    Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(boolType)));
-    TS_ASSERT_EQUALS(expected0, actual0);
+    addAndCheckUnique(actual0, elems);
     TS_ASSERT(!setEnumerator.isFinished());
 
     Node actual1 = *++setEnumerator;
-    Node expected1 = d_nm->mkNode(Kind::SINGLETON, d_nm->mkConst(false));
-    TS_ASSERT_EQUALS(expected1, actual1);
+    addAndCheckUnique(actual1, elems);
     TS_ASSERT(!setEnumerator.isFinished());
 
     Node actual2 = *++setEnumerator;
-    Node expected2 = d_nm->mkNode(Kind::SINGLETON, d_nm->mkConst(true));
-    TS_ASSERT_EQUALS(expected2, actual2);
+    addAndCheckUnique(actual2, elems);
     TS_ASSERT(!setEnumerator.isFinished());
 
     Node actual3 = Rewriter::rewrite(*++setEnumerator);
-    Node expected3 =
-        Rewriter::rewrite(d_nm->mkNode(Kind::UNION, expected1, expected2));
-    TS_ASSERT_EQUALS(expected3, actual3);
+    addAndCheckUnique(actual3, elems);
     TS_ASSERT(!setEnumerator.isFinished());
 
     TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
@@ -95,43 +98,14 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
     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());
+    std::vector<Node> elems;
+    for (unsigned i = 0; i < 7; i++)
+    {
+      Node actual = *setEnumerator;
+      addAndCheckUnique(actual, elems);
+      TS_ASSERT(!setEnumerator.isFinished());
+      ++setEnumerator;
+    }
   }
 
   void testSetOfFiniteDatatype()
@@ -151,46 +125,14 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
 
     Node blue = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor());
 
-    Node actual0 = *setEnumerator;
-    Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(datatype)));
-    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());
+    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());
@@ -204,92 +146,15 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
   {
     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)));
-    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());
+    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());