sets: fix a bug in model building, another in handling set of sets

5 files changed, 49 insertions, 9 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 9d00cde7b..af96b50d0 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -190,6 +190,29 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
     return;
   }
 
+  /**
+   * Disequality propagation if element type is set
+   */
+  if(x.getType().isSet()) {
+    if(polarity) {
+      const CDTNodeList* l = d_termInfoManager->getNonMembers(S);
+      for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+        TNode n = *it;
+        learnLiteral( /* atom = */ EQUAL(x, n),
+                      /* polarity = */ false,
+                      /* reason = */ AND( MEMBER(x, S), NOT( MEMBER(n, S)) ) );
+      }
+    } else {
+      const CDTNodeList* l = d_termInfoManager->getMembers(S);
+      for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+        TNode n = *it;
+        learnLiteral( /* atom = */ EQUAL(x, n),
+                      /* polarity = */ false,
+                      /* reason = */ AND( NOT(MEMBER(x, S)), MEMBER(n, S)) );
+      }
+    }
+  }
+
   for(; !j.isFinished(); ++j) {
     TNode S = (*j);
     Node cur_atom = MEMBER(x, S);
@@ -227,7 +250,10 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
   Debug("sets-prop") << "[sets-prop] doSettermPropagation("
                      << x << ", " << S << std::endl;
 
-  Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
+  Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType(),
+         ( std::string("types of S and x are ") + S.getType().toString() +
+           std::string(" and ") + x.getType().toString() +
+           std::string(" respectively") ).c_str()  );
 
   Node literal, left_literal, right_literal;
 
@@ -416,7 +442,8 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
         Unhandled();
       }
     } else {
-      Assert(k == kind::VARIABLE || k == kind::APPLY_UF);
+      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 */
     }
 
@@ -598,6 +625,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
   BOOST_FOREACH( TNode setterm, settermsModEq ) {
     Elements elements = getElements(setterm, settermElementsMap);
     Node shape = elementsToShape(elements, setterm.getType());
+    shape = theory::Rewriter::rewrite(shape);
     m->assertEquality(shape, setterm, true);
     m->assertRepresentative(shape);
   }
@@ -1042,6 +1070,14 @@ const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
   return d_info[x]->parents;
 }
 
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getMembers(TNode S) {
+  return d_info[S]->elementsInThisSet;
+}
+
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) {
+  return d_info[S]->elementsNotInThisSet;
+}
+
 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
   unsigned numChild = n.getNumChildren();
 
@@ -1052,8 +1088,7 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
 
   if(n.getKind() == kind::UNION ||
      n.getKind() == kind::INTERSECTION ||
-     n.getKind() == kind::SETMINUS ||
-     n.getKind() == kind::SET_SINGLETON) {
+     n.getKind() == kind::SETMINUS) {
 
     for(unsigned i = 0; i < numChild; ++i) {
       if(d_terms.contains(n[i])) {
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 7e9d60905..9225bfbfd 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -118,6 +118,8 @@ private:
     ~TermInfoManager();
     void notifyMembership(TNode fact);
     const CDTNodeList* getParents(TNode x);
+    const CDTNodeList* getMembers(TNode S);
+    const CDTNodeList* getNonMembers(TNode S);
     void addTerm(TNode n);
     void mergeTerms(TNode a, TNode b);
   };
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 328592abb..bcfbc46ae 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -201,12 +201,13 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette
         break;
       case kind::SET_SINGLETON:
         Assert(setterm[0].isConst());
-        cur.insert(setterm[0]);
+        cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node);
         break;
       default:
         Unhandled();
       }
     }
+    Debug("sets-rewrite-constant") << "[sets-rewrite-constant] "<< setterm << " " << setterm.getId() << std::endl;
 
     it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first;
   }
@@ -246,7 +247,10 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
     //rewrite set to normal form
     SettermElementsMap setTermElementsMap;   // cache
     const Elements& elements = collectConstantElements(node, setTermElementsMap);
-    return RewriteResponse(REWRITE_DONE, elementsToNormalConstant(elements, node.getType()));
+    RewriteResponse response(REWRITE_DONE, elementsToNormalConstant(elements, node.getType()));
+    Debug("sets-rewrite-constant") << "[sets-rewrite-constant] Rewriting " << node << std::endl
+                                   << "[sets-rewrite-constant]        to " << response.node << std::endl;
+    return response;
   }
 
   return RewriteResponse(REWRITE_DONE, node);
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index 715817508..6ce418e85 100644
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -83,7 +83,6 @@ public:
   static inline void shutdown() {
     // nothing to do
   }
-
 };/* class TheorySetsRewriter */
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 203f116bb..6c0018c05 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -70,8 +70,8 @@ Node TheoryModel::getValue(TNode n) const {
     //normalize
     nn = Rewriter::rewrite(nn);
   }
-  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ):  returning"
-                          << nn << std::endl;
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl
+                          << "[model-getvalue] returning " << nn << std::endl;
   return nn;
 }