klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
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 (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)
 
template<typename InputIterator >
bool satisfies (InputIterator begin, InputIterator end)
 

Public Attributes

bool allowFreeValues
 
bindings_ty bindings
 

Detailed Description

Definition at line 22 of file Assignment.h.

Member Typedef Documentation

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

Definition at line 24 of file Assignment.h.

Constructor & Destructor Documentation

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

Definition at line 30 of file Assignment.h.

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

Definition at line 32 of file Assignment.h.

References bindings.

Member Function Documentation

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

Definition at line 84 of file Assignment.h.

References klee::ExprVisitor::visit().

Here is the call graph for this function:

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

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

bool klee::Assignment::allowFreeValues

Definition at line 26 of file Assignment.h.

Referenced by evaluate().


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