Move cnfConversionTime statistic to CnfStream. (#6769)

The statistic in `smt_solver.cpp` was not accurate.

7 files changed, 27 insertions, 11 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 40853b33a..4897f8e6a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -21,14 +21,15 @@
 #include "base/output.h"
 #include "expr/node.h"
 #include "options/bv_options.h"
+#include "printer/printer.h"
 #include "proof/clause_id.h"
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
 #include "smt/dump.h"
 #include "smt/smt_engine.h"
-#include "printer/printer.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 
@@ -52,7 +53,8 @@ CnfStream::CnfStream(SatSolver* satSolver,
       d_registrar(registrar),
       d_name(name),
       d_removable(false),
-      d_resourceManager(rm)
+      d_resourceManager(rm),
+      d_stats(name)
 {
 }
 
@@ -139,6 +141,7 @@ void CnfStream::ensureLiteral(TNode n)
       n.toString().c_str(),
       n.getType().toString().c_str());
   Trace("cnf") << "ensureLiteral(" << n << ")\n";
+  TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
   if (hasLiteral(n))
   {
     ensureMappingForLiteral(n);
@@ -722,6 +725,7 @@ void CnfStream::convertAndAssert(TNode node,
                << ", negated = " << (negated ? "true" : "false")
                << ", removable = " << (removable ? "true" : "false") << ")\n";
   d_removable = removable;
+  TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
   convertAndAssert(node, negated);
 }
 
@@ -760,5 +764,11 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
   }
 }
 
+CnfStream::Statistics::Statistics(const std::string& name)
+    : d_cnfConversionTime(smtStatisticsRegistry().registerTimer(
+        name + "::CnfStream::cnfConversionTime"))
+{
+}
+
 }  // namespace prop
 }  // namespace cvc5
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 2959ae726..aeed97380 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -309,6 +309,14 @@ class CnfStream {
 
   /** Pointer to resource manager for associated SmtEngine */
   ResourceManager* d_resourceManager;
+
+ private:
+  struct Statistics
+  {
+    Statistics(const std::string& name);
+    TimerStat d_cnfConversionTime;
+  } d_stats;
+
 }; /* class CnfStream */
 
 }  // namespace prop
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index fe3a5ecff..62b2f655c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -107,7 +107,8 @@ PropEngine::PropEngine(TheoryEngine* te,
                               userContext,
                               &d_outMgr,
                               rm,
-                              FormulaLitPolicy::TRACK);
+                              FormulaLitPolicy::TRACK,
+                              "prop");
 
   // connect theory proxy
   d_theoryProxy->finishInit(d_cnfStream);
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
index 417d345cb..c76a8a2e7 100644
--- a/src/smt/smt_engine_stats.cpp
+++ b/src/smt/smt_engine_stats.cpp
@@ -25,8 +25,6 @@ SmtEngineStatistics::SmtEngineStatistics(const std::string& name)
         name + "definitionExpansionTime")),
       d_numConstantProps(
           smtStatisticsRegistry().registerInt(name + "numConstantProps")),
-      d_cnfConversionTime(
-          smtStatisticsRegistry().registerTimer(name + "cnfConversionTime")),
       d_numAssertionsPre(smtStatisticsRegistry().registerInt(
           name + "numAssertionsPreITERemoval")),
       d_numAssertionsPost(smtStatisticsRegistry().registerInt(
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
index 441721a54..db914b560 100644
--- a/src/smt/smt_engine_stats.h
+++ b/src/smt/smt_engine_stats.h
@@ -30,8 +30,6 @@ struct SmtEngineStatistics
   TimerStat d_definitionExpansionTime;
   /** number of constant propagations found during nonclausal simp */
   IntStat d_numConstantProps;
-  /** time spent converting to CNF */
-  TimerStat d_cnfConversionTime;
   /** Number of assertions before ite removal */
   IntStat d_numAssertionsPre;
   /** Number of assertions after ite removal */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index d7b70f501..f5783ab6b 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -239,7 +239,6 @@ void SmtSolver::processAssertions(Assertions& as)
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
-    TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
     const std::vector<Node>& assertions = ap.ref();
     // It is important to distinguish the input assertions from the skolem
     // definitions, as the decision justification heuristic treates the latter
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index dc2c7e2a3..414e57e19 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -96,17 +96,19 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s,
   {
     case options::SatSolverMode::CRYPTOMINISAT:
       d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
-          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
+          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
       break;
     default:
       d_satSolver.reset(prop::SatSolverFactory::createCadical(
-          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
+          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
   }
   d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
                                         d_bbRegistrar.get(),
                                         d_nullContext.get(),
                                         nullptr,
-                                        smt::currentResourceManager()));
+                                        smt::currentResourceManager(),
+                                        prop::FormulaLitPolicy::INTERNAL,
+                                        "theory::bv::BVSolverBitblast"));
 }
 
 void BVSolverBitblast::postCheck(Theory::Effort level)