add construles, type_rules rm redundant, kinds cleanup

5 files changed, 89 insertions, 102 deletions

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index e46f3a4f8..12f114fc0 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -4,24 +4,25 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h"
+theory THEORY_SETS \
+    ::CVC4::theory::sets::TheorySets \
+    "theory/sets/theory_sets.h"
 typechecker "theory/sets/theory_sets_type_rules.h"
-rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h"
+rewriter ::CVC4::theory::sets::TheorySetsRewriter \
+    "theory/sets/theory_sets_rewriter.h"
 
 properties parametric
-properties check propagate #presolve postsolve
+properties check propagate
 
-# Theory content goes here.
-
-# constants...
+# constants
 constant EMPTYSET \
     ::CVC4::EmptySet \
     ::CVC4::EmptySetHashFunction \
     "util/emptyset.h" \
     "empty set"
 
-# types...
-operator SET_TYPE 1 "set type"   # the type
+# the type
+operator SET_TYPE 1 "set type"
 cardinality SET_TYPE \
     "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
     "theory/sets/theory_sets_type_rules.h"
@@ -33,24 +34,25 @@ enumerator SET_TYPE \
     "::CVC4::theory::sets::SetEnumerator" \
     "theory/sets/theory_sets_type_enumerator.h"
 
-# operators...
-operator UNION 2 "set union"
-operator INTERSECTION 2 "set intersection"
-operator SETMINUS 2 "set subtraction"
-operator SUBSET 2 "subset"
-operator MEMBER 2 "set membership"
-
-operator SET_SINGLETON 1 "singleton set"
-
-typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
-typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule
-typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule
-typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule
-typerule MEMBER ::CVC4::theory::sets::SetMemberTypeRule
-typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
-typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
-
-construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule
-construle UNION ::CVC4::theory::sets::SetConstTypeRule
+# operators
+operator UNION         2  "set union"
+operator INTERSECTION  2  "set intersection"
+operator SETMINUS      2  "set subtraction"
+operator SUBSET        2  "subset"
+operator MEMBER        2  "set membership"
+operator SET_SINGLETON 1  "singleton set"
+
+typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
+typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
+typerule SETMINUS       ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
+typerule SUBSET         ::CVC4::theory::sets::SubsetTypeRule
+typerule MEMBER         ::CVC4::theory::sets::MemberTypeRule
+typerule SET_SINGLETON  ::CVC4::theory::sets::SetSingletonTypeRule
+typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule
+
+construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
+construle INTERSECTION  ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
+construle SETMINUS      ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
+construle SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
 
 endtheory
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 70b757f0c..f487e1566 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -419,15 +419,14 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
 }
 
 
-
-void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const {
+bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const {
 
   Debug("sets-model") << "[sets-model] checkModel(..., " << S << "): "
                       << std::endl;
 
   Assert(S.getType().isSet());
 
-  Elements emptySetOfElements;
+  const Elements emptySetOfElements;
   const Elements& saved =
     d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ?
     emptySetOfElements :
@@ -438,9 +437,18 @@ void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
 
   if(S.getNumChildren() == 2) {
 
-    Elements cur, left, right;
-    left = settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second;
-    right = settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second;
+    Elements cur;
+
+    const Elements& left =
+      d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET ?
+      emptySetOfElements :
+      settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second;
+
+    const Elements&  right =
+      d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET ?
+      emptySetOfElements :
+      settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second;
+
     switch(S.getKind()) {
     case kind::UNION:
       if(left.size() >= right.size()) {
@@ -466,16 +474,18 @@ void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
     Debug("sets-model") << " }" << std::endl;
 
     if(saved != cur) {
-      Debug("sets-model") << "[sets-model] *** ERRROR *** cur != saved "
+      Debug("sets-model") << "[sets-model] *** ERROR *** cur != saved "
                           << std::endl;
-      Debug("sets-model") << "[sets-model]   FYI: "
-                          << "  [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", "
-                          << "  [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", "
-                          << "  [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n";
+      Debug("sets-model")
+	<< "[sets-model]   FYI: "
+	<< "  [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", "
+	<< "  [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", "
+	<< "  [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n";
 
+      return false;
     }
-    Assert( saved == cur );
   }
+  return true;
 }
 
 Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) const
@@ -516,6 +526,15 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
       TNode x = d_equalityEngine.getRepresentative(n[0]);
       TNode S = d_equalityEngine.getRepresentative(n[1]);
       settermElementsMap[S].insert(x);
+      if(Debug.isOn("sets-model-details")) {
+	vector<TNode> explanation;
+	d_equalityEngine.explainPredicate(n, true, explanation);
+	Debug("sets-model-details")
+	  << "[sets-model-details]  >  node: " << n << ", explanation:" << std::endl;
+	BOOST_FOREACH(TNode m, explanation) {
+	  Debug("sets-model-details") << "[sets-model-details]  >>  " << m << std::endl;
+	}
+      }
     }
   }
 
@@ -560,11 +579,14 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
   }
 
 #ifdef CVC4_ASSERTIONS
