Move cnfConversionTime statistic to CnfStream. (#6769)

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

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 40853b33a55f9eb90a96cd0e3db84091575fd923..4897f8e6a33a140a9d549e9fe32394363b84a292 100644 (file)
--- 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 2959ae726b67d76c503edbbc1328997bd1d41d79..aeed973806cdedce32861ebb9051511ae0838789 100644 (file)
--- 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 fe3a5ecffae9a29919abda9748faae3695ffaf60..62b2f655cee200d844392e3bea3e330280999c7e 100644 (file)
--- 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 417d345cb7ad9841ec85bb000b6b3994d748a1dc..c76a8a2e76af344fb80c7b1946a835e2053c43a2 100644 (file)
--- 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 441721a544a8af88901e3c1d9869943d6c9390fc..db914b560d4e1a86c4ce12054fac5e7563467fdc 100644 (file)
--- 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 d7b70f5015b70b834a26f965b59f2c345050fe98..f5783ab6b34f29ec56267b08b50b974924545e2b 100644 (file)
--- 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 dc2c7e2a39f66b6165f0ec431f305b2dce0b8ac6..414e57e19c177a9d18c509cc6802dd4aee8f5d4a 100644 (file)
--- 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)