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 acee0c4964cef62dd511bfbfd4c0815c5aa8d469..e411c7b138c06fee7269880720de2a8f9e893e91 100644 (file)
--- 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 c2de931c16c86a675f1dd4884b1ab874aaaa8743..0c9bbd7ae55d9e5c668e416199d5c614b95a11b7 100644 (file)
--- 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[];