CexCachingSolver Class Reference

Inheritance diagram for CexCachingSolver:

[legend]

Collaboration diagram for CexCachingSolver:

[legend]

List of all members.

Public Member Functions
	CexCachingSolver (Solver *_solver)
	~CexCachingSolver ()
bool	computeTruth (const Query &, bool &isValid)
bool	computeValidity (const Query &, Solver::Validity &result)
bool	computeValue (const Query &, ref< Expr > &result)
bool	computeInitialValues (const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
Private Types
typedef std::set< Assignment *, AssignmentLessThan >	assignmentsTable_ty
Private Member Functions
bool	searchForAssignment (KeyType &key, Assignment *&result)
bool	lookupAssignment (const Query &query, Assignment *&result)
bool	getAssignment (const Query &query, Assignment *&result)
Private Attributes
Solver *	solver
MapOfSets< ref< Expr > , Assignment * >	cache
assignmentsTable_ty	assignmentsTable

---

Detailed Description

Definition at line 53 of file CexCachingSolver.cpp.

---

Member Typedef Documentation

typedef std::set<Assignment*, AssignmentLessThan> CexCachingSolver::assignmentsTable_ty [private]

Definition at line 54 of file CexCachingSolver.cpp.

---

Constructor & Destructor Documentation

CexCachingSolver::CexCachingSolver

(

Solver *

_solver

)

[inline]

Definition at line 70 of file CexCachingSolver.cpp.

CexCachingSolver::~CexCachingSolver

(

)

Definition at line 204 of file CexCachingSolver.cpp.

References assignmentsTable, cache, klee::MapOfSets< K, V >::clear(), and solver.

Here is the call graph for this function:

---

Member Function Documentation

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

Implements klee::SolverImpl.

Definition at line 278 of file CexCachingSolver.cpp.

References klee::Assignment::bindings, klee::stats::cexCacheTime, getAssignment(), and klee::Array::size.

Here is the call graph for this function:

bool CexCachingSolver::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 236 of file CexCachingSolver.cpp.

References klee::stats::cexCacheTime, getAssignment(), lookupAssignment(), and klee::Query::negateExpr().

Here is the call graph for this function:

bool CexCachingSolver::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 212 of file CexCachingSolver.cpp.

References klee::stats::cexCacheTime, klee::Assignment::evaluate(), klee::Query::expr, getAssignment(), klee::Query::negateExpr(), and klee::Query::withFalse().

Here is the call graph for this function:

bool CexCachingSolver::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 263 of file CexCachingSolver.cpp.

References klee::stats::cexCacheTime, klee::Assignment::evaluate(), klee::Query::expr, getAssignment(), and klee::Query::withFalse().

Here is the call graph for this function:

bool CexCachingSolver::getAssignment	(	const Query &	query,
		Assignment *&	result
	)			[private]

Definition at line 153 of file CexCachingSolver.cpp.

References assignmentsTable, klee::ConstraintManager::begin(), cache, klee::SolverImpl::computeInitialValues(), klee::Query::constraints, klee::ConstraintManager::end(), klee::Query::expr, klee::findSymbolicObjects(), klee::Solver::impl, klee::MapOfSets< K, V >::insert(), klee::Assignment::satisfies(), searchForAssignment(), and solver.

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

Here is the call graph for this function:

Here is the caller graph for this function:

bool CexCachingSolver::lookupAssignment	(	const Query &	query,
		Assignment *&	result
	)			[private]

Definition at line 137 of file CexCachingSolver.cpp.

References klee::ConstraintManager::begin(), klee::Query::constraints, klee::ConstraintManager::end(), klee::Query::expr, and searchForAssignment().

Referenced by computeTruth().

Here is the call graph for this function:

Here is the caller graph for this function:

bool CexCachingSolver::searchForAssignment	(	KeyType &	key,
		Assignment *&	result
	)			[private]

Definition at line 102 of file CexCachingSolver.cpp.

References assignmentsTable, cache, klee::MapOfSets< K, V >::findSubset(), klee::MapOfSets< K, V >::findSuperset(), klee::MapOfSets< K, V >::lookup(), and klee::Assignment::satisfies().

Referenced by getAssignment(), and lookupAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

---

Member Data Documentation

assignmentsTable_ty CexCachingSolver::assignmentsTable [private]

Definition at line 60 of file CexCachingSolver.cpp.

Referenced by getAssignment(), searchForAssignment(), and ~CexCachingSolver().

MapOfSets<ref<Expr>, Assignment*> CexCachingSolver::cache [private]

Definition at line 58 of file CexCachingSolver.cpp.

Referenced by getAssignment(), searchForAssignment(), and ~CexCachingSolver().

Solver* CexCachingSolver::solver [private]

Definition at line 56 of file CexCachingSolver.cpp.

Referenced by getAssignment(), and ~CexCachingSolver().

---

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

• lib/Solver/CexCachingSolver.cpp