Fixes for doubled-statistics (bug 171), a fix to muzzled builds and some minor code

cleanup found while searching for additional cases.  Closes bug 171.

10 files changed, 22 insertions, 29 deletions

diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index adc0505db..6a94d877a 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -519,5 +519,5 @@ getSourceName				(pANTLR3_INT_STREAM is)
 }
 
 
-}
-}
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h
index fede14bd1..289480e2d 100644
--- a/src/parser/bounded_token_buffer.h
+++ b/src/parser/bounded_token_buffer.h
@@ -23,7 +23,7 @@
 #ifndef	__CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
 #define	__CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
 
-#include    <antlr3defs.h>
+#include <antlr3defs.h>
 
 namespace CVC4 {
 namespace parser {
@@ -50,12 +50,10 @@ void
 BoundedTokenBufferFree(pBOUNDED_TOKEN_BUFFER buffer);
 
 #ifdef __cplusplus
-}
+}/* extern "C" */
 #endif
 
-}
-}
-
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H */
-
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0f44e692a..4fd22a079 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -55,7 +55,7 @@ options {
 
 namespace CVC4 {
   class Expr;
-}
+}/* CVC4 namespace */
 }
 
 @parser::postinclude {
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index 7748a1cca..aad5aaec0 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -112,6 +112,7 @@ void UnmapFile(pANTLR3_INPUT_STREAM input) {
   input->close(input);
 }
 
-}
-}
-}
+}/* extern "C" */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index e0b144513..ecb3d39b6 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -57,7 +57,7 @@ options {
 
 namespace CVC4 {
   class Expr;
-}
+}/* CVC4 namespace */
 }
 
 @parser::postinclude {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 56457d006..91f2f205b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -71,7 +71,7 @@ using namespace CVC4::parser;
 
 namespace CVC4 {
   class Expr;
-}
+}/* CVC4 namespace */
 }
 
 @parser::postinclude {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 24d1f4790..0027903df 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -95,7 +95,6 @@ class TheoryEngine {
     void propagate(TNode lit, bool) throw(theory::Interrupted, AssertionException) {
       d_propagatedLiterals.push_back(lit);
       ++(d_engine->d_statistics.d_statPropagate);
-      ++(d_engine->d_statistics.d_statPropagate);
     }
 
     void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
@@ -108,8 +107,7 @@ class TheoryEngine {
     }
     void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) {
       d_explanationNode = explanationNode;
-      ++(d_engine->d_statistics.d_statExplanatation);
-      ++(d_engine->d_statistics.d_statExplanatation);
+      ++(d_engine->d_statistics.d_statExplanation);
     }
   };
 
@@ -320,19 +318,19 @@ public:
 private:
   class Statistics {
   public:
-    IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanatation;
+    IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanation;
     Statistics():
       d_statConflicts("theory::conflicts",0),
       d_statPropagate("theory::propagate",0),
       d_statLemma("theory::lemma",0),
       d_statAugLemma("theory::aug_lemma", 0),
-      d_statExplanatation("theory::explanation", 0)
+      d_statExplanation("theory::explanation", 0)
     {
       StatisticsRegistry::registerStat(&d_statConflicts);
       StatisticsRegistry::registerStat(&d_statPropagate);
       StatisticsRegistry::registerStat(&d_statLemma);
       StatisticsRegistry::registerStat(&d_statAugLemma);
-      StatisticsRegistry::registerStat(&d_statExplanatation);
+      StatisticsRegistry::registerStat(&d_statExplanation);
     }
 
     ~Statistics() {
@@ -340,12 +338,11 @@ private:
       StatisticsRegistry::unregisterStat(&d_statPropagate);
       StatisticsRegistry::unregisterStat(&d_statLemma);
       StatisticsRegistry::unregisterStat(&d_statAugLemma);
-      StatisticsRegistry::unregisterStat(&d_statExplanatation);
+      StatisticsRegistry::unregisterStat(&d_statExplanation);
     }
   };
   Statistics d_statistics;
 
-
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index e77de7d33..f09a44d50 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -43,11 +43,10 @@ public:
       }
     return fType.getRangeType();
   }
-};
-
-}
-}
-}
+};/* class UfTypeRule */
 
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ */
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 8a0bdd298..36ab77dd0 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -142,7 +142,6 @@ void TraceC::printf(string tag, const char* fmt, ...) {
 
 NullDebugC Debug CVC4_PUBLIC;
 NullC Warning CVC4_PUBLIC;
-NullC Warning CVC4_PUBLIC;
 NullC Message CVC4_PUBLIC;
 NullC Notice CVC4_PUBLIC;
 NullC Chat CVC4_PUBLIC;
diff --git a/src/util/output.h b/src/util/output.h
index 355d15760..84e566e94 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -512,7 +512,6 @@ public:
 
 extern NullDebugC Debug CVC4_PUBLIC;
 extern NullC Warning CVC4_PUBLIC;
-extern NullC Warning CVC4_PUBLIC;
 extern NullC Message CVC4_PUBLIC;
 extern NullC Notice CVC4_PUBLIC;
 extern NullC Chat CVC4_PUBLIC;