From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 11 Feb 2011 00:43:00 +0000 (+0000)
Subject: Add categories to the RunTime class for new simplifications
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=056259fcad931994315d16e6498215d6e5501152;p=francis%2Fstp.git

Add categories to the RunTime class for new simplifications

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

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index acee0c4..e411c7b 100644
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -16,7 +16,7 @@
 #include "../sat/utils/System.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", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions"};
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Remove Unconstrained", "Pure Literals" };
 
 namespace BEEV
 {
diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index c2de931..0c9bbd7 100644
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -32,7 +32,9 @@ public:
       SATSimplifying,
       ConstantBitPropagation,
       ArrayReadRefinement,
-      ApplyingSubstitutions
+      ApplyingSubstitutions,
+      RemoveUnconstrained,
+      PureLiterals
     };
 
   static std::string CategoryNames[];