Represents a set of integers by a union of intervals, which are stored in increasing order for efficient union and intersection (linear time in both cases). More...

#include <interval_union.h>

Collaboration diagram for interval_uniont:

Public Types
using	intervalt = interval_templatet< mp_integer >

Public Member Functions
	interval_uniont ()=default
	Empty union. More...

interval_uniont	make_intersection (const interval_uniont &other) const
	Return a new interval_uniontt object representing the set of intergers in the intersection of this object and `other`. More...

interval_uniont	make_union (const interval_uniont &other) const
	Return a new interval_uniontt object representing the set of intergers in the union of this object and `other`. More...

bool	is_empty () const

std::optional< mp_integer >	maximum () const
	empty optional means either unbounded on the right or empty, is_empty has to be called to distinguish between the two More...

std::optional< mp_integer >	minimum () const
	empty optional means either unbounded on the left or empty, is_empty has to be called to distinguish between the two More...

std::string	to_string () const
	Convert the set to a string representing a sequence of intervals, each interval being of the form "[lower:upper]", "[:upper]" if there is no lower bound, "[lower:]" if there is no upper bound, "[:]" for the whole set of integers and "[]" for the empty set. More...

exprt	make_contains_expr (const exprt &e) const
	Expression which is true exactly when `e` belongs to the set. More...

std::optional< mp_integer >	as_singleton () const
	If the set contains only one element, return the value of this element. More...

Static Public Member Functions
static interval_uniont	all_integers ()
	Set of all integers. More...

static interval_uniont	greater_or_equal (const mp_integer &value)
	Construct interval_uniont object representing the set of integers that are greater or equal to `value`. More...

static interval_uniont	smaller_or_equal (const mp_integer &value)
	Construct interval_uniont object representing the set of integers that are greater or equal to `value`. More...

static std::optional< interval_uniont >	of_string (const std::string &to_parse)
	Parse a string which is a comma `,` separated list of intervals of the form "[lower1:upper1]", for example: "[-3:-2],[4:5]". More...

static interval_uniont	of_interval (intervalt interval)
	Construct interval union from a single interval. More...

Private Member Functions
bool	validate () const
	Check that intervals are strictly ordered. More...

Private Attributes
std::vector< intervalt >	intervals
	Non-overlapping intervals stored in order of their lower bound, so that each interval is strictly below the following one. More...

Detailed Description

Represents a set of integers by a union of intervals, which are stored in increasing order for efficient union and intersection (linear time in both cases).

Definition at line 26 of file interval_union.h.

Member Typedef Documentation

◆ intervalt

using interval_uniont::intervalt = interval_templatet<mp_integer>

Definition at line 29 of file interval_union.h.

Constructor & Destructor Documentation

◆ interval_uniont()

interval_uniont::interval_uniont ( )

default

Empty union.

Member Function Documentation

◆ all_integers()

interval_uniont interval_uniont::all_integers ( )

static

Set of all integers.

Definition at line 17 of file interval_union.cpp.

◆ as_singleton()

std::optional< mp_integer > interval_uniont::as_singleton ( ) const

If the set contains only one element, return the value of this element.

Definition at line 238 of file interval_union.cpp.

◆ greater_or_equal()

interval_uniont interval_uniont::greater_or_equal ( const mp_integer & value )

static

Construct interval_uniont object representing the set of integers that are greater or equal to value.

Definition at line 22 of file interval_union.cpp.

◆ is_empty()

bool interval_uniont::is_empty ( ) const

Definition at line 147 of file interval_union.cpp.

◆ make_contains_expr()

exprt interval_uniont::make_contains_expr ( const exprt & e ) const

Expression which is true exactly when e belongs to the set.

Definition at line 190 of file interval_union.cpp.

◆ make_intersection()

interval_uniont interval_uniont::make_intersection ( const interval_uniont & other ) const

Return a new interval_uniontt object representing the set of intergers in the intersection of this object and other.

Definition at line 41 of file interval_union.cpp.

◆ make_union()

interval_uniont interval_uniont::make_union ( const interval_uniont & other ) const

Return a new interval_uniontt object representing the set of intergers in the union of this object and other.

Definition at line 60 of file interval_union.cpp.

◆ maximum()

std::optional< mp_integer > interval_uniont::maximum ( ) const

empty optional means either unbounded on the right or empty, is_empty has to be called to distinguish between the two

Definition at line 152 of file interval_union.cpp.

◆ minimum()

std::optional< mp_integer > interval_uniont::minimum ( ) const

empty optional means either unbounded on the left or empty, is_empty has to be called to distinguish between the two

Definition at line 162 of file interval_union.cpp.

◆ of_interval()

interval_uniont interval_uniont::of_interval ( interval_uniont::intervalt interval )

static

Construct interval union from a single interval.

Definition at line 209 of file interval_union.cpp.

◆ of_string()

std::optional< interval_uniont > interval_uniont::of_string ( const std::string & to_parse )

static

Parse a string which is a comma , separated list of intervals of the form "[lower1:upper1]", for example: "[-3:-2],[4:5]".

Return an empty optional if the string doesn't match the format.

Definition at line 217 of file interval_union.cpp.

◆ smaller_or_equal()

interval_uniont interval_uniont::smaller_or_equal ( const mp_integer & value )

static

Construct interval_uniont object representing the set of integers that are greater or equal to value.

Definition at line 31 of file interval_union.cpp.

◆ to_string()

std::string interval_uniont::to_string ( ) const

Convert the set to a string representing a sequence of intervals, each interval being of the form "[lower:upper]", "[:upper]" if there is no lower bound, "[lower:]" if there is no upper bound, "[:]" for the whole set of integers and "[]" for the empty set.

Definition at line 172 of file interval_union.cpp.

◆ validate()

bool interval_uniont::validate ( ) const

private

Check that intervals are strictly ordered.

Definition at line 258 of file interval_union.cpp.

Member Data Documentation

◆ intervals

std::vector<intervalt> interval_uniont::intervals

private

Non-overlapping intervals stored in order of their lower bound, so that each interval is strictly below the following one.

As a consequence an interval without a lower-bound can only occur in first position and one without an upper-bound in last position.

Definition at line 89 of file interval_union.h.

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

/home/runner/work/cbmc/cbmc/src/util/interval_union.h
/home/runner/work/cbmc/cbmc/src/util/interval_union.cpp

Public Types

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ intervalt

Constructor & Destructor Documentation

◆ interval_uniont()

Member Function Documentation

◆ all_integers()

◆ as_singleton()

◆ greater_or_equal()

◆ is_empty()

◆ make_contains_expr()

◆ make_intersection()

◆ make_union()

◆ maximum()

◆ minimum()

◆ of_interval()

◆ of_string()

◆ smaller_or_equal()

◆ to_string()

◆ validate()

Member Data Documentation

◆ intervals