some debugging changes

diff --git a/src/Makefile.am b/src/Makefile.am
index d75535e1587b18fc54e3218dff3a24f4c22353c1..2d306d4649118be6fe44d285d0ba0a9f0a4482cc 100644 (file)
--- 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/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h
new file mode 100644 (file)
index 0000000..a0e2a1d
--- /dev/null
+++ b/src/theory/sets/scrutinize.h
@@ -0,0 +1,44 @@
+/*********************                                                        */
+/*! \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 "theory/sets/theory_sets_private.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsScrutinize {
+  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
+  }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f487e1566a9b76f079c31c9665d895dcd16d4604..b29e2d4c6fbadc0eb0b8125d726cfc6b9830592b 100644 (file)
--- 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"
 
@@ -88,7 +89,10 @@ 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) {
+      if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); }
+      return;
+    }
     Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
   }
 
@@ -96,6 +100,8 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     d_external.d_out->lemma(getLemma());
   }
 
+  if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); }
+
   return;
 }/* TheorySetsPrivate::check() */
 
@@ -526,14 +532,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 +605,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 +759,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 +771,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 +782,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 +801,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 +812,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;
+  }
 }
 
 

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 9576384bbcf336b9b29bc4bdbfe45e1a3e4a379c..a4c9fb726979156a708e55f061125a5cbe6789ba 100644 (file)
--- 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:
@@ -166,6 +167,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 */