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

#include <Constraints.h>

Public Types

typedef std::vector< ref< Expr > > constraints_ty
 
typedef constraints_ty::iterator iterator
 
typedef
constraints_ty::const_iterator 
const_iterator
 
typedef std::vector< ref< Expr >
>::const_iterator 
constraint_iterator
 

Public Member Functions

 ConstraintManager ()
 
 ConstraintManager (const std::vector< ref< Expr > > &_constraints)
 
 ConstraintManager (const ConstraintManager &cs)
 
void simplifyForValidConstraint (ref< Expr > e)
 
ref< ExprsimplifyExpr (ref< Expr > e) const
 
void addConstraint (ref< Expr > e)
 
bool empty () const
 
ref< Exprback () const
 
constraint_iterator begin () const
 
constraint_iterator end () const
 
size_t size () const
 
bool operator== (const ConstraintManager &other) const
 

Private Member Functions

bool rewriteConstraints (ExprVisitor &visitor)
 
void addConstraintInternal (ref< Expr > e)
 

Private Attributes

std::vector< ref< Expr > > constraints
 

Detailed Description

Definition at line 23 of file Constraints.h.

Member Typedef Documentation

typedef constraints_ty::const_iterator klee::ConstraintManager::const_iterator

Definition at line 27 of file Constraints.h.

Definition at line 38 of file Constraints.h.

Definition at line 25 of file Constraints.h.

typedef constraints_ty::iterator klee::ConstraintManager::iterator

Definition at line 26 of file Constraints.h.

Constructor & Destructor Documentation

klee::ConstraintManager::ConstraintManager ( )
inline

Definition at line 29 of file Constraints.h.

klee::ConstraintManager::ConstraintManager ( const std::vector< ref< Expr > > &  _constraints)
inlineexplicit

Definition at line 33 of file Constraints.h.

klee::ConstraintManager::ConstraintManager ( const ConstraintManager cs)
inline

Definition at line 36 of file Constraints.h.

Member Function Documentation

void ConstraintManager::addConstraint ( ref< Expr e)

Definition at line 159 of file Constraints.cpp.

References addConstraintInternal(), and simplifyExpr().

Referenced by klee::ExecutionState::addConstraint(), and klee::ExecutionState::merge().

Here is the call graph for this function:

Here is the caller graph for this function:

void ConstraintManager::addConstraintInternal ( ref< Expr e)
private

Definition at line 120 of file Constraints.cpp.

References klee::Expr::And, klee::Expr::Constant, constraints, klee::Expr::Eq, klee::Expr::getKind(), klee::BinaryExpr::left, rewriteConstraints(), and klee::BinaryExpr::right.

Referenced by addConstraint(), and rewriteConstraints().

Here is the call graph for this function:

Here is the caller graph for this function:

ref<Expr> klee::ConstraintManager::back ( ) const
inline

Definition at line 51 of file Constraints.h.

References constraints.

bool klee::ConstraintManager::empty ( ) const
inline

Definition at line 48 of file Constraints.h.

References constraints.

Referenced by klee::ExprPPrinter::printQuery().

Here is the caller graph for this function:

bool klee::ConstraintManager::operator== ( const ConstraintManager other) const
inline

Definition at line 64 of file Constraints.h.

References constraints.

bool ConstraintManager::rewriteConstraints ( ExprVisitor visitor)
private

Definition at line 70 of file Constraints.cpp.

References addConstraintInternal(), constraints, and klee::ExprVisitor::visit().

Referenced by addConstraintInternal().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< Expr > ConstraintManager::simplifyExpr ( ref< Expr e) const
void ConstraintManager::simplifyForValidConstraint ( ref< Expr e)

Definition at line 91 of file Constraints.cpp.

size_t klee::ConstraintManager::size ( ) const
inline

Definition at line 60 of file Constraints.h.

References constraints.

Referenced by klee::ExprSMTLIBLetPrinter::printLetExpression().

Here is the caller graph for this function:

Member Data Documentation

std::vector< ref<Expr> > klee::ConstraintManager::constraints
private

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