* -t times how long sending the clauses to the SAT solver takes.

* Remove unreachable code in the loop sending clauses to the SAT solver.

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

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index 4c30ceb8e5df08a0744d237817b9b86773a12730..069a51da6748e5702329494a6270634a87abd693 100644 (file)
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -15,7 +15,7 @@
 #include <utility>
 
 // 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"};
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver"};
 
 namespace BEEV
 {

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index a7c9fd65bef33b25f442dabf4024eecd84e317c6..832587c2567a73a3700e24ed5b946ac066407e6f 100644 (file)
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -10,7 +10,7 @@ class RunTimes
 public:
        enum Category
                {
-                       Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving, BVSolver, CreateSubstitutionMap
+                       Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving, BVSolver, CreateSubstitutionMap, SendingToSAT
        };
 
        static std::string CategoryNames[];

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 55582e31758a740614ea96a21e9627afafbdc535..f26884b0f298215fd42d110e3c50476662eb8adb 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -54,6 +54,8 @@ namespace BEEV
   {
     CountersAndStats("SAT Solver");
 
+    runTimes.start(RunTimes::SendingToSAT);
+
     //iterate through the list (conjunction) of ASTclauses cll
     BeevMgr::ClauseList::const_iterator i = cll.begin(), iend = cll.end();
 
@@ -74,6 +76,7 @@ namespace BEEV
       {
         //Clause for the SATSolver
         MINISAT::vec<MINISAT::Lit> satSolverClause;
+        satSolverClause.capacity((*i)->size());
 
         //now iterate through the internals of the ASTclause itself
         vector<const ASTNode*>::const_iterator j = (*i)->begin(), jend = (*i)->end();
@@ -104,15 +107,12 @@ namespace BEEV
         else
           {
             PrintStats(newS);
+            runTimes.stop(RunTimes::SendingToSAT);
             return false;
           }
-
-        if (!newS.simplify())
-          {
-            PrintStats(newS);
-            return false;
           }
-      }
+
+    runTimes.stop(RunTimes::SendingToSAT);
 
     // if input is UNSAT return false, else return true
     if (!newS.simplify())