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.

1 files changed, 37 insertions, 172 deletions

diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index dff4b2e98..ec0293876 100644
--- 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());