From 056259fcad931994315d16e6498215d6e5501152 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 11 Feb 2011 00:43:00 +0000 Subject: [PATCH] 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 --- src/AST/RunTimes.cpp | 2 +- src/AST/RunTimes.h | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) 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[]; -- 2.47.3