Rename FoldingExprBuilder -> SimplifyingExprBuilder

Also, start printing query # with -print-ast (for testing purposes).


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73350 91177308-0d34-0410-b5e6-96231b3b80d8

3 files changed, 20 insertions, 13 deletions

diff --git a/include/klee/ExprBuilder.h b/include/klee/ExprBuilder.h
index e39da38c..6c1f6809 100644
--- a/include/klee/ExprBuilder.h
+++ b/include/klee/ExprBuilder.h
@@ -69,11 +69,12 @@ namespace klee {
   /// Base - The base builder to use when constructing expressions.
   ExprBuilder *createConstantFoldingExprBuilder(ExprBuilder *Base);
 
-  /// createFoldingExprBuilder - Create an expression builder which attemps to
-  /// fold redundant expressions and normalize expressions for improved caching.
+  /// createSimplifyingExprBuilder - Create an expression builder which attemps
+  /// to fold redundant expressions and normalize expressions for improved
+  /// caching.
   ///
   /// Base - The base builder to use when constructing expressions.
-  ExprBuilder *createFoldingExprBuilder(ExprBuilder *Base);
+  ExprBuilder *createSimplifyingExprBuilder(ExprBuilder *Base);
 }
 
 #endif
diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index f373e2b8..0445222d 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -397,12 +397,12 @@ namespace {
     }
   };
 
-  class FoldingExprBuilder : public ExprBuilder {
+  class SimplifyingExprBuilder : public ExprBuilder {
     ExprBuilder *Base;
 
   public:
-    FoldingExprBuilder(ExprBuilder *_Base) : Base(_Base) {}
-    ~FoldingExprBuilder() { 
+    SimplifyingExprBuilder(ExprBuilder *_Base) : Base(_Base) {}
+    ~SimplifyingExprBuilder() { 
       delete Base;
     }
 
@@ -543,6 +543,6 @@ ExprBuilder *klee::createConstantFoldingExprBuilder(ExprBuilder *Base) {
   return new ConstantFoldingExprBuilder(Base);
 }
 
-ExprBuilder *klee::createFoldingExprBuilder(ExprBuilder *Base) {
-  return new FoldingExprBuilder(Base);
+ExprBuilder *klee::createSimplifyingExprBuilder(ExprBuilder *Base) {
+  return new SimplifyingExprBuilder(Base);
 }
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 8762d332..e45b65d0 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -47,7 +47,7 @@ namespace {
   enum BuilderKinds {
     DefaultBuilder,
     ConstantFoldingBuilder,
-    FoldingBuilder
+    SimplifyingBuilder
   };
 
   static llvm::cl::opt<BuilderKinds> 
@@ -59,7 +59,7 @@ namespace {
                          "Default expression construction."),
               clEnumValN(ConstantFoldingBuilder, "constant-folding",
                          "Fold constant expressions."),
-              clEnumValN(FoldingBuilder, "folding",
+              clEnumValN(SimplifyingBuilder, "simplify",
                          "Fold constants and simplify expressions."),
               clEnumValEnd));
 }
@@ -100,9 +100,15 @@ static bool PrintInputAST(const char *Filename,
   std::vector<Decl*> Decls;
   Parser *P = Parser::Create(Filename, MB, Builder);
   P->SetMaxErrors(20);
+
+  unsigned NumQueries = 0;
   while (Decl *D = P->ParseTopLevelDecl()) {
-    if (!P->GetNumErrors())
+    if (!P->GetNumErrors()) {
+      if (isa<QueryCommand>(D))
+        llvm::cout << "# Query " << ++NumQueries << "\n";
+
       D->dump();
+    }
     Decls.push_back(D);
   }
 
@@ -261,10 +267,10 @@ int main(int argc, char **argv) {
     Builder = createDefaultExprBuilder();
     Builder = createConstantFoldingExprBuilder(Builder);
     break;
-  case FoldingBuilder:
+  case SimplifyingBuilder:
     Builder = createDefaultExprBuilder();
     Builder = createConstantFoldingExprBuilder(Builder);
-    Builder = createFoldingExprBuilder(Builder);
+    Builder = createSimplifyingExprBuilder(Builder);
     break;
   }