From: Kshitij Bansal Date: Sun, 24 Aug 2014 21:34:02 +0000 (-0400) Subject: remove some debugging code X-Git-Tag: cvc5-1.0.0~6648 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8fc068f1f70f5f8e6f5494d7709d681cc9d7d7f9;p=cvc5.git 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 a8f6dcc38..d9cc23cbf 100644 --- 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::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 > 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& 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 b293c63e6..72c041d49 100644 --- 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 index eaf29932b..000000000 --- a/src/util/partitions.h +++ /dev/null @@ -1,94 +0,0 @@ -#include -#include - -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 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 , - 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; -} - -} -}