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

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)
 
- 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 Attributes

Solver * solver
 
Solver * oracle
 

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 18 of file ValidatingSolver.cpp.

Constructor & Destructor Documentation

◆ ValidatingSolver()

klee::ValidatingSolver::ValidatingSolver ( Solver *  _solver,
Solver *  _oracle 
)
inline

Definition at line 23 of file ValidatingSolver.cpp.

◆ ~ValidatingSolver()

klee::ValidatingSolver::~ValidatingSolver ( )
inline

Definition at line 25 of file ValidatingSolver.cpp.

References solver.

Member Function Documentation

◆ computeInitialValues()

bool klee::ValidatingSolver::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 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.

Here is the call graph for this function:

◆ computeTruth()

bool klee::ValidatingSolver::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 39 of file ValidatingSolver.cpp.

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

Here is the call graph for this function:

◆ computeValidity()

bool klee::ValidatingSolver::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 53 of file ValidatingSolver.cpp.

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

Here is the call graph for this function:

◆ computeValue()

bool klee::ValidatingSolver::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 68 of file ValidatingSolver.cpp.

References klee::SolverImpl::computeTruth(), klee::SolverImpl::computeValue(), klee::Query::expr, klee::Solver::impl, oracle, solver, and klee::Query::withExpr().

Here is the call graph for this function:

◆ getConstraintLog()

char * klee::ValidatingSolver::getConstraintLog ( const Query &  query)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 131 of file ValidatingSolver.cpp.

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

Here is the call graph for this function:

◆ getOperationStatusCode()

SolverImpl::SolverRunStatus klee::ValidatingSolver::getOperationStatusCode ( )
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.

Here is the call graph for this function:

◆ setCoreSolverTimeout()

void klee::ValidatingSolver::setCoreSolverTimeout ( time::Span  timeout)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 135 of file ValidatingSolver.cpp.

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

Here is the call graph for this function:

Member Data Documentation

◆ oracle

Solver * klee::ValidatingSolver::oracle
private

Definition at line 20 of file ValidatingSolver.cpp.

Referenced by computeInitialValues(), computeTruth(), computeValidity(), and computeValue().

◆ solver

Solver* klee::ValidatingSolver::solver
private

Definition at line 20 of file ValidatingSolver.cpp.

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

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