CachingSolver Class Reference

Inheritance diagram for CachingSolver:

[legend]

Collaboration diagram for CachingSolver:

[legend]

List of all members.

Classes
struct	CacheEntry
struct	CacheEntryHash
Public Member Functions
	CachingSolver (Solver *s)
	~CachingSolver ()
bool	computeValidity (const Query &, Solver::Validity &result)
bool	computeTruth (const Query &, bool &isValid)
bool	computeValue (const Query &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 Types
typedef std::tr1::unordered_map < CacheEntry, IncompleteSolver::PartialValidity, CacheEntryHash >	cache_map
Private Member Functions
ref< Expr >	canonicalizeQuery (ref< Expr > originalQuery, bool &negationUsed)
void	cacheInsert (const Query &query, IncompleteSolver::PartialValidity result)
	Inserts the given query, result pair into the cache.
bool	cacheLookup (const Query &query, IncompleteSolver::PartialValidity &result)
Private Attributes
Solver *	solver
cache_map	cache

---

Detailed Description

Definition at line 24 of file CachingSolver.cpp.

---

Member Typedef Documentation

typedef std::tr1::unordered_map<CacheEntry, IncompleteSolver::PartialValidity, CacheEntryHash> CachingSolver::cache_map [private]

Definition at line 64 of file CachingSolver.cpp.

---

Constructor & Destructor Documentation

CachingSolver::CachingSolver

(

Solver *

s

)

[inline]

Definition at line 70 of file CachingSolver.cpp.

CachingSolver::~CachingSolver

(

)

[inline]

Definition at line 71 of file CachingSolver.cpp.

References cache, and solver.

---

Member Function Documentation

void CachingSolver::cacheInsert	(	const Query &	query,
		IncompleteSolver::PartialValidity	result
	)			[private]

Inserts the given query, result pair into the cache.

Definition at line 125 of file CachingSolver.cpp.

References cache, canonicalizeQuery(), klee::Query::constraints, and klee::Query::expr.

Referenced by computeTruth(), and computeValidity().

Here is the call graph for this function:

Here is the caller graph for this function:

bool CachingSolver::cacheLookup	(	const Query &	query,
		IncompleteSolver::PartialValidity &	result
	)			[private]

Returns:

true on a cache hit, false of a cache miss. Reference value result only valid on a cache hit.

Definition at line 106 of file CachingSolver.cpp.

References cache, canonicalizeQuery(), klee::Query::constraints, and klee::Query::expr.

Referenced by computeTruth(), and computeValidity().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< Expr > CachingSolver::canonicalizeQuery	(	ref< Expr >	originalQuery,
		bool &	negationUsed
	)			[private]

Returns:

the canonical version of the given query. The reference negationUsed is set to true if the original query was negated in the canonicalization process.

Definition at line 90 of file CachingSolver.cpp.

References klee::ref< T >::compare().

Referenced by cacheInsert(), and cacheLookup().

Here is the call graph for this function:

Here is the caller graph for this function:

bool CachingSolver::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 78 of file CachingSolver.cpp.

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

Here is the call graph for this function:

bool CachingSolver::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 203 of file CachingSolver.cpp.

References cacheInsert(), cacheLookup(), klee::SolverImpl::computeTruth(), klee::Solver::impl, klee::stats::queryCacheHits, klee::stats::queryCacheMisses, and solver.

Here is the call graph for this function:

bool CachingSolver::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 137 of file CachingSolver.cpp.

References cacheInsert(), cacheLookup(), klee::SolverImpl::computeTruth(), klee::SolverImpl::computeValidity(), klee::Solver::impl, klee::Query::negateExpr(), klee::stats::queryCacheHits, klee::stats::queryCacheMisses, and solver.

Here is the call graph for this function:

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

computeValue - Compute a feasible value for the expression.

The query expression is guaranteed to be non-constant.

Implements klee::SolverImpl.

Definition at line 75 of file CachingSolver.cpp.

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

Here is the call graph for this function:

---

Member Data Documentation

cache_map CachingSolver::cache [private]

Definition at line 67 of file CachingSolver.cpp.

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

Solver* CachingSolver::solver [private]

Definition at line 66 of file CachingSolver.cpp.

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

---

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

• lib/Solver/CachingSolver.cpp