klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::StagedSolverImpl Class Reference

#include <IncompleteSolver.h>

Inheritance diagram for klee::StagedSolverImpl:
Collaboration diagram for klee::StagedSolverImpl:

Public Member Functions

 StagedSolverImpl (IncompleteSolver *_primary, Solver *_secondary)
 
 ~StagedSolverImpl ()
 
bool computeTruth (const Query &, bool &isValid)
 
bool computeValidity (const Query &, Solver::Validity &result)
 
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 (double timeout)
 
- Public Member Functions inherited from klee::SolverImpl
 SolverImpl ()
 
virtual ~SolverImpl ()
 

Private Attributes

IncompleteSolverprimary
 
Solversecondary
 

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

StagedSolver - Adapter class for staging an incomplete solver with a complete secondary solver, to form an (optimized) complete solver.

Definition at line 88 of file IncompleteSolver.h.

Constructor & Destructor Documentation

StagedSolverImpl::StagedSolverImpl ( IncompleteSolver _primary,
Solver _secondary 
)

Definition at line 61 of file IncompleteSolver.cpp.

StagedSolverImpl::~StagedSolverImpl ( )

Definition at line 67 of file IncompleteSolver.cpp.

References primary, and secondary.

Member Function Documentation

bool StagedSolverImpl::computeInitialValues ( const Query query,
const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  values,
bool &  hasSolution 
)
virtual
bool StagedSolverImpl::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 72 of file IncompleteSolver.cpp.

References klee::IncompleteSolver::computeTruth(), klee::SolverImpl::computeTruth(), klee::Solver::impl, klee::IncompleteSolver::MustBeTrue, klee::IncompleteSolver::None, primary, and secondary.

Here is the call graph for this function:

bool StagedSolverImpl::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 83 of file IncompleteSolver.cpp.

References klee::SolverImpl::computeTruth(), klee::SolverImpl::computeValidity(), klee::IncompleteSolver::computeValidity(), klee::Solver::False, klee::Solver::impl, klee::IncompleteSolver::MayBeFalse, klee::IncompleteSolver::MayBeTrue, klee::IncompleteSolver::MustBeFalse, klee::IncompleteSolver::MustBeTrue, klee::Query::negateExpr(), primary, secondary, klee::Solver::True, klee::IncompleteSolver::TrueOrFalse, and klee::Solver::Unknown.

Here is the call graph for this function:

bool StagedSolverImpl::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 116 of file IncompleteSolver.cpp.

References klee::IncompleteSolver::computeValue(), klee::SolverImpl::computeValue(), klee::Solver::impl, primary, and secondary.

Here is the call graph for this function:

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

Reimplemented from klee::SolverImpl.

Definition at line 142 of file IncompleteSolver.cpp.

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

Here is the call graph for this function:

SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode ( )
virtual

getOperationStatusCode - get the status of the last solver operation

Implements klee::SolverImpl.

Definition at line 138 of file IncompleteSolver.cpp.

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

Here is the call graph for this function:

void StagedSolverImpl::setCoreSolverTimeout ( double  timeout)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 146 of file IncompleteSolver.cpp.

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

Here is the call graph for this function:

Member Data Documentation

IncompleteSolver* klee::StagedSolverImpl::primary
private

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