diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-09-14 03:22:51 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-09-14 03:22:51 +0000 |
commit | d37cfff40c4e72f476b3ee5c1eb2c0f9790fcf00 (patch) | |
tree | 7d5b2023783e4612b62bb1ed8e2bc0735187d818 /src/util/congruence_closure.h | |
parent | bd9eb727cd4897a8dbb80ea730082886ce1c18e4 (diff) |
ensure uf/congruence closure debugging stuff isn't called in production builds
Diffstat (limited to 'src/util/congruence_closure.h')
-rw-r--r-- | src/util/congruence_closure.h | 104 |
1 files changed, 64 insertions, 40 deletions
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 7d7e26bbe..2b7cddcf0 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -43,6 +43,11 @@ template <class OutputChannel> std::ostream& operator<<(std::ostream& out, const CongruenceClosure<OutputChannel>& cc); +/** + * A CongruenceClosureException is thrown by + * CongruenceClosure::explain() when that method is asked to explain a + * congruence that doesn't exist. + */ class CVC4_PUBLIC CongruenceClosureException : public Exception { public: inline CongruenceClosureException(std::string msg) : @@ -158,7 +163,9 @@ public: * indirectly, so it can throw anything that that function can. */ void addEquality(TNode inputEq) { - Debug("cc") << "CC addEquality[" << d_context->getLevel() << "]: " << inputEq << std::endl; + if(Debug.isOn("cc")) { + Debug("cc") << "CC addEquality[" << d_context->getLevel() << "]: " << inputEq << std::endl; + } Assert(inputEq.getKind() == kind::EQUAL || inputEq.getKind() == kind::IFF); NodeBuilder<> eqb(inputEq.getKind()); @@ -216,11 +223,13 @@ public: * context. */ inline bool areCongruent(TNode a, TNode b) const throw(AssertionException) { - Debug("cc") << "CC areCongruent? " << a << " == " << b << std::endl; - Debug("cc") << " a " << a << std::endl; - Debug("cc") << " a' " << normalize(a) << std::endl; - Debug("cc") << " b " << b << std::endl; - Debug("cc") << " b' " << normalize(b) << std::endl; + if(Debug.isOn("cc")) { + Debug("cc") << "CC areCongruent? " << a << " == " << b << std::endl; + Debug("cc") << " a " << a << std::endl; + Debug("cc") << " a' " << normalize(a) << std::endl; + Debug("cc") << " b " << b << std::endl; + Debug("cc") << " b' " << normalize(b) << std::endl; + } Node ap = find(a), bp = find(b); @@ -365,9 +374,11 @@ void CongruenceClosure<OutputChannel>::addTerm(TNode t) { Node trm = replace(flatten(t)); Node trmp = find(trm); - Debug("cc") << "CC addTerm [" << d_careSet.size() << "] " << d_careSet.contains(t) << ": " << t << std::endl - << " [" << d_careSet.size() << "] " << d_careSet.contains(trm) << ": " << trm << std::endl - << " [" << d_careSet.size() << "] " << d_careSet.contains(trmp) << ": " << trmp << std::endl; + if(Debug.isOn("cc")) { + Debug("cc") << "CC addTerm [" << d_careSet.size() << "] " << d_careSet.contains(t) << ": " << t << std::endl + << " [" << d_careSet.size() << "] " << d_careSet.contains(trm) << ": " << trm << std::endl + << " [" << d_careSet.size() << "] " << d_careSet.contains(trmp) << ": " << trmp << std::endl; + } if(t != trm && !d_careSet.contains(t)) { // we take care to only notify our client once of congruences @@ -393,7 +404,9 @@ template <class OutputChannel> void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) { d_proofRewrite[eq] = inputEq; - Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl; + if(Debug.isOn("cc")) { + Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl; + } Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF); Assert(eq[1].getKind() != kind::APPLY_UF); @@ -458,7 +471,7 @@ Node CongruenceClosure<OutputChannel>::buildRepresentativesOfApply(TNode apply, template <class OutputChannel> void CongruenceClosure<OutputChannel>::propagate(TNode seed) { Debug("cc:detail") << "=== doing a round of propagation ===" << std::endl - << "the \"seed\" propagation is: " << seed << std::endl; + << "the \"seed\" propagation is: " << seed << std::endl; std::list<Node> pending; @@ -468,8 +481,8 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { Node e = pending.front(); pending.pop_front(); - Debug("cc") << "=== top of propagate loop ===" << std::endl; - Debug("cc") << "=== e is " << e << " ===" << std::endl; + Debug("cc") << "=== top of propagate loop ===" << std::endl + << "=== e is " << e << " ===" << std::endl; TNode a, b; if(e.getKind() == kind::EQUAL || @@ -503,12 +516,14 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { Debug("cc") << " ( " << a << " , " << b << " )" << std::endl; } - Debug("cc:detail") << "=====at start=====" << std::endl - << "a :" << a << std::endl - << "NORMALIZE a:" << normalize(a) << std::endl - << "b :" << b << std::endl - << "NORMALIZE b:" << normalize(b) << std::endl - << "alreadyCongruent?:" << areCongruent(a,b) << std::endl; + if(Debug.isOn("cc")) { + Debug("cc:detail") << "=====at start=====" << std::endl + << "a :" << a << std::endl + << "NORMALIZE a:" << normalize(a) << std::endl + << "b :" << b << std::endl + << "NORMALIZE b:" << normalize(b) << std::endl + << "alreadyCongruent?:" << areCongruent(a,b) << std::endl; + } // change from paper: need to normalize() here since in our // implementation, a and b can be applications @@ -557,9 +572,11 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { i != cl->end(); ++i) { TNode c = *i; - Debug("cc") << "c is " << c << "\n" - << " from cl of " << ap << std::endl; - Debug("cc") << " it's find ptr is: " << find(c) << std::endl; + if(Debug.isOn("cc")) { + Debug("cc") << "c is " << c << "\n" + << " from cl of " << ap << std::endl; + Debug("cc") << " it's find ptr is: " << find(c) << std::endl; + } Assert(find(c) == ap); Debug("cc:detail") << "calling merge2 " << c << bp << std::endl; merge(c, bp); @@ -573,9 +590,11 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { } { // use list handling - Debug("cc:detail") << "ap is " << ap << std::endl; - Debug("cc:detail") << "find(ap) is " << find(ap) << std::endl; - Debug("cc:detail") << "CC in prop go through useList of " << ap << std::endl; + if(Debug.isOn("cc:detail")) { + Debug("cc:detail") << "ap is " << ap << std::endl; + Debug("cc:detail") << "find(ap) is " << find(ap) << std::endl; + Debug("cc:detail") << "CC in prop go through useList of " << ap << std::endl; + } UseLists::iterator usei = d_useList.find(ap); if(usei != d_useList.end()) { UseList* ul = (*usei).second; @@ -628,16 +647,17 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { }/* use lists */ Debug("cc:detail") << "CC in prop done with useList of " << ap << std::endl; } else { - Debug("cc:detail") << "CCs the same ( == " << ap << "), do nothing." - << std::endl; + Debug("cc:detail") << "CCs the same ( == " << ap << "), do nothing." << std::endl; } - Debug("cc") << "=====at end=====" << std::endl - << "a :" << a << std::endl - << "NORMALIZE a:" << normalize(a) << std::endl - << "b :" << b << std::endl - << "NORMALIZE b:" << normalize(b) << std::endl - << "alreadyCongruent?:" << areCongruent(a,b) << std::endl; + if(Debug.isOn("cc")) { + Debug("cc") << "=====at end=====" << std::endl + << "a :" << a << std::endl + << "NORMALIZE a:" << normalize(a) << std::endl + << "b :" << b << std::endl + << "NORMALIZE b:" << normalize(b) << std::endl + << "alreadyCongruent?:" << areCongruent(a,b) << std::endl; + } Assert(areCongruent(a, b)); } while(!pending.empty()); }/* propagate() */ @@ -646,12 +666,14 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { template <class OutputChannel> void CongruenceClosure<OutputChannel>::merge(TNode ec1, TNode ec2) { /* - Debug("cc:detail") << " -- merging " << ec1 - << (d_careSet.find(ec1) == d_careSet.end() ? - " -- NOT in care set" : " -- IN CARE SET") << std::endl - << " and " << ec2 - << (d_careSet.find(ec2) == d_careSet.end() ? - " -- NOT in care set" : " -- IN CARE SET") << std::endl; + if(Debug.isOn("cc:detail")) { + Debug("cc:detail") << " -- merging " << ec1 + << (d_careSet.find(ec1) == d_careSet.end() ? + " -- NOT in care set" : " -- IN CARE SET") << std::endl + << " and " << ec2 + << (d_careSet.find(ec2) == d_careSet.end() ? + " -- NOT in care set" : " -- IN CARE SET") << std::endl; + } */ Debug("cc") << "CC setting rep of " << ec1 << std::endl; @@ -850,7 +872,9 @@ Node CongruenceClosure<OutputChannel>::explain(Node a, Node b) explainAlongPath(b, c, pending, unionFind, terms); } while(!pending.empty()); - Debug("cc") << "CC EXPLAIN final proof has size " << terms.size() << std::endl; + if(Debug.isOn("cc")) { + Debug("cc") << "CC EXPLAIN final proof has size " << terms.size() << std::endl; + } NodeBuilder<> pf(kind::AND); while(!terms.empty()) { |