klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
main.cpp
Go to the documentation of this file.
1 #include "SMTParser.h"
2 
3 #include "klee/ExprBuilder.h"
4 
5 using namespace klee;
6 
7 int main(int argc, char** argv) {
8  if (argc != 2) {
9  cout << "Usage: " << argv[0] << " <smt-filename>\n";
10  return 1;
11  }
12 
13  enum BuilderKinds {
14  DefaultBuilder,
15  ConstantFoldingBuilder,
16  SimplifyingBuilder
17  } BuilderKind = SimplifyingBuilder;
18 
19  ExprBuilder *Builder = 0;
20  switch (BuilderKind) {
21  case DefaultBuilder:
22  Builder = createDefaultExprBuilder();
23  break;
24  case ConstantFoldingBuilder:
25  Builder = createDefaultExprBuilder();
26  Builder = createConstantFoldingExprBuilder(Builder);
27  break;
28  case SimplifyingBuilder:
29  Builder = createDefaultExprBuilder();
30  Builder = createConstantFoldingExprBuilder(Builder);
31  Builder = createSimplifyingExprBuilder(Builder);
32  break;
33  }
34 
35  klee::expr::SMTParser smtParser(argv[1], Builder);
36  smtParser.Parse();
37  int result = smtParser.Solve();
38 
39  cout << (result ? "UNSAT":"SAT") << "\n";
40 }
ExprBuilder * createSimplifyingExprBuilder(ExprBuilder *Base)
ExprBuilder * createDefaultExprBuilder()
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
BuilderKinds
Definition: main.cpp:91
int main(int argc, char **argv)
Definition: main.cpp:449
ExprBuilder * createConstantFoldingExprBuilder(ExprBuilder *Base)