Merge pull request #23 from kbansal/sets-model

Sets model

9 files changed, 96 insertions, 208 deletions

diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index 97cfe43af..74bce743e 100755
--- a/contrib/get-antlr-3.4
+++ b/contrib/get-antlr-3.4
@@ -26,6 +26,12 @@ function webget {
 }
 
 if [ -z "${MACHINE_TYPE}" ]; then
+  if ! [ -e config/config.guess ]; then
+   echo "$(basename $0): I need the file config/config.guess to tell MACHINE_TYPE" >&2
+   echo "Try running ./autogen.sh, or set the MACHINE_TYPE environment variable." >&2
+   exit 1
+  fi
+
   # get first nibble from config.guess (x86_64, i686, ...)
   MACHINE_TYPE=`config/config.guess | sed 's,-.*,,'`
 fi
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();
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index c4f06e396..9b9fc56d7 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -172,96 +172,6 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) {
 }
 
 
-/* We use subMap to simplify the left-hand sides of the current substitution map.  If rewrite is true,
- * we also apply the rewriter to the result.
- * We want to maintain the invariant that all lhs are distinct from each other and from all rhs.
- * If for some l -> r, l reduces to l', we try to add a new rule l' -> r.  There are two cases
- * where this fails
- *   (i) if l' is equal to some ll (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list
- *   (i) if l' is equalto some rr (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list
- */
-/*
-void SubstitutionMap::simplifyLHS(const SubstitutionMap& subMap, vector<pair<Node, Node> >& equalities, bool rewrite)
-{
-  Assert(d_worklist.empty());
-  // First, apply subMap to every LHS in d_substitutions
-  NodeMap::iterator it = d_substitutions.begin();
-  NodeMap::iterator it_end = d_substitutions.end();
-  Node newLeft;
-  for(; it != it_end; ++ it) {
-    newLeft = subMap.apply((*it).first);
-    if (newLeft != (*it).first) {
-      if (rewrite) {
-        newLeft = Rewriter::rewrite(newLeft);
-      }
-      d_worklist.push_back(pair<Node,Node>(newLeft, (*it).second));
-    }
-  }
-  processWorklist(equalities, rewrite);
-  Assert(d_worklist.empty());
-}
-
-
-void SubstitutionMap::simplifyLHS(TNode lhs, TNode rhs, vector<pair<Node,Node> >& equalities, bool rewrite)
-{
-  Assert(d_worklist.empty());
-  d_worklist.push_back(pair<Node,Node>(lhs,rhs));
-  processWorklist(equalities, rewrite);                       
-  Assert(d_worklist.empty());
-}
-
-
-void SubstitutionMap::processWorklist(vector<pair<Node, Node> >& equalities, bool rewrite)
-{
-  // Add each new rewrite rule, taking care not to invalidate invariants and looking
-  // for any new rewrite rules we can learn
-  Node newLeft, newRight;
-  while (!d_worklist.empty()) {
-    newLeft = d_worklist.back().first;
-    newRight = d_worklist.back().second;
-    d_worklist.pop_back();
-
-    NodeCache tempCache;
-    tempCache[newLeft] = newRight;
-
-    Node newLeft2;
-    unsigned size = d_worklist.size();
-    bool addThisRewrite = true;
-    NodeMap::iterator it = d_substitutions.begin();
-    NodeMap::iterator it_end = d_substitutions.end();
-
-    for(; it != it_end; ++ it) {
-
-      // Check for invariant violation.  If new rewrite is redundant, do nothing
-      // Otherwise, add an equality to the output equalities
-      // In either case undo any work done by this rewrite
-      if (newLeft == (*it).first || newLeft == (*it).second) {
-        if ((*it).second != newRight) {
-          equalities.push_back(pair<Node,Node>((*it).second, newRight));
-        }
-        while (d_worklist.size() > size) {
-          d_worklist.pop_back();
-        }
-        addThisRewrite = false;
-        break;
-      }
-
-      newLeft2 = internalSubstituteOld((*it).first, tempCache);
-      if (newLeft2 != (*it).first) {
-        if (rewrite) {
-          newLeft2 = Rewriter::rewrite(newLeft2);
-        }
-        d_worklist.push_back(pair<Node,Node>(newLeft2, (*it).second));
-      }
-    }
-    if (addThisRewrite) {
-      d_substitutions[newLeft] = newRight;
-      d_cacheInvalidated = true;
-    }
-  }
-}
-*/
-
 void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
 {
   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 5a478a250..8572a6abd 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -95,10 +95,6 @@ private:
    */
   CacheInvalidator d_cacheInvalidator;
 
-  // Helper list and method for simplifyLHS methods
-  // std::vector<std::pair<Node, Node> > d_worklist;
-  // void processWorklist(std::vector<std::pair<Node, Node> >& equalities, bool rewrite);
-
 public:
 
   SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) :
@@ -186,18 +182,6 @@ public:
   // Simplify right-hand sides of current map with lhs -> rhs
   void simplifyRHS(TNode lhs, TNode rhs);
 
-  /*
-  // Simplify left-hand sides of current map using the given substitutions
-  void simplifyLHS(const SubstitutionMap& subMap,
-                   std::vector<std::pair<Node,Node> >& equalities,
-                   bool rewrite = true);
-
-  // Simplify left-hand sides of current map with lhs -> rhs and then add lhs -> rhs to the substitutions set
-  void simplifyLHS(TNode lhs, TNode rhs,
-                   std::vector<std::pair<Node,Node> >& equalities,
-                   bool rewrite = true);
-  */
-
   bool isSolvedForm() const { return d_solvedForm; }
 
   /**
diff --git a/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 b/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2
new file mode 100644
index 000000000..70c0057f9
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2
@@ -0,0 +1 @@
+; PLACEHOLDER: benchmark to be added