about summary refs log tree commit diff homepage
path: root/lib/SMT/main.cpp
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2017-02-13 23:13:00 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2017-02-13 23:13:00 +0000
commitffd0b9133ac4fa0b3939616767854e8ffc54feab (patch)
treeccc98d862633c997f6d7e69f3bcb55d394540181 /lib/SMT/main.cpp
parent13d8b4cb78c81bff97501cbe586f0fd8f1adc4d2 (diff)
downloadklee-ffd0b9133ac4fa0b3939616767854e8ffc54feab.tar.gz
Removing unused lib/SMT directory
Diffstat (limited to 'lib/SMT/main.cpp')
-rw-r--r--lib/SMT/main.cpp40
1 files changed, 0 insertions, 40 deletions
diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
deleted file mode 100644
index 31fa311d..00000000
--- a/lib/SMT/main.cpp
+++ /dev/null
@@ -1,40 +0,0 @@
-#include "SMTParser.h"
-
-#include "klee/ExprBuilder.h"
-
-using namespace klee;
-
-int main(int argc, char** argv) {
-  if (argc != 2) {
-    cout << "Usage: " << argv[0] << " <smt-filename>\n";
-    return 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.Parse();
-  int result = smtParser.Solve();
-  
-  cout << (result ? "UNSAT":"SAT") << "\n"; 
-}