diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-18 22:24:59 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-18 22:24:59 +0000 |
commit | fd6af9181e763cd9564245114cfa47f3952484db (patch) | |
tree | 0b058ad4e0624f1bf11ed9c65d63a4cfbdbdc66e /src/prop | |
parent | 968f250b473d97db537aa7628bf111d15a2db299 (diff) |
Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.h | 3 | ||||
-rw-r--r-- | src/prop/sat.h | 53 |
2 files changed, 51 insertions, 5 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 4adaa1434..c33982ddc 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -90,8 +90,7 @@ public: * PropEngine and Theory). For now, there's nothing to do here in * the PropEngine. */ - void shutdown() { - } + void shutdown() { } /** * Converts the given formula to CNF and assert the CNF to the sat solver. diff --git a/src/prop/sat.h b/src/prop/sat.h index e023410c7..f64697d7b 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -26,6 +26,7 @@ #define __CVC4_USE_MINISAT #include "util/options.h" +#include "util/stats.h" #ifdef __CVC4_USE_MINISAT @@ -132,6 +133,49 @@ class SatSolver : public SatInputInterface { /** Minisat solver */ minisat::SimpSolver* d_minisat; + class Statistics { + private: + 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() : + 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); + } + void init(minisat::SimpSolver* d_minisat){ + d_statStarts.setData(d_minisat->starts); + d_statDecisions.setData(d_minisat->decisions); + d_statRndDecisions.setData(d_minisat->rnd_decisions); + d_statPropagations.setData(d_minisat->propagations); + d_statConflicts.setData(d_minisat->conflicts); + d_statClausesLiterals.setData(d_minisat->clauses_literals); + d_statLearntsLiterals.setData(d_minisat->learnts_literals); + d_statMaxLiterals.setData(d_minisat->max_literals); + d_statTotLiterals.setData(d_minisat->tot_literals); + } + }; + Statistics d_statistics; + #endif /* __CVC4_USE_MINISAT */ protected: @@ -150,7 +194,7 @@ public: ~SatSolver(); bool solve(); - + void addClause(SatClause& clause, bool lemma); SatVariable newVar(bool theoryAtom = false); @@ -158,7 +202,7 @@ public: void theoryCheck(SatClause& conflict); void enqueueTheoryLiteral(const SatLiteral& l); - + void setCnfStream(CnfStream* cnfStream); SatLiteralValue value(SatLiteral l); @@ -173,7 +217,8 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_propEngine(propEngine), d_cnfStream(NULL), d_theoryEngine(theoryEngine), - d_context(context) + d_context(context), + d_statistics() { // Create the solver d_minisat = new minisat::SimpSolver(this, d_context); @@ -183,6 +228,8 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_minisat->remove_satisfied = false; // Make minisat reuse the literal values d_minisat->polarity_mode = minisat::SimpSolver::polarity_user; + + d_statistics.init(d_minisat); } inline SatSolver::~SatSolver() { |