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

Classes

struct  CacheEntry
 
struct  CacheEntryHash
 

Public Member Functions

 CachingSolver (Solver *s)
 
 ~CachingSolver ()
 
bool computeValidity (const Query &, Solver::Validity &result)
 
bool computeTruth (const Query &, bool &isValid)
 
bool computeValue (const Query &query, ref< Expr > &result)
 
bool computeInitialValues (const Query &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 &)
 
void setCoreSolverTimeout (double timeout)
 
- Public Member Functions inherited from klee::SolverImpl
 SolverImpl ()
 
virtual ~SolverImpl ()
 

Private Types

typedef
std::tr1::unordered_map
< CacheEntry,
IncompleteSolver::PartialValidity,
CacheEntryHash
cache_map
 

Private Member Functions

ref< ExprcanonicalizeQuery (ref< Expr > originalQuery, bool &negationUsed)
 
void cacheInsert (const Query &query, IncompleteSolver::PartialValidity result)
 Inserts the given query, result pair into the cache. More...
 
bool cacheLookup (const Query &query, IncompleteSolver::PartialValidity &result)
 

Private Attributes

Solversolver
 
cache_map cache
 

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 24 of file CachingSolver.cpp.

Member Typedef Documentation

Definition at line 64 of file CachingSolver.cpp.

Constructor & Destructor Documentation

CachingSolver::CachingSolver ( Solver s)
inline

Definition at line 70 of file CachingSolver.cpp.

CachingSolver::~CachingSolver ( )
inline

Definition at line 71 of file CachingSolver.cpp.

Member Function Documentation

void CachingSolver::cacheInsert ( const Query query,
IncompleteSolver::PartialValidity  result 
)
private

Inserts the given query, result pair into the cache.

Definition at line 130 of file CachingSolver.cpp.

References klee::Query::constraints, klee::Query::expr, and klee::IncompleteSolver::negatePartialValidity().

Here is the call graph for this function:

bool CachingSolver::cacheLookup ( const Query query,
IncompleteSolver::PartialValidity result 
)
private
Returns
true on a cache hit, false of a cache miss. Reference value result only valid on a cache hit.

Definition at line 111 of file CachingSolver.cpp.

References klee::Query::constraints, klee::Query::expr, and klee::IncompleteSolver::negatePartialValidity().

Here is the call graph for this function:

ref< Expr > CachingSolver::canonicalizeQuery ( ref< Expr originalQuery,
bool &  negationUsed 
)
private
Returns
the canonical version of the given query. The reference negationUsed is set to true if the original query was negated in the canonicalization process.

Definition at line 95 of file CachingSolver.cpp.

References klee::ref< T >::compare(), and klee::Expr::createIsZero().

Here is the call graph for this function:

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

Implements klee::SolverImpl.

Definition at line 79 of file CachingSolver.cpp.

References klee::stats::queryCacheMisses.

bool CachingSolver::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 211 of file CachingSolver.cpp.

References klee::IncompleteSolver::MayBeFalse, klee::IncompleteSolver::MayBeTrue, klee::IncompleteSolver::MustBeTrue, klee::stats::queryCacheHits, klee::stats::queryCacheMisses, and klee::IncompleteSolver::TrueOrFalse.

bool CachingSolver::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 142 of file CachingSolver.cpp.

References klee::Solver::False, klee::IncompleteSolver::MayBeFalse, klee::IncompleteSolver::MayBeTrue, klee::IncompleteSolver::MustBeFalse, klee::IncompleteSolver::MustBeTrue, klee::Query::negateExpr(), klee::stats::queryCacheHits, klee::stats::queryCacheMisses, klee::Solver::True, klee::IncompleteSolver::TrueOrFalse, and klee::Solver::Unknown.

Here is the call graph for this function:

bool CachingSolver::computeValue ( const Query query,
ref< Expr > &  result 
)
inlinevirtual

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 75 of file CachingSolver.cpp.

References klee::stats::queryCacheMisses.

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

Reimplemented from klee::SolverImpl.

Definition at line 249 of file CachingSolver.cpp.

SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode ( )
virtual

getOperationStatusCode - get the status of the last solver operation

Implements klee::SolverImpl.

Definition at line 245 of file CachingSolver.cpp.

void CachingSolver::setCoreSolverTimeout ( double  timeout)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 253 of file CachingSolver.cpp.

Member Data Documentation

cache_map CachingSolver::cache
private

Definition at line 67 of file CachingSolver.cpp.

Solver* CachingSolver::solver
private

Definition at line 66 of file CachingSolver.cpp.


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