From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 14 Sep 2009 14:28:29 +0000 (+0000)
Subject: The result of the -t option (quick statistics), also gives solver time
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=82c4f389a9109bd48c8b8dd913e232a2583db3a4;p=francis%2Fstp.git

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 2ac0582..80e0d7e 100644
--- 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 8991c66..f428823 100644
--- 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 aa15002..78906ac 100644
--- 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 5079fb5..2e4770e 100644
--- 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);