Merge pull request #24 from kbansal/sets-model

sets, misc

7 files changed, 236 insertions, 60 deletions

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.