klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::Solver Class Reference

#include <Solver.h>

Inheritance diagram for klee::Solver:
Collaboration diagram for klee::Solver:

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 (double 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

SolverImplimpl
 

Private Member Functions

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

Detailed Description

Definition at line 47 of file Solver.h.

Member Enumeration Documentation

Enumerator
True 
False 
Unknown 

Definition at line 53 of file Solver.h.

Constructor & Destructor Documentation

klee::Solver::Solver ( const Solver )
private
klee::Solver::Solver ( SolverImpl _impl)
inline

Definition at line 67 of file Solver.h.

Solver::~Solver ( )
virtual

Definition at line 120 of file Solver.cpp.

Member Function Documentation

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 132 of file Solver.cpp.

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

Here is the call graph for this function:

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

Reimplemented in klee::STPSolver.

Definition at line 124 of file Solver.cpp.

Referenced by klee::TimingSolver::getConstraintLog().

Here is the caller graph for this function:

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 193 of file Solver.cpp.

Referenced by EvaluateInputAST().

Here is the caller graph for this function:

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 206 of file Solver.cpp.

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

Here is the call graph for this function:

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 176 of file Solver.cpp.

References klee::Query::expr.

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

Here is the caller graph for this function:

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 168 of file Solver.cpp.

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 160 of file Solver.cpp.

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 156 of file Solver.cpp.

References klee::Query::negateExpr().

Here is the call graph for this function:

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 144 of file Solver.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::Solver::operator= ( const Solver )
private
void Solver::setCoreSolverTimeout ( double  timeout)
virtual

Reimplemented in klee::STPSolver.

Definition at line 128 of file Solver.cpp.

Referenced by EvaluateInputAST(), and klee::TimingSolver::setTimeout().

Here is the caller graph for this function:

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

validity_to_str - Return the name of given Validity enum value.

Definition at line 112 of file Solver.cpp.

Member Data Documentation


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