klee
|
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) |
![]() | |
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 | |
![]() | |
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 const char * | getOperationStatusString (SolverRunStatus statusCode) |
Definition at line 23 of file CachingSolver.cpp.
|
private |
Definition at line 63 of file CachingSolver.cpp.
|
inline |
Definition at line 69 of file CachingSolver.cpp.
|
inline |
Definition at line 70 of file CachingSolver.cpp.
|
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().
|
private |
Definition at line 110 of file CachingSolver.cpp.
References cache, canonicalizeQuery(), klee::Query::constraints, and klee::Query::expr.
Referenced by computeTruth(), and computeValidity().
|
private |
Definition at line 94 of file CachingSolver.cpp.
References klee::ref< T >::compare().
Referenced by cacheInsert(), and cacheLookup().
|
inlinevirtual |
Implements klee::SolverImpl.
Definition at line 78 of file CachingSolver.cpp.
References klee::SolverImpl::computeInitialValues(), klee::Solver::impl, klee::stats::queryCacheMisses, and solver.
|
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:
Where is some assignment,
are the constraints in the query and
is the query expression.
[out] | isValid | - On success, true iff the logical formula is true. |
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.
|
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.
[out] | result | - if
|
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.
computeValue - Compute a feasible value for the expression.
The query expression is guaranteed to be non-constant.
Implements klee::SolverImpl.
Definition at line 74 of file CachingSolver.cpp.
References klee::SolverImpl::computeValue(), klee::Solver::impl, klee::stats::queryCacheMisses, and solver.
|
virtual |
Reimplemented from klee::SolverImpl.
Definition at line 248 of file CachingSolver.cpp.
References klee::SolverImpl::getConstraintLog(), klee::Solver::impl, and solver.
|
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.
|
virtual |
Reimplemented from klee::SolverImpl.
Definition at line 252 of file CachingSolver.cpp.
References klee::Solver::impl, klee::SolverImpl::setCoreSolverTimeout(), and solver.
|
private |
Definition at line 66 of file CachingSolver.cpp.
Referenced by cacheInsert(), cacheLookup(), and ~CachingSolver().
|
private |
Definition at line 65 of file CachingSolver.cpp.
Referenced by computeInitialValues(), computeTruth(), computeValidity(), computeValue(), getConstraintLog(), getOperationStatusCode(), setCoreSolverTimeout(), and ~CachingSolver().