+  bool checkPassed = true;
   BOOST_FOREACH(TNode term, terms) {
     if( term.getType().isSet() ) {
-      checkModel(settermElementsMap, term);
+      checkPassed &= checkModel(settermElementsMap, term);
     }
   }
+  Assert( checkPassed,
+	  "THEORY_SETS check-model failed. Run with -d sets-model for details." );
 #endif
 }
 
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 62274e1ce..9576384bb 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -165,7 +165,7 @@ private:
   typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
   const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) const;
   Node elementsToShape(Elements elements, TypeNode setType) const;
-  void checkModel(const SettermElementsMap& settermElementsMap, TNode S) const;
+  bool checkModel(const SettermElementsMap& settermElementsMap, TNode S) const;
 };/* class TheorySetsPrivate */
 
 
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 109d8bb0e..328592abb 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -68,13 +68,13 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   switch(kind) {
 
   case kind::MEMBER: {
-    if(!node[0].isConst() || !node[1].isConst())
-      break;
-
-    // both are constants
-    TNode S = preRewrite(node[1]).node;
-    bool isMember = checkConstantMembership(node[0], S);
-    return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
+    if(node[0].isConst() && node[1].isConst()) {
+      // both are constants
+      TNode S = preRewrite(node[1]).node;
+      bool isMember = checkConstantMembership(node[0], S);
+      return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
+    }
+    break;
   }//kind::MEMBER
 
   case kind::SUBSET: {
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index aee2c92b5..3b2acd956 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -44,62 +44,34 @@ public:
 
 };/* class SetsTypeRule */
 
-// TODO: Union, Intersection and Setminus should be combined to one check
-struct SetUnionTypeRule {
+struct SetsBinaryOperatorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
-    Assert(n.getKind() == kind::UNION);
+    Assert(n.getKind() == kind::UNION ||
+           n.getKind() == kind::INTERSECTION ||
+           n.getKind() == kind::SETMINUS);
     TypeNode setType = n[0].getType(check);
     if( check ) {
       if(!setType.isSet()) {
-        throw TypeCheckingExceptionPrivate(n, "set union operating on non-set");
+        throw TypeCheckingExceptionPrivate(n, "operator expects a set, first argument is not");
       }
       TypeNode secondSetType = n[1].getType(check);
       if(secondSetType != setType) {
-        throw TypeCheckingExceptionPrivate(n, "set union operating on sets of different types");
+        throw TypeCheckingExceptionPrivate(n, "operator expects two sets of the same type");
       }
     }
     return setType;
   }
-};/* struct SetUnionTypeRule */
 
-struct SetIntersectionTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
-    Assert(n.getKind() == kind::INTERSECTION);
-    TypeNode setType = n[0].getType(check);
-    if( check ) {
-      if(!setType.isSet()) {
-        throw TypeCheckingExceptionPrivate(n, "set intersection operating on non-set");
-      }
-      TypeNode secondSetType = n[1].getType(check);
-      if(secondSetType != setType) {
-        throw TypeCheckingExceptionPrivate(n, "set intersection operating on sets of different types");
-      }
-    }
-    return setType;
-  }
-};/* struct SetIntersectionTypeRule */
-
-struct SetSetminusTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
-    Assert(n.getKind() == kind::SETMINUS);
-    TypeNode setType = n[0].getType(check);
-    if( check ) {
-      if(!setType.isSet()) {
-        throw TypeCheckingExceptionPrivate(n, "set setminus operating on non-set");
-      }
-      TypeNode secondSetType = n[1].getType(check);
-      if(secondSetType != setType) {
-        throw TypeCheckingExceptionPrivate(n, "set setminus operating on sets of different types");
-      }
-    }
-    return setType;
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+    Assert(n.getKind() == kind::UNION ||
+           n.getKind() == kind::INTERSECTION ||
+           n.getKind() == kind::SETMINUS);
+    return n[0].isConst() && n[1].isConst();
   }
-};/* struct SetSetminusTypeRule */
+};/* struct SetUnionTypeRule */
 
-struct SetSubsetTypeRule {
+struct SubsetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::SUBSET);
@@ -117,7 +89,7 @@ struct SetSubsetTypeRule {
   }
 };/* struct SetSubsetTypeRule */
 
-struct SetMemberTypeRule {
+struct MemberTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::MEMBER);
@@ -141,25 +113,16 @@ struct SetSingletonTypeRule {
     Assert(n.getKind() == kind::SET_SINGLETON);
     return nodeManager->mkSetType(n[0].getType(check));
   }
-};/* struct SetInTypeRule */
 
-struct SetConstTypeRule {
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    switch(n.getKind()) {
-    case kind::SET_SINGLETON:
-      return n[0].isConst();
-    case kind::UNION:
-      return n[0].isConst() && n[1].isConst();
-    default:
-      Unhandled();
-    }
+    Assert(n.getKind() == kind::SET_SINGLETON);
+    return n[0].isConst();
   }
-};
+};/* struct SetInTypeRule */
 
 struct EmptySetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
-
     Assert(n.getKind() == kind::EMPTYSET);
     EmptySet emptySet = n.getConst<EmptySet>();
     Type setType = emptySet.getType();