Interval.defs.hh

Go to the documentation of this file.

/* Declarations for the Interval class and its constituents.
   Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
   Copyright (C) 2010-2012 BUGSENG srl (http://bugseng.com)

This file is part of the Parma Polyhedra Library (PPL).

The PPL is free software; you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by the
Free Software Foundation; either version 3 of the License, or (at your
option) any later version.

The PPL is distributed in the hope that it will be useful, but WITHOUT
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software Foundation,
Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.

For the most up-to-date information see the Parma Polyhedra Library
site: http://bugseng.com/products/ppl/ . */

#ifndef PPL_Interval_defs_hh
#define PPL_Interval_defs_hh 1

#include "globals.defs.hh"
#include "meta_programming.hh"
#include "assign_or_swap.hh"
#include "intervals.defs.hh"
#include "Interval.types.hh"
#include "Interval_Info.defs.hh"
#include <iosfwd>

// Temporary!
#include <iostream>

namespace Parma_Polyhedra_Library {

enum Ternary { T_YES, T_NO, T_MAYBE };

inline I_Result
combine(Result l, Result u) {
  unsigned res = static_cast<unsigned>(l) | (static_cast<unsigned>(u) << 6);
  return static_cast<I_Result>(res);
}

struct Interval_Base {
};

using namespace Boundary_NS;
using namespace Interval_NS;

template <typename T, typename Enable = void>
struct Is_Singleton : public Is_Native_Or_Checked<T> {};

template <typename T>
struct Is_Interval : public Is_Same_Or_Derived<Interval_Base, T> {};


template <typename Boundary, typename Info>
class Interval : public Interval_Base, private Info {
private:
  PPL_COMPILE_TIME_CHECK(!Info::store_special
                         || !std::numeric_limits<Boundary>::has_infinity,
                         "store_special is meaningless"
                         " when boundary type may contains infinity");
  Info& w_info() const {
    return const_cast<Interval&>(*this);
  }

public:
  typedef Boundary boundary_type;
  typedef Info info_type;

  typedef Interval_NS::Property Property;

  template <typename T>
  typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
  operator=(const T& x) {
    assign(x);
    return *this;
  }

  template <typename T>
  typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
  operator+=(const T& x) {
    add_assign(*this, x);
    return *this;
  }
  template <typename T>
  typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
  operator-=(const T& x) {
    sub_assign(*this, x);
    return *this;
  }
  template <typename T>
  typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
  operator*=(const T& x) {
    mul_assign(*this, x);
    return *this;
  }
  template <typename T>
  typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type
  operator/=(const T& x) {
    div_assign(*this, x);
    return *this;
  }

  void m_swap(Interval& y);

  Info& info() {
    return *this;
  }

  const Info& info() const {
    return *this;
  }

  Boundary& lower() {
    return lower_;
  }

  const Boundary& lower() const {
    return lower_;
  }

  Boundary& upper() {
    return upper_;
  }

  const Boundary& upper() const {
    return upper_;
  }

  I_Constraint<boundary_type> lower_constraint() const {
    PPL_ASSERT(!is_empty());
    if (info().get_boundary_property(LOWER, SPECIAL))
      return I_Constraint<boundary_type>();
    return i_constraint(lower_is_open() ? GREATER_THAN : GREATER_OR_EQUAL,
                        lower(), true);
  }
  I_Constraint<boundary_type> upper_constraint() const {
    PPL_ASSERT(!is_empty());
    if (info().get_boundary_property(UPPER, SPECIAL))
      return I_Constraint<boundary_type>();
    return i_constraint(upper_is_open() ? LESS_THAN : LESS_OR_EQUAL,
                        upper(), true);
  }

  bool is_empty() const {
    return lt(UPPER, upper(), info(), LOWER, lower(), info());
  }

  bool check_empty(I_Result r) const {
    return (r & I_ANY) == I_EMPTY
      || ((r & I_ANY) != I_NOT_EMPTY && is_empty());
  }

  bool is_singleton() const {
    return eq(LOWER, lower(), info(), UPPER, upper(), info());
  }

