From d7c83fc023506b1b8f3abbaf39b64a4c214d2f07 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 27 Jan 2011 06:28:11 +0000 Subject: [PATCH] Improvement. Output peak memory usage, and CPU time used when using the -t option. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1095 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/RunTimes.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index f45610c..9c8b2bf 100644 --- a/src/AST/RunTimes.cpp +++ b/src/AST/RunTimes.cpp @@ -13,6 +13,7 @@ #include #include #include "RunTimes.h" +#include "../sat/utils/System.h" // BE VERY CAREFUL> Update the Category Names to match. std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement"}; @@ -44,6 +45,8 @@ void RunTimes::print() std::map::const_iterator it1 = counts.begin(); std::map::const_iterator it2 = times.begin(); + int cummulative_ms = 0; + while (it1 != counts.end()) { int time_ms = 0; @@ -55,12 +58,18 @@ void RunTimes::print() result << " " << CategoryNames[it1->first] << ": " << it1->second; result << " [" << time_ms << "ms]"; result << std::endl; + cummulative_ms += time_ms; } it1++; } + std::cerr << result.str(); + std::cerr << std::fixed; + std::cerr.precision(2); + std::cerr << "Statistics Total: " << ((double)cummulative_ms)/1000 << "s" << std::endl; + std::cerr << "CPU Time Used : " << Minisat::cpuTime() << "s" << std::endl; + std::cerr << "Peak Memory Used: " << Minisat::memUsedPeak() << "MB" << std::endl; - std::cerr << result.str(); // iterator } -- 2.47.3