From b9f36ae0027e52da925416630ccad5d4b84779e9 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 6 Jul 2010 04:00:42 +0000 Subject: [PATCH] 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. --- src/parser/bounded_token_buffer.cpp | 4 ++-- src/parser/bounded_token_buffer.h | 10 ++++------ src/parser/cvc/Cvc.g | 2 +- src/parser/memory_mapped_input_buffer.cpp | 7 ++++--- src/parser/smt/Smt.g | 2 +- src/parser/smt2/Smt2.g | 2 +- src/theory/theory_engine.h | 13 +++++-------- src/theory/uf/theory_uf_type_rules.h | 9 ++++----- src/util/output.cpp | 1 - src/util/output.h | 1 - 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 +#include 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; -- 2.30.2