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

Public Member Functions

 FastCexSolver ()
 
 ~FastCexSolver ()
 
IncompleteSolver::PartialValidity computeTruth (const Query &)
 
bool computeValue (const Query &, ref< Expr > &result)
 computeValue - Attempt to compute a value for the given expression. More...
 
bool computeInitialValues (const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
 
- Public Member Functions inherited from klee::IncompleteSolver
 IncompleteSolver ()
 
virtual ~IncompleteSolver ()
 
virtual
IncompleteSolver::PartialValidity 
computeValidity (const Query &)
 

Additional Inherited Members

- Public Types inherited from klee::IncompleteSolver
enum  PartialValidity {
  MustBeTrue = 1, MustBeFalse = -1, MayBeTrue = 2, MayBeFalse = -2,
  TrueOrFalse = 0, None = 3
}
 
- Static Public Member Functions inherited from klee::IncompleteSolver
static PartialValidity negatePartialValidity (PartialValidity pv)
 

Detailed Description

Definition at line 968 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

FastCexSolver::FastCexSolver ( )

Definition at line 981 of file FastCexSolver.cpp.

FastCexSolver::~FastCexSolver ( )

Definition at line 983 of file FastCexSolver.cpp.

Member Function Documentation

bool FastCexSolver::computeInitialValues ( const Query ,
const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  values,
bool &  hasSolution 
)
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.

Implements klee::IncompleteSolver.

Definition at line 1087 of file FastCexSolver.cpp.

References klee::ConstantExpr::create(), klee::ReadExpr::create(), CexData::evaluatePossible(), klee::Array::getDomain(), propogateValues(), and klee::Array::size.

Here is the call graph for this function:

IncompleteSolver::PartialValidity FastCexSolver::computeTruth ( const Query )
virtual

computeValidity - Compute a partial validity for the given query.

The passed expression is non-constant with bool type.

Implements klee::IncompleteSolver.

Definition at line 1048 of file FastCexSolver.cpp.

References klee::IncompleteSolver::MayBeFalse, klee::IncompleteSolver::MustBeTrue, klee::IncompleteSolver::None, and propogateValues().

Here is the call graph for this function:

bool FastCexSolver::computeValue ( const Query ,
ref< Expr > &  result 
)
virtual

computeValue - Attempt to compute a value for the given expression.

Implements klee::IncompleteSolver.

Definition at line 1060 of file FastCexSolver.cpp.

References CexData::evaluatePossible(), klee::Query::expr, and propogateValues().

Here is the call graph for this function:


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