  bool lower_is_open() const {
    PPL_ASSERT(OK());
    return is_open(LOWER, lower(), info());
  }

  bool upper_is_open() const {
    PPL_ASSERT(OK());
    return is_open(UPPER, upper(), info());
  }

  bool lower_is_boundary_infinity() const {
    PPL_ASSERT(OK());
    return Boundary_NS::is_boundary_infinity(LOWER, lower(), info());
  }

  bool upper_is_boundary_infinity() const {
    PPL_ASSERT(OK());
    return Boundary_NS::is_boundary_infinity(UPPER, upper(), info());
  }

  bool lower_is_domain_inf() const {
    PPL_ASSERT(OK());
    return Boundary_NS::is_domain_inf(LOWER, lower(), info());
  }

  bool upper_is_domain_sup() const {
    PPL_ASSERT(OK());
    return Boundary_NS::is_domain_sup(UPPER, upper(), info());
  }

  bool is_bounded() const {
    PPL_ASSERT(OK());
    return !lower_is_boundary_infinity() && !upper_is_boundary_infinity();
  }

  bool is_universe() const {
    PPL_ASSERT(OK());
    return lower_is_domain_inf() && upper_is_domain_sup();
  }

  I_Result lower_extend() {
    info().clear_boundary_properties(LOWER);
    set_unbounded(LOWER, lower(), info());
    return I_ANY;
  }

  template <typename C>
  typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type
  lower_extend(const C& c);

  I_Result upper_extend() {
    info().clear_boundary_properties(UPPER);
    set_unbounded(UPPER, upper(), info());
    return I_ANY;
  }

  template <typename C>
  typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type
  upper_extend(const C& c);

  I_Result build() {
    return assign(UNIVERSE);
  }

  template <typename C>
  typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type
  build(const C& c) {
    Relation_Symbol rs;
    switch (c.rel()) {
    case V_LGE:
    case V_GT_MINUS_INFINITY:
    case V_LT_PLUS_INFINITY:
      return assign(UNIVERSE);
    default:
      return assign(EMPTY);
    case V_LT:
    case V_LE:
    case V_GT:
    case V_GE:
    case V_EQ:
    case V_NE:
      assign(UNIVERSE);
      rs = static_cast<Relation_Symbol>(c.rel());
      return refine_existential(rs, c.value());
    }
  }

  template <typename C1, typename C2>
  typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C1>::value
                     &&
                     Is_Same_Or_Derived<I_Constraint_Base, C2>::value,
                     I_Result>::type
  build(const C1& c1, const C2& c2) {
    switch (c1.rel()) {
    case V_LGE:
      return build(c2);
    case V_NAN:
      return assign(EMPTY);
    default:
      break;
    }
    switch (c2.rel()) {
    case V_LGE:
      return build(c1);
    case V_NAN:
      return assign(EMPTY);
    default:
      break;
    }
    build(c1);
    I_Result r = add_constraint(c2);
    return r - (I_CHANGED | I_UNCHANGED);
  }

  template <typename C>
  typename Enable_If<Is_Same_Or_Derived<I_Constraint_Base, C>::value, I_Result>::type
  add_constraint(const C& c) {
    Interval x;
    x.build(c);
    return intersect_assign(x);
  }

  I_Result assign(Degenerate_Element e) {
    I_Result r;
    info().clear();
    switch (e) {
    case EMPTY:
      lower_ = 1;
      upper_ = 0;
      r = I_EMPTY | I_EXACT;
      break;
    case UNIVERSE:
      set_unbounded(LOWER, lower(), info());
      set_unbounded(UPPER, upper(), info());
      r = I_UNIVERSE | I_EXACT;
      break;
    default:
      PPL_UNREACHABLE;
      r = I_EMPTY;
      break;
    }
    PPL_ASSERT(OK());
    return r;
  }

