Grid_defs.hh

Go to the documentation of this file.

/* Grid 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_Grid_defs_hh
#define PPL_Grid_defs_hh 1

#include "Grid_types.hh"
#include "globals_defs.hh"
#include "Variable_defs.hh"
#include "Variables_Set_types.hh"
#include "Linear_Expression_defs.hh"
#include "Constraint_types.hh"
#include "Constraint_System_defs.hh"
#include "Constraint_System_inlines.hh"
#include "Congruence_System_defs.hh"
#include "Congruence_System_inlines.hh"
#include "Grid_Generator_System_defs.hh"
#include "Grid_Generator_System_inlines.hh"
#include "Grid_Generator_types.hh"
#include "Poly_Con_Relation_defs.hh"
#include "Poly_Gen_Relation_defs.hh"
#include "Grid_Certificate_types.hh"
#include "Box_types.hh"
#include "Polyhedron_types.hh"
#include "BD_Shape_types.hh"
#include "Octagonal_Shape_types.hh"
#include <vector>
#include <iosfwd>

namespace Parma_Polyhedra_Library {

namespace IO_Operators {


std::ostream&
operator<<(std::ostream& s, const Grid& gr);

} // namespace IO_Operators


void swap(Grid& x, Grid& y);

bool operator==(const Grid& x, const Grid& y);

bool operator!=(const Grid& x, const Grid& y);

} // namespace Parma_Polyhedra_Library



class Parma_Polyhedra_Library::Grid {
public:
  typedef Coefficient coefficient_type;

  static dimension_type max_space_dimension();

  static bool can_recycle_congruence_systems();

  static bool can_recycle_constraint_systems();


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


  explicit Grid(const Congruence_System& cgs);


  Grid(Congruence_System& cgs, Recycle_Input dummy);


  explicit Grid(const Constraint_System& cs);


  Grid(Constraint_System& cs, Recycle_Input dummy);


  explicit Grid(const Grid_Generator_System& ggs);


  Grid(Grid_Generator_System& ggs, Recycle_Input dummy);


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


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


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

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


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

  Grid& operator=(const Grid& y);



  dimension_type space_dimension() const;

  dimension_type affine_dimension() const;

  Constraint_System constraints() const;

  Constraint_System minimized_constraints() const;

  const Congruence_System& congruences() const;

  const Congruence_System& minimized_congruences() const;

  const Grid_Generator_System& grid_generators() const;

  const Grid_Generator_System& minimized_grid_generators() const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and congruence \p cg are dimension-incompatible.
  */
  // FIXME: Poly_Con_Relation seems to encode exactly what we want
  // here.  We must find a new name for that class.  Temporarily,
  // we keep using it without changing the name.
  Poly_Con_Relation relation_with(const Congruence& cg) const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and generator \p g are dimension-incompatible.
  */
  // FIXME: see the comment for Poly_Con_Relation above.
  Poly_Gen_Relation
  relation_with(const Grid_Generator& g) const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and generator \p g are dimension-incompatible.
  */
  // FIXME: see the comment for Poly_Con_Relation above.
  Poly_Gen_Relation
  relation_with(const Generator& g) const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and constraint \p c are dimension-incompatible.
  */
  // FIXME: Poly_Con_Relation seems to encode exactly what we want
  // here.  We must find a new name for that class.  Temporarily,
  // we keep using it without changing the name.
  Poly_Con_Relation relation_with(const Constraint& c) const;

  bool is_empty() const;

  bool is_universe() const;

  bool is_topologically_closed() const;

  bool is_disjoint_from(const Grid& y) const;


  bool is_discrete() const;

  bool is_bounded() const;

  bool contains_integer_point() const;

  bool constrains(Variable var) 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& point) 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& point) const;

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


  bool contains(const Grid& y) const;

  bool strictly_contains(const Grid& y) const;


  bool OK(bool check_not_empty = false) const;





  void add_congruence(const Congruence& cg);

  void add_grid_generator(const Grid_Generator& g);


  void add_congruences(const Congruence_System& cgs);


  void add_recycled_congruences(Congruence_System& cgs);

  void add_constraint(const Constraint& c);

  void add_constraints(const Constraint_System& cs);

  void add_recycled_constraints(Constraint_System& cs);


  void refine_with_congruence(const Congruence& cg);


  void refine_with_congruences(const Congruence_System& cgs);


  void refine_with_constraint(const Constraint& c);


  void refine_with_constraints(const Constraint_System& cs);

  void add_grid_generators(const Grid_Generator_System& gs);

  void add_recycled_grid_generators(Grid_Generator_System& gs);

  void unconstrain(Variable var);

  void unconstrain(const Variables_Set& vars);

  void intersection_assign(const Grid& y);

  void upper_bound_assign(const Grid& y);

  bool upper_bound_assign_if_exact(const Grid& y);

  void difference_assign(const Grid& y);

  bool simplify_using_context_assign(const Grid& y);

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

  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(),
                           Coefficient_traits::const_reference modulus
                           = Coefficient_zero());

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

  void
  generalized_affine_image(const Linear_Expression& lhs,
                           Relation_Symbol relsym,
                           const Linear_Expression& rhs,
                           Coefficient_traits::const_reference modulus
                           = Coefficient_zero());

  void
  generalized_affine_preimage(const Linear_Expression& lhs,
                              Relation_Symbol relsym,
                              const Linear_Expression& rhs,
                              Coefficient_traits::const_reference modulus
                              = Coefficient_zero());

  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 Grid& 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 congruence_widening_assign(const Grid& y, unsigned* tp = NULL);

  void generator_widening_assign(const Grid& y, unsigned* tp = NULL);

  void widening_assign(const Grid& y, unsigned* tp = NULL);

  void limited_congruence_extrapolation_assign(const Grid& y,
                                               const Congruence_System& cgs,
                                               unsigned* tp = NULL);

  void limited_generator_extrapolation_assign(const Grid& y,
                                              const Congruence_System& cgs,
                                              unsigned* tp = NULL);

  void limited_extrapolation_assign(const Grid& y,
                                    const Congruence_System& cgs,
                                    unsigned* tp = NULL);




  void add_space_dimensions_and_embed(dimension_type m);

  void add_space_dimensions_and_project(dimension_type m);

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


  friend bool operator==(const Grid& x, const Grid& y);

  friend class Parma_Polyhedra_Library::Grid_Certificate;

  template <typename Interval> friend class Parma_Polyhedra_Library::Box;



  ~Grid();

  void m_swap(Grid& y);

  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;


private:

  Congruence_System con_sys;

  Grid_Generator_System gen_sys;

#define PPL_IN_Grid_CLASS
#include "Grid_Status_idefs.hh"
#undef PPL_IN_Grid_CLASS

  Status status;

  dimension_type space_dim;

  enum Dimension_Kind {
    PARAMETER = 0,
    LINE = 1,
    GEN_VIRTUAL = 2,
    PROPER_CONGRUENCE = PARAMETER,
    CON_VIRTUAL = LINE,
    EQUALITY = GEN_VIRTUAL
  };

  typedef std::vector<Dimension_Kind> Dimension_Kinds;

  // The type of row associated with each dimension.  If the virtual
  // rows existed then the reduced systems would be square and upper
  // or lower triangular, and the rows in each would have the types
  // given in this vector.  As the congruence system is reduced to an
  // upside-down lower triangular form the ordering of the congruence
  // types is last to first.
  Dimension_Kinds dim_kinds;


  void construct(dimension_type num_dimensions, Degenerate_Element kind);


  void construct(Congruence_System& cgs);


  void construct(Grid_Generator_System& ggs);




  bool marked_empty() const;

  bool congruences_are_up_to_date() const;

  bool generators_are_up_to_date() const;

  bool congruences_are_minimized() const;

  bool generators_are_minimized() const;




  void set_zero_dim_univ();

  void set_empty();

  void set_congruences_up_to_date();

  void set_generators_up_to_date();

  void set_congruences_minimized();

  void set_generators_minimized();




  void clear_empty();

  void clear_congruences_up_to_date();

  void clear_generators_up_to_date();

  void clear_congruences_minimized();

  void clear_generators_minimized();




  void update_congruences() const;


  bool update_generators() const;





  bool minimize() const;


  enum Three_Valued_Boolean {
    TVB_TRUE,
    TVB_FALSE,
    TVB_DONT_KNOW
  };

  Three_Valued_Boolean quick_equivalence_test(const Grid& y) const;

  bool is_included_in(const Grid& y) const;


  bool bounds(const Linear_Expression& expr, const char* method_call) const;


  bool max_min(const Linear_Expression& expr,
               const char* method_call,
               Coefficient& ext_n, Coefficient& ext_d, bool& included,
               Generator* point = NULL) const;

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


  bool bounds_no_check(const Linear_Expression& expr) const;

  void add_congruence_no_check(const Congruence& cg);

  void add_constraint_no_check(const Constraint& c);

  void refine_no_check(const Constraint& c);



  void select_wider_congruences(const Grid& y,
                                Congruence_System& selected_cgs) const;

  void select_wider_generators(const Grid& y,
                               Grid_Generator_System& widened_ggs) const;



  void add_space_dimensions(Congruence_System& cgs,
                            Grid_Generator_System& gs,
                            dimension_type dims);


  void add_space_dimensions(Grid_Generator_System& gs,
                            Congruence_System& cgs,
                            dimension_type dims);




  static void
  normalize_divisors(Grid_Generator_System& sys,
                     Coefficient& divisor,
                     const Grid_Generator* first_point = NULL);


  static void
  normalize_divisors(Grid_Generator_System& sys);


  static void normalize_divisors(Grid_Generator_System& sys,
                                 Grid_Generator_System& gen_sys);

  static void conversion(Congruence_System& source,
                         Grid_Generator_System& dest,
                         Dimension_Kinds& dim_kinds);

  static void conversion(Grid_Generator_System& source,
                         Congruence_System& dest,
                         Dimension_Kinds& dim_kinds);


  static bool simplify(Congruence_System& cgs,
                       Dimension_Kinds& dim_kinds);


  static void simplify(Grid_Generator_System& ggs,
                       Dimension_Kinds& dim_kinds);


  // A member of Grid for access to Matrix<Dense_Row>::rows.
  static void reduce_line_with_line(Grid_Generator& row,
                                    Grid_Generator& pivot,
                                    dimension_type column);


  // A member of Grid for access to Matrix<Dense_Row>::rows.
  static void reduce_equality_with_equality(Congruence& row,
                                            const Congruence& pivot,
                                            dimension_type column);


  // Part of Grid for access to Matrix<Dense_Row>::rows.
  template <typename R>
  static void reduce_pc_with_pc(R& row,
                                R& pivot,
                                dimension_type column,
                                dimension_type start,
                                dimension_type end);


  // This takes a parameter with type Swapping_Vector<Grid_Generator> (instead
  // of Grid_Generator_System) to simplify the implementation of `simplify()'.
  // NOTE: This may invalidate `row' and the rows in `sys'. Client code must
  // fix/check this.
  static void reduce_parameter_with_line(Grid_Generator& row,
                                         const Grid_Generator& pivot,
                                         dimension_type column,
                                         Swapping_Vector<Grid_Generator>& sys,
                                         dimension_type num_columns);


  // A member of Grid for access to Matrix<Dense_Row>::rows.
  // This takes a parameter with type Swapping_Vector<Congruence> (instead of
  // Congruence_System) to simplify the implementation of `conversion()'.
  static void reduce_congruence_with_equality(Congruence& row,
                                              const Congruence& pivot,
                                              dimension_type column,
                                              Swapping_Vector<Congruence>& sys);


  template <typename M>
  // This takes a parameter with type `Swapping_Vector<M::row_type>'
  // instead of `M' to simplify the implementation of simplify().
  // NOTE: This may invalidate the rows in `sys'. Client code must
  // fix/check this.
  static void reduce_reduced(Swapping_Vector<typename M::row_type>& sys,
                             dimension_type dim,
                             dimension_type pivot_index,
                             dimension_type start, dimension_type end,
                             const Dimension_Kinds& sys_dim_kinds,
                             bool generators = true);

  // A member of Grid for access to Matrix<Dense_Row>::rows and cgs::operator[].
  // The type of `dest' is Swapping_Vector<Congruence> instead of
  // Congruence_System to simplify the implementation of conversion().
  static void multiply_grid(const Coefficient& multiplier,
                            Congruence& cg,
                            Swapping_Vector<Congruence>& dest,
                            dimension_type num_rows);

  // A member of Grid for access to Grid_Generator::operator[].
  // The type of `dest' is Swapping_Vector<Grid_Generator> instead of
  // Grid_Generator_System to simplify the implementation of conversion().
  // NOTE: This does not check whether the rows are OK(). Client code
  // should do that.
  static void multiply_grid(const Coefficient& multiplier,
                            Grid_Generator& gen,
                            Swapping_Vector<Grid_Generator>& dest,
                            dimension_type num_rows);

  static bool lower_triangular(const Congruence_System& sys,
                               const Dimension_Kinds& dim_kinds);

  static bool upper_triangular(const Grid_Generator_System& sys,
                               const Dimension_Kinds& dim_kinds);

