klee
Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | Private Member Functions | List of all members
klee::Solver Class Reference

#include <Solver.h>

Inheritance diagram for klee::Solver:
Inheritance graph
[legend]
Collaboration diagram for klee::Solver:
Collaboration graph
[legend]

Public Types

enum  Validity { True = 1 , False = -1 , Unknown = 0 }
 

Public Member Functions

 Solver (SolverImpl *_impl)
 
virtual ~Solver ()
 
bool evaluate (const Query &, Validity &result)
 
bool mustBeTrue (const Query &, bool &result)
 
bool mustBeFalse (const Query &, bool &result)
 
bool mayBeTrue (const Query &, bool &result)
 
bool mayBeFalse (const Query &, bool &result)
 
bool getValue (const Query &, ref< ConstantExpr > &result)
 
bool getInitialValues (const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)
 
virtual std::pair< ref< Expr >, ref< Expr > > getRange (const Query &)
 
virtual char * getConstraintLog (const Query &query)
 
virtual void setCoreSolverTimeout (time::Span timeout)
 

Static Public Member Functions

static const char * validity_to_str (Validity v)
 validity_to_str - Return the name of given Validity enum value. More...
 

Public Attributes

SolverImpl * impl
 

Private Member Functions

 Solver (const Solver &)
 
void operator= (const Solver &)
 

Detailed Description

Definition at line 60 of file Solver.h.

Member Enumeration Documentation

◆ Validity

enum klee::Solver::Validity
Enumerator
True 
False 
Unknown 

Definition at line 66 of file Solver.h.

Constructor & Destructor Documentation

◆ Solver() [1/2]

klee::Solver::Solver ( const Solver &  )
private

◆ Solver() [2/2]

klee::Solver::Solver ( SolverImpl *  _impl)
inline

Definition at line 80 of file Solver.h.

◆ ~Solver()

Solver::~Solver ( )
virtual

Definition at line 25 of file Solver.cpp.

References impl.

Member Function Documentation

◆ evaluate()

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

evaluate - Determine for a particular state if the query expression is provably true, provably false or neither.

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.

Definition at line 37 of file Solver.cpp.

References klee::Expr::Bool, klee::SolverImpl::computeValidity(), klee::Query::expr, False, klee::Expr::getWidth(), impl, and True.

Referenced by getRange().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getConstraintLog()

char * Solver::getConstraintLog ( const Query &  query)
virtual

Reimplemented in klee::MetaSMTSolver< SolverContext >, klee::STPSolver, and klee::Z3Solver.

Definition at line 29 of file Solver.cpp.

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

Referenced by klee::AssignmentValidatingSolver::dumpAssignmentQuery().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getInitialValues()

bool Solver::getInitialValues ( const Query &  query,
const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  result 
)

getInitialValues - Compute the initial values for a list of objects.

Parameters
[out]result- On success, this vector will be filled in with an array of bytes for each given object (with length matching the object size). The bytes correspond to the initial values for the objects for some satisfying assignment.
Returns
True on success.

NOTE: This function returns failure if there is no satisfying assignment.

Definition at line 98 of file Solver.cpp.

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

Referenced by EvaluateInputAST().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getRange()

std::pair< ref< Expr >, ref< Expr > > Solver::getRange ( const Query &  query)
virtual

getRange - Compute a tight range of possible values for a given expression.

Returns
- A pair with (min, max) values for the expression.
Postcondition
(mustBeTrue(min <= e <= max) && mayBeTrue(min == e) && mayBeTrue(max == e))

Definition at line 111 of file Solver.cpp.

References klee::ConstantExpr::create(), evaluate(), klee::Query::expr, False, klee::Expr::getWidth(), klee::bits64::maxValueOfNBits(), mayBeTrue(), mustBeTrue(), True, and klee::Query::withExpr().

Here is the call graph for this function:

◆ getValue()

bool Solver::getValue ( const Query &  query,
ref< ConstantExpr > &  result 
)

getValue - Compute one possible value for the given expression.

Parameters
[out]result- On success, a value for the expression in some satisfying assignment.
Returns
True on success.

Definition at line 81 of file Solver.cpp.

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

Referenced by klee::ImpliedValue::checkForImpliedValues(), and EvaluateInputAST().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ mayBeFalse()

bool Solver::mayBeFalse ( const Query &  query,
bool &  result 
)

mayBeFalse - Determine if there is a valid assignment for the given state in which the expression evaluates to false.

This evaluates the following logical formula:

\[ \exists X constraints(X) \land \lnot query(X) \]

which is equivalent to

\[ \lnot \forall X constraints(X) \to query(X) \]

Where $X$ is some assignment, $constraints(X)$ are the constraints in the query and $query(X)$ is the query expression.

Parameters
[out]result- On success, true iff the logical formula may be false
Returns
True on success.

Definition at line 73 of file Solver.cpp.

References mustBeTrue().

Here is the call graph for this function:

◆ mayBeTrue()

bool Solver::mayBeTrue ( const Query &  query,
bool &  result 
)

mayBeTrue - Determine if there is a valid assignment for the given state in which the expression evaluates to true.

This evaluates the following logical formula:

\[ \exists X constraints(X) \land query(X) \]

which is equivalent to

