fix for bug586

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 592b4bc37fd870f1691b5644511f11df8df23f44..2035c18b0265ccfb83ad7a9ad806214f1b6f94ea 100644 (file)
--- 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 128783388c8acfa274c9c8bbd9980c57721e41b5..7500186dd857d2e3c854360da5b0ee9c31bdfcdc 100644 (file)
--- 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 (file)
index 0000000..7f6f247
--- /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;