From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 4 Jul 2010 06:31:05 +0000 (+0000)
Subject: fix to production build
X-Git-Tag: cvc5-1.0.0~8952
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18e073e53b49f24539f29a68e8ec905dd628e9d3;p=cvc5.git

fix to production build
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 03678e30e..096c99c06 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -416,8 +416,8 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) {
        * in the cache to make sure they are the same.  This is
        * especially necessary if a theory post-rewrites something into
        * a term of another theory. */
-      if(Debug.isOn("extra-checking") &&
-         !Debug.isOn("$extra-checking:inside-rewrite")) {
+      if(debugTagIsOn("extra-checking") &&
+         !debugTagIsOn("$extra-checking:inside-rewrite")) {
         ScopedDebug d("$extra-checking:inside-rewrite");
         Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel);
         Assert(rewrittenAgain == rse.d_node,
diff --git a/src/util/output.h b/src/util/output.h
index 87b7f69a6..851868c15 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -127,41 +127,6 @@ extern DebugC DebugOut CVC4_PUBLIC;
 #  define Debug if(0) debugNullCvc4Stream
 #endif /* CVC4_DEBUG */
 
-class CVC4_PUBLIC ScopedDebug {
-  std::string d_tag;
-  bool d_oldSetting;
-
-public:
-
-  ScopedDebug(std::string tag, bool newSetting = true) :
-    d_tag(tag) {
-    d_oldSetting = Debug.isOn(d_tag);
-    if(newSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-
-  ScopedDebug(const char* tag, bool newSetting = true) :
-    d_tag(tag) {
-    d_oldSetting = Debug.isOn(d_tag);
-    if(newSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-
-  ~ScopedDebug() {
-    if(d_oldSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-};/* class ScopedDebug */
-
 /** The warning output class */
 class CVC4_PUBLIC WarningC {
   std::ostream *d_os;
@@ -321,6 +286,55 @@ extern TraceC TraceOut CVC4_PUBLIC;
 #  define Trace if(0) debugNullCvc4Stream
 #endif /* CVC4_TRACING */
 
+#ifdef CVC4_DEBUG
+
+class CVC4_PUBLIC ScopedDebug {
+  std::string d_tag;
+  bool d_oldSetting;
+
+public:
+
+  ScopedDebug(std::string tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = DebugOut.isOn(d_tag);
+    if(newSetting) {
+      DebugOut.on(d_tag);
+    } else {
+      DebugOut.off(d_tag);
+    }
+  }
+
+  ScopedDebug(const char* tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Debug.isOn(d_tag);
+    if(newSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+
+  ~ScopedDebug() {
+    if(d_oldSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+};/* class ScopedDebug */
+
+#else /* CVC4_DEBUG */
+
+class CVC4_PUBLIC ScopedDebug {
+public:
+  ScopedDebug(std::string tag, bool newSetting = true) {}
+  ScopedDebug(const char* tag, bool newSetting = true) {}
+};/* class ScopedDebug */
+
+#endif /* CVC4_DEBUG */
+
+#ifdef CVC4_TRACING
+
 class CVC4_PUBLIC ScopedTrace {
   std::string d_tag;
   bool d_oldSetting;
@@ -356,6 +370,16 @@ public:
   }
 };/* class ScopedTrace */
 
+#else /* CVC4_TRACING */
+
+class CVC4_PUBLIC ScopedTrace {
+public:
+  ScopedTrace(std::string tag, bool newSetting = true) {}
+  ScopedTrace(const char* tag, bool newSetting = true) {}
+};/* class ScopedTrace */
+
+#endif /* CVC4_TRACING */
+
 #else /* ! CVC4_MUZZLE */
 
 #  define Debug if(0) debugNullCvc4Stream