Merge pull request #24 from kbansal/sets-model

sets, misc

15 files changed, 691 insertions, 61 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index d75535e15..2d306d464 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -223,6 +223,7 @@ libcvc4_la_SOURCES = \
 	theory/datatypes/theory_datatypes.cpp \
 	theory/sets/expr_patterns.h \
 	theory/sets/options_handlers.h \
+	theory/sets/scrutinize.h \
 	theory/sets/term_info.h \
 	theory/sets/theory_sets.cpp \
 	theory/sets/theory_sets.h \
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 47d112cd8..c57a315f5 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -417,6 +417,7 @@ public:
     }
 
   };/* class CDList<>::const_iterator */
+  typedef const_iterator iterator;
 
   /**
    * Returns an iterator pointing to the first item in the list.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7aebb60f6..8586bc9da 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1348,7 +1348,11 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
     return stats;
   } else if(key == "error-behavior") {
     // immediate-exit | continued-execution
-    return SExpr::Keyword("continued-execution");
+    if( options::continuedExecution() || options::interactive() ) {
+      return SExpr::Keyword("continued-execution");
+    } else {
+      return SExpr::Keyword("immediate-exit");
+    }
   } else if(key == "name") {
     return Configuration::getName();
   } else if(key == "version") {
diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h
new file mode 100644
index 000000000..7343662c6
--- /dev/null
+++ b/src/theory/sets/scrutinize.h
@@ -0,0 +1,75 @@
+/*********************                                                        */
+/*! \file scrutinize.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Check consistency of internal data structures.
+ **
+ ** Some checks are very low-level with respect to TheorySetsPrivate
+ ** implementation, and hence might become outdated pretty quickly.
+ **/
+
+#pragma once
+
+#include <boost/foreach.hpp>
+
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsScrutinize {
+  /* we don't want to accidentally modify theory data */
+  const TheorySetsPrivate* d_theory;
+public:
+  TheorySetsScrutinize(TheorySetsPrivate* theory): d_theory(theory) {
+    Debug("sets") << "[sets] scrunitize enabled" << std::endl;
+  }
+  void postCheckInvariants() const {
+    Debug("sets-scrutinize") << "[sets-scrutinize] postCheckInvariants()" << std::endl;
+    
+    // assume not in conflict, and complete:
+    // - try building model
+    // - check it
+    
+    TheorySetsPrivate::SettermElementsMap settermElementsMap;
+    TNode true_atom = NodeManager::currentNM()->mkConst<bool>(true);
+    std::set<Node> terms;
+    (d_theory->d_external).computeRelevantTerms(terms);
+    for(eq::EqClassIterator it_eqclasses(true_atom, &d_theory->d_equalityEngine);
+        ! it_eqclasses.isFinished() ; ++it_eqclasses) {
+      TNode n = (*it_eqclasses);
+      if(n.getKind() == kind::MEMBER) {
+        Assert(d_theory->d_equalityEngine.areEqual(n, true_atom));
+        TNode x = d_theory->d_equalityEngine.getRepresentative(n[0]);
+        TNode S = d_theory->d_equalityEngine.getRepresentative(n[1]);
+        settermElementsMap[S].insert(x);
+      }
+    }
+    bool checkPassed = true;
+    BOOST_FOREACH(TNode term, terms) {
+      if( term.getType().isSet() ) {
+        checkPassed &= d_theory->checkModel(settermElementsMap, term);
+      }
+    }
+    if(Debug.isOn("sets-checkmodel-ignore")) {
+      Debug("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl;
+    } else {
+      Assert( checkPassed,
+              "THEORY_SETS check-model failed. Run with -d sets-model for details." );
+    }
+  }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
diff --git a/src/theory/sets/term_info.h b/src/theory/sets/term_info.h
index ea435d9b7..2783faa79 100644
--- a/src/theory/sets/term_info.h
+++ b/src/theory/sets/term_info.h
@@ -31,12 +31,16 @@ class TheorySetsTermInfo {
 public:
   CDTNodeList* elementsInThisSet;
   CDTNodeList* elementsNotInThisSet;
+  CDTNodeList* setsContainingThisElement;
+  CDTNodeList* setsNotContainingThisElement;
   CDTNodeList* parents;
 
   TheorySetsTermInfo(context::Context* c)
   {
     elementsInThisSet = new(true)CDTNodeList(c);
     elementsNotInThisSet = new(true)CDTNodeList(c);
+    setsContainingThisElement = new(true)CDTNodeList(c);
+    setsNotContainingThisElement = new(true)CDTNodeList(c);
     parents = new(true)CDTNodeList(c);
   }
 
@@ -45,11 +49,19 @@ public:
     else elementsNotInThisSet -> push_back(n);
   }
 
+  void addToSetList(TNode n, bool polarity) {
+    if(polarity) setsContainingThisElement -> push_back(n);
+    else setsNotContainingThisElement -> push_back(n);
+  }
+
   ~TheorySetsTermInfo() {
     elementsInThisSet -> deleteSelf();
     elementsNotInThisSet -> deleteSelf();
+    setsContainingThisElement -> deleteSelf();
+    setsNotContainingThisElement -> deleteSelf();
     parents -> deleteSelf();
   }
+
 };
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index f40031514..9f74064cb 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -27,10 +27,12 @@ namespace theory {
 namespace sets {
 
 class TheorySetsPrivate;
+class TheorySetsScrutinize;
 
 class TheorySets : public Theory {
 private:
   friend class TheorySetsPrivate;
+  friend class TheorySetsScrutinize;
   TheorySetsPrivate* d_internal;
 public:
 
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f487e1566..f56f509b2 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -17,6 +17,7 @@
 #include <boost/foreach.hpp>
 
 #include "theory/theory_model.h"
+#include "theory/sets/scrutinize.h"
 #include "theory/sets/theory_sets.h"
 #include "theory/sets/theory_sets_private.h"
 
@@ -59,10 +60,12 @@ void TheorySetsPrivate::check(Theory::Effort level) {
         if (!d_equalityEngine.hasTerm(atom[0])) {
           Assert(atom[0].isConst());
           d_equalityEngine.addTerm(atom[0]);
+          d_termInfoManager->addTerm(atom[0]);
         }
         if (!d_equalityEngine.hasTerm(atom[1])) {
           Assert(atom[1].isConst());
           d_equalityEngine.addTerm(atom[1]);
+          d_termInfoManager->addTerm(atom[1]);
         }
       }
     }
@@ -88,14 +91,18 @@ void TheorySetsPrivate::check(Theory::Effort level) {
 
     Debug("sets") << "[sets]  in conflict = " << d_conflict << std::endl;
     Assert( d_conflict ^ d_equalityEngine.consistent() );
-    if(d_conflict) return;
+    if(d_conflict) { return; }
     Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
   }
 
   if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
     d_external.d_out->lemma(getLemma());
+    return;
   }
 
+  // if we are here, there is no conflict and we are complete
+  if(Debug.isOn("sets-scrutinize")) { d_scrutinize->postCheckInvariants(); }
+
   return;
 }/* TheorySetsPrivate::check() */
 
@@ -428,7 +435,8 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
 
   const Elements emptySetOfElements;
   const Elements& saved =
-    d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ?
+    d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ||
+    settermElementsMap.find(d_equalityEngine.getRepresentative(S)) == settermElementsMap.end() ?
     emptySetOfElements :
     settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second;
   Debug("sets-model") << "[sets-model] saved :  { ";
@@ -440,12 +448,14 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
     Elements cur;
 
     const Elements& left =
-      d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET ?
+      d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET ||
+      settermElementsMap.find(d_equalityEngine.getRepresentative(S[0])) == settermElementsMap.end() ?
       emptySetOfElements :
       settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second;
 
     const Elements&  right =
-      d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET ?
+      d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET ||
+      settermElementsMap.find(d_equalityEngine.getRepresentative(S[1])) == settermElementsMap.end() ?
       emptySetOfElements :
       settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second;
 
@@ -526,14 +536,28 @@ 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;
-	}
+    }
+    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;
+      }
+    }
+  }
+
+  if(Debug.isOn("sets-model-details")) {
+    for(eq::EqClassIterator it_eqclasses(false_atom, &d_equalityEngine);
+        ! it_eqclasses.isFinished() ; ++it_eqclasses) {
+      TNode n = (*it_eqclasses);
+      vector<TNode> explanation;
+      d_equalityEngine.explainPredicate(n, false, explanation);
+      Debug("sets-model-details")
+        << "[sets-model-details]  >  node: not: " << n << ", explanation:" << std::endl;
+      BOOST_FOREACH(TNode m, explanation) {
+        Debug("sets-model-details") << "[sets-model-details]  >>  " << m << std::endl;
       }
     }
   }
