klee

#include <IncompleteSolver.h>
Public Types  
enum  PartialValidity { MustBeTrue = 1, MustBeFalse = 1, MayBeTrue = 2, MayBeFalse = 2, TrueOrFalse = 0, None = 3 } 
Public Member Functions  
IncompleteSolver ()  
virtual  ~IncompleteSolver () 
virtual IncompleteSolver::PartialValidity  computeValidity (const Query &) 
virtual IncompleteSolver::PartialValidity  computeTruth (const Query &)=0 
virtual bool  computeValue (const Query &, ref< Expr > &result)=0 
computeValue  Attempt to compute a value for the given expression. More...  
virtual bool  computeInitialValues (const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)=0 
Static Public Member Functions  
static PartialValidity  negatePartialValidity (PartialValidity pv) 
IncompleteSolver  Base class for incomplete solver implementations.
Incomplete solvers are useful for implementing optimizations which may quickly compute an answer, but cannot always compute the correct answer. They can be used with the StagedSolver to provide a complete Solver implementation.
Definition at line 25 of file IncompleteSolver.h.
PartialValidity  Represent a possibility incomplete query validity.
Definition at line 29 of file IncompleteSolver.h.

inline 
Definition at line 54 of file IncompleteSolver.h.

inlinevirtual 
Definition at line 55 of file IncompleteSolver.h.

pure virtual 
computeInitialValues  Attempt to compute the constant values for the initial state of each given object. If a correct result is not found, then the values array must be unmodified.
Implemented in FastCexSolver.
Referenced by klee::StagedSolverImpl::computeInitialValues().

pure virtual 
computeValidity  Compute a partial validity for the given query.
The passed expression is nonconstant with bool type.
Implemented in FastCexSolver.
Referenced by klee::StagedSolverImpl::computeTruth().

virtual 
computeValidity  Compute a partial validity for the given query.
The passed expression is nonconstant with bool type.
The IncompleteSolver class provides an implementation of computeValidity using computeTruth. Subclasses may override this if a more efficient implementation is available.
Definition at line 32 of file IncompleteSolver.cpp.
References klee::Query::negateExpr().
Referenced by klee::StagedSolverImpl::computeValidity().

pure virtual 
computeValue  Attempt to compute a value for the given expression.
Implemented in FastCexSolver.
Referenced by klee::StagedSolverImpl::computeValue().

static 
Definition at line 20 of file IncompleteSolver.cpp.
Referenced by CachingSolver::cacheInsert(), and CachingSolver::cacheLookup().