more

5 files changed, 52 insertions, 15 deletions

diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h
index a0e2a1d5b..7343662c6 100644
--- a/src/theory/sets/scrutinize.h
+++ b/src/theory/sets/scrutinize.h
@@ -17,6 +17,9 @@
 
 #pragma once
 
+#include <boost/foreach.hpp>
+
+#include "theory/sets/theory_sets.h"
 #include "theory/sets/theory_sets_private.h"
 
 namespace CVC4 {
@@ -24,7 +27,8 @@ namespace theory {
 namespace sets {
 
 class TheorySetsScrutinize {
-  TheorySetsPrivate* d_theory;
+  /* 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;
@@ -35,6 +39,33 @@ public:
     // 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." );
+    }
   }
 };
 
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 b29e2d4c6..2cc182819 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -89,18 +89,17 @@ void TheorySetsPrivate::check(Theory::Effort level) {
 
     Debug("sets") << "[sets]  in conflict = " << d_conflict << std::endl;
     Assert( d_conflict ^ d_equalityEngine.consistent() );
-    if(d_conflict) {
-      if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); }
-      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(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); }
+  // if we are here, there is no conflict and we are complete
+  if(Debug.isOn("sets-scrutinize")) { d_scrutinize->postCheckInvariants(); }
 
   return;
 }/* TheorySetsPrivate::check() */
@@ -434,7 +433,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 :  { ";
@@ -446,12 +446,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;
 
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.