klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
QueryLog.h
Go to the documentation of this file.
1 //===-- QueryLog.h ----------------------------------------------*- C++ -*-===//
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 #ifndef KLEE_OPT_LOGGINGSOLVER_H
11 #define KLEE_OPT_LOGGINGSOLVER_H
12 
13 #include "klee/Expr.h"
14 
15 #include <vector>
16 
17 namespace klee {
18  struct Query;
19 
20  class QueryLogEntry {
21  public:
22  enum Type {
27  };
28 
29  typedef std::vector< ref<Expr> > exprs_ty;
31 
34  unsigned instruction;
35  std::vector<const Array*> objects;
36 
37  public:
38  QueryLogEntry() : query(ConstantExpr::alloc(0,Expr::Bool)) {}
39  QueryLogEntry(const QueryLogEntry &b);
40  QueryLogEntry(const Query &_query,
41  Type _type,
42  const std::vector<const Array*> *objects = 0);
43  };
44 
46  public:
47  uint64_t result;
48  double time;
49 
50  public:
52  QueryLogResult(bool _success, uint64_t _result, double _time)
53  : result(_result), time(_time) {
54  if (!_success) { // la la la
55  result = 0;
56  time = -1;
57  }
58  }
59  };
60 
61 }
62 
63 #endif
std::vector< const Array * > objects
Definition: QueryLog.h:35
Class representing symbolic expressions.
Definition: Expr.h:88
ref< Expr > query
Definition: QueryLog.h:33
QueryLogResult(bool _success, uint64_t _result, double _time)
Definition: QueryLog.h:52
std::vector< ref< Expr > > exprs_ty
Definition: QueryLog.h:29
exprs_ty exprs
Definition: QueryLog.h:30
unsigned instruction
Definition: QueryLog.h:34