Add timer for BV inequality solver. (#2265)

3 files changed, 19 insertions, 15 deletions

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 456f627d0..8ea474ad7 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -2,7 +2,7 @@
 /*! \file bv_subtheory_algebraic.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Tim King, Aina Niemetz
+ **   Liana Hadarean, Aina Niemetz, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -252,21 +252,16 @@ AlgebraicSolver::~AlgebraicSolver() {
 
 
 
-bool AlgebraicSolver::check(Theory::Effort e) {
+bool AlgebraicSolver::check(Theory::Effort e)
+{
   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
 
-  if (!Theory::fullEffort(e)) {
-    return true;
-  }
-
-  if (!useHeuristic()) {
-    return true;
-  }
-
-  ++(d_numCalls);
+  if (!Theory::fullEffort(e)) { return true; }
+  if (!useHeuristic()) { return true; }
 
   TimerStat::CodeTimer algebraicTimer(d_statistics.d_solveTime);
   Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check (" << e << ")\n";
+  ++(d_numCalls);
   ++(d_statistics.d_numCallstoCheck);
 
   d_explanations.clear();
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 41ee74e8d..6fc167793 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -31,6 +31,7 @@ using namespace CVC4::theory::bv::utils;
 
 bool InequalitySolver::check(Theory::Effort e) {
   Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
+  TimerStat::CodeTimer inequalityTimer(d_statistics.d_solveTime);
   ++(d_statistics.d_numCallstoCheck);
   d_bv->spendResource(options::theoryCheckStep());
 
@@ -246,10 +247,15 @@ bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact)
 }
 
 InequalitySolver::Statistics::Statistics()
-  : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
+    : d_numCallstoCheck("theory::bv::inequality::NumCallsToCheck", 0),
+      d_solveTime("theory::bv::inequality::SolveTime")
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->registerStat(&d_solveTime);
 }
-InequalitySolver::Statistics::~Statistics() {
+
+InequalitySolver::Statistics::~Statistics()
+{
   smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
 }
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 06c39754f..1bdec8386 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -38,9 +38,12 @@ typedef expr::Attribute<IneqOnlyAttributeId, bool> IneqOnlyAttribute;
 struct IneqOnlyComputedAttributeId {};
 typedef expr::Attribute<IneqOnlyComputedAttributeId, bool> IneqOnlyComputedAttribute;
 
-class InequalitySolver: public SubtheorySolver {
-  struct Statistics {
+class InequalitySolver : public SubtheorySolver
+{
+  struct Statistics
+  {
     IntStat d_numCallstoCheck;
+    TimerStat d_solveTime;
     Statistics();
     ~Statistics();
   };