Box_defs.hh

Go to the documentation of this file.

/* Box class declaration.
   Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
   Copyright (C) 2010-2016 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_Box_defs_hh
#define PPL_Box_defs_hh 1

#include "Box_types.hh"
#include "globals_types.hh"
#include "Coefficient_defs.hh"
#include "Variable_types.hh"
#include "Variables_Set_types.hh"
#include "Linear_Expression_types.hh"
#include "Constraint_types.hh"
#include "Constraint_defs.hh"
#include "Constraint_System_types.hh"
#include "Generator_types.hh"
#include "Generator_System_types.hh"
#include "Congruence_types.hh"
#include "Congruence_System_types.hh"
#include "BD_Shape_types.hh"
#include "Octagonal_Shape_types.hh"
#include "Poly_Con_Relation_types.hh"
#include "Poly_Gen_Relation_types.hh"
#include "Polyhedron_types.hh"
#include "Grid_types.hh"
#include "Partially_Reduced_Product_types.hh"
#include "intervals_defs.hh"
#include "Interval_types.hh"
#include "Linear_Form_types.hh"
#include <vector>
#include <iosfwd>

namespace Parma_Polyhedra_Library {

struct Interval_Base;


template <typename ITV>
void swap(Box<ITV>& x, Box<ITV>& y);


template <typename ITV>
bool operator==(const Box<ITV>& x, const Box<ITV>& y);


template <typename ITV>
bool operator!=(const Box<ITV>& x, const Box<ITV>& y);

namespace IO_Operators {


template <typename ITV>
std::ostream& operator<<(std::ostream& s, const Box<ITV>& box);

} // namespace IO_Operators


template <typename To, typename ITV>
bool
rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                            const Box<ITV>& x,
                            const Box<ITV>& y,
                            Rounding_Dir dir);


template <typename Temp, typename To, typename ITV>
bool
rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                            const Box<ITV>& x,
                            const Box<ITV>& y,
                            Rounding_Dir dir);


template <typename Temp, typename To, typename ITV>
bool
rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                            const Box<ITV>& x,
                            const Box<ITV>& y,
                            Rounding_Dir dir,
                            Temp& tmp0,
                            Temp& tmp1,
                            Temp& tmp2);


template <typename To, typename ITV>
bool
euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                          const Box<ITV>& x,
                          const Box<ITV>& y,
                          Rounding_Dir dir);


template <typename Temp, typename To, typename ITV>
bool
euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                          const Box<ITV>& x,
                          const Box<ITV>& y,
                          Rounding_Dir dir);


template <typename Temp, typename To, typename ITV>
bool
euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                          const Box<ITV>& x,
                          const Box<ITV>& y,
                          Rounding_Dir dir,
                          Temp& tmp0,
                          Temp& tmp1,
                          Temp& tmp2);


template <typename To, typename ITV>
bool
l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                           const Box<ITV>& x,
                           const Box<ITV>& y,
                           Rounding_Dir dir);


template <typename Temp, typename To, typename ITV>
bool
l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                           const Box<ITV>& x,
                           const Box<ITV>& y,
                           Rounding_Dir dir);


template <typename Temp, typename To, typename ITV>
bool
l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                           const Box<ITV>& x,
                           const Box<ITV>& y,
                           Rounding_Dir dir,
                           Temp& tmp0,
                           Temp& tmp1,
                           Temp& tmp2);

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
template <typename Specialization,
          typename Temp, typename To, typename ITV>
bool
l_m_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                    const Box<ITV>& x, const Box<ITV>& y,
                    Rounding_Dir dir,
                    Temp& tmp0, Temp& tmp1, Temp& tmp2);

} // namespace Parma_Polyhedra_Library


template <typename ITV>
class Parma_Polyhedra_Library::Box {
public:
  typedef ITV interval_type;

  static dimension_type max_space_dimension();

  static bool can_recycle_constraint_systems();

  static bool can_recycle_congruence_systems();




  explicit Box(dimension_type num_dimensions = 0,
               Degenerate_Element kind = UNIVERSE);


  Box(const Box& y,
      Complexity_Class complexity = ANY_COMPLEXITY);


  template <typename Other_ITV>
  explicit Box(const Box<Other_ITV>& y,
               Complexity_Class complexity = ANY_COMPLEXITY);


  explicit Box(const Constraint_System& cs);


  Box(const Constraint_System& cs, Recycle_Input dummy);


  explicit Box(const Generator_System& gs);


  Box(const Generator_System& gs, Recycle_Input dummy);

  explicit Box(const Congruence_System& cgs);

  Box(const Congruence_System& cgs, Recycle_Input dummy);


  template <typename T>
  explicit Box(const BD_Shape<T>& bds,
               Complexity_Class complexity = POLYNOMIAL_COMPLEXITY);


  template <typename T>
  explicit Box(const Octagonal_Shape<T>& oct,
               Complexity_Class complexity = POLYNOMIAL_COMPLEXITY);


  explicit Box(const Polyhedron& ph,
               Complexity_Class complexity = ANY_COMPLEXITY);


  explicit Box(const Grid& gr,
               Complexity_Class complexity = POLYNOMIAL_COMPLEXITY);


  template <typename D1, typename D2, typename R>
  explicit Box(const Partially_Reduced_Product<D1, D2, R>& dp,
               Complexity_Class complexity = ANY_COMPLEXITY);

  Box& operator=(const Box& y);

  void m_swap(Box& y);




  dimension_type space_dimension() const;

  dimension_type affine_dimension() const;

  bool is_empty() const;

  bool is_universe() const;

  bool is_topologically_closed() const;

  bool is_discrete() const;

  bool is_bounded() const;

  bool contains_integer_point() const;

  bool constrains(Variable var) const;


  Poly_Con_Relation relation_with(const Constraint& c) const;


  Poly_Con_Relation relation_with(const Congruence& cg) const;


  Poly_Gen_Relation relation_with(const Generator& g) const;

  bool bounds_from_above(const Linear_Expression& expr) const;

  bool bounds_from_below(const Linear_Expression& expr) const;

  bool maximize(const Linear_Expression& expr,
                Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;

  bool maximize(const Linear_Expression& expr,
                Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
                Generator& g) const;

  bool minimize(const Linear_Expression& expr,
                Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;

  bool minimize(const Linear_Expression& expr,
                Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
                Generator& g) const;

  bool frequency(const Linear_Expression& expr,
                 Coefficient& freq_n, Coefficient& freq_d,
                 Coefficient& val_n, Coefficient& val_d) const;

  bool contains(const Box& y) const;

  bool strictly_contains(const Box& y) const;

  bool is_disjoint_from(const Box& y) const;

  bool OK() const;




  void add_constraint(const Constraint& c);

  void add_constraints(const Constraint_System& cs);

  void add_recycled_constraints(Constraint_System& cs);

  void add_congruence(const Congruence& cg);

  void add_congruences(const Congruence_System& cgs);

  void add_recycled_congruences(Congruence_System& cgs);

  void refine_with_constraint(const Constraint& c);

  void refine_with_constraints(const Constraint_System& cs);

  void refine_with_congruence(const Congruence& cg);

  void refine_with_congruences(const Congruence_System& cgs);

  void propagate_constraint(const Constraint& c);

  void propagate_constraints(const Constraint_System& cs,
                             dimension_type max_iterations = 0);

  void unconstrain(Variable var);

  void unconstrain(const Variables_Set& vars);


  void intersection_assign(const Box& y);

  void upper_bound_assign(const Box& y);

  bool upper_bound_assign_if_exact(const Box& y);

  void difference_assign(const Box& y);

  bool simplify_using_context_assign(const Box& y);

  void affine_image(Variable var,
                    const Linear_Expression& expr,
                    Coefficient_traits::const_reference denominator
                      = Coefficient_one());

  // FIXME: To be completed.
  void affine_form_image(Variable var,
                         const Linear_Form<ITV>& lf);

  void affine_preimage(Variable var,
                       const Linear_Expression& expr,
                       Coefficient_traits::const_reference denominator
                         = Coefficient_one());

  void generalized_affine_image(Variable var,
                                Relation_Symbol relsym,
                                const Linear_Expression& expr,
                                Coefficient_traits::const_reference denominator
                                  = Coefficient_one());

  void
  generalized_affine_preimage(Variable var,
                              Relation_Symbol relsym,
                              const Linear_Expression& expr,
                              Coefficient_traits::const_reference denominator
                              = Coefficient_one());

  void generalized_affine_image(const Linear_Expression& lhs,
                                Relation_Symbol relsym,
                                const Linear_Expression& rhs);

  void generalized_affine_preimage(const Linear_Expression& lhs,
                                   Relation_Symbol relsym,
                                   const Linear_Expression& rhs);

  void bounded_affine_image(Variable var,
                            const Linear_Expression& lb_expr,
                            const Linear_Expression& ub_expr,
                            Coefficient_traits::const_reference denominator
                            = Coefficient_one());

  void bounded_affine_preimage(Variable var,
                               const Linear_Expression& lb_expr,
                               const Linear_Expression& ub_expr,
                               Coefficient_traits::const_reference denominator
                               = Coefficient_one());

  void time_elapse_assign(const Box& y);

  void topological_closure_assign();

  void wrap_assign(const Variables_Set& vars,
                   Bounded_Integer_Type_Width w,
                   Bounded_Integer_Type_Representation r,
                   Bounded_Integer_Type_Overflow o,
                   const Constraint_System* cs_p = 0,
                   unsigned complexity_threshold = 16,
                   bool wrap_individually = true);

  void drop_some_non_integer_points(Complexity_Class complexity
                                    = ANY_COMPLEXITY);

  void drop_some_non_integer_points(const Variables_Set& vars,
                                    Complexity_Class complexity
                                    = ANY_COMPLEXITY);

  template <typename T>
  typename Enable_If<Is_Same<T, Box>::value
                     && Is_Same_Or_Derived<Interval_Base, ITV>::value,
                     void>::type
  CC76_widening_assign(const T& y, unsigned* tp = 0);

  template <typename T, typename Iterator>
  typename Enable_If<Is_Same<T, Box>::value
                     && Is_Same_Or_Derived<Interval_Base, ITV>::value,
                     void>::type
  CC76_widening_assign(const T& y,
                       Iterator first, Iterator last);

  void widening_assign(const Box& y, unsigned* tp = 0);

  void limited_CC76_extrapolation_assign(const Box& y,
                                         const Constraint_System& cs,
                                         unsigned* tp = 0);

  template <typename T>
  typename Enable_If<Is_Same<T, Box>::value
                     && Is_Same_Or_Derived<Interval_Base, ITV>::value,
                     void>::type
  CC76_narrowing_assign(const T& y);





  void add_space_dimensions_and_embed(dimension_type m);

  void add_space_dimensions_and_project(dimension_type m);

  void concatenate_assign(const Box& y);


  void remove_space_dimensions(const Variables_Set& vars);

  void remove_higher_space_dimensions(dimension_type new_dimension);

  template <typename Partial_Function>
  void map_space_dimensions(const Partial_Function& pfunc);


  void expand_space_dimension(Variable var, dimension_type m);


  void fold_space_dimensions(const Variables_Set& vars, Variable dest);


  const ITV& get_interval(Variable var) const;

  void set_interval(Variable var, const ITV& i);

  bool has_lower_bound(Variable var,
                       Coefficient& n, Coefficient& d, bool& closed) const;

  bool has_upper_bound(Variable var,
                       Coefficient& n, Coefficient& d, bool& closed) const;

  Constraint_System constraints() const;

  Constraint_System minimized_constraints() const;

  Congruence_System congruences() const;

  Congruence_System minimized_congruences() const;

  memory_size_type total_memory_in_bytes() const;

  memory_size_type external_memory_in_bytes() const;

  int32_t hash_code() const;

  PPL_OUTPUT_DECLARATIONS

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  bool ascii_load(std::istream& s);

private:
  template <typename Other_ITV>
  friend class Parma_Polyhedra_Library::Box;

  friend bool
  operator==<ITV>(const Box<ITV>& x, const Box<ITV>& y);

  friend std::ostream&
  Parma_Polyhedra_Library
  ::IO_Operators::operator<<<>(std::ostream& s, const Box<ITV>& box);

  template <typename Specialization, typename Temp, typename To, typename I>
  friend bool Parma_Polyhedra_Library
  ::l_m_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                        const Box<I>& x, const Box<I>& y,
                        const Rounding_Dir dir,
                        Temp& tmp0, Temp& tmp1, Temp& tmp2);

  typedef std::vector<ITV> Sequence;

  typedef ITV Tmp_Interval_Type;

  Sequence seq;

#define PPL_IN_Box_CLASS
#include "Box_Status_idefs.hh"
#undef PPL_IN_Box_CLASS

  Status status;

  bool marked_empty() const;

public:
  void set_empty();

private:
  void set_nonempty();

  void set_empty_up_to_date();

  void reset_empty_up_to_date();

  bool check_empty() const;

  const ITV& operator[](dimension_type k) const;

  static I_Result
  refine_interval_no_check(ITV& itv,
                           Constraint::Type type,
                           Coefficient_traits::const_reference numer,
                           Coefficient_traits::const_reference denom);

  void
  add_interval_constraint_no_check(dimension_type var_id,
                                   Constraint::Type type,
                                   Coefficient_traits::const_reference numer,
                                   Coefficient_traits::const_reference denom);

  void add_constraint_no_check(const Constraint& c);

  void add_constraints_no_check(const Constraint_System& cs);

  void add_congruence_no_check(const Congruence& cg);

  void add_congruences_no_check(const Congruence_System& cgs);

  void refine_no_check(const Constraint& c);

  void refine_no_check(const Constraint_System& cs);

  void refine_no_check(const Congruence& cg);

  void refine_no_check(const Congruence_System& cgs);

  void propagate_constraint_no_check(const Constraint& c);

  void propagate_constraints_no_check(const Constraint_System& cs,
                                      dimension_type max_iterations);


  bool bounds(const Linear_Expression& expr, bool from_above) const;


  bool max_min(const Linear_Expression& expr,
               bool maximize,
               Coefficient& ext_n, Coefficient& ext_d, bool& included,
               Generator& g) const;


  bool max_min(const Linear_Expression& expr,
               bool maximize,
               Coefficient& ext_n, Coefficient& ext_d, bool& included) const;

  void get_limiting_box(const Constraint_System& cs,
                        Box& limiting_box) const;


  void throw_dimension_incompatible(const char* method,
                                    const Box& y) const;

  void throw_dimension_incompatible(const char* method,
                                    dimension_type required_dim) const;

  void throw_dimension_incompatible(const char* method,
                                    const Constraint& c) const;

  void throw_dimension_incompatible(const char* method,
                                    const Congruence& cg) const;

  void throw_dimension_incompatible(const char* method,
                                    const Constraint_System& cs) const;

  void throw_dimension_incompatible(const char* method,
                                    const Congruence_System& cgs) const;

  void throw_dimension_incompatible(const char* method,
                                    const Generator& g) const;

  void throw_dimension_incompatible(const char* method,
                                    const char* le_name,
                                    const Linear_Expression& le) const;

  template <typename C>
  void throw_dimension_incompatible(const char* method,
                                    const char* lf_name,
                                    const Linear_Form<C>& lf) const;

  static void throw_constraint_incompatible(const char* method);

  static void throw_expression_too_complex(const char* method,
                                           const Linear_Expression& le);

  static void throw_invalid_argument(const char* method, const char* reason);
};

namespace Parma_Polyhedra_Library {

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
template <typename ITV>
Poly_Con_Relation
interval_relation(const ITV& i,
                  const Constraint::Type constraint_type,
                  Coefficient_traits::const_reference numer,
                  Coefficient_traits::const_reference denom
                  = Coefficient_one());

class Box_Helpers {
public:
  // This is declared here so that Linear_Expression needs to be friend of
  // Box_Helpers only, and doesn't need to be friend of this, too.
  #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

  #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  static bool extract_interval_constraint(const Constraint& c,
                                          dimension_type& c_num_vars,
                                          dimension_type& c_only_var);

  // This is declared here so that Linear_Expression needs to be friend of
  // Box_Helpers only, and doesn't need to be friend of this, too.
  static bool extract_interval_congruence(const Congruence& cg,
                                          dimension_type& cg_num_vars,
                                          dimension_type& cg_only_var);
};

} // namespace Parma_Polyhedra_Library

#include "Box_Status_inlines.hh"
#include "Box_inlines.hh"
#include "Box_templates.hh"

#endif // !defined(PPL_Box_defs_hh)