@@ -585,8 +609,12 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
       checkPassed &= checkModel(settermElementsMap, term);
     }
   }
-  Assert( checkPassed,
-	  "THEORY_SETS check-model failed. Run with -d sets-model for details." );
+  if(Debug.isOn("sets-checkmodel-ignore")) {
+    Debug("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl;
+  } else {
+    Assert( checkPassed,
+            "THEORY_SETS check-model failed. Run with -d sets-model for details." );
+  }
 #endif
 }
 
@@ -735,10 +763,10 @@ bool TheorySetsPrivate::isComplete() {
 Node TheorySetsPrivate::getLemma() {
   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
 
-  Node lemma;
+  Node n, lemma;
 
   if(!d_pending.empty()) {
-    Node n = d_pending.front();
+    n = d_pending.front();
     d_pending.pop();
     d_pendingEverInserted.insert(n);
 
@@ -747,7 +775,7 @@ Node TheorySetsPrivate::getLemma() {
 
     lemma = OR(n, NOT(n));
   } else {
-    Node n = d_pendingDisequal.front();
+    n = d_pendingDisequal.front();
     d_pendingDisequal.pop();
     d_pendingEverInserted.insert(n);
 
@@ -758,7 +786,7 @@ Node TheorySetsPrivate::getLemma() {
     lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
   }
 
-  Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl;
+  Debug("sets-lemma") << "[sets-lemma] Generating for " << n << ", lemma: " << lemma << std::endl;
 
   return  lemma;
 }
@@ -777,7 +805,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_nodeSaver(c),
   d_pending(u),
   d_pendingDisequal(u),
-  d_pendingEverInserted(u)
+  d_pendingEverInserted(u),
+  d_scrutinize(NULL)
 {
   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
 
@@ -787,12 +816,20 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 
   d_equalityEngine.addFunctionKind(kind::MEMBER);
   d_equalityEngine.addFunctionKind(kind::SUBSET);
+
+  if( Debug.isOn("sets-scrutinize") ) {
+    d_scrutinize = new TheorySetsScrutinize(this);
+  }
 }/* TheorySetsPrivate::TheorySetsPrivate() */
 
 
 TheorySetsPrivate::~TheorySetsPrivate()
 {
   delete d_termInfoManager;
+  if( Debug.isOn("sets-scrutinize") ) {
+    Assert(d_scrutinize != NULL);
+    delete d_scrutinize;
+  }
 }
 
 
@@ -998,6 +1035,7 @@ void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
                          << " in " << S << " " << polarity << std::endl;
 
   d_info[S]->addToElementList(x, polarity);
+  d_info[x]->addToSetList(S, polarity);
 }
 
 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
@@ -1029,46 +1067,78 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
 }
 
 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
+(TNode x, TNode S, bool polarity)
+{
+  Node cur_atom = MEMBER(x, S);
+
+  // propagation : empty set
+  if(polarity && S.getKind() == kind::EMPTYSET) {
+    Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
+                       << std::endl;
+    d_theory.learnLiteral(cur_atom, false, cur_atom);
+    return;
+  }// propagation: empty set
+
+  // propagation : children
+  if(S.getKind() == kind::UNION ||
+     S.getKind() == kind::INTERSECTION ||
+     S.getKind() == kind::SETMINUS ||
+     S.getKind() == kind::SET_SINGLETON) {
+    d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
+  }// propagation: children
+
+  // propagation : parents
+  const CDTNodeList* parentList = getParents(S);
+  for(typeof(parentList->begin()) k = parentList->begin();
+      k != parentList->end(); ++k) {
+    d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
+  }// propagation : parents
+
+}
+
+void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
+(TNode x, CDTNodeList* l, bool polarity)
+{
+  set<TNode> alreadyProcessed;
+
+  BOOST_FOREACH(TNode S, (*l) ) {
+    Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
+                       << MEMBER(x, d_eqEngine->getRepresentative(S))
+                       << std::endl;
+
+    TNode repS = d_eqEngine->getRepresentative(S);
+    if(alreadyProcessed.find(repS) != alreadyProcessed.end()) {
+      continue;
+    } else {
+      alreadyProcessed.insert(repS);
+    }
+
+    d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), repS));
+
+    for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
+        !j.isFinished(); ++j) {
+
+      pushToSettermPropagationQueue(x, *j, polarity);
+
+    }//j loop
+  }
+}
+
+void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
 (CDTNodeList* l, TNode S, bool polarity)
 {
-  for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
+  BOOST_FOREACH(TNode x, (*l) ) {
     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
-                       << MEMBER(*i, d_eqEngine->getRepresentative(S))
+                       << MEMBER(x, d_eqEngine->getRepresentative(S))
                        << std::endl;
 
-    d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(*i),
+    d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x),
 			       d_eqEngine->getRepresentative(S)));
 
     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
         !j.isFinished(); ++j) {
 
-      TNode x = (*i);
-      TNode S = (*j);
-      Node cur_atom = MEMBER(x, S);
-
-      // propagation : empty set
-      if(polarity && S.getKind() == kind::EMPTYSET) {
-        Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
-                           << std::endl;
-        d_theory.learnLiteral(cur_atom, false, cur_atom);
-        return;
-      }// propagation: empty set
-
-      // propagation : children
-      if(S.getKind() == kind::UNION ||
-         S.getKind() == kind::INTERSECTION ||
-         S.getKind() == kind::SETMINUS ||
-         S.getKind() == kind::SET_SINGLETON) {
-        d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
-      }// propagation: children
-
-      // propagation : parents
-      const CDTNodeList* parentList = getParents(S);
-      for(typeof(parentList->begin()) k = parentList->begin();
-          k != parentList->end(); ++k) {
-        d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
-      }// propagation : parents
-
+      pushToSettermPropagationQueue(x, *j, polarity);
 
     }//j loop
 
