klee
Public Types | Public Member Functions | Public Attributes | List of all members
klee::Assignment Class Reference

#include <Assignment.h>

Public Types

typedef std::map< const Array *, std::vector< unsigned char > > bindings_ty
 

Public Member Functions

 Assignment (bool _allowFreeValues=false)
 
 Assignment (const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool _allowFreeValues=false)
 
ref< Expr > evaluate (const Array *mo, unsigned index) const
 
ref< Expr > evaluate (ref< Expr > e)
 
ConstraintSet createConstraintsFromAssignment () const
 
template<typename InputIterator >
bool satisfies (InputIterator begin, InputIterator end)
 
void dump ()
 

Public Attributes

bool allowFreeValues
 
bindings_ty bindings
 

Detailed Description

Definition at line 21 of file Assignment.h.

Member Typedef Documentation

◆ bindings_ty

typedef std::map<const Array*, std::vector<unsigned char> > klee::Assignment::bindings_ty

Definition at line 23 of file Assignment.h.

Constructor & Destructor Documentation

◆ Assignment() [1/2]

klee::Assignment::Assignment ( bool  _allowFreeValues = false)
inline

Definition at line 29 of file Assignment.h.

◆ Assignment() [2/2]

klee::Assignment::Assignment ( const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  values,
bool  _allowFreeValues = false 
)
inline

Definition at line 31 of file Assignment.h.

References bindings.

Member Function Documentation

◆ createConstraintsFromAssignment()

ConstraintSet klee::Assignment::createConstraintsFromAssignment ( ) const

Definition at line 28 of file Assignment.cpp.

References klee::ConstantExpr::alloc(), bindings, klee::ReadExpr::create(), and klee::ConstraintSet::push_back().

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

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

◆ dump()

void klee::Assignment::dump ( )

Definition at line 14 of file Assignment.cpp.

References bindings.

Referenced by klee::AssignmentValidatingSolver::computeInitialValues(), and CexCachingSolver::getAssignment().

Here is the caller graph for this function:

◆ evaluate() [1/2]

ref< Expr > klee::Assignment::evaluate ( const Array *  mo,
unsigned  index 
) const
inline

Definition at line 69 of file Assignment.h.

References klee::ConstantExpr::alloc(), allowFreeValues, bindings, klee::ReadExpr::create(), klee::Array::getDomain(), and klee::Array::getRange().

Referenced by assertCreatedPointEvaluatesToTrue(), klee::AssignmentValidatingSolver::computeInitialValues(), CexCachingSolver::computeValidity(), CexCachingSolver::computeValue(), klee::AssignmentEvaluator::getInitialValue(), and klee::SeedInfo::patchSeed().

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

◆ evaluate() [2/2]

ref< Expr > klee::Assignment::evaluate ( ref< Expr >  e)
inline

Definition at line 85 of file Assignment.h.

References klee::ExprVisitor::visit().

Here is the call graph for this function:

◆ satisfies()

template<typename InputIterator >
bool klee::Assignment::satisfies ( InputIterator  begin,
InputIterator  end 
)
inline

Definition at line 91 of file Assignment.h.

References klee::Expr::isTrue(), and klee::ExprVisitor::visit().

Referenced by CexCachingSolver::getAssignment(), NullOrSatisfyingAssignment::operator()(), and CexCachingSolver::searchForAssignment().

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

Member Data Documentation

◆ allowFreeValues

bool klee::Assignment::allowFreeValues

Definition at line 25 of file Assignment.h.

Referenced by evaluate().

◆ bindings

bindings_ty klee::Assignment::bindings

Definition at line 26 of file Assignment.h.

Referenced by assertCreatedPointEvaluatesToTrue(), Assignment(), CexCachingSolver::computeInitialValues(), createConstraintsFromAssignment(), dump(), evaluate(), klee::Executor::executeMakeSymbolic(), klee::AssignmentGenerator::helperGenerateAssignment(), AssignmentLessThan::operator()(), and klee::SeedInfo::patchSeed().

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