From c24562b54776bac49018371d8d15a00a926debda Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Sat, 11 Jul 2009 00:39:27 +0000
Subject: 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
---
 lib/SMT/main.cpp | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

(limited to 'lib/SMT/main.cpp')

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();
   
-- 
cgit 1.4.1