klee
Public Types | Public Member Functions | Static Public Member Functions | Private Member Functions | List of all members
klee::SolverImpl Class Referenceabstract

SolverImpl - Abstract base clase for solver implementations. More...

#include <SolverImpl.h>

Inheritance diagram for klee::SolverImpl:
Inheritance graph
[legend]

Public Types

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
}
 

Public Member Functions

 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)
 

Static Public Member Functions

static const char * getOperationStatusString (SolverRunStatus statusCode)
 

Private Member Functions

 SolverImpl (const SolverImpl &)
 
void operator= (const SolverImpl &)
 

Detailed Description

SolverImpl - Abstract base clase for solver implementations.

Definition at line 25 of file SolverImpl.h.

Member Enumeration Documentation

◆ SolverRunStatus

enum klee::SolverImpl::SolverRunStatus
Enumerator
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 

Definition at line 34 of file SolverImpl.h.

Constructor & Destructor Documentation

◆ SolverImpl() [1/2]

klee::SolverImpl::SolverImpl ( const SolverImpl &  )
private

◆ SolverImpl() [2/2]

klee::SolverImpl::SolverImpl ( )
inline

Definition at line 31 of file SolverImpl.h.

◆ ~SolverImpl()

SolverImpl::~SolverImpl ( )
virtual

Definition at line 15 of file SolverImpl.cpp.

Member Function Documentation

◆ computeInitialValues()

virtual bool klee::SolverImpl::computeInitialValues ( const Query &  query,
const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  values,
bool &  hasSolution 
)
pure virtual
See also
Solver::getInitialValues()

Implemented in klee::StagedSolverImpl, klee::AssignmentValidatingSolver, CexCachingSolver, klee::DummySolverImpl, klee::ValidatingSolver, CachingSolver, IndependentSolver, and QueryLoggingSolver.

Referenced by klee::StagedSolverImpl::computeInitialValues(), klee::AssignmentValidatingSolver::computeInitialValues(), klee::ValidatingSolver::computeInitialValues(), CachingSolver::computeInitialValues(), IndependentSolver::computeInitialValues(), QueryLoggingSolver::computeInitialValues(), CexCachingSolver::getAssignment(), and klee::Solver::getInitialValues().

Here is the caller graph for this function:

◆ computeTruth()

virtual bool klee::SolverImpl::computeTruth ( const Query &  query,
bool &  isValid 
)
pure 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

Implemented in klee::StagedSolverImpl, klee::AssignmentValidatingSolver, CachingSolver, CexCachingSolver, klee::DummySolverImpl, IndependentSolver, klee::ValidatingSolver, and QueryLoggingSolver.

Referenced by klee::ValidatingSolver::computeInitialValues(), klee::StagedSolverImpl::computeTruth(), klee::AssignmentValidatingSolver::computeTruth(), CachingSolver::computeTruth(), IndependentSolver::computeTruth(), klee::ValidatingSolver::computeTruth(), QueryLoggingSolver::computeTruth(), klee::StagedSolverImpl::computeValidity(), CachingSolver::computeValidity(), computeValidity(), klee::ValidatingSolver::computeValue(), and klee::Solver::mustBeTrue().

Here is the caller graph for this function:

◆ computeValidity()

bool SolverImpl::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 in klee::StagedSolverImpl, klee::AssignmentValidatingSolver, CachingSolver, CexCachingSolver, klee::DummySolverImpl, IndependentSolver, klee::ValidatingSolver, and QueryLoggingSolver.

Definition at line 17 of file SolverImpl.cpp.

References computeTruth(), klee::Solver::False, klee::Query::negateExpr(), klee::Solver::True, and klee::Solver::Unknown.

Referenced by klee::StagedSolverImpl::computeValidity(), klee::AssignmentValidatingSolver::computeValidity(), CachingSolver::computeValidity(), IndependentSolver::computeValidity(), klee::ValidatingSolver::computeValidity(), QueryLoggingSolver::computeValidity(), and klee::Solver::evaluate().

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

◆ computeValue()

virtual bool klee::SolverImpl::computeValue ( const Query &  query,
ref< Expr > &  result 
)
pure virtual