  template <typename From>
  typename Enable_If<Is_Special<From>::value, I_Result>::type
  assign(const From&) {
    info().clear();
    Result rl, ru;
    switch (From::vclass) {
    case VC_MINUS_INFINITY:
      rl = Boundary_NS::set_minus_infinity(LOWER, lower(), info());
      ru = Boundary_NS::set_minus_infinity(UPPER, upper(), info());
      break;
    case VC_PLUS_INFINITY:
      rl = Boundary_NS::set_plus_infinity(LOWER, lower(), info());
      ru = Boundary_NS::set_plus_infinity(UPPER, upper(), info());
      break;
    default:
      PPL_UNREACHABLE;
      rl = V_NAN;
      ru = V_NAN;
      break;
    }
    PPL_ASSERT(OK());
    return combine(rl, ru);
  }

  I_Result set_infinities() {
    info().clear();
    Result rl = Boundary_NS::set_minus_infinity(LOWER, lower(), info());
    Result ru = Boundary_NS::set_plus_infinity(UPPER, upper(), info());
    PPL_ASSERT(OK());
    return combine(rl, ru);
  }

  static bool is_always_topologically_closed() {
    return !Info::store_open;
  }

  bool is_topologically_closed() const {
    PPL_ASSERT(OK());
    return is_always_topologically_closed()
      || is_empty()
      || ((lower_is_boundary_infinity() || !lower_is_open())
          && (upper_is_boundary_infinity() || !upper_is_open()));
  }

  void topological_closure_assign() {
    if (!Info::store_open || is_empty())
      return;
    if (lower_is_open() && !lower_is_boundary_infinity())
      info().set_boundary_property(LOWER, OPEN, false);
    if (upper_is_open() && !upper_is_boundary_infinity())
      info().set_boundary_property(UPPER, OPEN, false);
  }

  void remove_inf() {
    PPL_ASSERT(!is_empty());
    if (!Info::store_open)
      return;
    info().set_boundary_property(LOWER, OPEN, true);
  }

  void remove_sup() {
    PPL_ASSERT(!is_empty());
    if (!Info::store_open)
      return;
    info().set_boundary_property(UPPER, OPEN, true);
  }

  int infinity_sign() const {
    PPL_ASSERT(OK());
    if (is_reverse_infinity(LOWER, lower(), info()))
      return 1;
    else if (is_reverse_infinity(UPPER, upper(), info()))
      return -1;
    else
      return 0;
  }

  bool contains_integer_point() const {
    PPL_ASSERT(OK());
    if (is_empty())
      return false;
    if (!is_bounded())
      return true;
    Boundary l;
    if (lower_is_open()) {
      add_assign_r(l, lower(), Boundary(1), ROUND_DOWN);
      floor_assign_r(l, l, ROUND_DOWN);
    }
    else
      ceil_assign_r(l, lower(), ROUND_DOWN);
    Boundary u;
    if (upper_is_open()) {
      sub_assign_r(u, upper(), Boundary(1), ROUND_UP);
      ceil_assign_r(u, u, ROUND_UP);
    }
    else
      floor_assign_r(u, upper(), ROUND_UP);
    return u >= l;
  }

  void drop_some_non_integer_points() {
    if (is_empty())
      return;
    if (lower_is_open() && !lower_is_boundary_infinity()) {
      add_assign_r(lower(), lower(), Boundary(1), ROUND_DOWN);
      floor_assign_r(lower(), lower(), ROUND_DOWN);
      info().set_boundary_property(LOWER, OPEN, false);
    }
    else
      ceil_assign_r(lower(), lower(), ROUND_DOWN);
    if (upper_is_open() && !upper_is_boundary_infinity()) {
      sub_assign_r(upper(), upper(), Boundary(1), ROUND_UP);
      ceil_assign_r(upper(), upper(), ROUND_UP);
      info().set_boundary_property(UPPER, OPEN, false);
    }
    else
      floor_assign_r(upper(), upper(), ROUND_UP);
  }

