remove some debugging code

(it can be brought back from version control, if needed)

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index a8f6dcc38c55287e1e86f8409a174e0ae7769113..d9cc23cbf78939909fff66a00901f81cc79e6817 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -27,8 +27,6 @@
 #include "util/emptyset.h"
 #include "util/result.h"
 
-#include "util/partitions.h"
-
 using namespace std;
 using namespace CVC4::expr::pattern;
 
@@ -419,14 +417,8 @@ void TheorySetsPrivate::addSharedTerm(TNode n) {
   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 }
 
-
-void TheorySetsPrivate::computeCareGraph() {
-  Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
-
-  // dump our understanding of assertions
-  if(Trace.isOn("sets-assertions")
-     || Trace.isOn("sets-care-dump"))
-  {
+void TheorySetsPrivate::dumpAssertionsHumanified() const
+{
     std::string tag = "sets-assertions";
     context::CDList<Assertion>::const_iterator it = d_external.facts_begin(), it_end = d_external.facts_end();
 
@@ -438,7 +430,7 @@ void TheorySetsPrivate::computeCareGraph() {
 
     for (unsigned i = 0; it != it_end; ++ it, ++i) {
       TNode ass = (*it).assertion;
-      Trace("sets-care-dump") << AssertCommand(ass.toExpr()) << endl;
+      // Trace("sets-care-dump") << AssertCommand(ass.toExpr()) << endl;
       bool polarity = ass.getKind() != kind::NOT;
       ass = polarity ? ass : ass[0];
       Assert( ass.getNumChildren() == 2);
@@ -512,35 +504,33 @@ void TheorySetsPrivate::computeCareGraph() {
       }
     }
     Trace(tag) << std::endl;
+#undef FORIT
+}
 
-  }
+void TheorySetsPrivate::computeCareGraph() {
+  Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
 
-  std::map<TypeNode, std::set<TNode> > careGraphVertices;
+  if(Trace.isOn("sets-assertions")) {
+    // dump our understanding of assertions
+    dumpAssertionsHumanified();
+  }
 
-  for (unsigned i = d_ccg_i; i < d_external.d_sharedTerms.size(); ++ i) {
+  unsigned i_st = 0;
+  if(options::setsCare1()) { i_st = d_ccg_i; }
+  for (unsigned i = i_st; i < d_external.d_sharedTerms.size(); ++ i) {
     TNode a = d_external.d_sharedTerms[i];
     TypeNode aType = a.getType();
-    // if(a.getType().isSet()) {
-    //   int sizeMem = d_termInfoManager->getMembers(d_equalityEngine.getRepresentative(a))->size();
-    //   int sizeNonMem = d_termInfoManager->getNonMembers(d_equalityEngine.getRepresentative(a))->size();
-    //   Debug("sets-care") << "[sets-care] " << a << " : " << sizeMem << " " << sizeNonMem << std::endl;
-    //   if(sizeMem == 0 && sizeNonMem == 0) continue;
-    // }
-    unsigned j_st;
-    if(i == d_ccg_i) j_st = d_ccg_j + 1;
-    else j_st = i + 1;
+
+    unsigned j_st = i + 1;
+    if(options::setsCare1()) { if(i == d_ccg_i) j_st = d_ccg_j + 1; }
+
     for (unsigned j = j_st; j < d_external.d_sharedTerms.size(); ++ j) {
       TNode b = d_external.d_sharedTerms[j];
       if (b.getType() != aType) {
         // We don't care about the terms of different types
         continue;
       }
-      // if(b.getType().isSet()) {
-      //   int sizeMem = d_termInfoManager->getMembers(d_equalityEngine.getRepresentative(b))->size();
-      //   int sizeNonMem = d_termInfoManager->getNonMembers(d_equalityEngine.getRepresentative(b))->size();
-      //   Debug("sets-care") << "[sets-care] " << a << " : " << sizeMem << " " << sizeNonMem << std::endl;
-      //   if(sizeMem == 0 && sizeNonMem == 0) continue;
-      // }
+
       switch (d_external.d_valuation.getEqualityStatus(a, b)) {
       case EQUALITY_TRUE_AND_PROPAGATED:
         // If we know about it, we should have propagated it, so we can skip
@@ -570,44 +560,12 @@ void TheorySetsPrivate::computeCareGraph() {
           d_ccg_j = j;
           return;
         }
-        if(Trace.isOn("sets-care-dump")) {
-          careGraphVertices[a.getType()].insert(a);
-          careGraphVertices[a.getType()].insert(b);
-        }
         break;
       default:
        Unreachable();
       }
     }
   }
-
-  if(Trace.isOn("sets-care-dump")) {
-    FORIT(it, careGraphVertices) {
-      // Trace("sets-care-dump") << "For " << (*it).first << ": " << std::endl;
-      std::set<TNode>& S = (*it).second;
-      for(util::partition::iterator subsets(S.size());
-          !subsets.isFinished(); ++subsets) {
-        Trace("sets-care-dump") << ";---split---" << std::endl;
-        Trace("sets-care-dump") << ";";
-        for(unsigned i = 0; i < S.size(); ++i) Trace("sets-care-dump") << subsets.get(i);
-        Trace("sets-care-dump") << std::endl;
-        int j = 0;
-        FORIT(jt, (*it).second) {
-          int k = 0;
-          FORIT(kt, (*it).second) {
-            if(j == k) continue;
-            Node n = EQUAL( (*jt), (*kt) );
-            if(!subsets.equal(j, k)) n = NOT(n);
-            Trace("sets-care-dump") << AssertCommand(n.toExpr()) << std::endl;
-            ++k;
-          }
-          ++j;
-        }
-      }
-    }
-    Trace("sets-care-dump") << ";---split---" << std::endl;
-#undef FORIT
-  }
 }
 
 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index b293c63e611fe5e50772c40170287ae4c32a41ed..72c041d491e87cad3259eef475c2d0b96c0b6b25 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -192,6 +192,7 @@ private:
   // more debugging stuff
   friend class TheorySetsScrutinize;
   TheorySetsScrutinize* d_scrutinize;
+  void dumpAssertionsHumanified() const;  /** do some formatting to make them more readable */
 };/* class TheorySetsPrivate */
 
 

diff --git a/src/util/partitions.h b/src/util/partitions.h
deleted file mode 100644 (file)
index eaf2993..0000000
--- a/src/util/partitions.h
+++ /dev/null
@@ -1,94 +0,0 @@
-#include <vector>
-#include <algorithm>
-
-namespace CVC4 {
-namespace util {
-
-class partition
-{
-public:
-  class iterator
-  {
-  public:
-    /** 
-     * iterate over all partitions of [0, 1, ... n-1] (same as
-     * generating equivalence relations)
-     * 
-     * corresponds to n-th bell number (A000110 in OEIS)
-     */
-    iterator(unsigned n, bool first = true);
-
-    unsigned  size()     const { return kappa.size();      }
-
-    /** How many partitions does the current paritioning use */
-    unsigned  subsets()  const { return M[size() - 1] + 1; }
-
-    /** Which partition is 'i' in? Numbering starts with 0. */
-    int get(int i) { return kappa[i]; }
-
-    /** Are 'i' and 'j' in the same partition */
-    bool equal(int i, int j) { return kappa[i] == kappa[j]; }
-
-    /** go to next partitioning */
-    iterator& operator++();
-
-    bool isFinished() { return d_finished; }
-  protected:
-    std::vector<unsigned> kappa, M;
-    bool d_finished;
-  };
-};
-
-/**
-   Implementation from
-   https://www.cs.bgu.ac.il/~orlovm/papers/partitions-source.tar.gz
-
-   Released in public domain by Michael Orlov <orlovm@cs.bgu.ac.il>,
-   according to the accompaning paper (Efficient Generation of Set
-   Partitions, Appendix A).
-
-   --Kshitij Bansal, Tue Aug  5 15:57:20 EDT 2014
-*/
-
-partition::iterator::
-iterator(unsigned n, bool first)
-  : kappa(n), M(n), d_finished(false)
-{
-  if (n <= 0)
-    throw std::invalid_argument
-      ("partition::iterator: n must be positive");
-
-  if (! first)
-    for (unsigned i = 1; i < n; ++i) {
-      kappa[i] = i;
-      M[i] = i;
-    }
-}
-
-partition::iterator&
-partition::iterator::
-operator++()
-{
-  const unsigned n = size();
-
-  for (unsigned i = n-1; i > 0; --i)
-    if (kappa[i] <= M[i-1]) {
-      ++kappa[i];
-
-      const unsigned new_max = std::max(M[i], kappa[i]);
-      M[i] = new_max;
-      for (unsigned j = i + 1; j < n; ++j) {
-        kappa[j] = 0;
-        M[j] = new_max;
-      }
-
-      // integrityCheck();
-      return *this;
-    }
-
-  d_finished = true;
-  return *this;
-}
-
-}
-}