From d37cfff40c4e72f476b3ee5c1eb2c0f9790fcf00 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 14 Sep 2010 03:22:51 +0000 Subject: [PATCH] ensure uf/congruence closure debugging stuff isn't called in production builds --- src/theory/uf/morgan/theory_uf_morgan.cpp | 61 ++++++++----- src/util/congruence_closure.h | 104 +++++++++++++--------- 2 files changed, 104 insertions(+), 61 deletions(-) diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index f3c16e515..a11fc06d4 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -184,8 +184,10 @@ void TheoryUFMorgan::merge(TNode a, TNode b) { } DiseqList* deq = (*deq_i).second; - Debug("uf") << "a == " << a << std::endl; - Debug("uf") << "size of deq(a) is " << deq->size() << std::endl; + if(Debug.isOn("uf")) { + Debug("uf") << "a == " << a << std::endl; + Debug("uf") << "size of deq(a) is " << deq->size() << std::endl; + } for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) { Debug("uf") << " deq(a) ==> " << *j << std::endl; TNode deqn = *j; @@ -193,10 +195,12 @@ void TheoryUFMorgan::merge(TNode a, TNode b) { deqn.getKind() == kind::IFF); TNode s = deqn[0]; TNode t = deqn[1]; - Debug("uf") << " s ==> " << s << std::endl - << " t ==> " << t << std::endl - << " find(s) ==> " << debugFind(s) << std::endl - << " find(t) ==> " << debugFind(t) << std::endl; + if(Debug.isOn("uf")) { + Debug("uf") << " s ==> " << s << std::endl + << " t ==> " << t << std::endl + << " find(s) ==> " << debugFind(s) << std::endl + << " find(t) ==> " << debugFind(t) << std::endl; + } TNode sp = find(s); TNode tp = find(t); if(sp == tp) { @@ -236,7 +240,9 @@ void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) { deq = (*deq_i).second; } deq->push_back(eq); - Debug("uf") << " size is now " << deq->size() << std::endl; + if(Debug.isOn("uf")) { + Debug("uf") << " size is now " << deq->size() << std::endl; + } } void TheoryUFMorgan::addDisequality(TNode eq) { @@ -282,8 +288,11 @@ void TheoryUFMorgan::check(Effort level) { assertion, d_trueNode); d_cc.addTerm(assertion); d_cc.addEquality(eq); - Debug("uf") << "true == false ? " - << (find(d_trueNode) == find(d_falseNode)) << std::endl; + + if(Debug.isOn("uf")) { + Debug("uf") << "true == false ? " + << (find(d_trueNode) == find(d_falseNode)) << std::endl; + } Assert(find(d_trueNode) != find(d_falseNode)); @@ -302,10 +311,12 @@ void TheoryUFMorgan::check(Effort level) { d_cc.addTerm(a); d_cc.addTerm(b); - Debug("uf") << " a ==> " << a << std::endl - << " b ==> " << b << std::endl - << " find(a) ==> " << debugFind(a) << std::endl - << " find(b) ==> " << debugFind(b) << std::endl; + if(Debug.isOn("uf")) { + Debug("uf") << " a ==> " << a << std::endl + << " b ==> " << b << std::endl + << " find(a) ==> " << debugFind(a) << std::endl + << " find(b) ==> " << debugFind(b) << std::endl; + } // There are two ways to get a conflict here. if(!d_conflict.isNull()) { @@ -338,12 +349,15 @@ void TheoryUFMorgan::check(Effort level) { // assert it's a predicate Assert(assertion[0].getOperator().getType().getRangeType().isBoolean()); - Node eq = NodeManager::currentNM()->mkNode(kind::IFF, assertion[0], d_falseNode); + Node eq = NodeManager::currentNM()->mkNode(kind::IFF, + assertion[0], d_falseNode); d_cc.addTerm(assertion[0]); d_cc.addEquality(eq); - Debug("uf") << "true == false ? " - << (find(d_trueNode) == find(d_falseNode)) << std::endl; + if(Debug.isOn("uf")) { + Debug("uf") << "true == false ? " + << (find(d_trueNode) == find(d_falseNode)) << std::endl; + } Assert(find(d_trueNode) != find(d_falseNode)); @@ -366,11 +380,13 @@ void TheoryUFMorgan::check(Effort level) { TNode left = (*diseqIter)[0]; TNode right = (*diseqIter)[1]; - Debug("uf") << "testing left: " << left << std::endl - << " right: " << right << std::endl - << " find(L): " << debugFind(left) << std::endl - << " find(R): " << debugFind(right) << std::endl - << " areCong: " << d_cc.areCongruent(left, right) << std::endl; + if(Debug.isOn("uf")) { + Debug("uf") << "testing left: " << left << std::endl + << " right: " << right << std::endl + << " find(L): " << debugFind(left) << std::endl + << " find(R): " << debugFind(right) << std::endl + << " areCong: " << d_cc.areCongruent(left, right) << std::endl; + } Assert((debugFind(left) == debugFind(right)) == d_cc.areCongruent(left, right)); } @@ -383,6 +399,9 @@ void TheoryUFMorgan::propagate(Effort level) { } void TheoryUFMorgan::dump() { + if(!Debug.isOn("uf")) { + return; + } Debug("uf") << "============== THEORY_UF ==============" << std::endl; Debug("uf") << "Active assertions list:" << std::endl; for(context::CDList::const_iterator i = d_activeAssertions.begin(); 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 std::ostream& operator<<(std::ostream& out, const CongruenceClosure& 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::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 void CongruenceClosure::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::buildRepresentativesOfApply(TNode apply, template void CongruenceClosure::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 pending; @@ -468,8 +481,8 @@ void CongruenceClosure::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::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::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::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::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::propagate(TNode seed) { template void CongruenceClosure::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::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()) { -- 2.30.2