  template <typename From>
  typename Enable_If<Is_Singleton<From>::value || Is_Interval<From>::value, I_Result>::type
  wrap_assign(Bounded_Integer_Type_Width w,
              Bounded_Integer_Type_Representation r,
              const From& refinement) {
    if (is_empty())
      return I_EMPTY;
    if (lower_is_boundary_infinity() || upper_is_boundary_infinity())
      return assign(refinement);
    PPL_DIRTY_TEMP(Boundary, u);
    Result result = sub_2exp_assign_r(u, upper(), w, ROUND_UP);
    if (result_overflow(result) == 0 && u > lower())
      return assign(refinement);
    info().clear();
    switch (r) {
    case UNSIGNED:
      umod_2exp_assign(LOWER, lower(), info(),
                       LOWER, lower(), info(), w);
      umod_2exp_assign(UPPER, upper(), info(),
                       UPPER, upper(), info(), w);
      break;
    case SIGNED_2_COMPLEMENT:
      smod_2exp_assign(LOWER, lower(), info(),
                       LOWER, lower(), info(), w);
      smod_2exp_assign(UPPER, upper(), info(),
                       UPPER, upper(), info(), w);
      break;
    default:
      PPL_UNREACHABLE;
      break;
    }
    if (le(LOWER, lower(), info(), UPPER, upper(), info()))
      return intersect_assign(refinement);
    PPL_DIRTY_TEMP(Interval, tmp);
    tmp.info().clear();
    Boundary_NS::assign(LOWER, tmp.lower(), tmp.info(),
                        LOWER, lower(), info());
    set_unbounded(UPPER, tmp.upper(), tmp.info());
    tmp.intersect_assign(refinement);
    lower_extend();
    intersect_assign(refinement);
    return join_assign(tmp);
  }

  memory_size_type total_memory_in_bytes() const;

  memory_size_type external_memory_in_bytes() const;

  void ascii_dump(std::ostream& s) const;
  bool ascii_load(std::istream& s);

  bool OK() const {
#if 0
    if (!Info::may_be_empty && is_empty()) {
#ifndef NDEBUG
        std::cerr << "The interval is unexpectedly empty.\n";
#endif
        return false;
    }
#endif

    if (is_open(LOWER, lower(), info())) {
      if (is_plus_infinity(LOWER, lower(), info())) {
#ifndef NDEBUG
        std::cerr << "The lower boundary is +inf open.\n";
#endif
      }
    }
    else if (!Info::may_contain_infinity
             && (is_minus_infinity(LOWER, lower(), info())
                 || is_plus_infinity(LOWER, lower(), info()))) {
#ifndef NDEBUG
      std::cerr << "The lower boundary is unexpectedly infinity.\n";
#endif
      return false;
    }
    if (!info().get_boundary_property(LOWER, SPECIAL)) {
      if (is_not_a_number(lower())) {
#ifndef NDEBUG
        std::cerr << "The lower boundary is not a number.\n";
#endif
        return false;
      }
    }

    if (is_open(UPPER, upper(), info())) {
      if (is_minus_infinity(UPPER, upper(), info())) {
#ifndef NDEBUG
        std::cerr << "The upper boundary is -inf open.\n";
#endif
      }
    }
    else if (!Info::may_contain_infinity
             && (is_minus_infinity(UPPER, upper(), info())
                 || is_plus_infinity(UPPER, upper(), info()))) {
#ifndef NDEBUG
      std::cerr << "The upper boundary is unexpectedly infinity."
                << std::endl;
#endif
      return false;
    }
    if (!info().get_boundary_property(UPPER, SPECIAL)) {
      if (is_not_a_number(upper())) {
#ifndef NDEBUG
        std::cerr << "The upper boundary is not a number.\n";
#endif
        return false;
      }
    }

    // Everything OK.
    return true;
  }

  Interval() {
  }

  template <typename T>
  explicit Interval(const T& x) {
    assign(x);
  }

  explicit Interval(const char* s);

  template <typename T>
  typename Enable_If<Is_Singleton<T>::value
                     || Is_Interval<T>::value, bool>::type
  contains(const T& y) const;

