klee
Classes | Public Member Functions | Private Types | Private Member Functions | Private Attributes | List of all members
CachingSolver Class Reference
Inheritance diagram for CachingSolver:
Inheritance graph
[legend]
Collaboration diagram for CachingSolver:
Collaboration graph
[legend]

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

Private Types

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

Private Member Functions

ref< Expr > canonicalizeQuery (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

Solver * solver
 
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 23 of file CachingSolver.cpp.

Member Typedef Documentation

◆ cache_map

typedef std::unordered_map<CacheEntry, IncompleteSolver::PartialValidity, CacheEntryHash> CachingSolver::cache_map
private

Definition at line 63 of file CachingSolver.cpp.

Constructor & Destructor Documentation

◆ CachingSolver()

CachingSolver::CachingSolver ( Solver *  s)
inline

Definition at line 69 of file CachingSolver.cpp.

◆ ~CachingSolver()

CachingSolver::~CachingSolver ( )
inline

Definition at line 70 of file CachingSolver.cpp.

References cache, and solver.

Member Function Documentation

◆ cacheInsert()

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

Inserts the given query, result pair into the cache.

Definition at line 129 of file CachingSolver.cpp.

References cache, canonicalizeQuery(), klee::Query::constraints, and klee::Query::expr.

Referenced by computeTruth(), and computeValidity().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ cacheLookup()

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

References cache, canonicalizeQuery(), klee::Query::constraints, and klee::Query::expr.

Referenced by computeTruth(), and computeValidity().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ canonicalizeQuery()

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

References klee::ref< T >::compare().

Referenced by cacheInsert(), and cacheLookup().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ computeInitialValues()

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

References klee::SolverImpl::computeInitialValues(), klee::Solver::impl, klee::stats::queryCacheMisses, and solver.

Here is the call graph for this function:

◆ computeTruth()

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

References cacheInsert(), cacheLookup(), klee::SolverImpl::computeTruth(), klee::Solver::impl, klee::stats::queryCacheHits, klee::stats::queryCacheMisses, and solver.

Here is the call graph for this function:

◆ computeValidity()

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

References cacheInsert(), cacheLookup(), klee::SolverImpl::computeTruth(), klee::SolverImpl::computeValidity(), klee::Solver::impl, klee::Query::negateExpr(), klee::stats::queryCacheHits, klee::stats::queryCacheMisses, and solver.

Here is the call graph for this function:

◆ computeValue()

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

References klee::SolverImpl::computeValue(), klee::Solver::impl, klee::stats::queryCacheMisses, and solver.

Here is the call graph for this function:

◆ getConstraintLog()

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

Reimplemented from klee::SolverImpl.

Definition at line 248 of file CachingSolver.cpp.

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

Here is the call graph for this function:

◆ getOperationStatusCode()

SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode ( )
virtual

getOperationStatusCode - get the status of the last solver operation

Implements klee::SolverImpl.

Definition at line 244 of file CachingSolver.cpp.

References klee::SolverImpl::getOperationStatusCode(), klee::Solver::impl, and solver.

Here is the call graph for this function:

◆ setCoreSolverTimeout()

void CachingSolver::setCoreSolverTimeout ( time::Span  timeout)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 252 of file CachingSolver.cpp.

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

Here is the call graph for this function:

Member Data Documentation

◆ cache

cache_map CachingSolver::cache
private

Definition at line 66 of file CachingSolver.cpp.

Referenced by cacheInsert(), cacheLookup(), and ~CachingSolver().

◆ solver

Solver* CachingSolver::solver
private

Definition at line 65 of file CachingSolver.cpp.

Referenced by computeInitialValues(), computeTruth(), computeValidity(), computeValue(), getConstraintLog(), getOperationStatusCode(), setCoreSolverTimeout(), and ~CachingSolver().

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