diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-21 10:41:37 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-21 17:41:37 +0000 |
commit | 38bf0edcc479a20dceeb5bcf7710862c7e60a0b8 (patch) | |
tree | 43ad4c60d609aaeef14dd4ee9420725a029b22b6 /src/prop | |
parent | 7c4a214cf3ce2facf4c98cd3bd347562c66f10a6 (diff) |
Move cnfConversionTime statistic to CnfStream. (#6769)
The statistic in `smt_solver.cpp` was not accurate.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 14 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 8 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 3 |
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); |