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

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index f45610cd8933e54ad1fbfded9acced536f3e8db7..9c8b2bf98694a980083298f030af8a1c744eeaf9 100644 (file)
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -13,6 +13,7 @@
 #include <iostream>
 #include <utility>
 #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<Category, int>::const_iterator it1 = counts.begin();
   std::map<Category, long>::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
 }