klee
Public Types | Public Member Functions | Private Attributes | Friends | List of all members
klee::ConstraintSet Class Reference

#include <Constraints.h>

Public Types

using constraints_ty = std::vector< ref< Expr > >
 
using iterator = constraints_ty::iterator
 
using const_iterator = constraints_ty::const_iterator
 
using constraint_iterator = const_iterator
 

Public Member Functions

bool empty () const
 
constraint_iterator begin () const
 
constraint_iterator end () const
 
size_t size () const noexcept
 
 ConstraintSet (constraints_ty cs)
 
 ConstraintSet ()=default
 
void push_back (const ref< Expr > &e)
 
bool operator== (const ConstraintSet &b) const
 

Private Attributes

constraints_ty constraints
 

Friends

class ConstraintManager
 

Detailed Description

Resembles a set of constraints that can be passed around

Definition at line 19 of file Constraints.h.

Member Typedef Documentation

◆ const_iterator

using klee::ConstraintSet::const_iterator = constraints_ty::const_iterator

Definition at line 25 of file Constraints.h.

◆ constraint_iterator

using klee::ConstraintSet::constraint_iterator = const_iterator

Definition at line 27 of file Constraints.h.

◆ constraints_ty

using klee::ConstraintSet::constraints_ty = std::vector<ref<Expr> >

Definition at line 23 of file Constraints.h.

◆ iterator

using klee::ConstraintSet::iterator = constraints_ty::iterator

Definition at line 24 of file Constraints.h.

Constructor & Destructor Documentation

◆ ConstraintSet() [1/2]

klee::ConstraintSet::ConstraintSet ( constraints_ty  cs)
inlineexplicit

Definition at line 34 of file Constraints.h.

◆ ConstraintSet() [2/2]

klee::ConstraintSet::ConstraintSet ( )
default

Member Function Documentation

◆ begin()

klee::ConstraintSet::constraint_iterator ConstraintSet::begin ( ) const

Definition at line 168 of file Constraints.cpp.

References constraints.

Referenced by CexCachingSolver::lookupAssignment(), klee::ExecutionState::merge(), klee::ExprPPrinter::printQuery(), and klee::ExprSMTLIBPrinter::printQueryInSingleAssert().

Here is the caller graph for this function:

◆ empty()

bool ConstraintSet::empty ( ) const

Definition at line 166 of file Constraints.cpp.

References constraints.

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

Here is the caller graph for this function:

◆ end()

klee::ConstraintSet::constraint_iterator ConstraintSet::end ( ) const

Definition at line 172 of file Constraints.cpp.

References constraints.

Referenced by CexCachingSolver::lookupAssignment(), klee::ExecutionState::merge(), klee::ExprPPrinter::printQuery(), and klee::ExprSMTLIBPrinter::printQueryInSingleAssert().

Here is the caller graph for this function:

◆ operator==()

bool klee::ConstraintSet::operator== ( const ConstraintSet &  b) const
inline

Definition at line 39 of file Constraints.h.

References constraints.

◆ push_back()

void ConstraintSet::push_back ( const ref< Expr > &  e)

Definition at line 178 of file Constraints.cpp.

References constraints.

Referenced by klee::ConstraintManager::addConstraintInternal(), klee::ImpliedValue::checkForImpliedValues(), klee::ValidatingSolver::computeInitialValues(), klee::Assignment::createConstraintsFromAssignment(), klee::AssignmentValidatingSolver::dumpAssignmentQuery(), and klee::ConstraintManager::rewriteConstraints().

Here is the caller graph for this function:

◆ size()

size_t ConstraintSet::size ( ) const
noexcept

Definition at line 176 of file Constraints.cpp.

References constraints.

Friends And Related Function Documentation

◆ ConstraintManager

friend class ConstraintManager
friend

Definition at line 20 of file Constraints.h.

Member Data Documentation

◆ constraints

constraints_ty klee::ConstraintSet::constraints
private

Definition at line 44 of file Constraints.h.

Referenced by begin(), empty(), end(), operator==(), push_back(), and size().

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