klee
|
Public Member Functions | |
ValidatingSolver (Solver *_solver, Solver *_oracle) | |
~ValidatingSolver () | |
bool | computeValidity (const Query &, Solver::Validity &result) |
bool | computeTruth (const Query &, bool &isValid) |
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 &) |
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 Attributes | |
Solver * | solver |
Solver * | oracle |
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 18 of file ValidatingSolver.cpp.
Definition at line 23 of file ValidatingSolver.cpp.
|
inline |
Definition at line 25 of file ValidatingSolver.cpp.
References solver.
|
virtual |
Implements klee::SolverImpl.
Definition at line 85 of file ValidatingSolver.cpp.
References klee::ConstantExpr::alloc(), klee::SolverImpl::computeInitialValues(), klee::SolverImpl::computeTruth(), klee::Query::constraints, klee::ReadExpr::create(), klee::Expr::createIsZero(), klee::Query::expr, klee::Array::getDomain(), klee::Array::getRange(), klee::Solver::impl, oracle, klee::ConstraintSet::push_back(), klee::Array::size, 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 39 of file ValidatingSolver.cpp.
References klee::SolverImpl::computeTruth(), klee::Solver::impl, oracle, 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 53 of file ValidatingSolver.cpp.
References klee::SolverImpl::computeValidity(), klee::Solver::impl, oracle, 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 68 of file ValidatingSolver.cpp.
References klee::SolverImpl::computeTruth(), klee::SolverImpl::computeValue(), klee::Query::expr, klee::Solver::impl, oracle, solver, and klee::Query::withExpr().
|
virtual |
Reimplemented from klee::SolverImpl.
Definition at line 131 of file ValidatingSolver.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 127 of file ValidatingSolver.cpp.
References klee::SolverImpl::getOperationStatusCode(), klee::Solver::impl, and solver.
|
virtual |
Reimplemented from klee::SolverImpl.
Definition at line 135 of file ValidatingSolver.cpp.
References klee::Solver::impl, klee::SolverImpl::setCoreSolverTimeout(), and solver.
|
private |
Definition at line 20 of file ValidatingSolver.cpp.
Referenced by computeInitialValues(), computeTruth(), computeValidity(), and computeValue().
|
private |
Definition at line 20 of file ValidatingSolver.cpp.
Referenced by computeInitialValues(), computeTruth(), computeValidity(), computeValue(), getConstraintLog(), getOperationStatusCode(), setCoreSolverTimeout(), and ~ValidatingSolver().