Pointset_Ask_Tell_defs.hh

Go to the documentation of this file.

/* Pointset_Ask_Tell 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_Ask_Tell_defs_hh
#define PPL_Pointset_Ask_Tell_defs_hh

#include "Pointset_Ask_Tell_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 "Variables_Set_types.hh"
#include "Determinate_defs.hh"
#include "Ask_Tell_defs.hh"
#include <iosfwd>
#include <list>
#include <map>


template <typename PSET>
class Parma_Polyhedra_Library::Pointset_Ask_Tell
  : public Parma_Polyhedra_Library::Ask_Tell
<Parma_Polyhedra_Library::Determinate<PSET> > {
public:
  typedef PSET element_type;

private:
  typedef Determinate<PSET> Det_PSET;
  typedef Ask_Tell<Det_PSET> Base;
  typedef typename Base::Pair Pair;

public:
  static dimension_type max_space_dimension();




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

  Pointset_Ask_Tell(const Pointset_Ask_Tell& y);

  explicit Pointset_Ask_Tell(const PSET& ph);

  template <typename QH>
  explicit Pointset_Ask_Tell(const Pointset_Ask_Tell<QH>& y);

  explicit Pointset_Ask_Tell(const Constraint_System& cs);

  explicit Pointset_Ask_Tell(const Congruence_System& cgs);




  dimension_type space_dimension() const;

  bool geometrically_covers(const Pointset_Ask_Tell& y) const;

  bool geometrically_equals(const Pointset_Ask_Tell& y) 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 add_constraints(const Constraint_System& cs);

  void pairwise_reduce();

  void unconstrain(Variable var);

  void unconstrain(const Variables_Set& vars);


  void intersection_assign(const Pointset_Ask_Tell& y);


  void poly_difference_assign(const Pointset_Ask_Tell& y);

  void time_elapse_assign(const Pointset_Ask_Tell& y);

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

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




  Pointset_Ask_Tell& operator=(const Pointset_Ask_Tell& y);

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

  void m_swap(Pointset_Ask_Tell& y);

  void add_space_dimensions_and_embed(dimension_type m);

  void add_space_dimensions_and_project(dimension_type m);


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


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;

  template <typename Widening>
  void BGP99_heuristics_assign(const Pointset_Ask_Tell& 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;

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


namespace Parma_Polyhedra_Library {


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

// 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_Ask_Tell<NNC_Polyhedron>
::Pointset_Ask_Tell(const Pointset_Ask_Tell<QH>& y);

// 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_Ask_Tell<C_Polyhedron>
::Pointset_Ask_Tell(const Pointset_Ask_Tell<QH>& y);

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

template <>
template <>
Pointset_Ask_Tell<C_Polyhedron>
::Pointset_Ask_Tell(const Pointset_Ask_Tell<NNC_Polyhedron>& y);

template <>
void
Pointset_Ask_Tell<NNC_Polyhedron>
::poly_difference_assign(const Pointset_Ask_Tell& y);

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

} // namespace Parma_Polyhedra_Library

#include "Pointset_Ask_Tell_inlines.hh"
#include "Pointset_Ask_Tell_templates.hh"

#endif // !defined(PPL_Pointset_Ask_Tell_defs_hh)