Fixed time stats for MiniSat solve time. (#1431)

Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file.

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<BVMinisat::Lit>& 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<BVMinisat::Lit>& 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<BVMinisat::Lit>& 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<uint64_t> d_statTotLiterals;
     ReferenceStat<int> d_statEliminatedVars;
     IntStat d_statCallsToSolve;
-    BackedStat<double> d_statSolveTime;
+    TimerStat d_statSolveTime;
     bool d_registerStats;
     Statistics(StatisticsRegistry* registry, const std::string& prefix);
     ~Statistics();