Bugs resolved by this commit: #314, #322, #359, #364, #365.

See below for details.

* Fix the "assert" name-collision bug (resolves bug #364).

  Our identifiers should never be named "assert", as that's a preprocessor
  definition in <assert.h>, which is often #included indirectly (so simply
  having a policy of not including <assert.h> isn't good enough---one of
  our dependences might include it).  It was once the case that we didn't
  have anything named "assert", but "assert()" has now crept back in.
  Instead, name things "assertFoo()" or similar.  Thanks to Tim for the
  report.

  To fix this, I've changed some of Dejan's circuit-propagator code from
  "assert()" to "assertTrue()".  Ditto for Andy's explanation manager.
  Guys, if you prefer a different name in your code, please change it.

* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
  Inner lets now shadow outer lets (previously, they incorrectly gave an
  error).  Additionally, while looking at this, I found that a sequential let
  was implemented rather than a parallel let.  This is now fixed.  Thanks to
  Liana for the report.

* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).

* There were a lot of Debug lines in bitvectors that had embedded toString()
  calls.  This wasted a LOT of time in debug builds for BV benchmarks
  (like in "make regress").  Added if(Debug.isOn(...)) guards; much faster
  now.

* Support for building public-facing interface documentation only (as opposed
  to all internals documentation).  Now "make doc" does the public-facing and
  "make doc-internals" does documentation of everything.  (Along with changes
  to the nightly build script---which will now build and publish both types
  of Doxygen documentation---this resolves bug #359).

* Fix the lambda typechecking bug (resolves bug #322).  Thanks to Andy for the
  report (a long long time ago--sorry).

* The default output language for all streams is now based on the current set
  of Options (if there is one).  This has been a constant annoyance, especially
  when stringstreams are used to construct output.  However, it doesn't work
  for calls from outside the library, so it's mainly an annoyance-fixer for
  CVC4 library code itself.

* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
  are used only in assertions-enabled builds (and thus give warnings in
  production builds).  This was briefly discussed at the meeting this week.

2 files changed, 39 insertions, 17 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index bb6dfe40b..8cfdab5af 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -345,8 +345,10 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     bits.push_back(utils::mkBitOf(node, i));
   }
 
-  BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
-  BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
+    BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
+  }
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
@@ -363,7 +365,9 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
       bits.push_back(utils::mkTrue()); 
     }
   }
-  BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  }
 }
 
 
@@ -391,7 +395,9 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
     }
   }
   Assert (bits.size() == utils::getSize(node)); 
-  BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  }
 }
 
 void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
@@ -512,7 +518,9 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
     shiftAddMultiplier(res, current, newres);
     res = newres;
   }
-  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  }
 }
 
 void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
@@ -709,7 +717,9 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  }
 }
 
 void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
@@ -740,7 +750,9 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  }
 }
 
 void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
@@ -773,8 +785,9 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
-
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  }
 }
 
 void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
@@ -791,9 +804,10 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
   }
   Assert (bits.size() == high - low + 1);   
 
-  BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
-  BVDebug("bitvector-bb") << "                               with bits " << toString(bits); 
-       
+  if(Debug.isOn("bitvector-bb")) {
+    BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+    BVDebug("bitvector-bb") << "                               with bits " << toString(bits); 
+  }
 }
 
 
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index e43479381..1f15bffa8 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -72,8 +72,10 @@ class BacktrackableSetCollection {
     while (d_nodesInserted < d_memory.size()) {
       const tree_entry_type& node = d_memory.back();
 
-      BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
-                                 << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl;
+      if(Debug.isOn("cd_set_collection")) {
+        BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
+                                     << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl;
+      }
 
       if (node.hasParent()) {
         if (node.isLeft()) {
@@ -278,7 +280,9 @@ public:
 
     // Find the biggest node smaleer than value (it must exist)
     while (set != null) {
-      BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
+      if(Debug.isOn("set_collection")) {
+        BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
+      }
       const tree_entry_type& node = d_memory[set];
       if (node.getValue() >= value) {
         // If the node is bigger than the value, we need a smaller one
@@ -305,7 +309,9 @@ public:
 
     // Find the smallest node bigger than value (it must exist)
     while (set != null) {
-      BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
+      if(Debug.isOn("set_collection")) {
+        BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
+      }
       const tree_entry_type& node = d_memory[set];
       if (node.getValue() <= value) {
         // If the node is smaller than the value, we need a bigger one
@@ -372,7 +378,9 @@ public:
     backtrack();
     Assert(isValid(set));
 
-    BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
+    if(Debug.isOn("set_collection")) {
+      BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
+    }
 
     // Empty set no elements
     if (set == null) {