Use a builder in the SMT parser instead of constructing expressions

directly.



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

1 files changed, 26 insertions, 1 deletions

diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
index 38bfac86..934f0702 100644
--- a/lib/SMT/main.cpp
+++ b/lib/SMT/main.cpp
@@ -1,8 +1,11 @@
 #include "SMTParser.h"
 
+#include "klee/ExprBuilder.h"
+
 #include <iostream>
 
 using namespace std;
+using namespace klee;
 
 int main(int argc, char** argv) {
   if (argc != 2) {
@@ -10,7 +13,29 @@ int main(int argc, char** argv) {
     return 1;
   }
   
-  klee::expr::SMTParser smtParser(argv[1]);
+  enum BuilderKinds {
+    DefaultBuilder,
+    ConstantFoldingBuilder,
+    SimplifyingBuilder
+  } BuilderKind = SimplifyingBuilder;
+
+  ExprBuilder *Builder = 0;
+  switch (BuilderKind) {
+  case DefaultBuilder:
+    Builder = createDefaultExprBuilder();
+    break;
+  case ConstantFoldingBuilder:
+    Builder = createDefaultExprBuilder();
+    Builder = createConstantFoldingExprBuilder(Builder);
+    break;
+  case SimplifyingBuilder:
+    Builder = createDefaultExprBuilder();
+    Builder = createConstantFoldingExprBuilder(Builder);
+    Builder = createSimplifyingExprBuilder(Builder);
+    break;
+  }
+  
+  klee::expr::SMTParser smtParser(argv[1], Builder);
 
   smtParser.Init();