klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CexCachingSolver Class Reference
Inheritance diagram for CexCachingSolver:
Collaboration diagram for CexCachingSolver:

Public Member Functions

 CexCachingSolver (Solver *_solver)
 
 ~CexCachingSolver ()
 
bool computeTruth (const Query &, bool &isValid)
 
bool computeValidity (const Query &, Solver::Validity &result)
 
bool computeValue (const Query &, ref< Expr > &result)
 
bool computeInitialValues (const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
 
SolverRunStatus getOperationStatusCode ()
 getOperationStatusCode - get the status of the last solver operation More...
 
char * getConstraintLog (const Query &query)
 
void setCoreSolverTimeout (double timeout)
 
- Public Member Functions inherited from klee::SolverImpl
 SolverImpl ()
 
virtual ~SolverImpl ()
 

Private Types

typedef std::set< Assignment
*, AssignmentLessThan
assignmentsTable_ty
 

Private Member Functions

bool searchForAssignment (KeyType &key, Assignment *&result)
 
bool lookupAssignment (const Query &query, KeyType &key, Assignment *&result)
 
bool lookupAssignment (const Query &query, Assignment *&result)
 
bool getAssignment (const Query &query, Assignment *&result)
 

Private Attributes

Solversolver
 
MapOfSets< ref< Expr >
, Assignment * > 
cache
 
assignmentsTable_ty assignmentsTable
 

Additional Inherited Members

- Public Types inherited from klee::SolverImpl
enum  SolverRunStatus {
  SOLVER_RUN_STATUS_SUCCESS_SOLVABLE, SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE, SOLVER_RUN_STATUS_FAILURE, SOLVER_RUN_STATUS_TIMEOUT,
  SOLVER_RUN_STATUS_FORK_FAILED, SOLVER_RUN_STATUS_INTERRUPTED, SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE, SOLVER_RUN_STATUS_WAITPID_FAILED
}
 
- Static Public Member Functions inherited from klee::SolverImpl
static const char * getOperationStatusString (SolverRunStatus statusCode)
 

Detailed Description

Definition at line 53 of file CexCachingSolver.cpp.

Member Typedef Documentation

Definition at line 54 of file CexCachingSolver.cpp.

Constructor & Destructor Documentation

CexCachingSolver::CexCachingSolver ( Solver _solver)
inline

Definition at line 75 of file CexCachingSolver.cpp.

CexCachingSolver::~CexCachingSolver ( )

Definition at line 245 of file CexCachingSolver.cpp.

Member Function Documentation

bool CexCachingSolver::computeInitialValues ( const Query query,
const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  values,
bool &  hasSolution 
)
virtual
See also
Solver::getInitialValues()

Implements klee::SolverImpl.

Definition at line 319 of file CexCachingSolver.cpp.

References klee::Assignment::bindings, klee::stats::cexCacheTime, and klee::Array::size.

bool CexCachingSolver::computeTruth ( const Query query,
bool &  isValid 
)
virtual

computeTruth - Determine whether the given query expression is provably true given the constraints.

The query expression is guaranteed to be non-constant and have bool type.

This method should evaluate the logical formula:

\[ \forall X constraints(X) \to query(X) \]

Where $X$ is some assignment, $constraints(X)$ are the constraints in the query and $query(X)$ is the query expression.

Parameters
[out]isValid- On success, true iff the logical formula is true.
Returns
True on success

Implements klee::SolverImpl.

Definition at line 277 of file CexCachingSolver.cpp.

References klee::stats::cexCacheTime, and klee::Query::negateExpr().

Here is the call graph for this function:

bool CexCachingSolver::computeValidity ( const Query query,
Solver::Validity result 
)
virtual

computeValidity - Compute a full validity result for the query.

The query expression is guaranteed to be non-constant and have bool type.

SolverImpl provides a default implementation which uses computeTruth. Clients should override this if a more efficient implementation is available.

Parameters
[out]result- if

\[ \forall X constraints(X) \to query(X) \]

then Solver::True, else if

\[ \forall X constraints(X) \to \lnot query(X) \]

then Solver::False, else Solver::Unknown
Returns
True on success

Reimplemented from klee::SolverImpl.

Definition at line 253 of file CexCachingSolver.cpp.

References klee::stats::cexCacheTime, klee::Assignment::evaluate(), klee::Query::expr, klee::Solver::False, klee::Query::negateExpr(), klee::Solver::True, klee::Solver::Unknown, and klee::Query::withFalse().

Here is the call graph for this function:

bool CexCachingSolver::computeValue ( const Query query,
ref< Expr > &  result 
)
virtual

computeValue - Compute a feasible value for the expression.

The query expression is guaranteed to be non-constant.

Returns
True on success

Implements klee::SolverImpl.

Definition at line 304 of file CexCachingSolver.cpp.

References klee::stats::cexCacheTime, klee::Assignment::evaluate(), klee::Query::expr, and klee::Query::withFalse().

Here is the call graph for this function:

bool CexCachingSolver::getAssignment ( const Query query,
Assignment *&  result 
)
private

Definition at line 205 of file CexCachingSolver.cpp.

References klee::findSymbolicObjects(), and klee::Assignment::satisfies().

Here is the call graph for this function:

char * CexCachingSolver::getConstraintLog ( const Query query)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 355 of file CexCachingSolver.cpp.

SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode ( )
virtual

getOperationStatusCode - get the status of the last solver operation

Implements klee::SolverImpl.

Definition at line 351 of file CexCachingSolver.cpp.

bool CexCachingSolver::lookupAssignment ( const Query query,
KeyType key,
Assignment *&  result 
)
private

lookupAssignment - Lookup a cached result for the given

  • query.
Parameters
query- The query to lookup.
key[out] - On return, the key constructed for the query.
result[out] - The cached result, if the lookup is succesful. This is either a satisfying assignment (for a satisfiable query), or 0 (for an unsatisfiable query).
Returns
True if a cached result was found.

Definition at line 182 of file CexCachingSolver.cpp.

References klee::ConstraintManager::begin(), klee::Query::constraints, klee::Expr::createIsZero(), klee::ConstraintManager::end(), klee::Query::expr, klee::stats::queryCexCacheHits, and klee::stats::queryCexCacheMisses.

Here is the call graph for this function:

bool CexCachingSolver::lookupAssignment ( const Query query,
Assignment *&  result 
)
inlineprivate

Definition at line 67 of file CexCachingSolver.cpp.

bool CexCachingSolver::searchForAssignment ( KeyType key,
Assignment *&  result 
)
private

searchForAssignment - Look for a cached solution for a query.

Parameters
key- The query to look up.
result[out] - The cached result, if the lookup is succesful. This is either a satisfying assignment (for a satisfiable query), or 0 (for an unsatisfiable query).
Returns
- True if a cached result was found.

Definition at line 117 of file CexCachingSolver.cpp.

References klee::Assignment::satisfies().

Here is the call graph for this function:

void CexCachingSolver::setCoreSolverTimeout ( double  timeout)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 359 of file CexCachingSolver.cpp.

Member Data Documentation

assignmentsTable_ty CexCachingSolver::assignmentsTable
private

Definition at line 60 of file CexCachingSolver.cpp.

MapOfSets<ref<Expr>, Assignment*> CexCachingSolver::cache
private

Definition at line 58 of file CexCachingSolver.cpp.

Solver* CexCachingSolver::solver
private

Definition at line 56 of file CexCachingSolver.cpp.


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