\[ \lnot \forall X constraints(X) \to \lnot query(X) \]

Where $X$ is some assignment, $constraints(X)$ are the constraints in the query and $query(X)$ is the query expression.

Parameters
[out]result- On success, true iff the logical formula may be true
Returns
True on success.

Definition at line 65 of file Solver.cpp.

References mustBeFalse().

Referenced by getRange().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ mustBeFalse()

bool Solver::mustBeFalse ( const Query &  query,
bool &  result 
)

mustBeFalse - Determine if the expression is provably false.

This evaluates the following logical formula:

\[ \lnot \exists X constraints(X) \land query(X) \]

which is equivalent to

\[ \forall X constraints(X) \to \lnot query(X) \]

Where $X$ is some assignment, $constraints(X)$ are the constraints in the query and $query(X)$ is the query expression.

Parameters
[out]result- On success, true iff the logical formula is false
Returns
True on success.

Definition at line 61 of file Solver.cpp.

References mustBeTrue(), and klee::Query::negateExpr().

Referenced by mayBeTrue().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ mustBeTrue()

bool Solver::mustBeTrue ( const Query &  query,
bool &  result 
)

mustBeTrue - Determine if the expression is provably true.

This evaluates the following logical formula:

\[ \forall X constraints(X) \to query(X) \]

which is equivalent to

\[ \lnot \exists X constraints(X) \land \lnot query(X) \]

Where $X$ is some assignment, $constraints(X)$ are the constraints in the query and $query(X)$ is the query expression.

Parameters
[out]result- On success, true iff the logical formula is true
Returns
True on success.

Definition at line 49 of file Solver.cpp.

References klee::Expr::Bool, klee::SolverImpl::computeTruth(), klee::Query::expr, klee::Expr::getWidth(), and impl.

Referenced by klee::ImpliedValue::checkForImpliedValues(), EvaluateInputAST(), getRange(), mayBeFalse(), and mustBeFalse().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ operator=()

void klee::Solver::operator= ( const Solver &  )
private

◆ setCoreSolverTimeout()

void Solver::setCoreSolverTimeout ( time::Span  timeout)
virtual

Reimplemented in klee::MetaSMTSolver< SolverContext >, klee::STPSolver, and klee::Z3Solver.

Definition at line 33 of file Solver.cpp.

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

Referenced by EvaluateInputAST().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ validity_to_str()

const char * Solver::validity_to_str ( Validity  v)
static

validity_to_str - Return the name of given Validity enum value.

Definition at line 17 of file Solver.cpp.

References False, and True.

Member Data Documentation

◆ impl

SolverImpl* klee::Solver::impl

Definition at line 77 of file Solver.h.

Referenced by klee::StagedSolverImpl::computeInitialValues(), klee::AssignmentValidatingSolver::computeInitialValues(), klee::ValidatingSolver::computeInitialValues(), CachingSolver::computeInitialValues(), IndependentSolver::computeInitialValues(), QueryLoggingSolver::computeInitialValues(), klee::StagedSolverImpl::computeTruth(), klee::AssignmentValidatingSolver::computeTruth(), CachingSolver::computeTruth(), IndependentSolver::computeTruth(), klee::ValidatingSolver::computeTruth(), QueryLoggingSolver::computeTruth(), klee::StagedSolverImpl::computeValidity(), klee::AssignmentValidatingSolver::computeValidity(), CachingSolver::computeValidity(), IndependentSolver::computeValidity(), klee::ValidatingSolver::computeValidity(), QueryLoggingSolver::computeValidity(), klee::StagedSolverImpl::computeValue(), klee::AssignmentValidatingSolver::computeValue(), IndependentSolver::computeValue(), klee::ValidatingSolver::computeValue(), CachingSolver::computeValue(), QueryLoggingSolver::computeValue(), evaluate(), EvaluateInputAST(), QueryLoggingSolver::finishQuery(), QueryLoggingSolver::flushBuffer(), CexCachingSolver::getAssignment(), klee::StagedSolverImpl::getConstraintLog(), klee::AssignmentValidatingSolver::getConstraintLog(), CachingSolver::getConstraintLog(), IndependentSolver::getConstraintLog(), QueryLoggingSolver::getConstraintLog(), klee::ValidatingSolver::getConstraintLog(), getConstraintLog(), CexCachingSolver::getConstraintLog(), getInitialValues(), klee::StagedSolverImpl::getOperationStatusCode(), klee::AssignmentValidatingSolver::getOperationStatusCode(), CachingSolver::getOperationStatusCode(), CexCachingSolver::getOperationStatusCode(), IndependentSolver::getOperationStatusCode(), QueryLoggingSolver::getOperationStatusCode(), klee::ValidatingSolver::getOperationStatusCode(), getValue(), mustBeTrue(), klee::StagedSolverImpl::setCoreSolverTimeout(), setCoreSolverTimeout(), klee::AssignmentValidatingSolver::setCoreSolverTimeout(), CachingSolver::setCoreSolverTimeout(), CexCachingSolver::setCoreSolverTimeout(), IndependentSolver::setCoreSolverTimeout(), QueryLoggingSolver::setCoreSolverTimeout(), klee::ValidatingSolver::setCoreSolverTimeout(), and ~Solver().

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