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/sat.h | |
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/sat.h')
-rw-r--r-- | src/prop/sat.h | 53 |
1 files changed, 50 insertions, 3 deletions
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() { |