Add a new class for tracking the runtimes. e.g. SimplifyTopLevel was called 5 times...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@224 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 056789c5490b6494c9c8bb6b253cec56a9aa919c..6385f8dcf71965f9ddf77cfa80b2b599c4c54855 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -36,6 +36,7 @@
 #include <stdint.h>
 #include <stdlib.h>
 #include "../extlib-constbv/constantbv.h"
+#include "RunTimes.h"
 
 /*****************************************************************************
  * LIST OF CLASSES DECLARED IN THIS FILE:
@@ -1556,6 +1557,7 @@ namespace BEEV
     bool CheckMap(ASTNodeMap* VarConstMap, 
                  const ASTNode& key, ASTNode& output);
 
+    RunTimes runTimes;
 
     //substitution
     bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output);

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
new file mode 100644 (file)
index 0000000..2ac0582
--- /dev/null
+++ b/src/AST/RunTimes.cpp
@@ -0,0 +1,99 @@
+//Hold the runtime statistics. E.g. how long was spent in simplification.
+//The times don't add up to the runtime, because we allow multiple times to
+//be counted simultaneously. For example, the current Transform()s call
+//Simplify_TopLevel, so inside simplify time will be couunted towards both
+//Simplify_TopLevel & Transform.
+
+// This is intended as a low overhead profiling class. So it can be always run.
+
+#include "RunTimes.h"
+#include <cassert>
+#include <sys/time.h>
+#include <sstream>
+#include <iostream>
+#include <utility>
+
+
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplify Top Level", "Parsing","Transforming" , "CNF Conversion", "Bit Blasting", "Solving"};
+
+namespace BEEV
+{
+       void FatalError(const char * str);
+}
+
+
+long RunTimes::getCurrentTime()
+{
+       timeval t;
+       gettimeofday(&t, NULL);
+       return (1000 * t.tv_sec) + (t.tv_usec / 1000);
+}
+
+void RunTimes::print()
+{
+       if (0 !=  category_stack.size())
+               BEEV::FatalError("category stack is not yet emptuy");
+
+       std::ostringstream result;
+       result << "statistics\n";
+       std::map<Category, int>::const_iterator it1 = counts.begin();
+       std::map<Category, long>::const_iterator it2 = times.begin();
+
+       while (it1 != counts.end())
+       {
+               result << " " << CategoryNames[it1->first] << ": " << it1->second;
+               if ((it2 = times.find(it1->first)) != times.end())
+                       result << " [" << it2->second << "ms]";
+               result << std::endl;
+               it1++;
+       }
+
+       std::cerr << result.str();
+       // iterator
+}
+
+void RunTimes::addTime(Category c, long milliseconds)
+{
+       std::map<Category, long>::iterator it;
+       if ((it = times.find(c)) == times.end())
+       {
+               times[c] = milliseconds;
+       }
+       else
+       {
+               it->second += milliseconds;
+       }
+
+}
+
+void RunTimes::addCount(Category c)
+{
+       std::map<Category, int>::iterator it;
+       if ((it = counts.find(c)) == counts.end())
+       {
+               counts[c] = 1;
+       }
+       else
+       {
+               it->second++;
+       }
+}
+
+void RunTimes::stop(Category c)
+{
+       Element e = category_stack.top();
+       category_stack.pop();
+       if (e.first != c)
+       {
+               std::cerr << e.first;
+               std::cerr << c;
+               BEEV::FatalError("Don't match");
+       }
+       addTime(c, getCurrentTime() - e.second);
+       addCount(c);
+}
+
+void RunTimes::start(Category c)
+{
+       category_stack.push(std::make_pair(c, getCurrentTime()));
+}

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
new file mode 100644 (file)
index 0000000..8991c66
--- /dev/null
+++ b/src/AST/RunTimes.h
@@ -0,0 +1,51 @@
+#ifndef RUNTIMES_H
+#define RUNTIMES_H
+
+#include <stack>
+#include <map>
+#include <string>
+
+class RunTimes
+{
+public:
+       enum Category
+       { // BE VERY CAREFUL> Update the Category Names to match.
+               Transforming = 0, SimplifyTopLevel, Parsing, TransformFormulaTopLevel, CNFConversion, BitBlasting, Solving
+       };
+       static std::string CategoryNames[];
+
+       typedef std::pair<Category, long> Element;
+
+private:
+       RunTimes& operator =(const RunTimes&);
+       RunTimes(const RunTimes& other);
+
+       std::map<Category, int> counts;
+       std::map<Category, long> times;
+       std::stack<Element> category_stack;
+
+       // millisecond precision timer.
+       long getCurrentTime();
+       void addTime(Category c, long milliseconds);
+
+public:
+
+       void addCount(Category c);
+       void start(Category c);
+       void stop(Category c);
+       void print();
+
+       RunTimes(){}
+
+       void clear()
+       {
+               counts.clear();
+               times.clear();
+               category_stack.empty();
+       }
+
+
+
+};
+
+#endif

diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index 9ef0244bb6c18e880516cc16da3b8e8f6f228f8c..9dd11fa4331a7e1b9d4b0ddbc179e5655d353c74 100644 (file)
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -38,6 +38,8 @@ namespace BEEV
   // up the cache that the others use.
   ASTNode BeevMgr::TransformFormula_TopLevel(const ASTNode& form)
   {
+       runTimes.start(RunTimes::TransformFormulaTopLevel);
+
     assert(TransformMap == NULL);
     TransformMap = new ASTNodeMap(100);
     ASTNode result = TransformFormula(form);
@@ -46,6 +48,9 @@ namespace BEEV
     TransformMap->clear();
     delete TransformMap;
     TransformMap = NULL;
+
+    runTimes.stop(RunTimes::TransformFormulaTopLevel);
+
     return result;
   }
 

diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp
index 40519c22bbfa88081767a73a44fbcde2be5bc4b8..5b1fe1fb4cb8fb59271b095ced8ef9a9423fb85b 100644 (file)
--- a/src/AST/printer/SMTLIBPrinter.cpp
+++ b/src/AST/printer/SMTLIBPrinter.cpp
@@ -23,7 +23,7 @@ namespace printer
 
   string functionToSMTLIBName(const BEEV::Kind k);
   void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize);
-  void printVarDeclsToStream( const BeevMgr mgr, ostream &os);
+  void printVarDeclsToStream( const BeevMgr& mgr, ostream &os);
 
   // Initial version intended to print the whole thing back.
   void SMTLIB_PrintBack(ostream &os, const ASTNode& n) {
@@ -35,7 +35,7 @@ namespace printer
          os << ")" << endl;
   }
 
-  void printVarDeclsToStream( const BeevMgr mgr, ostream &os) {
+  void printVarDeclsToStream( const BeevMgr& mgr, ostream &os) {
       for(ASTVec::const_iterator i = mgr.ListOfDeclaredVars.begin(),iend=mgr.ListOfDeclaredVars.end();i!=iend;i++) {
         const BEEV::ASTNode& a = *i;
 

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 76c1c29275676cbfc2d73ed2227316acb34472ba..ffe6e7024486af8de8a5bcc887e892d3d2df808d 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -44,6 +44,8 @@ int main(int argc, char ** argv) {
       FatalError("Initial allocation of memory failed.");
     }
 
+  bool quick_statistics_flag=false;
+
   //populate the help string
   helpstring += "STP version: " + version + "\n\n";
   helpstring +=  "-a  : switch optimizations off (optimizations are ON by default)\n";
@@ -57,6 +59,7 @@ int main(int argc, char ** argv) {
   helpstring +=  "-p  : print counterexample\n";
   helpstring +=  "-r  : switch refinement off (optimizations are ON by default)\n";
   helpstring +=  "-s  : print function statistics\n";
+  helpstring +=  "-t  : print quick statistics\n";
   helpstring +=  "-v  : print nodes \n";
   helpstring +=  "-w  : switch wordlevel solver off (optimizations are ON by default)\n";
   helpstring +=  "-x  : flatten nested XORs\n";
@@ -123,6 +126,9 @@ int main(int argc, char ** argv) {
             case 's' :
               stats_flag = true;
               break;
+            case 't':
+               quick_statistics_flag = true;
+               break;
             case 'u':
               arraywrite_refinement_flag = false;
               break;
@@ -179,6 +185,7 @@ int main(int argc, char ** argv) {
   GlobalBeevMgr = new BeevMgr();
   ASTVec * AssertsQuery = new ASTVec;
 
+  GlobalBeevMgr->runTimes.start(RunTimes::Parsing);
   if (smtlib_parser_flag)
     {
       smtparse((void*)AssertsQuery);
@@ -187,6 +194,7 @@ int main(int argc, char ** argv) {
     {
       cvcparse((void*)AssertsQuery);
     }
+  GlobalBeevMgr->runTimes.stop(RunTimes::Parsing);
 
   ASTNode asserts = (*(ASTVec*)AssertsQuery)[0];
   ASTNode query   = (*(ASTVec*)AssertsQuery)[1];
@@ -205,6 +213,8 @@ int main(int argc, char ** argv) {
     } //end of PrintBack if
 
   SOLVER_RETURN_TYPE ret = GlobalBeevMgr->TopLevelSAT(asserts, query);
+  if (quick_statistics_flag)
+         GlobalBeevMgr->runTimes.print();
   GlobalBeevMgr->PrintOutput(ret);
   return 0;
 }//end of Main

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 3c1021c1f2aa180fcc23f926eb052d2b07363ba0..8fb9aea5ecf0f87ade4a6fbbac21de9b5fc7a7d9 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -311,12 +311,13 @@ ASTNode Flatten(const ASTNode& a)
   BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, 
                                    bool pushNeg, ASTNodeMap* VarConstMap)
   {
+       runTimes.start(RunTimes::SimplifyTopLevel);
     ResetSimplifyMaps();
-
     if (smtlib_parser_flag)
     BuildReferenceCountMap(b);
     ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
     ResetSimplifyMaps();
+    runTimes.stop(RunTimes::SimplifyTopLevel);
     return out;
   }
 

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 3e5b3c9f6a3150597f5eaf4237c2a25ff2afbb53..3557c7aa7aed09ab7c64d5ab4e185b6b048024ad 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -50,6 +50,7 @@ namespace BEEV
 
     BeevMgr::ClauseList* convertToCNF(const ASTNode& varphi)
     {
+      varphi.GetBeevMgr().runTimes.start(RunTimes::CNFConversion);
       scanFormula(varphi, true);
       ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
       BeevMgr::ClauseList* defs = SINGLETON(dummy_true_var);
@@ -58,6 +59,7 @@ namespace BEEV
       defs->insert(defs->begin() + 1, top->begin(), top->end());
 
       cleanup(varphi);
+      varphi.GetBeevMgr().runTimes.stop(RunTimes::CNFConversion);
       return defs;
     }
 
@@ -1780,7 +1782,10 @@ namespace BEEV
                                                   const ASTNode& modified_input,
                                                   const ASTNode& original_input)
   {
+    runTimes.start(RunTimes::BitBlasting);
     ASTNode BBFormula = BBForm(modified_input);
+       runTimes.stop(RunTimes::BitBlasting);
+
     CNFMgr* cm = new CNFMgr(this);
     ClauseList* cl = cm->convertToCNF(BBFormula);
     if (stats_flag)

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 2fbb4386157a2d92c9f2b932bf93877f1772d3f0..5079fb51b44c317aad3559af458bcc98001cf056 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -10,6 +10,7 @@
 #include "../AST/AST.h"
 #include "../simplifier/bvsolver.h"
 #include "../sat/sat.h"
+#include "../AST/RunTimes.h"
 
 namespace BEEV
 {
@@ -953,8 +954,10 @@ namespace BEEV
            //printf("##################################################\n");
            ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
 
+
            simplified_solved_InputToSAT = 
              SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+
            ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
          }
 
@@ -1061,6 +1064,7 @@ namespace BEEV
       }
 
     res = CallSAT_ResultCheck(newS, simplified_solved_InputToSAT, orig_input);
+
     if (SOLVER_UNDECIDED != res)
       {
         CountersAndStats("print_func_stats");