Loading...

Searching...

No Matches

interval_uniont Class Reference

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:

[フレーム]

[legend]

Public Types

using intervalt = interval_templatet< mp_integer >

Public Member Functions

interval_uniont ()=default

Empty union.

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.

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.

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

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

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.

exprt make_contains_expr (const exprt &e) const

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

std::optional< mp_integer > as_singleton () const

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

Static Public Member Functions

static interval_uniont all_integers ()

Set of all integers.

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.

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.

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]".

static interval_uniont of_interval (intervalt interval)

Construct interval union from a single interval.

Private Member Functions

bool validate () const

Check that intervals are strictly ordered.

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.

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