From 2624b945cbb1dd92efea28220fb38f5ebaf0b66a Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 6 Oct 2014 17:52:35 -0400
Subject: [PATCH] fix for bug586

---
 src/theory/sets/theory_sets_private.cpp | 51 ++++++++++++++-----------
 test/regress/regress0/Makefile.am       |  3 +-
 test/regress/regress0/bug586.cvc        | 26 +++++++++++++
 3 files changed, 56 insertions(+), 24 deletions(-)
 create mode 100644 test/regress/regress0/bug586.cvc

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 592b4bc37..2035c18b0 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -455,33 +455,38 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
   if( !alreadyCalculated ) {
 
     Kind k = setterm.getKind();
-    unsigned numChildren = setterm.getNumChildren();
     Elements cur;
-    if(numChildren == 2) {
+
+    switch(k) {
+    case kind::UNION: {
       const Elements& left = getElements(setterm[0], settermElementsMap);
       const Elements& right = getElements(setterm[1], settermElementsMap);
-      switch(k) {
-      case kind::UNION:
-        if(left.size() >= right.size()) {
-          cur = left; cur.insert(right.begin(), right.end());
-        } else {
-          cur = right; cur.insert(left.begin(), left.end());
-        }
-        break;
-      case kind::INTERSECTION:
-        std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
-                              std::inserter(cur, cur.begin()) );
-        break;
-      case kind::SETMINUS:
-        std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
-                            std::inserter(cur, cur.begin()) );
-        break;
-      default:
-        Unhandled();
+      if(left.size() >= right.size()) {
+        cur = left; cur.insert(right.begin(), right.end());
+      } else {
+        cur = right; cur.insert(left.begin(), left.end());
       }
-    } else {
-      Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
-             (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
+      break;
+    }
+    case kind::INTERSECTION: {
+      const Elements& left = getElements(setterm[0], settermElementsMap);
+      const Elements& right = getElements(setterm[1], settermElementsMap);
+      std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
+                            std::inserter(cur, cur.begin()) );
+      break;
+    }
+    case kind::SETMINUS: {
+      const Elements& left = getElements(setterm[0], settermElementsMap);
+      const Elements& right = getElements(setterm[1], settermElementsMap);
+      std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
+                          std::inserter(cur, cur.begin()) );
+      break;
+    }
+    default:
+      Assert(theory::kindToTheoryId(k) != theory::THEORY_SETS,
+             (std::string("Kind belonging to set theory not explicitly handled: ") + kindToString(k)).c_str());
+      // Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
+      //        (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
       /* assign emptyset, which is default */
     }
 
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 128783388..7500186dd 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -164,7 +164,8 @@ BUG_TESTS = \
 	bug576.smt2 \
 	bug576a.smt2 \
 	bug578.smt2 \
-	bug585.cvc
+	bug585.cvc \
+	bug586.cvc
 
 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug586.cvc b/test/regress/regress0/bug586.cvc
new file mode 100644
index 000000000..7f6f247ee
--- /dev/null
+++ b/test/regress/regress0/bug586.cvc
@@ -0,0 +1,26 @@
+% EXPECT: sat
+%%%
+%%% DATA TYPES DEFINITIONS
+%%%
+
+%%% the roles
+DATATYPE
+	role = r1 | r2 | r3
+	%%% adding two more roles ( | r4 | r5 ) to the type, but never referring to them make things work
+END;
+
+%%% structured datatypes
+roleSet: TYPE = SET OF role;
+roleGammaSet: TYPE = [# pos: roleSet, neg: roleSet #];
+delta: TYPE = ARRAY role OF roleGammaSet;
+
+emptyRoleSet : roleSet;
+ASSERT emptyRoleSet = {} :: SET OF role;
+
+d: delta;
+ASSERT d[r3].pos = {r1};
+ASSERT d[r2].pos = {r2,r3};
+ASSERT d[r2].neg = {r1};
+
+CHECKSAT;
+%COUNTEREXAMPLE;
-- 
2.30.2