diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 36 |
1 files changed, 7 insertions, 29 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index adc4daeee..7cb15ca97 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -26,7 +26,6 @@ #include "base/cvc4_assert.h" #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "options/smt_options.h" #include "prop/prop_engine.h" @@ -44,6 +43,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" +#include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -225,30 +225,8 @@ class TheoryEngine { IntStat conflicts, propagations, lemmas, requirePhase, flipDecision, restartDemands; - Statistics(theory::TheoryId theory): - conflicts(mkName("theory<", theory, ">::conflicts"), 0), - propagations(mkName("theory<", theory, ">::propagations"), 0), - lemmas(mkName("theory<", theory, ">::lemmas"), 0), - requirePhase(mkName("theory<", theory, ">::requirePhase"), 0), - flipDecision(mkName("theory<", theory, ">::flipDecision"), 0), - restartDemands(mkName("theory<", theory, ">::restartDemands"), 0) - { - StatisticsRegistry::registerStat(&conflicts); - StatisticsRegistry::registerStat(&propagations); - StatisticsRegistry::registerStat(&lemmas); - StatisticsRegistry::registerStat(&requirePhase); - StatisticsRegistry::registerStat(&flipDecision); - StatisticsRegistry::registerStat(&restartDemands); - } - - ~Statistics() { - StatisticsRegistry::unregisterStat(&conflicts); - StatisticsRegistry::unregisterStat(&propagations); - StatisticsRegistry::unregisterStat(&lemmas); - StatisticsRegistry::unregisterStat(&requirePhase); - StatisticsRegistry::unregisterStat(&flipDecision); - StatisticsRegistry::unregisterStat(&restartDemands); - } + Statistics(theory::TheoryId theory); + ~Statistics(); };/* class TheoryEngine::Statistics */ @@ -764,7 +742,7 @@ public: inline bool isTheoryEnabled(theory::TheoryId theoryId) const { return d_logicInfo.isTheoryEnabled(theoryId); } - + /** * Returns the equality status of the two terms, from the theory * that owns the domain type. The types of a and b must be the same. @@ -791,7 +769,7 @@ public: * Print solution for synthesis conjectures found by ce_guided_instantiation module */ void printSynthSolution( std::ostream& out ); - + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). @@ -835,11 +813,11 @@ public: SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } - + RemoveITE* getIteRemover() { return &d_iteRemover; } SortInference* getSortInference() { return &d_sortInfer; } - + /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); |