diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-02-13 23:13:00 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-02-13 23:13:00 +0000 |
commit | ffd0b9133ac4fa0b3939616767854e8ffc54feab (patch) | |
tree | ccc98d862633c997f6d7e69f3bcb55d394540181 /lib/SMT/main.cpp | |
parent | 13d8b4cb78c81bff97501cbe586f0fd8f1adc4d2 (diff) | |
download | klee-ffd0b9133ac4fa0b3939616767854e8ffc54feab.tar.gz |
Removing unused lib/SMT directory
Diffstat (limited to 'lib/SMT/main.cpp')
-rw-r--r-- | lib/SMT/main.cpp | 40 |
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"; -} |