klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::TimingSolver Class Reference

#include <TimingSolver.h>

Collaboration diagram for klee::TimingSolver:

Public Member Functions

 TimingSolver (Solver *_solver, bool _simplifyExprs=true)
 
 ~TimingSolver ()
 
void setTimeout (double t)
 
char * getConstraintLog (const Query &query)
 
bool evaluate (const ExecutionState &, ref< Expr >, Solver::Validity &result)
 
bool mustBeTrue (const ExecutionState &, ref< Expr >, bool &result)
 
bool mustBeFalse (const ExecutionState &, ref< Expr >, bool &result)
 
bool mayBeTrue (const ExecutionState &, ref< Expr >, bool &result)
 
bool mayBeFalse (const ExecutionState &, ref< Expr >, bool &result)
 
bool getValue (const ExecutionState &, ref< Expr > expr, ref< ConstantExpr > &result)
 
bool getInitialValues (const ExecutionState &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)
 
std::pair< ref< Expr >, ref
< Expr > > 
getRange (const ExecutionState &, ref< Expr > query)
 

Public Attributes

Solversolver
 
bool simplifyExprs
 

Detailed Description

TimingSolver - A simple class which wraps a solver and handles tracking the statistics that we care about.

Definition at line 24 of file TimingSolver.h.

Constructor & Destructor Documentation

klee::TimingSolver::TimingSolver ( Solver _solver,
bool  _simplifyExprs = true 
)
inline

TimingSolver - Construct a new timing solver.

Parameters
_simplifyExprs- Whether expressions should be simplified (via the constraint manager interface) prior to querying.

Definition at line 35 of file TimingSolver.h.

klee::TimingSolver::~TimingSolver ( )
inline

Definition at line 37 of file TimingSolver.h.

References solver.

Member Function Documentation

bool TimingSolver::evaluate ( const ExecutionState state,
ref< Expr expr,
Solver::Validity result 
)

Definition at line 26 of file TimingSolver.cpp.

References klee::ExecutionState::constraints, klee::Solver::False, klee::ExecutionState::queryCost, klee::ConstraintManager::simplifyExpr(), klee::stats::solverTime, and klee::Solver::True.

Referenced by klee::Executor::fork().

Here is the call graph for this function:

Here is the caller graph for this function:

char* klee::TimingSolver::getConstraintLog ( const Query query)
inline

Definition at line 45 of file TimingSolver.h.

References klee::Solver::getConstraintLog(), and solver.

Referenced by klee::Executor::getConstraintLog().

Here is the call graph for this function:

Here is the caller graph for this function:

bool TimingSolver::getInitialValues ( const ExecutionState state,
const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  result 
)

Definition at line 122 of file TimingSolver.cpp.

References klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::ExecutionState::constraints, klee::ExecutionState::queryCost, and klee::stats::solverTime.

Referenced by klee::Executor::getSymbolicSolution().

Here is the call graph for this function:

Here is the caller graph for this function:

std::pair< ref< Expr >, ref< Expr > > TimingSolver::getRange ( const ExecutionState state,
ref< Expr query 
)

Definition at line 146 of file TimingSolver.cpp.

References klee::ExecutionState::constraints.

Referenced by klee::Executor::getAddressInfo().

Here is the caller graph for this function:

bool TimingSolver::mayBeFalse ( const ExecutionState state,
ref< Expr expr,
bool &  result 
)

Definition at line 88 of file TimingSolver.cpp.

bool TimingSolver::mayBeTrue ( const ExecutionState state,
ref< Expr expr,
bool &  result 
)
bool TimingSolver::mustBeFalse ( const ExecutionState state,
ref< Expr expr,
bool &  result 
)

Definition at line 74 of file TimingSolver.cpp.

References klee::Expr::createIsZero().

Referenced by klee::Executor::addConstraint(), and klee::SeedInfo::patchSeed().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::TimingSolver::setTimeout ( double  t)
inline

Definition at line 41 of file TimingSolver.h.

References klee::Solver::setCoreSolverTimeout(), and solver.

Referenced by klee::Executor::executeMemoryOperation(), klee::Executor::fork(), klee::Executor::getSymbolicSolution(), and klee::Executor::toUnique().

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

bool klee::TimingSolver::simplifyExprs

Definition at line 27 of file TimingSolver.h.

Solver* klee::TimingSolver::solver

The documentation for this class was generated from the following files: