cprover
interval_index_ranget Class Reference
+ Inheritance diagram for interval_index_ranget:
+ Collaboration diagram for interval_index_ranget:

Public Member Functions

 interval_index_ranget (const constant_interval_exprt &interval, const namespacet &n)
 
const exprtcurrent () const override
 
bool advance_to_next () override
 
- Public Member Functions inherited from index_ranget
virtual ~index_ranget ()=default
 

Static Private Member Functions

static exprt next_element (const exprt &cur, const namespacet &ns)
 

Private Attributes

exprt index
 
exprt next
 
exprt upper
 
const namespacetns
 

Detailed Description

Definition at line 20 of file interval_abstract_value.cpp.

Constructor & Destructor Documentation

◆ interval_index_ranget()

interval_index_ranget::interval_index_ranget ( const constant_interval_exprt interval,
const namespacet n 
)
inline

Definition at line 23 of file interval_abstract_value.cpp.

Member Function Documentation

◆ advance_to_next()

bool interval_index_ranget::advance_to_next ( )
inlineoverridevirtual

Implements index_ranget.

Definition at line 37 of file interval_abstract_value.cpp.

◆ current()

const exprt& interval_index_ranget::current ( ) const
inlineoverridevirtual

Implements index_ranget.

Definition at line 33 of file interval_abstract_value.cpp.

◆ next_element()

static exprt interval_index_ranget::next_element ( const exprt cur,
const namespacet ns 
)
inlinestaticprivate

Definition at line 46 of file interval_abstract_value.cpp.

Member Data Documentation

◆ index

exprt interval_index_ranget::index
private

Definition at line 51 of file interval_abstract_value.cpp.

◆ next

exprt interval_index_ranget::next
private

Definition at line 52 of file interval_abstract_value.cpp.

◆ ns

const namespacet& interval_index_ranget::ns
private

Definition at line 54 of file interval_abstract_value.cpp.

◆ upper

exprt interval_index_ranget::upper
private

Definition at line 53 of file interval_abstract_value.cpp.


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