Partially_Reduced_Product_defs.hh

Go to the documentation of this file.

/* Partially_Reduced_Product 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_Partially_Reduced_Product_defs_hh
#define PPL_Partially_Reduced_Product_defs_hh 1

#include "Partially_Reduced_Product_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 "Generator_types.hh"
#include "Congruence_types.hh"
#include "Grid_Generator_types.hh"
#include "Constraint_System_types.hh"
#include "Generator_System_types.hh"
#include "Congruence_System_types.hh"
#include "Grid_Generator_System_types.hh"
#include "Poly_Con_Relation_defs.hh"
#include "Poly_Gen_Relation_defs.hh"
#include "C_Polyhedron_types.hh"
#include "NNC_Polyhedron_types.hh"
#include "Grid_types.hh"
#include "Box_types.hh"
#include "BD_Shape_types.hh"
#include "Octagonal_Shape_types.hh"

namespace Parma_Polyhedra_Library {

namespace IO_Operators {


template <typename D1, typename D2, typename R>
std::ostream&
operator<<(std::ostream& s, const Partially_Reduced_Product<D1, D2, R>& dp);

} // namespace IO_Operators


template <typename D1, typename D2, typename R>
void swap(Partially_Reduced_Product<D1, D2, R>& x,
          Partially_Reduced_Product<D1, D2, R>& y);

template <typename D1, typename D2, typename R>
bool operator==(const Partially_Reduced_Product<D1, D2, R>& x,
                const Partially_Reduced_Product<D1, D2, R>& y);

template <typename D1, typename D2, typename R>
bool operator!=(const Partially_Reduced_Product<D1, D2, R>& x,
                const Partially_Reduced_Product<D1, D2, R>& y);

} // namespace Parma_Polyhedra_Library


template <typename D1, typename D2>
class Parma_Polyhedra_Library::Smash_Reduction {
public:
  Smash_Reduction();

  void product_reduce(D1& d1, D2& d2);

  ~Smash_Reduction();
};

template <typename D1, typename D2>
class Parma_Polyhedra_Library::Constraints_Reduction {
public:
  Constraints_Reduction();

  void product_reduce(D1& d1, D2& d2);

  ~Constraints_Reduction();
};

template <typename D1, typename D2>
class Parma_Polyhedra_Library::Congruences_Reduction {
public:
  Congruences_Reduction();

  void product_reduce(D1& d1, D2& d2);

  ~Congruences_Reduction();
};

template <typename D1, typename D2>
class Parma_Polyhedra_Library::Shape_Preserving_Reduction {
public:
  Shape_Preserving_Reduction();

  void product_reduce(D1& d1, D2& d2);

  ~Shape_Preserving_Reduction();
};

template <typename D1, typename D2>
class Parma_Polyhedra_Library::No_Reduction {
public:
  No_Reduction();

  void product_reduce(D1& d1, D2& d2);

  ~No_Reduction();
};


template <typename D1, typename D2, typename R>
class Parma_Polyhedra_Library::Partially_Reduced_Product {
public:
  static dimension_type max_space_dimension();


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


  explicit Partially_Reduced_Product(const Congruence_System& cgs);


  explicit Partially_Reduced_Product(Congruence_System& cgs);


  explicit Partially_Reduced_Product(const Constraint_System& cs);


  explicit Partially_Reduced_Product(Constraint_System& cs);


  explicit
  Partially_Reduced_Product(const C_Polyhedron& ph,
                            Complexity_Class complexity = ANY_COMPLEXITY);


  explicit
  Partially_Reduced_Product(const NNC_Polyhedron& ph,
                            Complexity_Class complexity = ANY_COMPLEXITY);


  explicit
  Partially_Reduced_Product(const Grid& gr,
                            Complexity_Class complexity = ANY_COMPLEXITY);


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


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


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

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


  template <typename E1, typename E2, typename S>
  explicit
  Partially_Reduced_Product(const Partially_Reduced_Product<E1, E2, S>& y,
                            Complexity_Class complexity = ANY_COMPLEXITY);

  Partially_Reduced_Product& operator=(const Partially_Reduced_Product& y);



  dimension_type space_dimension() const;

  dimension_type affine_dimension() const;

  const D1& domain1() const;

  const D2& domain2() const;

  Constraint_System constraints() const;

  Constraint_System minimized_constraints() const;

  Congruence_System congruences() const;

  Congruence_System minimized_congruences() const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and congruence \p cg are dimension-incompatible.

    Returns the Poly_Con_Relation \p r for \p *this:
    suppose the first component returns \p r1 and the second \p r2,
    then \p r implies <CODE>is_included()</CODE>
    if and only if one or both of \p r1 and \p r2 imply
    <CODE>is_included()</CODE>;
    \p r implies <CODE>saturates()</CODE>
    if and only if one or both of \p r1 and \p r2 imply
    <CODE>saturates()</CODE>;
    \p r implies <CODE>is_disjoint()</CODE>
    if and only if one or both of \p r1 and \p r2 imply
    <CODE>is_disjoint()</CODE>;
    and \p r implies <CODE>nothing()</CODE>
    if and only if both \p r1 and \p r2 imply
    <CODE>strictly_intersects()</CODE>.
  */
  Poly_Con_Relation relation_with(const Constraint& c) const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and congruence \p cg are dimension-incompatible.
  */
  Poly_Con_Relation relation_with(const Congruence& cg) const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and generator \p g are dimension-incompatible.

    Returns the Poly_Gen_Relation \p r for \p *this:
    suppose the first component returns \p r1 and the second \p r2,
    then \p r = <CODE>subsumes()</CODE>
    if and only if \p r1 = \p r2 = <CODE>subsumes()</CODE>;
    and \p r = <CODE>nothing()</CODE>
    if and only if one or both of \p r1 and \p r2 = <CODE>nothing()</CODE>;
  */
  Poly_Gen_Relation relation_with(const Generator& g) const;

  bool is_empty() const;

  bool is_universe() const;

  bool is_topologically_closed() const;

  bool is_disjoint_from(const Partially_Reduced_Product& y) const;

  bool is_discrete() const;

  bool is_bounded() 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 contains(const Partially_Reduced_Product& y) const;

  bool strictly_contains(const Partially_Reduced_Product& y) const;

  bool OK() const;





  void add_constraint(const Constraint& c);

  void refine_with_constraint(const Constraint& c);


  void add_congruence(const Congruence& cg);

  void refine_with_congruence(const Congruence& cg);


  void add_congruences(const Congruence_System& cgs);

  void refine_with_congruences(const Congruence_System& cgs);


  void add_recycled_congruences(Congruence_System& cgs);


  void add_constraints(const Constraint_System& cs);

  void refine_with_constraints(const Constraint_System& cs);


  void add_recycled_constraints(Constraint_System& cs);

  void unconstrain(Variable var);

  void unconstrain(const Variables_Set& vars);

  void intersection_assign(const Partially_Reduced_Product& y);

  void upper_bound_assign(const Partially_Reduced_Product& y);

  bool upper_bound_assign_if_exact(const Partially_Reduced_Product& y);

  void difference_assign(const Partially_Reduced_Product& 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());

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

  void topological_closure_assign();

  // TODO: Add a way to call other widenings.

  // CHECKME: This may not be a real widening; it depends on the reduction
  //          class R and the widening used.

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

  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 add_space_dimensions_and_embed(dimension_type m);

  void add_space_dimensions_and_project(dimension_type m);

  void concatenate_assign(const Partially_Reduced_Product& 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 Partially_Reduced_Product<D1, D2, R>& x,
                           const Partially_Reduced_Product<D1, D2, R>& y);

  friend std::ostream&
  Parma_Polyhedra_Library::IO_Operators::
  operator<<<>(std::ostream& s, const Partially_Reduced_Product<D1, D2, R>& dp);



  ~Partially_Reduced_Product();

  void m_swap(Partially_Reduced_Product& 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;


  /*
    \return
    <CODE>true</CODE> if and only if either of the resulting component
    is strictly contained in the respective original.
  */
  bool reduce() const;

protected:
  typedef D1 Domain1;

  typedef D2 Domain2;

  D1 d1;

  D2 d2;

protected:
  void clear_reduced_flag() const;

  void set_reduced_flag() const;

  bool is_reduced() const;

  bool reduced;

private:
  void throw_space_dimension_overflow(const char* method,
                                      const char* reason);
};

namespace Parma_Polyhedra_Library {

template <typename D1, typename D2>
class Domain_Product {
public:
  typedef Partially_Reduced_Product<D1, D2, No_Reduction<D1, D2> >
  Direct_Product;

  typedef Partially_Reduced_Product<D1, D2, Smash_Reduction<D1, D2> >
  Smash_Product;

  typedef Partially_Reduced_Product<D1, D2, Constraints_Reduction<D1, D2> >
  Constraints_Product;

  typedef Partially_Reduced_Product<D1, D2, Congruences_Reduction<D1, D2> >
  Congruences_Product;

  typedef Partially_Reduced_Product<D1, D2, Shape_Preserving_Reduction<D1, D2> >
  Shape_Preserving_Product;
};

} // namespace Parma_Polyhedra_Library

#include "Partially_Reduced_Product_inlines.hh"
#include "Partially_Reduced_Product_templates.hh"

#endif // !defined(PPL_Partially_Reduced_Product_defs_hh)