FastCexSolver Class Reference

Inheritance diagram for FastCexSolver:

[legend]

Collaboration diagram for FastCexSolver:

[legend]

List of all members.

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

---

Detailed Description

Definition at line 742 of file FastCexSolver.cpp.

---

Constructor & Destructor Documentation

FastCexSolver::FastCexSolver

(

)

Definition at line 755 of file FastCexSolver.cpp.

FastCexSolver::~FastCexSolver

(

)

Definition at line 757 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 898 of file FastCexSolver.cpp.

References ObjectFinder::addObject(), klee::ConstraintManager::begin(), klee::Query::constraints, klee::ConstraintManager::end(), klee::Query::expr, CexData::exprMustBeValue(), CexData::fixValues(), CexData::forceExprToValue(), kMachinePointerType, CexData::objectValues, klee::Array::size, and klee::ExprVisitor::visit().

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

References klee::ConstraintManager::begin(), klee::Query::constraints, klee::ConstraintManager::end(), klee::Query::expr, CexData::exprMustBeValue(), CexData::fixValues(), CexData::forceExprToValue(), CexObjectData::size, CexObjectData::values, and klee::ExprVisitor::visit().

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

References klee::ConstraintManager::begin(), klee::Query::constraints, klee::ConstraintManager::end(), klee::Query::expr, CexData::exprMustBeValue(), CexData::fixValues(), CexData::forceExprToValue(), CexData::objectValues, and klee::ExprVisitor::visit().

Here is the call graph for this function:

---

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

• lib/Solver/FastCexSolver.cpp