Pointset_Powerset_defs.hh

Go to the documentation of this file.

/* Pointset_Powerset 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_Pointset_Powerset_defs_hh
#define PPL_Pointset_Powerset_defs_hh

#include "Pointset_Powerset_types.hh"
#include "globals_defs.hh"
#include "BHRZ03_Certificate_types.hh"
#include "Constraint_types.hh"
#include "Constraint_System_types.hh"
#include "Congruence_types.hh"
#include "Congruence_System_types.hh"
#include "C_Polyhedron_defs.hh"
#include "NNC_Polyhedron_defs.hh"
#include "Polyhedron_defs.hh"
#include "Grid_defs.hh"
#include "Partially_Reduced_Product_defs.hh"
#include "Variables_Set_types.hh"
#include "Determinate_defs.hh"
#include "Powerset_defs.hh"
#include "Poly_Con_Relation_defs.hh"
#include "Poly_Gen_Relation_defs.hh"
#include <iosfwd>
#include <list>
#include <map>


template <typename PSET>
class Parma_Polyhedra_Library::Pointset_Powerset
  : public Parma_Polyhedra_Library::Powerset
<Parma_Polyhedra_Library::Determinate<PSET> > {
public:
  typedef PSET element_type;

private:
  typedef Determinate<PSET> Det_PSET;
  typedef Powerset<Det_PSET> Base;

public:
  static dimension_type max_space_dimension();




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


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

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

  template <typename QH1, typename QH2, typename R>
  explicit
  Pointset_Powerset(const Partially_Reduced_Product<QH1, QH2, R>& prp,
                    Complexity_Class complexity = ANY_COMPLEXITY);

  explicit Pointset_Powerset(const Constraint_System& cs);

  explicit Pointset_Powerset(const Congruence_System& cgs);



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


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



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


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


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


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




  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_bounded() const;


  bool is_disjoint_from(const Pointset_Powerset& y) const;

  bool is_discrete() 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 geometrically_covers(const Pointset_Powerset& y) const;

  bool geometrically_equals(const Pointset_Powerset& y) const;

  bool contains(const Pointset_Powerset& y) const;

  bool strictly_contains(const Pointset_Powerset& y) const;

  bool contains_integer_point() 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;

  memory_size_type total_memory_in_bytes() const;

  memory_size_type external_memory_in_bytes() const;

  int32_t hash_code() const;

  bool OK() const;





  void add_disjunct(const PSET& ph);


  void add_constraint(const Constraint& c);

  void refine_with_constraint(const Constraint& c);


  void add_constraints(const Constraint_System& cs);

  void refine_with_constraints(const Constraint_System& cs);


  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 unconstrain(Variable var);

  void unconstrain(const Variables_Set& vars);

  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 intersection_assign(const Pointset_Powerset& y);

  void difference_assign(const Pointset_Powerset& y);

  bool simplify_using_context_assign(const Pointset_Powerset& 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 Pointset_Powerset& 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 pairwise_reduce();

  template <typename Widening>
  void BGP99_extrapolation_assign(const Pointset_Powerset& y,
                                  Widening widen_fun,
                                  unsigned max_disjuncts);

  template <typename Cert, typename Widening>
  void BHZ03_widening_assign(const Pointset_Powerset& y, Widening widen_fun);




  Pointset_Powerset& operator=(const Pointset_Powerset& y);

  template <typename QH>
  Pointset_Powerset& operator=(const Pointset_Powerset<QH>& y);

  void m_swap(Pointset_Powerset& y);

  void add_space_dimensions_and_embed(dimension_type m);

  void add_space_dimensions_and_project(dimension_type m);


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


public:
  typedef typename Base::size_type size_type;
  typedef typename Base::value_type value_type;
  typedef typename Base::iterator iterator;
  typedef typename Base::const_iterator const_iterator;
  typedef typename Base::reverse_iterator reverse_iterator;
  typedef typename Base::const_reverse_iterator const_reverse_iterator;

  PPL_OUTPUT_DECLARATIONS

  bool ascii_load(std::istream& s);

private:
  typedef typename Base::Sequence Sequence;
  typedef typename Base::Sequence_iterator Sequence_iterator;
  typedef typename Base::Sequence_const_iterator Sequence_const_iterator;

  dimension_type space_dim;

  bool intersection_preserving_enlarge_element(PSET& dest) const;

  template <typename Widening>
  void BGP99_heuristics_assign(const Pointset_Powerset& y, Widening widen_fun);

  template <typename Cert>
  void collect_certificates(std::map<Cert, size_type,
                                     typename Cert::Compare>& cert_ms) const;

  template <typename Cert>
  bool is_cert_multiset_stabilizing(const std::map<Cert, size_type,
                                                   typename Cert::Compare>&
                                    y_cert_ms) const;

  template <typename Cons_or_Congr>
  Poly_Con_Relation relation_with_aux(const Cons_or_Congr& c) const;

  // FIXME: here it should be enough to befriend the template constructor
  // template <typename QH>
  // Pointset_Powerset(const Pointset_Powerset<QH>&),
  // but, apparently, this cannot be done.
  friend class Pointset_Powerset<NNC_Polyhedron>;
};

namespace Parma_Polyhedra_Library {


template <typename PSET>
void swap(Pointset_Powerset<PSET>& x, Pointset_Powerset<PSET>& y);


template <typename PSET>
std::pair<PSET, Pointset_Powerset<NNC_Polyhedron> >
linear_partition(const PSET& p, const PSET& q);

bool
check_containment(const NNC_Polyhedron& ph,
                  const Pointset_Powerset<NNC_Polyhedron>& ps);


std::pair<Grid, Pointset_Powerset<Grid> >
approximate_partition(const Grid& p, const Grid& q, bool& finite_partition);

bool
check_containment(const Grid& ph,
                  const Pointset_Powerset<Grid>& ps);

template <typename PSET>
bool
check_containment(const PSET& ph, const Pointset_Powerset<PSET>& ps);

// CHECKME: according to the Intel compiler, the declaration of the
// following specialization (of the class template parameter) should come
// before the declaration of the corresponding full specialization
// (where the member template parameter is specialized too).
template <>
template <typename QH>
Pointset_Powerset<NNC_Polyhedron>
::Pointset_Powerset(const Pointset_Powerset<QH>& y,
                    Complexity_Class);

// Non-inline full specializations should be declared here
// so as to inhibit multiple instantiations of the generic template.
template <>
template <>
Pointset_Powerset<NNC_Polyhedron>
::Pointset_Powerset(const Pointset_Powerset<C_Polyhedron>& y,
                    Complexity_Class);

template <>
template <>
Pointset_Powerset<NNC_Polyhedron>
::Pointset_Powerset(const Pointset_Powerset<Grid>& y,
                    Complexity_Class);

template <>
template <>
Pointset_Powerset<C_Polyhedron>
::Pointset_Powerset(const Pointset_Powerset<NNC_Polyhedron>& y,
                    Complexity_Class);

template <>
void
Pointset_Powerset<NNC_Polyhedron>
::difference_assign(const Pointset_Powerset& y);

template <>
void
Pointset_Powerset<Grid>
::difference_assign(const Pointset_Powerset& y);

template <>
bool
Pointset_Powerset<NNC_Polyhedron>
::geometrically_covers(const Pointset_Powerset& y) const;

template <>
bool
Pointset_Powerset<Grid>
::geometrically_covers(const Pointset_Powerset& y) const;

} // namespace Parma_Polyhedra_Library

#include "Pointset_Powerset_inlines.hh"
#include "Pointset_Powerset_templates.hh"

#endif // !defined(PPL_Pointset_Powerset_defs_hh)