CBMC
alternatives_enumeratort Class Reference

Enumerators that enumerates expressions in the union of enumerated expressions of sub-enumerators. More...

#include <expr_enumerator.h>

+ Inheritance diagram for alternatives_enumeratort:
+ Collaboration diagram for alternatives_enumeratort:

Public Member Functions

 alternatives_enumeratort (const enumeratorst &enumerators, const namespacet &ns)
 
expr_sett enumerate (const std::size_t size) const override
 
- Public Member Functions inherited from enumerator_baset
 enumerator_baset (const namespacet &ns)
 
 enumerator_baset (const enumerator_baset &other)=delete
 
enumerator_basetoperator= (const enumerator_baset &other)=delete
 
virtual ~enumerator_baset ()=default
 

Protected Attributes

const enumeratorst sub_enumerators
 
- Protected Attributes inherited from enumerator_baset
const namespacetns
 

Detailed Description

Enumerators that enumerates expressions in the union of enumerated expressions of sub-enumerators.

For sub enumerator E_1 | E_2 | ... | E_n, an alternatives enumerator enumerates e in one of E_i.enumerate(size).

Definition at line 283 of file expr_enumerator.h.

Constructor & Destructor Documentation

◆ alternatives_enumeratort()

alternatives_enumeratort::alternatives_enumeratort ( const enumeratorst enumerators,
const namespacet ns 
)
inline

Definition at line 286 of file expr_enumerator.h.

Member Function Documentation

◆ enumerate()

expr_sett alternatives_enumeratort::enumerate ( const std::size_t  size) const
overridevirtual

Implements enumerator_baset.

Definition at line 405 of file expr_enumerator.cpp.

Member Data Documentation

◆ sub_enumerators

const enumeratorst alternatives_enumeratort::sub_enumerators
protected

Definition at line 296 of file expr_enumerator.h.


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