From f4ef7af0a2295691f281ee1604dfeb4082fe229c Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 8 Jan 2016 16:44:57 -0800 Subject: 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. --- src/theory/uf/equality_engine.h | 22 +++------------------- 1 file changed, 3 insertions(+), 19 deletions(-) (limited to 'src/theory/uf/equality_engine.h') 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 - -- cgit v1.2.3