diff options
author | Tim King <taking@google.com> | 2016-01-08 16:44:57 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-08 16:44:57 -0800 |
commit | f4ef7af0a2295691f281ee1604dfeb4082fe229c (patch) | |
tree | 995e512e5669cec6bbc9447d00ec912d5e4c19e3 /src/theory/uf | |
parent | def0a07f9676a292a849d7fc8269ffd0901ce156 (diff) |
Removing StatisticsRegistry's static functions current() and registerStat().
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 23 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 22 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 3 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 32 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 2 |
5 files changed, 44 insertions, 38 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index cd6459a3c..828d53144 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -17,10 +17,32 @@ #include "theory/uf/equality_engine.h" +#include "smt/smt_statistics_registry.h" + namespace CVC4 { namespace theory { namespace eq { +EqualityEngine::Statistics::Statistics(std::string name) + : mergesCount(name + "::mergesCount", 0), + termsCount(name + "::termsCount", 0), + functionTermsCount(name + "::functionTermsCount", 0), + constantTermsCount(name + "::constantTermsCount", 0) +{ + smtStatisticsRegistry()->registerStat(&mergesCount); + smtStatisticsRegistry()->registerStat(&termsCount); + smtStatisticsRegistry()->registerStat(&functionTermsCount); + smtStatisticsRegistry()->registerStat(&constantTermsCount); +} + +EqualityEngine::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&mergesCount); + smtStatisticsRegistry()->unregisterStat(&termsCount); + smtStatisticsRegistry()->unregisterStat(&functionTermsCount); + smtStatisticsRegistry()->unregisterStat(&constantTermsCount); +} + + /** * Data used in the BFS search through the equality graph. */ @@ -2058,4 +2080,3 @@ void EqProof::debug_print( const char * c, unsigned tb ){ } // Namespace uf } // Namespace theory } // Namespace CVC4 - diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f7f7f9ddd..87074aebc 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -29,10 +29,10 @@ #include "context/cdo.h" #include "expr/kind_map.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine_types.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -193,24 +193,9 @@ public: /** Number of constant terms managed by the system */ IntStat constantTermsCount; - Statistics(std::string name) - : mergesCount(name + "::mergesCount", 0), - termsCount(name + "::termsCount", 0), - functionTermsCount(name + "::functionTermsCount", 0), - constantTermsCount(name + "::constantTermsCount", 0) - { - StatisticsRegistry::registerStat(&mergesCount); - StatisticsRegistry::registerStat(&termsCount); - StatisticsRegistry::registerStat(&functionTermsCount); - StatisticsRegistry::registerStat(&constantTermsCount); - } + Statistics(std::string name); - ~Statistics() { - StatisticsRegistry::unregisterStat(&mergesCount); - StatisticsRegistry::unregisterStat(&termsCount); - StatisticsRegistry::unregisterStat(&functionTermsCount); - StatisticsRegistry::unregisterStat(&constantTermsCount); - } + ~Statistics(); };/* struct EqualityEngine::statistics */ private: @@ -900,4 +885,3 @@ public: } // Namespace eq } // Namespace theory } // Namespace CVC4 - diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index e49b4652a..763ced650 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -52,7 +52,8 @@ #include "context/context.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/statistics_registry.h" +#include "smt/smt_statistics_registry.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 0f8ccf49a..9fceedc96 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -2058,23 +2058,23 @@ StrongSolverTheoryUF::Statistics::Statistics(): d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0), d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1) { - StatisticsRegistry::registerStat(&d_clique_conflicts); - StatisticsRegistry::registerStat(&d_clique_lemmas); - StatisticsRegistry::registerStat(&d_split_lemmas); - StatisticsRegistry::registerStat(&d_disamb_term_lemmas); - StatisticsRegistry::registerStat(&d_sym_break_lemmas); - StatisticsRegistry::registerStat(&d_totality_lemmas); - StatisticsRegistry::registerStat(&d_max_model_size); + smtStatisticsRegistry()->registerStat(&d_clique_conflicts); + smtStatisticsRegistry()->registerStat(&d_clique_lemmas); + smtStatisticsRegistry()->registerStat(&d_split_lemmas); + smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas); + smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas); + smtStatisticsRegistry()->registerStat(&d_totality_lemmas); + smtStatisticsRegistry()->registerStat(&d_max_model_size); } StrongSolverTheoryUF::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_clique_conflicts); - StatisticsRegistry::unregisterStat(&d_clique_lemmas); - StatisticsRegistry::unregisterStat(&d_split_lemmas); - StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas); - StatisticsRegistry::unregisterStat(&d_sym_break_lemmas); - StatisticsRegistry::unregisterStat(&d_totality_lemmas); - StatisticsRegistry::unregisterStat(&d_max_model_size); + smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts); + smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_max_model_size); } @@ -2141,9 +2141,9 @@ void DisequalityPropagator::assertPredicate( Node p, bool polarity ) { DisequalityPropagator::Statistics::Statistics(): d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0) { - StatisticsRegistry::registerStat(& d_propagations); + smtStatisticsRegistry()->registerStat(& d_propagations); } DisequalityPropagator::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(& d_propagations); + smtStatisticsRegistry()->unregisterStat(& d_propagations); } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 45d7fc3cc..24d7f840f 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -21,8 +21,8 @@ #include "context/cdhashmap.h" #include "context/context.h" #include "context/context_mm.h" -#include "expr/statistics_registry.h" #include "theory/theory.h" +#include "util/statistics_registry.h" namespace CVC4 { |