From 38bf0edcc479a20dceeb5bcf7710862c7e60a0b8 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 21 Jun 2021 10:41:37 -0700 Subject: [PATCH] Move cnfConversionTime statistic to CnfStream. (#6769) The statistic in `smt_solver.cpp` was not accurate. --- src/prop/cnf_stream.cpp | 14 ++++++++++++-- src/prop/cnf_stream.h | 8 ++++++++ src/prop/prop_engine.cpp | 3 ++- src/smt/smt_engine_stats.cpp | 2 -- src/smt/smt_engine_stats.h | 2 -- src/smt/smt_solver.cpp | 1 - src/theory/bv/bv_solver_bitblast.cpp | 8 +++++--- 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& 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) -- 2.30.2