Polyhedron_defs.hh

Go to the documentation of this file.

/* Polyhedron 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_Polyhedron_defs_hh
#define PPL_Polyhedron_defs_hh 1

#include "Polyhedron_types.hh"
#include "globals_types.hh"
#include "Variable_defs.hh"
#include "Variables_Set_types.hh"
#include "Linear_Expression_types.hh"
#include "Constraint_System_defs.hh"
#include "Constraint_System_inlines.hh"
#include "Generator_System_defs.hh"
#include "Generator_System_inlines.hh"
#include "Congruence_System_defs.hh"
#include "Congruence_System_inlines.hh"
#include "Bit_Matrix_defs.hh"
#include "Constraint_types.hh"
#include "Generator_types.hh"
#include "Congruence_types.hh"
#include "Poly_Con_Relation_defs.hh"
#include "Poly_Gen_Relation_defs.hh"
#include "BHRZ03_Certificate_types.hh"
#include "H79_Certificate_types.hh"
#include "Box_types.hh"
#include "BD_Shape_types.hh"
#include "Octagonal_Shape_types.hh"
#include "Interval_types.hh"
#include "Linear_Form_types.hh"
#include <vector>
#include <iosfwd>

namespace Parma_Polyhedra_Library {

namespace IO_Operators {


std::ostream&
operator<<(std::ostream& s, const Polyhedron& ph);

} // namespace IO_Operators


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

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

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

namespace Interfaces {

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
bool is_necessarily_closed_for_interfaces(const Polyhedron& ph);

} // namespace Interfaces

} // namespace Parma_Polyhedra_Library



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

  static dimension_type max_space_dimension();

  static bool can_recycle_constraint_systems();

  static void initialize();

  static void finalize();

  static bool can_recycle_congruence_systems();

protected:

  Polyhedron(Topology topol,
             dimension_type num_dimensions,
             Degenerate_Element kind);


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


  Polyhedron(Topology topol, const Constraint_System& cs);


  Polyhedron(Topology topol, Constraint_System& cs, Recycle_Input dummy);


  Polyhedron(Topology topol, const Generator_System& gs);


  Polyhedron(Topology topol, Generator_System& gs, Recycle_Input dummy);


  template <typename Interval>
  Polyhedron(Topology topol, const Box<Interval>& box,
             Complexity_Class complexity = ANY_COMPLEXITY);

  Polyhedron& operator=(const Polyhedron& y);

public:


  dimension_type space_dimension() const;

  dimension_type affine_dimension() const;

  const Constraint_System& constraints() const;

  const Constraint_System& minimized_constraints() const;

  const Generator_System& generators() const;

  const Generator_System& minimized_generators() const;

  Congruence_System congruences() const;

  Congruence_System minimized_congruences() const;

  Poly_Con_Relation relation_with(const Constraint& c) const;

  Poly_Gen_Relation relation_with(const Generator& g) const;

  Poly_Con_Relation relation_with(const Congruence& cg) const;

  bool is_empty() const;

  bool is_universe() const;

  bool is_topologically_closed() const;


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


  bool strictly_contains(const Polyhedron& y) const;


  bool OK(bool check_not_empty = false) const;




  void add_constraint(const Constraint& c);

  void add_generator(const Generator& g);

  void add_congruence(const Congruence& cg);

  void add_constraints(const Constraint_System& cs);

  void add_recycled_constraints(Constraint_System& cs);

  void add_generators(const Generator_System& gs);

  void add_recycled_generators(Generator_System& gs);

  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 FP_Format, typename Interval_Info>
  void refine_with_linear_form_inequality(
  const Linear_Form< Interval<FP_Format, Interval_Info> >& left,
  const Linear_Form< Interval<FP_Format, Interval_Info> >& right,
  bool is_strict = false);

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


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

  void unconstrain(Variable var);

  void unconstrain(const Variables_Set& vars);

  void intersection_assign(const Polyhedron& y);

  void poly_hull_assign(const Polyhedron& y);

  void upper_bound_assign(const Polyhedron& y);

  void poly_difference_assign(const Polyhedron& y);

  void difference_assign(const Polyhedron& y);

  bool simplify_using_context_assign(const Polyhedron& y);

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

  // FIXME: To be completed.
  template <typename FP_Format, typename Interval_Info>
  void affine_form_image(Variable var,
  const Linear_Form<Interval <FP_Format, 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_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 Polyhedron& y);

  void positive_time_elapse_assign(const Polyhedron& 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 BHRZ03_widening_assign(const Polyhedron& y, unsigned* tp = 0);

  void limited_BHRZ03_extrapolation_assign(const Polyhedron& y,
                                           const Constraint_System& cs,
                                           unsigned* tp = 0);

  void bounded_BHRZ03_extrapolation_assign(const Polyhedron& y,
                                           const Constraint_System& cs,
                                           unsigned* tp = 0);

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

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

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

  void bounded_H79_extrapolation_assign(const Polyhedron& 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 Polyhedron& 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 Polyhedron& x, const Polyhedron& y);



  ~Polyhedron();

  void m_swap(Polyhedron& 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:
  static const Representation default_con_sys_repr = DENSE;
  static const Representation default_gen_sys_repr = DENSE;

  Constraint_System con_sys;

  Generator_System gen_sys;

  Bit_Matrix sat_c;

  Bit_Matrix sat_g;

#define PPL_IN_Polyhedron_CLASS
#include "Ph_Status_idefs.hh"
#undef PPL_IN_Polyhedron_CLASS

  Status status;

  dimension_type space_dim;

  Topology topology() const;

  bool is_necessarily_closed() const;

  friend bool
  Parma_Polyhedra_Library::Interfaces
  ::is_necessarily_closed_for_interfaces(const Polyhedron&);

  void refine_no_check(const Constraint& c);




  bool marked_empty() const;

  bool constraints_are_up_to_date() const;

  bool generators_are_up_to_date() const;


  bool constraints_are_minimized() const;


  bool generators_are_minimized() const;

  bool has_pending_constraints() const;

  bool has_pending_generators() const;

  bool has_something_pending() const;

  bool can_have_something_pending() const;

  bool sat_c_is_up_to_date() const;

  bool sat_g_is_up_to_date() const;




  void set_zero_dim_univ();

  void set_empty();

  void set_constraints_up_to_date();

  void set_generators_up_to_date();

  void set_constraints_minimized();

  void set_generators_minimized();

  void set_constraints_pending();

  void set_generators_pending();

  void set_sat_c_up_to_date();

  void set_sat_g_up_to_date();




  void clear_empty();


  void clear_constraints_up_to_date();


  void clear_generators_up_to_date();

  void clear_constraints_minimized();

  void clear_generators_minimized();

  void clear_pending_constraints();

  void clear_pending_generators();

  void clear_sat_c_up_to_date();

  void clear_sat_g_up_to_date();




  bool process_pending() const;


  bool process_pending_constraints() const;


  void process_pending_generators() const;

  void remove_pending_to_obtain_constraints() const;

  bool remove_pending_to_obtain_generators() const;





  void update_constraints() const;


  bool update_generators() const;


  void update_sat_c() const;


  void update_sat_g() const;


  void obtain_sorted_constraints() const;


  void obtain_sorted_generators() const;


  void obtain_sorted_constraints_with_sat_c() const;


  void obtain_sorted_generators_with_sat_g() const;





  bool minimize() const;


  bool strongly_minimize_constraints() const;


  bool strongly_minimize_generators() const;

  Constraint_System simplified_constraints() const;


  enum Three_Valued_Boolean {
    TVB_TRUE,
    TVB_FALSE,
    TVB_DONT_KNOW
  };

  Three_Valued_Boolean quick_equivalence_test(const Polyhedron& y) const;

  bool is_included_in(const Polyhedron& y) 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;



  void select_CH78_constraints(const Polyhedron& y,
                               Constraint_System& cs_selection) const;

  void select_H79_constraints(const Polyhedron& y,
                              Constraint_System& cs_selected,
                              Constraint_System& cs_not_selected) const;

  bool BHRZ03_combining_constraints(const Polyhedron& y,
                                    const BHRZ03_Certificate& y_cert,
                                    const Polyhedron& H79,
                                    const Constraint_System& x_minus_H79_cs);

  bool BHRZ03_evolving_points(const Polyhedron& y,
                              const BHRZ03_Certificate& y_cert,
                              const Polyhedron& H79);

  bool BHRZ03_evolving_rays(const Polyhedron& y,
                            const BHRZ03_Certificate& y_cert,
                            const Polyhedron& H79);

  static void modify_according_to_evolution(Linear_Expression& ray,
                                            const Linear_Expression& x,
                                            const Linear_Expression& y);



  template <typename Linear_System1, typename Linear_System2>
  static void add_space_dimensions(Linear_System1& sys1,
                                   Linear_System2& sys2,
                                   Bit_Matrix& sat1,
                                   Bit_Matrix& sat2,
                                   dimension_type add_dim);



  // Detailed Doxygen comment to be found in file minimize.cc.
  template <typename Source_Linear_System, typename Dest_Linear_System>
  static bool minimize(bool con_to_gen,
                       Source_Linear_System& source,
                       Dest_Linear_System& dest,
                       Bit_Matrix& sat);

  // Detailed Doxygen comment to be found in file minimize.cc.
  template <typename Source_Linear_System1, typename Source_Linear_System2,
            typename Dest_Linear_System>
  static bool add_and_minimize(bool con_to_gen,
                               Source_Linear_System1& source1,
                               Dest_Linear_System& dest,
                               Bit_Matrix& sat,
                               const Source_Linear_System2& source2);

  // Detailed Doxygen comment to be found in file minimize.cc.
  template <typename Source_Linear_System, typename Dest_Linear_System>
  static bool add_and_minimize(bool con_to_gen,
                               Source_Linear_System& source,
                               Dest_Linear_System& dest,
                               Bit_Matrix& sat);

  // Detailed Doxygen comment to be found in file conversion.cc.
  template <typename Source_Linear_System, typename Dest_Linear_System>
  static dimension_type conversion(Source_Linear_System& source,
                                   dimension_type start,
                                   Dest_Linear_System& dest,
                                   Bit_Matrix& sat,
                                   dimension_type num_lines_or_equalities);

  // Detailed Doxygen comment to be found in file simplify.cc.
  template <typename Linear_System1>
  static dimension_type simplify(Linear_System1& sys, Bit_Matrix& sat);


  static dimension_type* simplify_num_saturators_p;

  static size_t simplify_num_saturators_size;

  template <typename Interval> friend class Parma_Polyhedra_Library::Box;
  template <typename T> friend class Parma_Polyhedra_Library::BD_Shape;
  template <typename T> friend class Parma_Polyhedra_Library::Octagonal_Shape;
  friend class Parma_Polyhedra_Library::Grid;
  friend class Parma_Polyhedra_Library::BHRZ03_Certificate;
  friend class Parma_Polyhedra_Library::H79_Certificate;

protected:
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  bool BFT00_poly_hull_assign_if_exact(const Polyhedron& y);

  bool BHZ09_poly_hull_assign_if_exact(const Polyhedron& y);
  bool BHZ09_C_poly_hull_assign_if_exact(const Polyhedron& y);
  bool BHZ09_NNC_poly_hull_assign_if_exact(const Polyhedron& y);

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
protected:
  void throw_invalid_argument(const char* method, const char* reason) const;

  void throw_topology_incompatible(const char* method,
                                   const char* ph_name,
                                   const Polyhedron& ph) const;
  void throw_topology_incompatible(const char* method,
                                   const char* c_name,
                                   const Constraint& c) const;
  void throw_topology_incompatible(const char* method,
                                   const char* g_name,
                                   const Generator& g) const;
  void throw_topology_incompatible(const char* method,
                                   const char* cs_name,
                                   const Constraint_System& cs) const;
  void throw_topology_incompatible(const char* method,
                                   const char* gs_name,
                                   const Generator_System& gs) const;

  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* ph_name,
                                    const Polyhedron& ph) 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* c_name,
                                    const Constraint& c) 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* cg_name,
                                    const Congruence& cg) 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 Generator_System& gs) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* cgs_name,
                                    const Congruence_System& cgs) const;
  template <typename C>
  void throw_dimension_incompatible(const char* method,
                                    const char* lf_name,
                                    const Linear_Form<C>& lf) 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;

  // Note: the following three methods need to be static, because they
  // can be called inside constructors (before actually constructing the
  // polyhedron object).
  static dimension_type
  check_space_dimension_overflow(dimension_type dim, dimension_type max,
                                 const Topology topol,
                                 const char* method, const char* reason);

  static dimension_type
  check_space_dimension_overflow(dimension_type dim, const Topology topol,
                                 const char* method, const char* reason);

  template <typename Object>
  static Object&
  check_obj_space_dimension_overflow(Object& input, Topology topol,
                                     const char* method, const char* reason);

  void throw_invalid_generator(const char* method,
                               const char* g_name) const;

  void throw_invalid_generators(const char* method,
                                const char* gs_name) const;
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)

  void drop_some_non_integer_points(const Variables_Set* vars_p,
                                    Complexity_Class complexity);


  template <typename FP_Format, typename Interval_Info>
  void overapproximate_linear_form(
  const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,
  const dimension_type lf_dimension,
  Linear_Form<Interval <FP_Format, Interval_Info> >& result);

  template <typename FP_Format, typename Interval_Info>
  static void convert_to_integer_expression(
              const Linear_Form<Interval <FP_Format, Interval_Info> >& lf,
              const dimension_type lf_dimension,
              Linear_Expression& result);


  template <typename FP_Format, typename Interval_Info>
  static void
  convert_to_integer_expressions(const Linear_Form<Interval<FP_Format,
                                                            Interval_Info> >&
                                 lf,
                                 const dimension_type lf_dimension,
                                 Linear_Expression& res,
                                 Coefficient& res_low_coeff,
                                 Coefficient& res_hi_coeff,
                                 Coefficient& denominator);

  template <typename Linear_System1, typename Row2>
  static bool
  add_to_system_and_check_independence(Linear_System1& eq_sys,
                                       const Row2& eq);

  void positive_time_elapse_assign_impl(const Polyhedron& y);
};

#include "Ph_Status_inlines.hh"
#include "Polyhedron_inlines.hh"
#include "Polyhedron_templates.hh"
#include "Polyhedron_chdims_templates.hh"
#include "Polyhedron_conversion_templates.hh"
#include "Polyhedron_minimize_templates.hh"
#include "Polyhedron_simplify_templates.hh"

#endif // !defined(PPL_Polyhedron_defs_hh)