  template <typename T>
  typename Enable_If<Is_Singleton<T>::value
                     || Is_Interval<T>::value, bool>::type
  strictly_contains(const T& y) const;

  template <typename T>
  typename Enable_If<Is_Singleton<T>::value
                     || Is_Interval<T>::value, bool>::type
  is_disjoint_from(const T& y) const;


  template <typename From>
  typename Enable_If<Is_Singleton<From>::value
                     || Is_Interval<From>::value, I_Result>::type
  assign(const From& x);

  template <typename Type>
  typename Enable_If<Is_Singleton<Type>::value
                     || Is_Interval<Type>::value, bool>::type
  can_be_exactly_joined_to(const Type& x) const;

  template <typename From>
  typename Enable_If<Is_Singleton<From>::value
                     || Is_Interval<From>::value, I_Result>::type
  join_assign(const From& x);

  template <typename From1, typename From2>
  typename Enable_If<((Is_Singleton<From1>::value
                       || Is_Interval<From1>::value)
                      && (Is_Singleton<From2>::value
                          || Is_Interval<From2>::value)), I_Result>::type
  join_assign(const From1& x, const From2& y);

  template <typename From>
  typename Enable_If<Is_Singleton<From>::value
                     || Is_Interval<From>::value, I_Result>::type
  intersect_assign(const From& x);

  template <typename From1, typename From2>
  typename Enable_If<((Is_Singleton<From1>::value
                       || Is_Interval<From1>::value)
                      && (Is_Singleton<From2>::value
                          || Is_Interval<From2>::value)), I_Result>::type
  intersect_assign(const From1& x, const From2& y);

  template <typename From>
  typename Enable_If<Is_Singleton<From>::value
                     || Is_Interval<From>::value, I_Result>::type
  difference_assign(const From& x);

  template <typename From1, typename From2>
  typename Enable_If<((Is_Singleton<From1>::value
                       || Is_Interval<From1>::value)
                      && (Is_Singleton<From2>::value
                          || Is_Interval<From2>::value)), I_Result>::type
  difference_assign(const From1& x, const From2& y);

  template <typename From>
  typename Enable_If<Is_Singleton<From>::value
                     || Is_Interval<From>::value, I_Result>::type
  lower_approximation_difference_assign(const From& x);

  template <typename From>
  typename Enable_If<Is_Interval<From>::value, bool>::type
  simplify_using_context_assign(const From& y);

  template <typename From>
  typename Enable_If<Is_Interval<From>::value, void>::type
  empty_intersection_assign(const From& y);

  template <typename From>
  typename Enable_If<Is_Singleton<From>::value
                     || Is_Interval<From>::value, I_Result>::type
  refine_existential(Relation_Symbol rel, const From& x);

  template <typename From>
  typename Enable_If<Is_Singleton<From>::value
                     || Is_Interval<From>::value, I_Result>::type
  refine_universal(Relation_Symbol rel, const From& x);

  template <typename From>
  typename Enable_If<Is_Singleton<From>::value
                     || Is_Interval<From>::value, I_Result>::type
  neg_assign(const From& x);

  template <typename From1, typename From2>
  typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value)
                      && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type
  add_assign(const From1& x, const From2& y);

  template <typename From1, typename From2>
  typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value)
                      && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type
  sub_assign(const From1& x, const From2& y);

  template <typename From1, typename From2>
  typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value)
                      && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type
  mul_assign(const From1& x, const From2& y);

  template <typename From1, typename From2>
  typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value)
                      && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type
  div_assign(const From1& x, const From2& y);

  template <typename From, typename Iterator>
  typename Enable_If<Is_Interval<From>::value, void>::type
  CC76_widening_assign(const From& y, Iterator first, Iterator last);

private:
  Boundary lower_;
  Boundary upper_;
};


template <typename Boundary, typename Info>
void swap(Interval<Boundary, Info>& x, Interval<Boundary, Info>& y);

} // namespace Parma_Polyhedra_Library

#include "Interval.inlines.hh"
#include "Interval.templates.hh"

#endif // !defined(PPL_Interval_defs_hh)