IndependentSolver Class Reference

Inheritance diagram for IndependentSolver:

[legend]

Collaboration diagram for IndependentSolver:

[legend]

List of all members.

Public Member Functions
	IndependentSolver (Solver *_solver)
	~IndependentSolver ()
bool	computeTruth (const Query &, bool &isValid)
bool	computeValidity (const Query &, Solver::Validity &result)
bool	computeValue (const Query &, ref< Expr > &result)
bool	computeInitialValues (const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
Private Attributes
Solver *	solver

---

Detailed Description

Definition at line 264 of file IndependentSolver.cpp.

---

Constructor & Destructor Documentation

IndependentSolver::IndependentSolver

(

Solver *

_solver

)

[inline]

Definition at line 269 of file IndependentSolver.cpp.

IndependentSolver::~IndependentSolver

(

)

[inline]

Definition at line 271 of file IndependentSolver.cpp.

References solver.

---

Member Function Documentation

bool IndependentSolver::computeInitialValues	(	const Query &	query,
		const std::vector< const Array * > &	objects,
		std::vector< std::vector< unsigned char > > &	values,
		bool &	hasSolution
	)			[inline, virtual]

Implements klee::SolverImpl.

Definition at line 276 of file IndependentSolver.cpp.

References klee::SolverImpl::computeInitialValues(), klee::Solver::impl, and solver.

Here is the call graph for this function:

bool IndependentSolver::computeTruth	(	const Query &	query,
		bool &	isValid
	)			[virtual]

computeTruth - Determine whether the given query is provable.

The query expression is guaranteed to be non-constant and have bool type.

Implements klee::SolverImpl.

Definition at line 295 of file IndependentSolver.cpp.

References klee::SolverImpl::computeTruth(), klee::Query::expr, getIndependentConstraints(), klee::Solver::impl, and solver.

Here is the call graph for this function:

bool IndependentSolver::computeValidity	(	const Query &	query,
		Solver::Validity &	result
	)			[virtual]

computeValidity - Compute a full validity result for the query.

The query expression is guaranteed to be non-constant and have bool type.

SolverImpl provides a default implementation which uses computeTruth. Clients should override this if a more efficient implementation is available.

Reimplemented from klee::SolverImpl.

Definition at line 285 of file IndependentSolver.cpp.

References klee::SolverImpl::computeValidity(), klee::Query::expr, getIndependentConstraints(), klee::Solver::impl, and solver.

Here is the call graph for this function:

bool IndependentSolver::computeValue	(	const Query &	query,
		ref< Expr > &	result
	)			[virtual]

computeValue - Compute a feasible value for the expression.

The query expression is guaranteed to be non-constant.

Implements klee::SolverImpl.

Definition at line 304 of file IndependentSolver.cpp.

References klee::SolverImpl::computeValue(), klee::Query::expr, getIndependentConstraints(), klee::Solver::impl, and solver.

Here is the call graph for this function:

---

Member Data Documentation

Solver* IndependentSolver::solver [private]

Definition at line 266 of file IndependentSolver.cpp.

Referenced by computeInitialValues(), computeTruth(), computeValidity(), computeValue(), and ~IndependentSolver().

---

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

• lib/Solver/IndependentSolver.cpp