klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
TimingSolver.h
Go to the documentation of this file.
1 //===-- TimingSolver.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_TIMINGSOLVER_H
11 #define KLEE_TIMINGSOLVER_H
12 
13 #include "klee/Expr.h"
14 #include "klee/Solver.h"
15 
16 #include <vector>
17 
18 namespace klee {
19  class ExecutionState;
20  class Solver;
21 
24  class TimingSolver {
25  public:
28 
29  public:
35  TimingSolver(Solver *_solver, bool _simplifyExprs = true)
36  : solver(_solver), simplifyExprs(_simplifyExprs) {}
38  delete solver;
39  }
40 
41  void setTimeout(double t) {
43  }
44 
45  char *getConstraintLog(const Query& query) {
46  return solver->getConstraintLog(query);
47  }
48 
49  bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);
50 
51  bool mustBeTrue(const ExecutionState&, ref<Expr>, bool &result);
52 
53  bool mustBeFalse(const ExecutionState&, ref<Expr>, bool &result);
54 
55  bool mayBeTrue(const ExecutionState&, ref<Expr>, bool &result);
56 
57  bool mayBeFalse(const ExecutionState&, ref<Expr>, bool &result);
58 
59  bool getValue(const ExecutionState &, ref<Expr> expr,
60  ref<ConstantExpr> &result);
61 
62  bool getInitialValues(const ExecutionState&,
63  const std::vector<const Array*> &objects,
64  std::vector< std::vector<unsigned char> > &result);
65 
66  std::pair< ref<Expr>, ref<Expr> >
67  getRange(const ExecutionState&, ref<Expr> query);
68  };
69 
70 }
71 
72 #endif
void setTimeout(double t)
Definition: TimingSolver.h:41
bool getInitialValues(const ExecutionState &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)
char * getConstraintLog(const Query &query)
Definition: TimingSolver.h:45
bool mayBeFalse(const ExecutionState &, ref< Expr >, bool &result)
virtual char * getConstraintLog(const Query &query)
Definition: Solver.cpp:124
bool mayBeTrue(const ExecutionState &, ref< Expr >, bool &result)
bool mustBeFalse(const ExecutionState &, ref< Expr >, bool &result)
virtual void setCoreSolverTimeout(double timeout)
Definition: Solver.cpp:128
bool mustBeTrue(const ExecutionState &, ref< Expr >, bool &result)
TimingSolver(Solver *_solver, bool _simplifyExprs=true)
Definition: TimingSolver.h:35
std::pair< ref< Expr >, ref< Expr > > getRange(const ExecutionState &, ref< Expr > query)
bool getValue(const ExecutionState &, ref< Expr > expr, ref< ConstantExpr > &result)
bool evaluate(const ExecutionState &, ref< Expr >, Solver::Validity &result)