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< Exprevaluate (const Array *mo, unsigned index) const
ref< Exprevaluate (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)

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 

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

◆ evaluate() [2/2]

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

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 

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

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