cprover
interval_union.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Util
4 
5 Author: Diffblue Limited
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_INTERVAL_UNION_H
13 #define CPROVER_UTIL_INTERVAL_UNION_H
14 
15 #include <util/interval_template.h>
16 #include <util/mp_arith.h>
17 #include <util/nodiscard.h>
18 #include <util/optional.h>
19 #include <vector>
20 
21 class exprt;
22 
27 {
28 public:
30 
32  interval_uniont() = default;
33 
36 
39  static interval_uniont greater_or_equal(const mp_integer &value);
40 
43  static interval_uniont smaller_or_equal(const mp_integer &value);
44 
48  make_intersection(const interval_uniont &other) const;
49 
53 
54  bool is_empty() const;
55 
59 
63 
68  std::string to_string() const;
69 
73  static optionalt<interval_uniont> of_string(const std::string &to_parse);
74 
76  static interval_uniont of_interval(intervalt interval);
77 
79  exprt make_contains_expr(const exprt &e) const;
80 
83 
84 private:
89  std::vector<intervalt> intervals;
90 
92  bool validate() const;
93 };
94 
95 #endif // CPROVER_UTIL_INTERVAL_UNION_H
Base class for all expressions.
Definition: expr.h:54
Represents a set of integers by a union of intervals, which are stored in increasing order for effici...
NODISCARD 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 an...
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.
interval_uniont()=default
Empty union.
std::vector< intervalt > intervals
Non-overlapping intervals stored in order of their lower bound, so that each interval is strictly bel...
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 optionalt< 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]",...
optionalt< mp_integer > as_singleton() const
If the set contains only one element, return the value of this element.
bool validate() const
Check that intervals are strictly ordered.
bool is_empty() const
optionalt< mp_integer > minimum() const
empty optional means either unbounded on the left or empty, is_empty has to be called to distinguish ...
optionalt< mp_integer > maximum() const
empty optional means either unbounded on the right or empty, is_empty has to be called to distinguish...
std::string to_string() const
Convert the set to a string representing a sequence of intervals, each interval being of the form "[l...
static interval_uniont all_integers()
Set of all integers.
static interval_uniont of_interval(intervalt interval)
Construct interval union from a single interval.
NODISCARD 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 ob...
exprt make_contains_expr(const exprt &e) const
Expression which is true exactly when e belongs to the set.
#define NODISCARD
Definition: nodiscard.h:22
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:12