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/prop | |
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/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 103 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 24 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 65 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 25 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 3 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 5 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 9 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 6 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 11 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 6 |
11 files changed, 143 insertions, 116 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index ab157844a..be266b6d8 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -17,21 +17,23 @@ **/ #include "prop/bvminisat/bvminisat.h" + #include "prop/bvminisat/simp/SimpSolver.h" +#include "util/statistics_registry.h" -using namespace CVC4; -using namespace prop; +namespace CVC4 { +namespace prop { -BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name) +BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name) : context::ContextNotifyObj(mainSatContext, false), d_minisat(new BVMinisat::SimpSolver(mainSatContext)), d_minisatNotify(0), d_assertionsCount(0), d_assertionsRealCount(mainSatContext, 0), d_lastPropagation(mainSatContext, 0), - d_statistics(name) + d_statistics(registry, name) { - d_statistics.init(d_minisat); + d_statistics.init(d_minisat); } @@ -208,59 +210,63 @@ void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause, // Satistics for BVMinisatSatSolver -BVMinisatSatSolver::Statistics::Statistics(const std::string& prefix) : - d_statStarts("theory::bv::"+prefix+"bvminisat::starts"), - d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"), - d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"), - d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"), - d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"), - d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"), - d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"), - d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"), - d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"), - d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"), - d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0), - d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0), - d_registerStats(!prefix.empty()) +BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry, const std::string& prefix) + : d_registry(registry), + d_statStarts("theory::bv::"+prefix+"bvminisat::starts"), + d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"), + d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"), + d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"), + d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"), + d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"), + d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"), + d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"), + d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"), + d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"), + d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0), + d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0), + d_registerStats(!prefix.empty()) { - if (!d_registerStats) + if (!d_registerStats){ return; + } - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); - StatisticsRegistry::registerStat(&d_statEliminatedVars); - StatisticsRegistry::registerStat(&d_statCallsToSolve); - StatisticsRegistry::registerStat(&d_statSolveTime); + d_registry->registerStat(&d_statStarts); + d_registry->registerStat(&d_statDecisions); + d_registry->registerStat(&d_statRndDecisions); + d_registry->registerStat(&d_statPropagations); + d_registry->registerStat(&d_statConflicts); + d_registry->registerStat(&d_statClausesLiterals); + d_registry->registerStat(&d_statLearntsLiterals); + d_registry->registerStat(&d_statMaxLiterals); + d_registry->registerStat(&d_statTotLiterals); + d_registry->registerStat(&d_statEliminatedVars); + d_registry->registerStat(&d_statCallsToSolve); + d_registry->registerStat(&d_statSolveTime); } BVMinisatSatSolver::Statistics::~Statistics() { - if (!d_registerStats) + if (!d_registerStats){ return; - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); - StatisticsRegistry::unregisterStat(&d_statEliminatedVars); - StatisticsRegistry::unregisterStat(&d_statCallsToSolve); - StatisticsRegistry::unregisterStat(&d_statSolveTime); + } + d_registry->unregisterStat(&d_statStarts); + d_registry->unregisterStat(&d_statDecisions); + d_registry->unregisterStat(&d_statRndDecisions); + d_registry->unregisterStat(&d_statPropagations); + d_registry->unregisterStat(&d_statConflicts); + d_registry->unregisterStat(&d_statClausesLiterals); + d_registry->unregisterStat(&d_statLearntsLiterals); + d_registry->unregisterStat(&d_statMaxLiterals); + d_registry->unregisterStat(&d_statTotLiterals); + d_registry->unregisterStat(&d_statEliminatedVars); + d_registry->unregisterStat(&d_statCallsToSolve); + d_registry->unregisterStat(&d_statSolveTime); } void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ - if (!d_registerStats) + if (!d_registerStats){ return; - + } + d_statStarts.setData(minisat->starts); d_statDecisions.setData(minisat->decisions); d_statRndDecisions.setData(minisat->rnd_decisions); @@ -272,3 +278,6 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ d_statTotLiterals.setData(minisat->tot_literals); d_statEliminatedVars.setData(minisat->eliminated_vars); } + +} /* namespace CVC4::prop */ +} /* namespace CVC4 */ diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index fc5b29e89..986fbf339 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -20,9 +20,10 @@ #pragma once -#include "prop/sat_solver.h" -#include "prop/bvminisat/simp/SimpSolver.h" #include "context/cdo.h" +#include "prop/bvminisat/simp/SimpSolver.h" +#include "prop/sat_solver.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -67,13 +68,7 @@ protected: public: - BVMinisatSatSolver() : - ContextNotifyObj(NULL, false), - d_assertionsRealCount(NULL, (unsigned)0), - d_lastPropagation(NULL, (unsigned)0), - d_statistics("") - { Unreachable(); } - BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name = ""); + BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = ""); ~BVMinisatSatSolver() throw(AssertionException); void setNotify(Notify* notify); @@ -90,7 +85,7 @@ public: void markUnremovable(SatLiteral lit); void interrupt(); - + SatValue solve(); SatValue solve(long unsigned int&); void getUnsatCore(SatClause& unsatCore); @@ -117,11 +112,16 @@ public: void explain(SatLiteral lit, std::vector<SatLiteral>& explanation); SatValue assertAssumption(SatLiteral lit, bool propagate); - + void popAssumption(); +private: + /* Disable the default constructor. */ + BVMinisatSatSolver() CVC4_UNUSED; + class Statistics { public: + StatisticsRegistry* d_registry; ReferenceStat<uint64_t> d_statStarts, d_statDecisions; ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations; ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals; @@ -131,7 +131,7 @@ public: IntStat d_statCallsToSolve; BackedStat<double> d_statSolveTime; bool d_registerStats; - Statistics(const std::string& prefix); + Statistics(StatisticsRegistry* registry, const std::string& prefix); ~Statistics(); void init(BVMinisat::SimpSolver* minisat); }; diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index bef8e0a70..85556e935 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -22,9 +22,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define BVMinisat_SimpSolver_h #include "context/context.h" -#include "expr/statistics_registry.h" #include "prop/bvminisat/core/Solver.h" #include "prop/bvminisat/mtl/Queue.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace BVMinisat { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index d9b8bb4f8..ce5c1eb92 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -23,15 +23,17 @@ #include "options/prop_options.h" #include "options/smt_options.h" #include "prop/minisat/simp/SimpSolver.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { //// DPllMinisatSatSolver -MinisatSatSolver::MinisatSatSolver() : +MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) : d_minisat(NULL), - d_context(NULL) + d_context(NULL), + d_statistics(registry) {} MinisatSatSolver::~MinisatSatSolver() throw() @@ -229,38 +231,41 @@ void MinisatSatSolver::pop() { /// Statistics for MinisatSatSolver -MinisatSatSolver::Statistics::Statistics() : - d_statStarts("sat::starts"), - d_statDecisions("sat::decisions"), - d_statRndDecisions("sat::rnd_decisions"), - d_statPropagations("sat::propagations"), - d_statConflicts("sat::conflicts"), - d_statClausesLiterals("sat::clauses_literals"), - d_statLearntsLiterals("sat::learnts_literals"), - d_statMaxLiterals("sat::max_literals"), - d_statTotLiterals("sat::tot_literals") +MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) : + d_registry(registry), + d_statStarts("sat::starts"), + d_statDecisions("sat::decisions"), + d_statRndDecisions("sat::rnd_decisions"), + d_statPropagations("sat::propagations"), + d_statConflicts("sat::conflicts"), + d_statClausesLiterals("sat::clauses_literals"), + d_statLearntsLiterals("sat::learnts_literals"), + d_statMaxLiterals("sat::max_literals"), + d_statTotLiterals("sat::tot_literals") { - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); + d_registry->registerStat(&d_statStarts); + d_registry->registerStat(&d_statDecisions); + d_registry->registerStat(&d_statRndDecisions); + d_registry->registerStat(&d_statPropagations); + d_registry->registerStat(&d_statConflicts); + d_registry->registerStat(&d_statClausesLiterals); + d_registry->registerStat(&d_statLearntsLiterals); + d_registry->registerStat(&d_statMaxLiterals); + d_registry->registerStat(&d_statTotLiterals); } + MinisatSatSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); + d_registry->unregisterStat(&d_statStarts); + d_registry->unregisterStat(&d_statDecisions); + d_registry->unregisterStat(&d_statRndDecisions); + d_registry->unregisterStat(&d_statPropagations); + d_registry->unregisterStat(&d_statConflicts); + d_registry->unregisterStat(&d_statClausesLiterals); + d_registry->unregisterStat(&d_statLearntsLiterals); + d_registry->unregisterStat(&d_statMaxLiterals); + d_registry->unregisterStat(&d_statTotLiterals); } + void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ d_statStarts.setData(d_minisat->starts); d_statDecisions.setData(d_minisat->decisions); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 2564572c2..f279b3a5b 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -20,23 +20,15 @@ #include "prop/sat_solver.h" #include "prop/minisat/simp/SimpSolver.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { class MinisatSatSolver : public DPLLSatSolverInterface { - - /** The SatSolver used */ - Minisat::SimpSolver* d_minisat; - - /** Context we will be using to synchronize the sat solver */ - context::Context* d_context; - - void setupOptions(); - public: - MinisatSatSolver(); + MinisatSatSolver(StatisticsRegistry* registry); ~MinisatSatSolver() throw(); ; @@ -83,15 +75,26 @@ public: bool isDecision(SatVariable decn) const; +private: + + /** The SatSolver used */ + Minisat::SimpSolver* d_minisat; + + /** Context we will be using to synchronize the sat solver */ + context::Context* d_context; + + void setupOptions(); + class Statistics { private: + StatisticsRegistry* d_registry; ReferenceStat<uint64_t> d_statStarts, d_statDecisions; ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations; ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals; ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; ReferenceStat<uint64_t> d_statTotLiterals; public: - Statistics(); + Statistics(StatisticsRegistry* registry); ~Statistics(); void init(Minisat::SimpSolver* d_minisat); };/* class MinisatSatSolver::Statistics */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 96ca7480f..630825103 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -36,6 +36,7 @@ #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/command.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" @@ -83,7 +84,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext Debug("prop") << "Constructing the PropEngine" << endl; - d_satSolver = SatSolverFactory::createDPLLMinisat(); + d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry()); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 960881844..1c1dae410 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -24,9 +24,10 @@ #include <string> #include "context/cdlist.h" +#include "context/context.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "prop/sat_solver_types.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -101,7 +102,7 @@ public: virtual void notify(SatClause& clause) = 0; virtual void spendResource(unsigned ammount) = 0; virtual void safePoint(unsigned ammount) = 0; - + };/* class BVSatSolverInterface::Notify */ virtual void setNotify(Notify* notify) = 0; diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 98b8fce47..c131ca475 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -15,18 +15,19 @@ **/ #include "prop/sat_solver_factory.h" + #include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" namespace CVC4 { namespace prop { -BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) { - return new BVMinisatSatSolver(mainSatContext, name); +BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name) { + return new BVMinisatSatSolver(registry, mainSatContext, name); } -DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { - return new MinisatSatSolver(); +DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) { + return new MinisatSatSolver(registry); } } /* CVC4::prop namespace */ diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index e0446eb4a..434bf849d 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -21,7 +21,9 @@ #include <string> #include <vector> +#include "context/context.h" #include "prop/sat_solver.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -29,8 +31,8 @@ namespace prop { class SatSolverFactory { public: - static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = ""); - static DPLLSatSolverInterface* createDPLLMinisat(); + static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name = ""); + static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry); };/* class SatSolverFactory */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index d0830b9a5..e87046ad5 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -19,14 +19,15 @@ #include "context/context.h" #include "decision/decision_engine.h" #include "expr/expr_stream.h" -#include "expr/statistics_registry.h" #include "options/decision_options.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "smt_util/lemma_input_channel.h" #include "smt_util/lemma_output_channel.h" +#include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -42,11 +43,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), d_globals(globals), - d_queue(context) -{} + d_queue(context), + d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0) +{ + smtStatisticsRegistry()->registerStat(&d_replayedDecisions); +} TheoryProxy::~TheoryProxy() { /* nothing to do for now */ + smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions); } /** The lemma input channel we are using. */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 59bc859cb..261db8c87 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -27,12 +27,12 @@ #include "context/cdqueue.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "prop/sat_solver.h" #include "smt/smt_globals.h" #include "smt_util/lemma_output_channel.h" #include "smt_util/lemma_input_channel.h" #include "theory/theory.h" +#include "util/statistics_registry.h" namespace CVC4 { @@ -137,8 +137,8 @@ public: /** * Statistic: the number of replayed decisions (via --replay). */ - KEEP_STATISTIC(IntStat, d_replayedDecisions, - "prop::theoryproxy::replayedDecisions", 0); + IntStat d_replayedDecisions; + };/* class SatSolver */ }/* CVC4::prop namespace */ |