klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SMTLIBLoggingSolver.cpp
Go to the documentation of this file.
1 //===-- SMTLIBLoggingSolver.cpp -------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #include "QueryLoggingSolver.h"
12 
13 using namespace klee;
14 
18 {
19  private:
20 
22 
23  virtual void printQuery(const Query& query,
24  const Query* falseQuery = 0,
25  const std::vector<const Array*>* objects = 0)
26  {
27  if (0 == falseQuery)
28  {
29  printer->setQuery(query);
30  }
31  else
32  {
33  printer->setQuery(*falseQuery);
34  }
35 
36  if (0 != objects)
37  {
38  printer->setArrayValuesToGet(*objects);
39  }
40 
41  printer->generateOutput();
42  }
43 
44  public:
46  std::string path,
47  int queryTimeToLog)
48  : QueryLoggingSolver(_solver, path, ";", queryTimeToLog),
49  printer()
50  {
51  //Setup the printer
52  printer = createSMTLIBPrinter();
53  printer->setOutput(logBuffer);
54  }
55 
57  {
58  delete printer;
59  }
60 };
61 
62 
63 Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path,
64  int minQueryTimeToLog)
65 {
66  return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog));
67 }
Solver * createSMTLIBLoggingSolver(Solver *s, std::string path, int minQueryTimeToLog)
ExprSMTLIBPrinter * createSMTLIBPrinter()
virtual void printQuery(const Query &query, const Query *falseQuery=0, const std::vector< const Array * > *objects=0)
ExprSMTLIBPrinter * printer
SMTLIBLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog)