klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
PCLoggingSolver.cpp
Go to the documentation of this file.
1 //===-- PCLoggingSolver.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"
11 
12 #include "klee/Expr.h"
13 #include "klee/util/ExprPPrinter.h"
15 
16 using namespace klee;
17 
19 
21 
22 private :
24 
25  virtual void printQuery(const Query& query,
26  const Query* falseQuery = 0,
27  const std::vector<const Array*>* objects = 0) {
28 
29  const ref<Expr>* evalExprsBegin = 0;
30  const ref<Expr>* evalExprsEnd = 0;
31 
32  if (0 != falseQuery) {
33  evalExprsBegin = &query.expr;
34  evalExprsEnd = &query.expr + 1;
35  }
36 
37  const Array* const *evalArraysBegin = 0;
38  const Array* const *evalArraysEnd = 0;
39 
40  if ((0 != objects) && (false == objects->empty())) {
41  evalArraysBegin = &((*objects)[0]);
42  evalArraysEnd = &((*objects)[0]) + objects->size();
43  }
44 
45  const Query* q = (0 == falseQuery) ? &query : falseQuery;
46 
47  printer->printQuery(logBuffer, q->constraints, q->expr,
48  evalExprsBegin, evalExprsEnd,
49  evalArraysBegin, evalArraysEnd);
50  }
51 
52 public:
53  PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog)
54  : QueryLoggingSolver(_solver, path, "#", queryTimeToLog),
55  printer(ExprPPrinter::create(logBuffer)) {
56  }
57 
58  virtual ~PCLoggingSolver() {
59  delete printer;
60  }
61 };
62 
64 
65 Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path,
66  int minQueryTimeToLog) {
67  return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog));
68 }
ExprPPrinter * printer
unsigned size
Definition: Expr.h:605
ref< Expr > expr
Definition: Solver.h:25
PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog)
virtual void printQuery(const Query &query, const Query *falseQuery=0, const std::vector< const Array * > *objects=0)
virtual ~PCLoggingSolver()
const ConstraintManager & constraints
Definition: Solver.h:24
Solver * createPCLoggingSolver(Solver *s, std::string path, int minQueryTimeToLog)