First attempt at tracking time spent building the counter example. Doesn't properly...

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

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

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index 9f1ff004485543a2a81d57e916a655d441f6dc3f..20ccd3b682be850aaeac96dec8c99b0e4b7958ef 100644 (file)
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -27,7 +27,8 @@ public:
       Solving, 
       BVSolver, 
       CreateSubstitutionMap, 
-      SendingToSAT
+      SendingToSAT,
+      CounterExampleGeneration
     };
 
   static std::string CategoryNames[];

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 00bb6744a44ac4d053577981e07a5f1d69143e17..e4ab1d037d95a5baf2dbc5976165ab1adabf0543 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -955,7 +955,8 @@ namespace BEEV
       }
     else if (SatSolver.okay())
       {
-        CounterExampleMap.clear();
+       bm->GetRunTimes()->start(RunTimes::CounterExampleGeneration);
+       CounterExampleMap.clear();
         ConstructCounterExample(SatSolver);
         if (bm->UserFlags.stats_flag 
             && bm->UserFlags.print_nodes_flag)
@@ -971,6 +972,8 @@ namespace BEEV
           FatalError("TopLevelSat: Original input must compute to "\
                      "true or false against model");
 
+        bm->GetRunTimes()->stop(RunTimes::CounterExampleGeneration);
+
         // if the counterexample is indeed a good one, then return
         // invalid
         if (ASTTrue == orig_result)