klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
STPSolverImpl Class Reference
Inheritance diagram for STPSolverImpl:
Collaboration diagram for STPSolverImpl:

Public Member Functions

 STPSolverImpl (bool _useForkedSTP, bool _optimizeDivides=true)
 
 ~STPSolverImpl ()
 
char * getConstraintLog (const Query &)
 
void setCoreSolverTimeout (double _timeout)
 
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...
 
- Public Member Functions inherited from klee::SolverImpl
 SolverImpl ()
 
virtual ~SolverImpl ()
 
virtual bool computeValidity (const Query &query, Solver::Validity &result)
 

Private Attributes

VC vc
 
STPBuilderbuilder
 
double timeout
 
bool useForkedSTP
 
SolverRunStatus runStatusCode
 

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 495 of file Solver.cpp.

Constructor & Destructor Documentation

STPSolverImpl::STPSolverImpl ( bool  _useForkedSTP,
bool  _optimizeDivides = true 
)

Definition at line 528 of file Solver.cpp.

References builder, shared_memory_id, shared_memory_ptr, shared_memory_size, stp_error_handler(), useForkedSTP, and vc.

Here is the call graph for this function:

STPSolverImpl::~STPSolverImpl ( )

Definition at line 557 of file Solver.cpp.

References builder, and vc.

Member Function Documentation

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

bool STPSolverImpl::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 610 of file Solver.cpp.

References klee::Assignment::evaluate(), klee::Query::expr, klee::findSymbolicObjects(), and klee::Query::withFalse().

Here is the call graph for this function:

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

Reimplemented from klee::SolverImpl.

Definition at line 580 of file Solver.cpp.

References klee::ConstantExpr::alloc(), klee::ConstraintManager::begin(), klee::Expr::Bool, klee::Query::constraints, klee::ConstraintManager::end(), and klee::Query::expr.

Here is the call graph for this function:

SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode ( )
virtual

getOperationStatusCode - get the status of the last solver operation

Implements klee::SolverImpl.

Definition at line 826 of file Solver.cpp.

void STPSolverImpl::setCoreSolverTimeout ( double  _timeout)
inlinevirtual

Reimplemented from klee::SolverImpl.

Definition at line 508 of file Solver.cpp.

Member Data Documentation

STPBuilder* STPSolverImpl::builder
private

Definition at line 498 of file Solver.cpp.

Referenced by STPSolverImpl(), and ~STPSolverImpl().

SolverRunStatus STPSolverImpl::runStatusCode
private

Definition at line 501 of file Solver.cpp.

double STPSolverImpl::timeout
private

Definition at line 499 of file Solver.cpp.

bool STPSolverImpl::useForkedSTP
private

Definition at line 500 of file Solver.cpp.

Referenced by STPSolverImpl().

VC STPSolverImpl::vc
private

Definition at line 497 of file Solver.cpp.

Referenced by STPSolverImpl(), and ~STPSolverImpl().


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