CBMC
Public Types | Public Member Functions | Private Attributes | List of all members
abstract_object_sett Class Reference

#include <abstract_object_set.h>

+ Collaboration diagram for abstract_object_sett:

Public Types

using value_sett = std::unordered_set< abstract_object_pointert, abstract_hashert, abstract_equalert >
 
using const_iterator = value_sett::const_iterator
 
using value_type = value_sett::value_type
 
using size_type = value_sett::size_type
 

Public Member Functions

void insert (const abstract_object_pointert &o)
 
void insert (abstract_object_pointert &&o)
 
void insert (const abstract_object_sett &rhs)
 
void insert (const value_ranget &rhs)
 
void push_back (const abstract_object_pointert &v)
 
abstract_object_pointert first () const
 
const_iterator begin () const
 
const_iterator end () const
 
value_sett::size_type size () const
 
bool empty () const
 
bool operator== (const abstract_object_sett &rhs) const
 
void clear ()
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const
 
constant_interval_exprt to_interval () const
 Calculate the set of values as an interval. More...
 

Private Attributes

value_sett values
 

Detailed Description

Definition at line 18 of file abstract_object_set.h.

Member Typedef Documentation

◆ const_iterator

using abstract_object_sett::const_iterator = value_sett::const_iterator

Definition at line 25 of file abstract_object_set.h.

◆ size_type

using abstract_object_sett::size_type = value_sett::size_type

Definition at line 27 of file abstract_object_set.h.

◆ value_sett

using abstract_object_sett::value_sett = std::unordered_set< abstract_object_pointert, abstract_hashert, abstract_equalert>

Definition at line 21 of file abstract_object_set.h.

◆ value_type

using abstract_object_sett::value_type = value_sett::value_type

Definition at line 26 of file abstract_object_set.h.

Member Function Documentation

◆ begin()

const_iterator abstract_object_sett::begin ( ) const
inline

Definition at line 58 of file abstract_object_set.h.

◆ clear()

void abstract_object_sett::clear ( void  )
inline

Definition at line 81 of file abstract_object_set.h.

◆ empty()

bool abstract_object_sett::empty ( ) const
inline

Definition at line 71 of file abstract_object_set.h.

◆ end()

const_iterator abstract_object_sett::end ( ) const
inline

Definition at line 62 of file abstract_object_set.h.

◆ first()

abstract_object_pointert abstract_object_sett::first ( ) const
inline

Definition at line 53 of file abstract_object_set.h.

◆ insert() [1/4]

void abstract_object_sett::insert ( abstract_object_pointert &&  o)
inline

Definition at line 33 of file abstract_object_set.h.

◆ insert() [2/4]

void abstract_object_sett::insert ( const abstract_object_pointert &  o)
inline

Definition at line 29 of file abstract_object_set.h.

◆ insert() [3/4]

void abstract_object_sett::insert ( const abstract_object_sett &  rhs)
inline

Definition at line 37 of file abstract_object_set.h.

◆ insert() [4/4]

void abstract_object_sett::insert ( const value_ranget &  rhs)
inline

Definition at line 41 of file abstract_object_set.h.

◆ operator==()

bool abstract_object_sett::operator== ( const abstract_object_sett &  rhs) const
inline

Definition at line 76 of file abstract_object_set.h.

◆ output()

void abstract_object_sett::output ( std::ostream &  out,
const ai_baset &  ai,
const namespacet &  ns 
) const

Definition at line 25 of file abstract_object_set.cpp.

◆ push_back()

void abstract_object_sett::push_back ( const abstract_object_pointert &  v)
inline

Definition at line 47 of file abstract_object_set.h.

◆ size()

value_sett::size_type abstract_object_sett::size ( ) const
inline

Definition at line 67 of file abstract_object_set.h.

◆ to_interval()

constant_interval_exprt abstract_object_sett::to_interval ( ) const

Calculate the set of values as an interval.

Returns
the constant_interval_exprt bounding the values

Definition at line 42 of file abstract_object_set.cpp.

Member Data Documentation

◆ values

value_sett abstract_object_sett::values
private

Definition at line 94 of file abstract_object_set.h.

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