Move cnfConversionTime statistic to CnfStream. (#6769)

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

3 files changed, 22 insertions, 3 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);