From b907a5d240482a904dc0caf81e7f02f5a5b97641 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 14 Sep 2009 10:46:14 +0000 Subject: [PATCH] Add a new class for tracking the runtimes. e.g. SimplifyTopLevel was called 5 times, and took 100ms. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@224 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 2 + src/AST/RunTimes.cpp | 99 +++++++++++++++++++++++++++++++ src/AST/RunTimes.h | 51 ++++++++++++++++ src/AST/Transform.cpp | 5 ++ src/AST/printer/SMTLIBPrinter.cpp | 4 +- src/main/main.cpp | 10 ++++ src/simplifier/simplifier.cpp | 3 +- src/to-sat/ToCNF.cpp | 5 ++ src/to-sat/ToSAT.cpp | 4 ++ 9 files changed, 180 insertions(+), 3 deletions(-) create mode 100644 src/AST/RunTimes.cpp create mode 100644 src/AST/RunTimes.h diff --git a/src/AST/AST.h b/src/AST/AST.h index 056789c..6385f8d 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -36,6 +36,7 @@ #include #include #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 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 +#include +#include +#include +#include + + +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::const_iterator it1 = counts.begin(); + std::map::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::iterator it; + if ((it = times.find(c)) == times.end()) + { + times[c] = milliseconds; + } + else + { + it->second += milliseconds; + } + +} + +void RunTimes::addCount(Category c) +{ + std::map::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 index 0000000..8991c66 --- /dev/null +++ b/src/AST/RunTimes.h @@ -0,0 +1,51 @@ +#ifndef RUNTIMES_H +#define RUNTIMES_H + +#include +#include +#include + +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 Element; + +private: + RunTimes& operator =(const RunTimes&); + RunTimes(const RunTimes& other); + + std::map counts; + std::map times; + std::stack 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 9ef0244..9dd11fa 100644 --- 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 40519c2..5b1fe1f 100644 --- 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 76c1c29..ffe6e70 100644 --- 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 3c1021c..8fb9aea 100644 --- 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 3e5b3c9..3557c7a 100644 --- 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 2fbb438..5079fb5 100644 --- 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"); -- 2.47.3