From a97411d90188fc3ceda419faf7be4b3508e305a5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 6 Dec 2017 12:35:18 -0800 Subject: [PATCH] Fixed time stats for MiniSat solve time. (#1431) Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file. --- src/prop/bvminisat/bvminisat.cpp | 50 ++++++++++++++++++++++---------- src/prop/bvminisat/bvminisat.h | 40 ++++++++++--------------- 2 files changed, 50 insertions(+), 40 deletions(-) diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 21c41efd7..edd0d5a11 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -42,6 +42,17 @@ BVMinisatSatSolver::~BVMinisatSatSolver() { delete d_minisatNotify; } +void BVMinisatSatSolver::MinisatNotify::notify( + BVMinisat::vec& clause) +{ + SatClause satClause; + for (unsigned i = 0, n = clause.size(); i < n; ++i) + { + satClause.push_back(toSatLiteral(clause[i])); + } + d_notify->notify(satClause); +} + void BVMinisatSatSolver::setNotify(Notify* notify) { d_minisatNotify = new MinisatNotify(notify); d_minisat->setNotify(d_minisatNotify); @@ -112,13 +123,16 @@ void BVMinisatSatSolver::interrupt(){ d_minisat->interrupt(); } -SatValue BVMinisatSatSolver::solve(){ +SatValue BVMinisatSatSolver::solve() +{ + TimerStat::CodeTimer solveTimer(d_statistics.d_statSolveTime); ++d_statistics.d_statCallsToSolve; return toSatLiteralValue(d_minisat->solve()); } SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + TimerStat::CodeTimer solveTimer(d_statistics.d_statSolveTime); ++d_statistics.d_statCallsToSolve; if(resource == 0) { d_minisat->budgetOff(); @@ -222,23 +236,29 @@ void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause& clause, // Satistics for BVMinisatSatSolver -BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry, const std::string& prefix) +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_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"), d_registerStats(!prefix.empty()) { - if (!d_registerStats){ + if (!d_registerStats) + { return; } diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 54f4a9f71..7dd708ca2 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -27,33 +27,23 @@ namespace CVC4 { namespace prop { -class BVMinisatSatSolver : public BVSatSolverInterface, public context::ContextNotifyObj { - -private: - - class MinisatNotify : public BVMinisat::Notify { +class BVMinisatSatSolver : public BVSatSolverInterface, + public context::ContextNotifyObj +{ + private: + class MinisatNotify : public BVMinisat::Notify + { BVSatSolverInterface::Notify* d_notify; - public: - MinisatNotify(BVSatSolverInterface::Notify* notify) - : d_notify(notify) - {} - bool notify(BVMinisat::Lit lit) { - return d_notify->notify(toSatLiteral(lit)); - } - void notify(BVMinisat::vec& clause) { - SatClause satClause; - for (int i = 0; i < clause.size(); ++i) { - satClause.push_back(toSatLiteral(clause[i])); - } - d_notify->notify(satClause); - } - void spendResource(unsigned ammount) { - d_notify->spendResource(ammount); - } - void safePoint(unsigned ammount) { - d_notify->safePoint(ammount); + public: + MinisatNotify(BVSatSolverInterface::Notify* notify) : d_notify(notify) {} + bool notify(BVMinisat::Lit lit) + { + return d_notify->notify(toSatLiteral(lit)); } + void notify(BVMinisat::vec& clause); + void spendResource(unsigned amount) { d_notify->spendResource(amount); } + void safePoint(unsigned amount) { d_notify->safePoint(amount); } }; BVMinisat::SimpSolver* d_minisat; @@ -137,7 +127,7 @@ private: ReferenceStat d_statTotLiterals; ReferenceStat d_statEliminatedVars; IntStat d_statCallsToSolve; - BackedStat d_statSolveTime; + TimerStat d_statSolveTime; bool d_registerStats; Statistics(StatisticsRegistry* registry, const std::string& prefix); ~Statistics(); -- 2.30.2