klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::IncompleteSolver Class Referenceabstract

#include <IncompleteSolver.h>

Inheritance diagram for klee::IncompleteSolver:

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)
 

Detailed Description

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.

Member Enumeration Documentation

PartialValidity - Represent a possibility incomplete query validity.

Enumerator
MustBeTrue 

The query is provably true.

MustBeFalse 

The query is provably false.

MayBeTrue 

The query is not provably false (a true assignment is known to exist).

MayBeFalse 

The query is not provably true (a false assignment is known to exist).

TrueOrFalse 

The query is known to have both true and false assignments.

None 

The validity of the query is unknown.

Definition at line 29 of file IncompleteSolver.h.

Constructor & Destructor Documentation

klee::IncompleteSolver::IncompleteSolver ( )
inline

Definition at line 54 of file IncompleteSolver.h.

virtual klee::IncompleteSolver::~IncompleteSolver ( )
inlinevirtual

Definition at line 55 of file IncompleteSolver.h.

Member Function Documentation

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

Here is the caller graph for this function:

virtual IncompleteSolver::PartialValidity klee::IncompleteSolver::computeTruth ( const Query )
pure virtual

computeValidity - Compute a partial validity for the given query.

The passed expression is non-constant with bool type.

Implemented in FastCexSolver.

Referenced by klee::StagedSolverImpl::computeTruth().

Here is the caller graph for this function:

IncompleteSolver::PartialValidity IncompleteSolver::computeValidity ( const Query query)
virtual

computeValidity - Compute a partial validity for the given query.

The passed expression is non-constant with bool type.

The IncompleteSolver class provides an implementation of computeValidity using computeTruth. Sub-classes 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().

Here is the call graph for this function:

Here is the caller graph for this function:

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

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

Implemented in FastCexSolver.

Referenced by klee::StagedSolverImpl::computeValue().

Here is the caller graph for this function:

IncompleteSolver::PartialValidity IncompleteSolver::negatePartialValidity ( PartialValidity  pv)
static

Definition at line 20 of file IncompleteSolver.cpp.

Referenced by CachingSolver::cacheInsert(), and CachingSolver::cacheLookup().

Here is the caller graph for this function:


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