interval_union.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Util
 
Author: Diffblue Limited
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_INTERVAL_UNION_H
#define CPROVER_UTIL_INTERVAL_UNION_H
 
#include <util/interval_template.h>
#include <util/mp_arith.h>
 
#include <optional>
#include <vector>
 
class exprt;
 
class interval_uniont
{
public:
  using intervalt = interval_templatet<mp_integer>;
 
  interval_uniont() = default;
 
  static interval_uniont all_integers();
 
  static interval_uniont greater_or_equal(const mp_integer &value);
 
  static interval_uniont smaller_or_equal(const mp_integer &value);
 
  [[nodiscard]] interval_uniont
  make_intersection(const interval_uniont &other) const;
 
  [[nodiscard]] interval_uniont make_union(const interval_uniont &other) const;
 
  bool is_empty() const;
 
  std::optional<mp_integer> maximum() const;
 
  std::optional<mp_integer> minimum() const;
 
  std::string to_string() const;
 
  static std::optional<interval_uniont> of_string(const std::string &to_parse);
 
  static interval_uniont of_interval(intervalt interval);
 
  exprt make_contains_expr(const exprt &e) const;
 
  std::optional<mp_integer> as_singleton() const;
 
private:
  std::vector<intervalt> intervals;
 
  bool validate() const;
};
 
#endif // CPROVER_UTIL_INTERVAL_UNION_H