#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

enum klee::IncompleteSolver::PartialValidity

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

◆ IncompleteSolver()

klee::IncompleteSolver::IncompleteSolver ( )

inline

Definition at line 54 of file IncompleteSolver.h.

◆ ~IncompleteSolver()

virtual klee::IncompleteSolver::~IncompleteSolver ( )

inlinevirtual

Definition at line 55 of file IncompleteSolver.h.

Member Function Documentation

◆ computeInitialValues()

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:

◆ computeTruth()

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(), and computeValidity().

Here is the caller graph for this function:

◆ computeValidity()

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 computeTruth(), MayBeFalse, MayBeTrue, MustBeFalse, MustBeTrue, klee::Query::negateExpr(), None, and TrueOrFalse.

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

Here is the call graph for this function: