ensure uf/congruence closure debugging stuff isn't called in production builds

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<Node>::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 <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()) {