@@ -1076,11 +1146,10 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
 
 }
 
-void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
-  // merge b into a
 
-  if(!a.getType().isSet()) return;
 
+void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
+  // merge b into a
   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
                          << ", b = " << b << std::endl;
   Debug("sets-terminfo") << "[sets-terminfo] reps"
@@ -1094,16 +1163,25 @@ void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
   Assert(ita != d_info.end());
   Assert(itb != d_info.end());
 
+  /* elements in this sets */
   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
-
   mergeLists((*ita).second->elementsInThisSet,
              (*itb).second->elementsInThisSet);
-
   mergeLists((*ita).second->elementsNotInThisSet,
              (*itb).second->elementsNotInThisSet);
+
+  /* sets containing this element */
+  pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true);
+  pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false);
+  pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false);
+  pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true);
+  mergeLists( (*ita).second->setsContainingThisElement,
+              (*itb).second->setsContainingThisElement );
+  mergeLists( (*ita).second->setsNotContainingThisElement,
+              (*itb).second->setsNotContainingThisElement );
 }
 
 
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 9576384bb..7e9d60905 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -33,6 +33,7 @@ namespace sets {
 /** Internal classes, forward declared here */
 class TheorySetsTermInfoManager;
 class TheorySets;
+class TheorySetsScrutinize;
 
 class TheorySetsPrivate {
 public:
@@ -107,7 +108,9 @@ private:
     std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> d_info;
 
     void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const;
+    void pushToSettermPropagationQueue(TNode x, TNode S, bool polarity);
     void pushToSettermPropagationQueue(CDTNodeList* l, TNode S, bool polarity);
+    void pushToSettermPropagationQueue(TNode x, CDTNodeList* l, bool polarity);
   public:
     TermInfoManager(TheorySetsPrivate&,
                     context::Context* satContext,
@@ -166,6 +169,10 @@ private:
   const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) const;
   Node elementsToShape(Elements elements, TypeNode setType) const;
   bool checkModel(const SettermElementsMap& settermElementsMap, TNode S) const;
+
+  // more debugging stuff
+  friend class TheorySetsScrutinize;
+  TheorySetsScrutinize* d_scrutinize;
 };/* class TheorySetsPrivate */
 
 
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9a23d5518..c52ee936a 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -176,7 +176,7 @@ std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 }
 
 
-void Theory::collectTerms(TNode n, set<Node>& termSet)
+void Theory::collectTerms(TNode n, set<Node>& termSet) const
 {
   if (termSet.find(n) != termSet.end()) {
     return;
@@ -191,7 +191,7 @@ void Theory::collectTerms(TNode n, set<Node>& termSet)
 }
 
 
-void Theory::computeRelevantTerms(set<Node>& termSet)
+void Theory::computeRelevantTerms(set<Node>& termSet) const
 {
   // Collect all terms appearing in assertions
   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
diff --git a/src/theory/theory.h b/src/theory/theory.h
index ff648e1f2..c86aa17de 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -229,12 +229,14 @@ protected:
   /**
    * Helper function for computeRelevantTerms
    */
-  void collectTerms(TNode n, std::set<Node>& termSet);
+  void collectTerms(TNode n, std::set<Node>& termSet) const;
   /**
-   * Scans the current set of assertions and shared terms top-down until a theory-leaf is reached, and adds all terms found to termSet.
-   * This is used by collectModelInfo to delimit the set of terms that should be used when constructing a model
+   * Scans the current set of assertions and shared terms top-down
+   * until a theory-leaf is reached, and adds all terms found to
+   * termSet.  This is used by collectModelInfo to delimit the set of
+   * terms that should be used when constructing a model
    */
-  void computeRelevantTerms(std::set<Node>& termSet);
+  void computeRelevantTerms(std::set<Node>& termSet) const;
 
   /**
    * Construct a Theory.
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index fe53838be..6d718553d 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -55,6 +55,10 @@ TESTS =	\
 	eqtest.smt2 \
 	mar2014/lemmabug-ListElts317minimized.smt2 \
 	mar2014/sharing-preregister.smt2 \
+	mar2014/small.smt2 \
+	mar2014/smaller.smt2 \
+	mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \
+	mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \
 	emptyset.smt2 \
 	error2.smt2
 
diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
new file mode 100644
index 000000000..e6f187331
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
@@ -0,0 +1,209 @@
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+
+(declare-fun z3v66 () Int)
+(declare-fun z3v67 () Int)
+(assert (distinct z3v66 z3v67))
+
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3f72 (Int) mySet)
+(declare-fun z3f76 (Int) Bool)
+(declare-fun z3f77 (Int Int) Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3f79 (Int) Bool)
+(declare-fun z3v80 () Int)
+(declare-fun z3f81 (Int) Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v83 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3f88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3v92 () Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3f94 (Int) Int)
+(declare-fun z3f95 (Int) Int)
+(declare-fun z3f96 (Int Int Int) Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v98 () Int)
+(declare-fun z3v99 () Int)
+(declare-fun z3v100 () Int)
+(declare-fun z3v101 () Int)
+(declare-fun z3v102 () Int)
+(declare-fun z3v103 () Int)
+(declare-fun z3v104 () Int)
+(declare-fun z3v105 () Int)
+(declare-fun z3v106 () Int)
+(declare-fun z3v107 () Int)
+(declare-fun z3v108 () Int)
+(declare-fun z3v109 () Int)
+(declare-fun z3v110 () Int)
+(declare-fun z3v113 () Int)
+(declare-fun z3v114 () Int)
+(declare-fun z3v115 () Int)
+(declare-fun z3v116 () Int)
+(declare-fun z3v117 () Int)
+(declare-fun z3v118 () Int)
+(declare-fun z3v120 () Int)
+(declare-fun z3v121 () Int)
+(declare-fun z3v122 () Int)
+(declare-fun z3v124 () Int)
+(declare-fun z3v125 () Int)
+(declare-fun z3v126 () Int)
+(declare-fun z3v127 () Int)
+(declare-fun z3v128 () Int)
+(declare-fun z3v129 () Int)
+(declare-fun z3v131 () Int)
+(declare-fun z3v132 () Int)
+(declare-fun z3v133 () Int)
+(declare-fun z3v134 () Int)
+(declare-fun z3v135 () Int)
+(declare-fun z3v136 () Int)
+(declare-fun z3v137 () Int)
+(declare-fun z3v138 () Int)
+(declare-fun z3v139 () Int)
+(declare-fun z3v140 () Int)
+(declare-fun z3v141 () Int)
+(declare-fun z3v142 () Int)
+(declare-fun z3v144 () Int)
+(declare-fun z3v145 () Int)
+(declare-fun z3v146 () Int)
+(declare-fun z3v149 () Int)
+(declare-fun z3v151 () Int)
+(declare-fun z3v154 () Int)
+(declare-fun z3v155 () Int)
+(declare-fun z3v156 () Int)
+(declare-fun z3v157 () Int)
+(declare-fun z3v158 () Int)
+(declare-fun z3v159 () Int)
+(declare-fun z3v161 () Int)
+(declare-fun z3v163 () Int)
+(declare-fun z3v164 () Int)
+(declare-fun z3v165 () Int)
+(declare-fun z3v167 () Int)
+(declare-fun z3v170 () Int)
+(declare-fun z3v174 () Int)
+(declare-fun z3v175 () Int)
+(declare-fun z3v176 () Int)
+(declare-fun z3v179 () Int)
+(declare-fun z3v181 () Int)
+(declare-fun z3v182 () Int)
+(declare-fun z3v183 () Int)
+(declare-fun z3v184 () Int)
+(declare-fun z3v187 () Int)
+(declare-fun z3v188 () Int)
+(declare-fun z3v189 () Int)
+(declare-fun z3v190 () Int)
+(declare-fun z3f191 (Int) Int)
+(declare-fun z3f192 (Int) Int)
+(declare-fun z3v195 () Int)
+(declare-fun z3v196 () Int)
+(declare-fun z3v199 () Int)
+(declare-fun z3v200 () Int)
+(declare-fun z3v201 () Int)
+(declare-fun z3v202 () Int)
+(declare-fun z3v203 () Int)
+(declare-fun z3v206 () Int)
+(declare-fun z3v207 () Int)
+(declare-fun z3v208 () Int)
+(declare-fun z3v210 () Int)
+(declare-fun z3v211 () Int)
+(declare-fun z3v212 () Int)
+(declare-fun z3f213 (Int) Bool)
+(declare-fun z3f214 (Int) Int)
+(declare-fun z3v215 () Int)
+(declare-fun z3v216 () Int)
+(declare-fun z3v218 () Int)
+(declare-fun z3v220 () Int)
+(declare-fun z3v221 () Int)
+(declare-fun z3v222 () Int)
+(declare-fun z3v223 () Int)
+(declare-fun z3v224 () Int)
+(declare-fun z3v225 () Int)
+(declare-fun z3v226 () Int)
+(declare-fun z3v227 () Int)
+(declare-fun z3v228 () Int)
+(declare-fun z3v229 () Int)
+(declare-fun z3v230 () Int)
+(declare-fun z3v231 () Int)
+(declare-fun z3v233 () Int)
+(declare-fun z3v236 () Int)
+(declare-fun z3v242 () Int)
+(declare-fun z3v243 () Int)
+(declare-fun z3v244 () Int)
+(declare-fun z3v245 () Int)
+(declare-fun z3v247 () Int)
+(declare-fun z3v248 () Int)
+(declare-fun z3v249 () Int)
+(declare-fun z3v250 () Int)
+(declare-fun z3v251 () Int)
+(declare-fun z3v252 () Int)
+(declare-fun z3v253 () Int)
+(declare-fun z3v255 () Int)
+(declare-fun z3v256 () Int)
+(declare-fun z3v258 () Int)
+(declare-fun z3v259 () Int)
+(declare-fun z3v261 () Int)
+(declare-fun z3v262 () Int)
+(declare-fun z3v263 () Int)
+(declare-fun z3v264 () Int)
+(declare-fun z3v266 () Int)
+(declare-fun z3v268 () Int)
+(declare-fun z3v270 () Int)
+(declare-fun z3v271 () Int)
+(declare-fun z3v272 () Int)
+
+(assert (and (not (smt_set_mem z3v132 (z3f70 z3v131)))
+	     (= (z3f72 z3v131) smt_set_emp)
+	     (= (z3f72 z3v133) smt_set_emp)
+	     (= (z3f72 z3v242)
+		(ite (smt_set_mem z3v271 (z3f70 z3v270))
+		     (smt_set_cup (smt_set_add smt_set_emp z3v271)
+				  (z3f72 z3v270))
+		     (z3f72 z3v270)))
+	     (= (z3f70 z3v242)
+		(smt_set_cup (smt_set_add smt_set_emp z3v271)
+			     (z3f70 z3v270)))
+	     (= z3v242 (z3f77 z3v271 z3v270))
+	     (= z3v242 z3v243)
+	     (smt_set_sub (z3f70 z3v242)
+	     		  (z3f70 z3v244))
+	     (= (z3f72 z3v242) smt_set_emp)
+	     (smt_set_sub (z3f70 z3v243)
+			  (z3f70 z3v244))
+	     (= (z3f72 z3v243) smt_set_emp)
+	     (= (z3f72 z3v244)
+		(ite (smt_set_mem z3v132 (z3f70 z3v131))
+		     (smt_set_cup (smt_set_add smt_set_emp z3v132)
+				  (z3f72 z3v131))
+		     (z3f72 z3v131)))
+	     (= (z3f70 z3v244)
+	     	(smt_set_cup (smt_set_add smt_set_emp z3v132)
+	     		     (z3f70 z3v131)))
+	     (= (z3f94 z3v134) z3v133)
+	     (= (z3f95 z3v134) z3v131)
+	     (= z3v134 z3v135)
+	     (= (smt_set_cap (z3f70 (z3f94 z3v134))
+			     (z3f70 (z3f95 z3v134))) smt_set_emp)
+	     (= (smt_set_cap (z3f70 (z3f94 z3v135))
+			     (z3f70 (z3f95 z3v135))) smt_set_emp)
+	     (= z3v272 z3v133)
+	     (= (z3f72 z3v272) smt_set_emp)
+  	     (= (z3f81 z3v80) z3v80)
+	     (= (z3f81 z3v82) z3v82)
+	     (= (z3f81 z3v83) z3v83)
+	     ))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
new file mode 100644
index 000000000..b8a27b967
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
@@ -0,0 +1,202 @@
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3f72 (Int) mySet)
+(declare-fun z3f76 (Int) Bool)
+(declare-fun z3f77 (Int Int) Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3f79 (Int) Bool)
+(declare-fun z3v80 () Int)
+(declare-fun z3f81 (Int) Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v83 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3f88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3v92 () Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3f94 (Int) Int)
+(declare-fun z3f95 (Int) Int)
+(declare-fun z3f96 (Int Int Int) Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v98 () Int)
+(declare-fun z3v99 () Int)
+(declare-fun z3v100 () Int)
+(declare-fun z3v101 () Int)
+(declare-fun z3v102 () Int)
+(declare-fun z3v103 () Int)
+(declare-fun z3v104 () Int)
+(declare-fun z3v105 () Int)
+(declare-fun z3v106 () Int)
+(declare-fun z3v107 () Int)
+(declare-fun z3v108 () Int)
+(declare-fun z3v109 () Int)
+(declare-fun z3v110 () Int)
+(declare-fun z3v113 () Int)
+(declare-fun z3v114 () Int)
+(declare-fun z3v115 () Int)
+(declare-fun z3v116 () Int)
+(declare-fun z3v117 () Int)
+(declare-fun z3v118 () Int)
+(declare-fun z3v120 () Int)
+(declare-fun z3v121 () Int)
+(declare-fun z3v122 () Int)
+(declare-fun z3v124 () Int)
+(declare-fun z3v125 () Int)
+(declare-fun z3v126 () Int)
+(declare-fun z3v127 () Int)
+(declare-fun z3v128 () Int)
+(declare-fun z3v129 () Int)
+(declare-fun z3v131 () Int)
+(declare-fun z3v132 () Int)
+(declare-fun z3v133 () Int)
+(declare-fun z3v134 () Int)
+(declare-fun z3v135 () Int)
+(declare-fun z3v136 () Int)
+(declare-fun z3v137 () Int)
+(declare-fun z3v138 () Int)
+(declare-fun z3v139 () Int)
+(declare-fun z3v140 () Int)
+(declare-fun z3v141 () Int)
+(declare-fun z3v142 () Int)
+(declare-fun z3v144 () Int)
+(declare-fun z3v145 () Int)
+(declare-fun z3v146 () Int)
+(declare-fun z3v149 () Int)
+(declare-fun z3v151 () Int)
+(declare-fun z3v154 () Int)
+(declare-fun z3v155 () Int)
+(declare-fun z3v156 () Int)
+(declare-fun z3v157 () Int)
+(declare-fun z3v158 () Int)
+(declare-fun z3v159 () Int)
+(declare-fun z3v161 () Int)
+(declare-fun z3v163 () Int)
+(declare-fun z3v164 () Int)
+(declare-fun z3v165 () Int)
+(declare-fun z3v167 () Int)
+(declare-fun z3v170 () Int)
+(declare-fun z3v174 () Int)
+(declare-fun z3v175 () Int)
+(declare-fun z3v176 () Int)
+(declare-fun z3v179 () Int)
+(declare-fun z3v181 () Int)
+(declare-fun z3v182 () Int)
+(declare-fun z3v183 () Int)
+(declare-fun z3v184 () Int)
+(declare-fun z3v187 () Int)
+(declare-fun z3v188 () Int)
+(declare-fun z3v189 () Int)
+(declare-fun z3v190 () Int)
+(declare-fun z3f191 (Int) Int)
+(declare-fun z3f192 (Int) Int)
+(declare-fun z3v195 () Int)
+(declare-fun z3v196 () Int)
+(declare-fun z3v199 () Int)
+(declare-fun z3v200 () Int)
+(declare-fun z3v201 () Int)
+(declare-fun z3v202 () Int)
+(declare-fun z3v203 () Int)
+(declare-fun z3v206 () Int)
+(declare-fun z3v207 () Int)
+(declare-fun z3v208 () Int)
+(declare-fun z3v210 () Int)
+(declare-fun z3v211 () Int)
+(declare-fun z3v212 () Int)
+(declare-fun z3f213 (Int) Bool)
+(declare-fun z3f214 (Int) Int)
+(declare-fun z3v215 () Int)
+(declare-fun z3v216 () Int)
+(declare-fun z3v218 () Int)
+(declare-fun z3v220 () Int)
+(declare-fun z3v221 () Int)
+(declare-fun z3v222 () Int)
+(declare-fun z3v223 () Int)
+(declare-fun z3v224 () Int)
+(declare-fun z3v225 () Int)
+(declare-fun z3v226 () Int)
+(declare-fun z3v227 () Int)
+(declare-fun z3v228 () Int)
+(declare-fun z3v229 () Int)
+(declare-fun z3v230 () Int)
+(declare-fun z3v231 () Int)
+(declare-fun z3v233 () Int)
+(declare-fun z3v236 () Int)
+(declare-fun z3v242 () Int)
+(declare-fun z3v243 () Int)
+(declare-fun z3v244 () Int)
+(declare-fun z3v245 () Int)
+(declare-fun z3v247 () Int)
+(declare-fun z3v248 () Int)
+(declare-fun z3v249 () Int)
+(declare-fun z3v250 () Int)
+(declare-fun z3v251 () Int)
+(declare-fun z3v252 () Int)
+(declare-fun z3v253 () Int)
+(declare-fun z3v255 () Int)
+(declare-fun z3v256 () Int)
+(declare-fun z3v258 () Int)
+(declare-fun z3v259 () Int)
+(declare-fun z3v261 () Int)
+(declare-fun z3v262 () Int)
+(declare-fun z3v263 () Int)
+(declare-fun z3v264 () Int)
+(declare-fun z3v266 () Int)
+(declare-fun z3v268 () Int)
+(declare-fun z3v270 () Int)
+(declare-fun z3v271 () Int)
+(declare-fun z3v272 () Int)
+
+
+(declare-fun z3v66 () Int)
+(declare-fun z3v67 () Int)
+(assert (distinct z3v66 z3v67))
+(assert (not (smt_set_mem z3v132 (z3f70 z3v131))))
+(assert (= (z3f72 z3v131) smt_set_emp))
+(assert (= (z3f72 z3v242)
+           (ite (smt_set_mem z3v271 (z3f70 z3v270))
+                (smt_set_cup (smt_set_add smt_set_emp z3v271)
+                             (z3f72 z3v270))
+                (z3f72 z3v270))))
+(assert (= (z3f70 z3v242)
+           (smt_set_cup (smt_set_add smt_set_emp z3v271)
+                        (z3f70 z3v270))))
+(assert (= z3v242 (z3f77 z3v271 z3v270)))
+(assert (= z3v242 z3v243))
+(assert (subseteq (z3f70 z3v242)
+                  (z3f70 z3v244)))
+(assert (= (z3f72 z3v243) smt_set_emp))
+(assert (= (z3f72 z3v244)
+           (ite (smt_set_mem z3v132 (z3f70 z3v131))
+                (smt_set_cup (smt_set_add smt_set_emp z3v132)
+                             (z3f72 z3v131))
+                (z3f72 z3v131))))
+(assert (= (z3f70 z3v244)
+           (smt_set_cup (smt_set_add smt_set_emp z3v132)
+                        (z3f70 z3v131))))
+(assert (= (z3f94 z3v134) z3v133))
+(assert (= (z3f95 z3v134) z3v131))
+(assert (= z3v134 z3v135))
+(assert (= (smt_set_cap (z3f70 (z3f94 z3v135))
+                        (z3f70 (z3f95 z3v135))) smt_set_emp))
+(assert (= z3v272 z3v133))
+(assert (= (z3f72 z3v272) smt_set_emp))
+(assert (= (z3f81 z3v80) z3v80))
+(assert (= (z3f81 z3v82) z3v82))
+(assert (= (z3f81 z3v83) z3v83))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/mar2014/small.smt2 b/test/regress/regress0/sets/mar2014/small.smt2
new file mode 100644
index 000000000..838a27919
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/small.smt2
@@ -0,0 +1,18 @@
+; EXPECT: unsat
+; COMMAND-LINE: --simplification=none
+
+; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2
+; unlike original benchmark, this is unsat.
+
+(set-logic QF_UFLIA_SETS)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(assert (in x (union a b)))
+(assert (not (in y a)))
+(assert (not (in z b)))
+(assert (= z y))
+(assert (= x y))
+(check-sat)
diff --git a/test/regress/regress0/sets/mar2014/smaller.smt2 b/test/regress/regress0/sets/mar2014/smaller.smt2
new file mode 100644
index 000000000..876311de8
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/smaller.smt2
@@ -0,0 +1,15 @@
+; EXPECT: sat
+; COMMAND-LINE: --simplification=none
+
+; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2
+; fails check-model, even though answer is correct
+
+(set-logic QF_UFLIA_SETS)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(assert (in x (union a b)))
+(assert (not (in y a)))
+(assert (= x y))
+(check-sat)