computeValue - Compute a feasible value for the expression.

The query expression is guaranteed to be non-constant.

Returns
True on success

Implemented in klee::StagedSolverImpl, klee::AssignmentValidatingSolver, CexCachingSolver, klee::DummySolverImpl, IndependentSolver, klee::ValidatingSolver, CachingSolver, and QueryLoggingSolver.

Referenced by klee::StagedSolverImpl::computeValue(), klee::AssignmentValidatingSolver::computeValue(), IndependentSolver::computeValue(), klee::ValidatingSolver::computeValue(), CachingSolver::computeValue(), QueryLoggingSolver::computeValue(), and klee::Solver::getValue().

Here is the caller graph for this function:

◆ getConstraintLog()

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

Reimplemented in klee::StagedSolverImpl, klee::AssignmentValidatingSolver, CachingSolver, IndependentSolver, QueryLoggingSolver, klee::ValidatingSolver, and CexCachingSolver.

Definition at line 104 of file SolverImpl.h.

Referenced by klee::StagedSolverImpl::getConstraintLog(), klee::AssignmentValidatingSolver::getConstraintLog(), CachingSolver::getConstraintLog(), IndependentSolver::getConstraintLog(), QueryLoggingSolver::getConstraintLog(), klee::ValidatingSolver::getConstraintLog(), klee::Solver::getConstraintLog(), and CexCachingSolver::getConstraintLog().

Here is the caller graph for this function:

◆ getOperationStatusCode()

virtual SolverRunStatus klee::SolverImpl::getOperationStatusCode ( )
pure virtual

getOperationStatusCode - get the status of the last solver operation

Implemented in klee::StagedSolverImpl, klee::AssignmentValidatingSolver, CachingSolver, CexCachingSolver, klee::DummySolverImpl, IndependentSolver, QueryLoggingSolver, and klee::ValidatingSolver.

Referenced by EvaluateInputAST(), QueryLoggingSolver::finishQuery(), QueryLoggingSolver::flushBuffer(), klee::StagedSolverImpl::getOperationStatusCode(), klee::AssignmentValidatingSolver::getOperationStatusCode(), CachingSolver::getOperationStatusCode(), CexCachingSolver::getOperationStatusCode(), IndependentSolver::getOperationStatusCode(), QueryLoggingSolver::getOperationStatusCode(), and klee::ValidatingSolver::getOperationStatusCode().

Here is the caller graph for this function:

◆ getOperationStatusString()

const char * SolverImpl::getOperationStatusString ( SolverRunStatus  statusCode)
static

getOperationStatusString - get string representation of the operation status code

Definition at line 31 of file SolverImpl.cpp.

References SOLVER_RUN_STATUS_FAILURE, SOLVER_RUN_STATUS_FORK_FAILED, SOLVER_RUN_STATUS_INTERRUPTED, SOLVER_RUN_STATUS_SUCCESS_SOLVABLE, SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE, SOLVER_RUN_STATUS_TIMEOUT, SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE, and SOLVER_RUN_STATUS_WAITPID_FAILED.

◆ operator=()

void klee::SolverImpl::operator= ( const SolverImpl &  )
private

◆ setCoreSolverTimeout()

virtual void klee::SolverImpl::setCoreSolverTimeout ( time::Span  timeout)
inlinevirtual

Reimplemented in klee::StagedSolverImpl, klee::AssignmentValidatingSolver, CachingSolver, CexCachingSolver, IndependentSolver, QueryLoggingSolver, and klee::ValidatingSolver.

Definition at line 109 of file SolverImpl.h.

Referenced by klee::StagedSolverImpl::setCoreSolverTimeout(), klee::Solver::setCoreSolverTimeout(), klee::AssignmentValidatingSolver::setCoreSolverTimeout(), CachingSolver::setCoreSolverTimeout(), CexCachingSolver::setCoreSolverTimeout(), IndependentSolver::setCoreSolverTimeout(), QueryLoggingSolver::setCoreSolverTimeout(), and klee::ValidatingSolver::setCoreSolverTimeout().

Here is the caller graph for this function:
The documentation for this class was generated from the following files: