BD_Shape_defs.hh

Go to the documentation of this file.

/* BD_Shape 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_BD_Shape_defs_hh
#define PPL_BD_Shape_defs_hh 1

#include "BD_Shape_types.hh"
#include "globals_defs.hh"
#include "Constraint_types.hh"
#include "Generator_types.hh"
#include "Congruence_types.hh"
#include "Linear_Expression_types.hh"
#include "Constraint_System_types.hh"
#include "Generator_System_types.hh"
#include "Congruence_System_types.hh"
#include "Poly_Con_Relation_types.hh"
#include "Poly_Gen_Relation_types.hh"
#include "Polyhedron_types.hh"
#include "Box_types.hh"
#include "Grid_types.hh"
#include "Octagonal_Shape_types.hh"
#include "Variable_defs.hh"
#include "Variables_Set_types.hh"
#include "DB_Matrix_defs.hh"
#include "DB_Row_defs.hh"
#include "Checked_Number_defs.hh"
#include "WRD_coefficient_types_defs.hh"
#include "Bit_Matrix_defs.hh"
#include "Coefficient_defs.hh"
#include "Interval_types.hh"
#include "Linear_Form_types.hh"
#include <cstddef>
#include <iosfwd>
#include <vector>

namespace Parma_Polyhedra_Library {

namespace IO_Operators {


template <typename T>
std::ostream&
operator<<(std::ostream& s, const BD_Shape<T>& bds);

} // namespace IO_Operators


template <typename T>
void swap(BD_Shape<T>& x, BD_Shape<T>& y);


template <typename T>
bool operator==(const BD_Shape<T>& x, const BD_Shape<T>& y);


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


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


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


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


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


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


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


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


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


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

// This class contains some helper functions that need to be friends of
// Linear_Expression.
class BD_Shape_Helpers {
public:
  #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

  #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  static bool extract_bounded_difference(const Constraint& c,
                                         dimension_type& c_num_vars,
                                         dimension_type& c_first_var,
                                         dimension_type& c_second_var,
                                         Coefficient& c_coeff);
};

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
void compute_leader_indices(const std::vector<dimension_type>& predecessor,
                            std::vector<dimension_type>& indices);

} // namespace Parma_Polyhedra_Library


template <typename T>
class Parma_Polyhedra_Library::BD_Shape {
private:
#ifndef NDEBUG
  typedef Checked_Number<T, Debug_WRD_Extended_Number_Policy> N;
#else
  typedef Checked_Number<T, WRD_Extended_Number_Policy> N;
#endif

public:
  typedef T coefficient_type_base;

  typedef N coefficient_type;

  static dimension_type max_space_dimension();

  static bool can_recycle_constraint_systems();

  static bool can_recycle_congruence_systems();




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


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


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


  explicit BD_Shape(const Constraint_System& cs);


  explicit BD_Shape(const Congruence_System& cgs);


  explicit BD_Shape(const Generator_System& gs);


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


  template <typename Interval>
  explicit BD_Shape(const Box<Interval>& box,
                    Complexity_Class complexity = ANY_COMPLEXITY);


  explicit BD_Shape(const Grid& grid,
                    Complexity_Class complexity = ANY_COMPLEXITY);


  template <typename U>
  explicit BD_Shape(const Octagonal_Shape<U>& os,
                    Complexity_Class complexity = ANY_COMPLEXITY);

  BD_Shape& operator=(const BD_Shape& y);

  void m_swap(BD_Shape& y);

  ~BD_Shape();




  dimension_type space_dimension() const;

  dimension_type affine_dimension() const;

  Constraint_System constraints() const;

  Constraint_System minimized_constraints() const;

  Congruence_System congruences() const;

  Congruence_System minimized_congruences() 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 BD_Shape& y) const;


  bool strictly_contains(const BD_Shape& y) const;


  bool is_disjoint_from(const BD_Shape& y) 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 is_empty() const;

  bool is_universe() const;

  bool is_discrete() const;

  bool is_topologically_closed() const;

  bool is_bounded() const;

  bool contains_integer_point() const;

  bool constrains(Variable var) const;

  bool OK() const;




  void add_constraint(const Constraint& c);

  void add_congruence(const Congruence& cg);

  void add_constraints(const Constraint_System& cs);

  void add_recycled_constraints(Constraint_System& cs);

  void add_congruences(const Congruence_System& cgs);

  void add_recycled_congruences(Congruence_System& cgs);

  void refine_with_constraint(const Constraint& c);

  void refine_with_congruence(const Congruence& cg);

  void refine_with_constraints(const Constraint_System& cs);

  void refine_with_congruences(const Congruence_System& cgs);

  template <typename Interval_Info>
  void refine_with_linear_form_inequality(
                   const Linear_Form<Interval<T, Interval_Info> >& left,
                   const Linear_Form<Interval<T, Interval_Info> >& right);

  template <typename Interval_Info>
  void generalized_refine_with_linear_form_inequality(
                   const Linear_Form<Interval<T, Interval_Info> >& left,
                   const Linear_Form<Interval<T, Interval_Info> >& right,
                   Relation_Symbol relsym);


  template <typename U>
  void export_interval_constraints(U& dest) const;

  void unconstrain(Variable var);

  void unconstrain(const Variables_Set& vars);


  void intersection_assign(const BD_Shape& y);

  void upper_bound_assign(const BD_Shape& y);

  bool upper_bound_assign_if_exact(const BD_Shape& y);

  bool integer_upper_bound_assign_if_exact(const BD_Shape& y);

  void difference_assign(const BD_Shape& y);

  bool simplify_using_context_assign(const BD_Shape& y);

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

  // FIXME: To be completed.
  template <typename Interval_Info>
  void affine_form_image(Variable var,
                        const Linear_Form<Interval<T, Interval_Info> >& 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_image(const Linear_Expression& lhs,
                                Relation_Symbol relsym,
                                const Linear_Expression& rhs);

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

  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 BD_Shape& y);

  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);

  void topological_closure_assign();

  void CC76_extrapolation_assign(const BD_Shape& y, unsigned* tp = 0);

  template <typename Iterator>
  void CC76_extrapolation_assign(const BD_Shape& y,
                                 Iterator first, Iterator last,
                                 unsigned* tp = 0);

  void BHMZ05_widening_assign(const BD_Shape& y, unsigned* tp = 0);

  void limited_BHMZ05_extrapolation_assign(const BD_Shape& y,
                                           const Constraint_System& cs,
                                           unsigned* tp = 0);

  void CC76_narrowing_assign(const BD_Shape& y);

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

  void H79_widening_assign(const BD_Shape& y, unsigned* tp = 0);

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

  void limited_H79_extrapolation_assign(const BD_Shape& y,
                                        const Constraint_System& cs,
                                        unsigned* tp = 0);





  void add_space_dimensions_and_embed(dimension_type m);

  void add_space_dimensions_and_project(dimension_type m);

  void concatenate_assign(const BD_Shape& 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);


  template <typename Interval_Info>
  void refine_fp_interval_abstract_store(Box<Interval<T, Interval_Info> >&
                                         store) const;



  PPL_OUTPUT_DECLARATIONS

  bool ascii_load(std::istream& s);

  memory_size_type total_memory_in_bytes() const;

  memory_size_type external_memory_in_bytes() const;

  int32_t hash_code() const;

  friend bool operator==<T>(const BD_Shape<T>& x, const BD_Shape<T>& y);

  template <typename Temp, typename To, typename U>
  friend bool Parma_Polyhedra_Library
  ::rectilinear_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                                const BD_Shape<U>& x, const BD_Shape<U>& y,
                                const Rounding_Dir dir,
                                Temp& tmp0, Temp& tmp1, Temp& tmp2);
  template <typename Temp, typename To, typename U>
  friend bool Parma_Polyhedra_Library
  ::euclidean_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                              const BD_Shape<U>& x, const BD_Shape<U>& y,
                              const Rounding_Dir dir,
                              Temp& tmp0, Temp& tmp1, Temp& tmp2);
  template <typename Temp, typename To, typename U>
  friend bool Parma_Polyhedra_Library
  ::l_infinity_distance_assign(Checked_Number<To, Extended_Number_Policy>& r,
                               const BD_Shape<U>& x, const BD_Shape<U>& y,
                               const Rounding_Dir dir,
                               Temp& tmp0, Temp& tmp1, Temp& tmp2);

private:
  template <typename U> friend class Parma_Polyhedra_Library::BD_Shape;
  template <typename Interval> friend class Parma_Polyhedra_Library::Box;

  DB_Matrix<N> dbm;

#define PPL_IN_BD_Shape_CLASS
#include "BDS_Status_idefs.hh"
#undef PPL_IN_BD_Shape_CLASS

  Status status;

  Bit_Matrix redundancy_dbm;

  bool marked_zero_dim_univ() const;

  bool marked_empty() const;

  bool marked_shortest_path_closed() const;

  bool marked_shortest_path_reduced() const;

  void set_empty();

  void set_zero_dim_univ();

  void set_shortest_path_closed();

  void set_shortest_path_reduced();

  void reset_shortest_path_closed();

  void reset_shortest_path_reduced();

  void shortest_path_closure_assign() const;

  void shortest_path_reduction_assign() const;

  bool is_shortest_path_reduced() const;

  void incremental_shortest_path_closure_assign(Variable var) const;


  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;

  bool BFT00_upper_bound_assign_if_exact(const BD_Shape& y);

  template <bool integer_upper_bound>
  bool BHZ09_upper_bound_assign_if_exact(const BD_Shape& y);

  void refine_no_check(const Constraint& c);

  void refine_no_check(const Congruence& cg);

  void add_dbm_constraint(dimension_type i, dimension_type j, const N& k);

  void add_dbm_constraint(dimension_type i, dimension_type j,
                          Coefficient_traits::const_reference numer,
                          Coefficient_traits::const_reference denom);

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

  void forget_all_dbm_constraints(dimension_type v);
  void forget_binary_dbm_constraints(dimension_type v);


  void deduce_v_minus_u_bounds(dimension_type v,
                               dimension_type last_v,
                               const Linear_Expression& sc_expr,
                               Coefficient_traits::const_reference sc_denom,
                               const N& ub_v);

  template <typename Interval_Info>
  void inhomogeneous_affine_form_image(const dimension_type& var_id,
                                       const Interval<T, Interval_Info>& b);

  template <typename Interval_Info>
  void
  one_variable_affine_form_image(const dimension_type& var_id,
                                 const Interval<T, Interval_Info>& b,
                                 const Interval<T, Interval_Info>& w_coeff,
                                 const dimension_type& w_id,
                                 const dimension_type& space_dim);

  template <typename Interval_Info>
  void
  two_variables_affine_form_image(const dimension_type& var_id,
                                  const Linear_Form<Interval<T,Interval_Info> >& lf,
                                  const dimension_type& space_dim);

  template <typename Interval_Info>
  void
  left_inhomogeneous_refine(const dimension_type& right_t,
                            const dimension_type& right_w_id,
                            const Linear_Form<Interval<T, Interval_Info> >& left,
                            const Linear_Form<Interval<T, Interval_Info> >& right);

  template <typename Interval_Info>
  void
  left_one_var_refine(const dimension_type& left_w_id,
                      const dimension_type& right_t,
                      const dimension_type& right_w_id,
                      const Linear_Form<Interval<T, Interval_Info> >& left,
                      const Linear_Form<Interval<T, Interval_Info> >& right);

  template <typename Interval_Info>
  void general_refine(const dimension_type& left_w_id,
                      const dimension_type& right_w_id,
                      const Linear_Form<Interval<T, Interval_Info> >& left,
                      const Linear_Form<Interval<T, Interval_Info> >& right);

  template <typename Interval_Info>
  void linear_form_upper_bound(const Linear_Form<Interval<T, Interval_Info> >&
                               lf,
                               N& result) const;


  void deduce_u_minus_v_bounds(dimension_type v,
                               dimension_type last_v,
                               const Linear_Expression& sc_expr,
                               Coefficient_traits::const_reference sc_denom,
                               const N& minus_lb_v);

  void get_limiting_shape(const Constraint_System& cs,
                          BD_Shape& limiting_shape) const;


  void compute_predecessors(std::vector<dimension_type>& predecessor) const;


  void compute_leaders(std::vector<dimension_type>& leaders) const;

  void drop_some_non_integer_points_helper(N& elem);

  friend std::ostream&
  Parma_Polyhedra_Library::IO_Operators
  ::operator<<<>(std::ostream& s, const BD_Shape<T>& c);


  void throw_dimension_incompatible(const char* method,
                                    const BD_Shape& 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 Generator& g) const;

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

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

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

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

#include "BDS_Status_inlines.hh"
#include "BD_Shape_inlines.hh"
#include "BD_Shape_templates.hh"

#endif // !defined(PPL_BD_Shape_defs_hh)