diff options
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 22 |
1 files changed, 3 insertions, 19 deletions
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 - |