about summary refs log tree commit diff homepage
path: root/lib/SMT/main.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/SMT/main.cpp')
-rw-r--r--lib/SMT/main.cpp27
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();