#ifndef NDEBUG

  template <typename M, typename R>
  static bool rows_are_zero(M& system,
                            dimension_type first,
                            dimension_type last,
                            dimension_type row_size);
#endif


#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
protected:
  void throw_dimension_incompatible(const char* method,
                                    const char* other_name,
                                    dimension_type other_dim) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* gr_name,
                                    const Grid& gr) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* le_name,
                                    const Linear_Expression& le) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* cg_name,
                                    const Congruence& cg) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* c_name,
                                    const Constraint& c) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* g_name,
                                    const Grid_Generator& g) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* g_name,
                                    const Generator& g) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* cgs_name,
                                    const Congruence_System& cgs) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* cs_name,
                                    const Constraint_System& cs) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* gs_name,
                                    const Grid_Generator_System& gs) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* var_name,
                                    Variable var) const;
  void throw_dimension_incompatible(const char* method,
                                    dimension_type required_space_dim) const;

  static void throw_invalid_argument(const char* method,
                                     const char* reason);
  static void throw_invalid_constraint(const char* method,
                                       const char* c_name);
  static void throw_invalid_constraints(const char* method,
                                        const char* cs_name);
  static void throw_invalid_generator(const char* method,
                                      const char* g_name);
  static void throw_invalid_generators(const char* method,
                                       const char* gs_name);
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)

};

#include "Grid_Status_inlines.hh"
#include "Grid_inlines.hh"
#include "Grid_templates.hh"

#endif // !defined(PPL_Grid_defs_hh)