klee
Public Member Functions | List of all members
FastCexSolver Class Reference
Inheritance diagram for FastCexSolver:
Inheritance graph
[legend]
Collaboration diagram for FastCexSolver:
Collaboration graph
[legend]

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 &)
 
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
 

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 977 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

◆ FastCexSolver()

FastCexSolver::FastCexSolver ( )

Definition at line 990 of file FastCexSolver.cpp.

◆ ~FastCexSolver()

FastCexSolver::~FastCexSolver ( )

Definition at line 992 of file FastCexSolver.cpp.

Member Function Documentation

◆ computeInitialValues()

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 1094 of file FastCexSolver.cpp.

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

Here is the call graph for this function:

◆ computeTruth()

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 1055 of file FastCexSolver.cpp.

References propogateValues().

Here is the call graph for this function:

◆ computeValue()

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 1067 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: