Add Valuation::getSatValue() so that theories can access the current

(propositional) assignment for theory atoms.

Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list.
This implementation leads to some compiler warnings in production builds,
but these will be corrected in coming days.  There appears to be a small
speedup in the parser as a result of this fix:

  http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5

Cleaned up a few CD Boolean attribute things.

Various small fixes to coding guidelines / test coverage.

This commit:
* Resolves bug 252 (tracing not disabled in production builds)
* Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())

1 files changed, 63 insertions, 57 deletions

diff --git a/src/util/output.cpp b/src/util/output.cpp
index 34a3af93e..080409ed8 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -34,109 +34,115 @@ NullC nullCvc4Stream CVC4_PUBLIC;
 
 #ifndef CVC4_MUZZLE
 
-#ifdef CVC4_DEBUG
-DebugC Debug CVC4_PUBLIC (&cout);
-#else /* CVC4_DEBUG */
-NullDebugC Debug CVC4_PUBLIC;
-#endif /* CVC4_DEBUG */
-
+DebugC DebugChannel CVC4_PUBLIC (&cout);
 WarningC Warning CVC4_PUBLIC (&cerr);
 MessageC Message CVC4_PUBLIC (&cout);
 NoticeC Notice CVC4_PUBLIC (&cout);
 ChatC Chat CVC4_PUBLIC (&cout);
+TraceC TraceChannel CVC4_PUBLIC (&cout);
 
-#ifdef CVC4_TRACING
-TraceC Trace CVC4_PUBLIC (&cout);
-#else /* CVC4_TRACING */
-NullDebugC Trace CVC4_PUBLIC;
-#endif /* CVC4_TRACING */
-
-void DebugC::printf(const char* tag, const char* fmt, ...) {
-  if(d_tags.find(string(tag)) != d_tags.end()) {
-    // chop off output after 1024 bytes
-    char buf[1024];
-    va_list vl;
-    va_start(vl, fmt);
-    vsnprintf(buf, sizeof(buf), fmt, vl);
-    va_end(vl);
-    *d_os << buf;
+int DebugC::printf(const char* tag, const char* fmt, ...) {
+  if(d_tags.find(string(tag)) == d_tags.end()) {
+    return 0;
   }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
 }
 
-void DebugC::printf(std::string tag, const char* fmt, ...) {
-  if(d_tags.find(tag) != d_tags.end()) {
-    // chop off output after 1024 bytes
-    char buf[1024];
-    va_list vl;
-    va_start(vl, fmt);
-    vsnprintf(buf, sizeof(buf), fmt, vl);
-    va_end(vl);
-    *d_os << buf;
+int DebugC::printf(std::string tag, const char* fmt, ...) {
+  if(d_tags.find(tag) == d_tags.end()) {
+    return 0;
   }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
 }
 
-void WarningC::printf(const char* fmt, ...) {
+int WarningC::printf(const char* fmt, ...) {
   // chop off output after 1024 bytes
   char buf[1024];
   va_list vl;
   va_start(vl, fmt);
-  vsnprintf(buf, sizeof(buf), fmt, vl);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
   va_end(vl);
   *d_os << buf;
+  return retval;
 }
 
-void MessageC::printf(const char* fmt, ...) {
+int MessageC::printf(const char* fmt, ...) {
   // chop off output after 1024 bytes
   char buf[1024];
   va_list vl;
   va_start(vl, fmt);
-  vsnprintf(buf, sizeof(buf), fmt, vl);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
   va_end(vl);
   *d_os << buf;
+  return retval;
 }
 
-void NoticeC::printf(const char* fmt, ...) {
+int NoticeC::printf(const char* fmt, ...) {
   // chop off output after 1024 bytes
   char buf[1024];
   va_list vl;
   va_start(vl, fmt);
-  vsnprintf(buf, sizeof(buf), fmt, vl);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
   va_end(vl);
   *d_os << buf;
+  return retval;
 }
 
-void ChatC::printf(const char* fmt, ...) {
+int ChatC::printf(const char* fmt, ...) {
   // chop off output after 1024 bytes
   char buf[1024];
   va_list vl;
   va_start(vl, fmt);
-  vsnprintf(buf, sizeof(buf), fmt, vl);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
   va_end(vl);
   *d_os << buf;
+  return retval;
 }
 
-void TraceC::printf(const char* tag, const char* fmt, ...) {
-  if(d_tags.find(string(tag)) != d_tags.end()) {
-    // chop off output after 1024 bytes
-    char buf[1024];
-    va_list vl;
-    va_start(vl, fmt);
-    vsnprintf(buf, sizeof(buf), fmt, vl);
-    va_end(vl);
-    *d_os << buf;
+int TraceC::printf(const char* tag, const char* fmt, ...) {
+  if(d_tags.find(string(tag)) == d_tags.end()) {
+    return 0;
   }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
 }
 
-void TraceC::printf(std::string tag, const char* fmt, ...) {
-  if(d_tags.find(tag) != d_tags.end()) {
-    // chop off output after 1024 bytes
-    char buf[1024];
-    va_list vl;
-    va_start(vl, fmt);
-    vsnprintf(buf, sizeof(buf), fmt, vl);
-    va_end(vl);
-    *d_os << buf;
+int TraceC::printf(std::string tag, const char* fmt, ...) {
+  if(d_tags.find(tag) == d_tags.end()) {
+    return 0;
   }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
 }
 
 #else /* ! CVC4_MUZZLE */