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.

diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index adc0505db5451632c5319b0cbf167612b8c9e13b..6a94d877ababa61229636e86da6315bb29bdcb6b 100644 (file)
--- 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 fede14bd1725431e85a75707833fe0c7c4341cd1..289480e2da6761cb56789f9c7eaf16c29a79820e 100644 (file)
--- 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 0f44e692a904d5f1c2965410f3494e9ee7cca3e4..4fd22a07918be2fe23a539a012d25e4f202698f2 100644 (file)
--- 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 7748a1ccae3d382dcf46ab0d3c9a3ec70a1afcf9..aad5aaec0cec5d25e180a4d11da317b091bf761f 100644 (file)
--- 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 e0b14451378c0c4b4422875bb04b8e6771018353..ecb3d39b6f173d97a55638d70deed7a00837fd61 100644 (file)
--- 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 56457d00655ecedacf166d5b430064cd91d8ef30..91f2f205b0deceb78aaf59223d84adeefd28be27 100644 (file)
--- 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 24d1f4790b8ce332f750ee0f59e92ca0d723af73..0027903dfbf7fcb507ede9c46853d3700695e84e 100644 (file)
--- 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 e77de7d33fc0bb1598b9295824e3b8a85436ccc0..f09a44d509869183e545f23776260785a3e12ffc 100644 (file)
--- 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 8a0bdd29847fadcb1c6f7da7babdcd95bd3313dd..36ab77dd009ba5ae2ab90f407ed076b0a770e46d 100644 (file)
--- 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 355d15760cc3e0a944a4a4baf0dc528a6ebe9efe..84e566e94db818cb63ef63dcfa726d59c78808ab 100644 (file)
--- 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;