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/smt | |
parent | 7c4a214cf3ce2facf4c98cd3bd347562c66f10a6 (diff) |
Move cnfConversionTime statistic to CnfStream. (#6769)
The statistic in `smt_solver.cpp` was not accurate.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine_stats.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine_stats.h | 2 | ||||
-rw-r--r-- | src/smt/smt_solver.cpp | 1 |
3 files changed, 0 insertions, 5 deletions
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 |