Inheritance diagram for CexCachingSolver:

Collaboration diagram for CexCachingSolver:

[legend]

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)

SolverRunStatus	getOperationStatusCode ()
	getOperationStatusCode - get the status of the last solver operation More...

char *	getConstraintLog (const Query &query)

void	setCoreSolverTimeout (time::Span timeout)

Public Member Functions inherited from klee::SolverImpl
	SolverImpl ()

virtual	~SolverImpl ()

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

virtual bool	computeTruth (const Query &query, bool &isValid)=0

virtual bool	computeValue (const Query &query, ref< Expr > &result)=0

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

virtual SolverRunStatus	getOperationStatusCode ()=0
	getOperationStatusCode - get the status of the last solver operation More...

virtual char *	getConstraintLog (const Query &query)

virtual void	setCoreSolverTimeout (time::Span timeout)

Private Types
typedef std::set< Assignment *, AssignmentLessThan >	assignmentsTable_ty

Private Member Functions
bool	searchForAssignment (KeyType &key, Assignment *&result)

bool	lookupAssignment (const Query &query, 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

Additional Inherited Members
Public Types inherited from klee::SolverImpl
enum	SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE , SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE , SOLVER_RUN_STATUS_FAILURE , SOLVER_RUN_STATUS_TIMEOUT , SOLVER_RUN_STATUS_FORK_FAILED , SOLVER_RUN_STATUS_INTERRUPTED , SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE , SOLVER_RUN_STATUS_WAITPID_FAILED }

Static Public Member Functions inherited from klee::SolverImpl
static const char *	getOperationStatusString (SolverRunStatus statusCode)

Detailed Description

Definition at line 66 of file CexCachingSolver.cpp.

Member Typedef Documentation

◆ assignmentsTable_ty

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

private

Definition at line 67 of file CexCachingSolver.cpp.

Constructor & Destructor Documentation

◆ CexCachingSolver()

CexCachingSolver::CexCachingSolver ( Solver * _solver )

inline

Definition at line 88 of file CexCachingSolver.cpp.

◆ ~CexCachingSolver()

CexCachingSolver::~CexCachingSolver ( )

Definition at line 266 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

◆ computeInitialValues()

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

virtual

See also: Solver::getInitialValues()

Implements klee::SolverImpl.

Definition at line 340 of file CexCachingSolver.cpp.

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

Here is the call graph for this function:

◆ computeTruth()

bool CexCachingSolver::computeTruth	(	const Query &	query,
		bool &	isValid
	)

virtual

computeTruth - Determine whether the given query expression is provably true given the constraints.

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

This method should evaluate the logical formula:

$\forall X constraints(X) \to query(X)$

Where is some assignment, are the constraints in the query and is the query expression.

Parameters

[out] isValid - On success, true iff the logical formula is true.

Returns: True on success

Implements klee::SolverImpl.

Definition at line 298 of file CexCachingSolver.cpp.

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

Here is the call graph for this function:

◆ computeValidity()

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.

Parameters

[out]

result

- if

$\forall X constraints(X) \to query(X)$

then Solver::True, else if

$\forall X constraints(X) \to \lnot query(X)$

then Solver::False, else Solver::Unknown

Returns: True on success

Reimplemented from klee::SolverImpl.

Definition at line 274 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:

◆ computeValue()

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.

Returns: True on success

Implements klee::SolverImpl.

Definition at line 325 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:

◆ getAssignment()

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

private

Definition at line 222 of file CexCachingSolver.cpp.

References assignmentsTable, cache, klee::SolverImpl::computeInitialValues(), klee::Assignment::dump(), klee::Query::dump(), klee::findSymbolicObjects(), klee::Solver::impl, klee::MapOfSets< K, V >::insert(), klee::klee_error(), lookupAssignment(), klee::Assignment::satisfies(), 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:

◆ getConstraintLog()

char * CexCachingSolver::getConstraintLog ( const Query & query )

virtual

Reimplemented from klee::SolverImpl.

Definition at line 376 of file CexCachingSolver.cpp.

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

Here is the call graph for this function:

◆ getOperationStatusCode()

SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode ( )

virtual

getOperationStatusCode - get the status of the last solver operation

Implements klee::SolverImpl.

Definition at line 372 of file CexCachingSolver.cpp.

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

Here is the call graph for this function:

◆ lookupAssignment() [1/2]

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

inlineprivate

Definition at line 80 of file CexCachingSolver.cpp.

References lookupAssignment().

Here is the call graph for this function:

◆ lookupAssignment() [2/2]

bool CexCachingSolver::lookupAssignment	(	const Query &	query,
		KeyType &	key,
		Assignment *&	result
	)

private

lookupAssignment - Lookup a cached result for the given

query.

Parameters

query	- The query to lookup.
key	[out] - On return, the key constructed for the query.
result	[out] - The cached result, if the lookup is successful. This is either a satisfying assignment (for a satisfiable query), or 0 (for an unsatisfiable query).

Returns: True if a cached result was found.

Definition at line 199 of file CexCachingSolver.cpp.

References klee::ConstraintSet::begin(), klee::Query::constraints, klee::ConstraintSet::end(), klee::Query::expr, klee::stats::queryCexCacheHits, klee::stats::queryCexCacheMisses, and searchForAssignment().

Referenced by computeTruth(), getAssignment(), and lookupAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ searchForAssignment()

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

private

searchForAssignment - Look for a cached solution for a query.

Parameters

key	- The query to look up.
result	[out] - The cached result, if the lookup is successful. This is either a satisfying assignment (for a satisfiable query), or 0 (for an unsatisfiable query).

Returns: - True if a cached result was found.

Definition at line 130 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 lookupAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setCoreSolverTimeout()

void CexCachingSolver::setCoreSolverTimeout ( time::Span timeout )

virtual

Reimplemented from klee::SolverImpl.

Definition at line 380 of file CexCachingSolver.cpp.

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

Here is the call graph for this function:

Member Data Documentation

◆ assignmentsTable

assignmentsTable_ty CexCachingSolver::assignmentsTable

private

Definition at line 73 of file CexCachingSolver.cpp.

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

◆ cache

MapOfSets<ref<Expr>, Assignment*> CexCachingSolver::cache

private

Definition at line 71 of file CexCachingSolver.cpp.

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

◆ solver

Solver* CexCachingSolver::solver

private

Definition at line 69 of file CexCachingSolver.cpp.

Referenced by getAssignment(), getConstraintLog(), getOperationStatusCode(), setCoreSolverTimeout(), and ~CexCachingSolver().

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

/Users/cristic/klee/lib/Solver/CexCachingSolver.cpp

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ assignmentsTable_ty

Constructor & Destructor Documentation

◆ CexCachingSolver()

◆ ~CexCachingSolver()

Member Function Documentation

◆ computeInitialValues()

◆ computeTruth()

◆ computeValidity()

◆ computeValue()

◆ getAssignment()

◆ getConstraintLog()

◆ getOperationStatusCode()

◆ lookupAssignment() [1/2]

◆ lookupAssignment() [2/2]

◆ searchForAssignment()

◆ setCoreSolverTimeout()

Member Data Documentation

◆ assignmentsTable

◆ cache

◆ solver