The result of the -t option (quick statistics), also gives solver time

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

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index 2ac0582d4fa0cb454cc3e40857386269755e8adc..80e0d7e98bb8281d9b1964fd8a240361c186a785 100644 (file)
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -1,10 +1,11 @@
 //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, so inside simplify time will be counted towards both
 //Simplify_TopLevel & Transform.
 
-// This is intended as a low overhead profiling class. So it can be always run.
+// This is intended as a low overhead profiling class. So runtimes can
+// always be tracked.
 
 #include "RunTimes.h"
 #include <cassert>
@@ -13,8 +14,8 @@
 #include <iostream>
 #include <utility>
 
-
-std::string RunTimes::CategoryNames[] = { "Transforming", "Simplify Top Level", "Parsing","Transforming" , "CNF Conversion", "Bit Blasting", "Solving"};
+// BE VERY CAREFUL> Update the Category Names to match.
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "Solving"};
 
 namespace BEEV
 {

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index 8991c66271d0621c20fd054291895d8ccf581864..f4288236a78fa616908a0f52e875f2c128555f8f 100644 (file)
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -9,9 +9,10 @@ class RunTimes
 {
 public:
        enum Category
-       { // BE VERY CAREFUL> Update the Category Names to match.
-               Transforming = 0, SimplifyTopLevel, Parsing, TransformFormulaTopLevel, CNFConversion, BitBlasting, Solving
+               {
+                       Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving
        };
+
        static std::string CategoryNames[];
 
        typedef std::pair<Category, long> Element;

diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile
index aa1500255fbb503ec8263c3fb57277561b83c135..78906ac8566a1bf90f6d5bc592daf6fadb15bc04 100644 (file)
--- a/src/sat/core/Makefile
+++ b/src/sat/core/Makefile
@@ -1,7 +1,7 @@
 MTL       = ../mtl
 CHDRS     = $(wildcard *.h) $(wildcard $(MTL)/*.h)
 EXEC      = minisat
-CFLAGS    = -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store
+CFLAGS    = -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store -m32
 LFLAGS    = -lz
 
 
@@ -9,4 +9,4 @@ include ../mtl/template.mk
 all:
        ranlib libminisat.a
        cp *.or ../
-       cp libminisat.a ../
\ No newline at end of file
+       cp libminisat.a ../

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 5079fb51b44c317aad3559af458bcc98001cf056..2e4770e6523549de9b9bf42baf2a75cf214c5d93 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -125,7 +125,11 @@ namespace BEEV
     //ChangeActivityLevels_Of_SATVars(newS);
     //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS);
     //newS.solve();
+
+    runTimes.start(RunTimes::Solving);
     newS.solve();
+    runTimes.stop(RunTimes::Solving);
+
     //PrintActivityLevels_Of_SATVars("After SAT",newS);
 
     PrintStats(newS);