Imported Upstream version 0.11.2upstream/0.11.2upstream

1 files changed, 1754 insertions, 0 deletions

diff --git a/interfaces/C/C_interface.dox b/interfaces/C/C_interface.dox
new file mode 100644
index 000000000..df185b37b
--- /dev/null
+++ b/interfaces/C/C_interface.dox
@@ -0,0 +1,1754 @@
+/* Doxumentation for the C language interface.
+   Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
+   Copyright (C) 2010-2011 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://www.cs.unipr.it/ppl/ . */
+
+/*! \interface ppl_Polyhedron_tag
+  \brief
+  Types and functions for the domains of C and NNC convex polyhedra.
+
+  The types and functions for convex polyhedra provide a single interface
+  for accessing both topologically closed (C) and not necessarily closed
+  (NNC) convex polyhedra.
+  The distinction between C and NNC polyhedra need only be explicitly
+  stated when <em>creating</em> or <em>assigning</em> a polyhedron object,
+  by means of one of the functions <code>ppl_new_*</code> and
+  <code>ppl_assign_*</code>.
+
+  Having a single datatype does not mean that C and NNC polyhedra can be
+  freely interchanged: as specified in the main manual, most library
+  functions require their arguments to be topologically and/or
+  space-dimension compatible.
+*/
+
+#if !defined(PPL_DOXYGEN_CONFIGURED_MANUAL)
+
+/*! \brief Opaque pointer \ingroup Datatypes */
+typedef struct ppl_Polyhedron_tag* ppl_Polyhedron_t;
+
+/*! \brief Opaque pointer to const object \ingroup Datatypes */
+typedef struct ppl_Polyhedron_tag const* ppl_const_Polyhedron_t;
+
+#endif /* !defined(PPL_DOXYGEN_CONFIGURED_MANUAL) */
+
+/*! \brief \name Constructors and Assignment for C_Polyhedron */
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a C polyhedron of dimension \p d and writes an handle to it
+  at address \p pph. If \p empty is different from zero, the newly created
+  polyhedron will be empty; otherwise, it will be a universe polyhedron.
+*/
+int
+ppl_new_C_Polyhedron_from_space_dimension
+(ppl_Polyhedron_t* pph, ppl_dimension_type d, int empty);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a C polyhedron that is a copy of \p ph; writes a handle
+  for the newly created polyhedron at address \p pph.
+*/
+int
+ppl_new_C_Polyhedron_from_C_Polyhedron
+(ppl_Polyhedron_t* pph, ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a C polyhedron that is a copy of \p ph;
+  writes a handle for the newly created polyhedron at address \p pph.
+
+  \note
+  The complexity argument is ignored.
+*/
+int
+ppl_new_C_Polyhedron_from_C_Polyhedron_with_complexity
+(ppl_Polyhedron_t* pph, ppl_const_Polyhedron_t ph, int complexity);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new C polyhedron from the system of constraints
+  \p cs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p cs.
+*/
+int
+ppl_new_C_Polyhedron_from_Constraint_System
+(ppl_Polyhedron_t* pph, ppl_const_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new C polyhedron recycling the system of constraints
+  \p cs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p cs.
+
+  \warning
+  This function modifies the constraint system referenced by \p cs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_new_C_Polyhedron_recycle_Constraint_System
+(ppl_Polyhedron_t* pph, ppl_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new C polyhedron from the system of congruences \p cs
+  and writes a handle for the newly created polyhedron at address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p cs.
+*/
+int
+ppl_new_C_Polyhedron_from_Congruence_System
+(ppl_Polyhedron_t* pph, ppl_const_Congruence_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new C polyhedron recycling the system of congruences
+  \p cs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p cs.
+
+  \warning
+  This function modifies the congruence system referenced by \p cs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_new_C_Polyhedron_recycle_Congruence_System
+(ppl_Polyhedron_t* pph, ppl_Congruence_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns a copy of the C polyhedron \p src to the C polyhedron \p dst.
+*/
+int
+ppl_assign_C_Polyhedron_from_C_Polyhedron
+(ppl_Polyhedron_t dst, ppl_const_Polyhedron_t src);
+
+/*@}*/ /* Constructors and Assignment for C_Polyhedron */
+
+/*! \brief \name Constructors and Assignment for NNC_Polyhedron */
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds an NNC polyhedron of dimension \p d and writes an handle to it
+  at address \p pph. If \p empty is different from zero, the newly created
+  polyhedron will be empty; otherwise, it will be a universe polyhedron.
+*/
+int
+ppl_new_NNC_Polyhedron_from_space_dimension
+(ppl_Polyhedron_t* pph, ppl_dimension_type d, int empty);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds an NNC polyhedron that is a copy of \p ph; writes a handle
+  for the newly created polyhedron at address \p pph.
+*/
+int
+ppl_new_NNC_Polyhedron_from_NNC_Polyhedron
+(ppl_Polyhedron_t* pph, ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds an NNC polyhedron that is a copy of \p ph;
+  writes a handle for the newly created polyhedron at address \p pph.
+
+  \note
+  The complexity argument is ignored.
+*/
+int
+ppl_new_NNC_Polyhedron_from_NNC_Polyhedron_with_complexity
+(ppl_Polyhedron_t* pph, ppl_const_Polyhedron_t ph, int complexity);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new NNC polyhedron from the system of constraints
+  \p cs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p cs.
+*/
+int
+ppl_new_NNC_Polyhedron_from_Constraint_System
+(ppl_Polyhedron_t* pph, ppl_const_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new NNC polyhedron recycling the system of constraints
+  \p cs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p cs.
+
+  \warning
+  This function modifies the constraint system referenced by \p cs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_new_NNC_Polyhedron_recycle_Constraint_System
+(ppl_Polyhedron_t* pph, ppl_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new NNC polyhedron from the system of congruences
+  \p cs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p cs.
+*/
+int
+ppl_new_NNC_Polyhedron_from_Congruence_System
+PPL_PROTO((ppl_Polyhedron_t* pph, ppl_const_Congruence_System_t cs));
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new NNC polyhedron recycling the system of congruences
+  \p cs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p cs.
+
+  \warning
+  This function modifies the congruence system referenced by \p cs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_new_NNC_Polyhedron_recycle_Congruence_System
+PPL_PROTO((ppl_Polyhedron_t* pph, ppl_Congruence_System_t cs));
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns a copy of the NNC polyhedron \p src to the NNC
+  polyhedron \p dst.
+*/
+int
+ppl_assign_NNC_Polyhedron_from_NNC_Polyhedron
+(ppl_Polyhedron_t dst, ppl_const_Polyhedron_t src);
+
+/*@}*/ /* Constructors and Assignment for NNC Polyhedron */
+
+/*! \name Constructors Behaving as Conversion Operators
+  Besides the conversions listed here below, the library also
+  provides conversion operators that build a semantic geometric
+  description starting from \b any other semantic geometric
+  description (e.g., ppl_new_Grid_from_C_Polyhedron,
+  ppl_new_C_Polyhedron_from_BD_Shape_mpq_class, etc.).
+  Clearly, the conversion operators are only available if both
+  the source and the target semantic geometric descriptions have
+  been enabled when configuring the library.
+  The conversions also taking as argument a complexity class
+  sometimes provide non-trivial precision/efficiency trade-offs.
+*/
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a C polyhedron that is a copy of the topological closure
+  of the NNC polyhedron \p ph; writes a handle for the newly created
+  polyhedron at address \p pph.
+*/
+int
+ppl_new_C_Polyhedron_from_NNC_Polyhedron(ppl_Polyhedron_t* pph,
+					 ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a C polyhedron that approximates NNC_Polyhedron \p ph,
+  using an algorithm whose complexity does not exceed \p complexity;
+  writes a handle for the newly created polyhedron at address \p pph.
+
+  \note
+  The complexity argument, which can take values
+  \c PPL_COMPLEXITY_CLASS_POLYNOMIAL, \c PPL_COMPLEXITY_CLASS_SIMPLEX
+  and \c PPL_COMPLEXITY_CLASS_ANY, is ignored since the exact constructor
+  has polynomial complexity.
+*/
+int
+ppl_new_C_Polyhedron_from_NNC_Polyhedron_with_complexity
+(ppl_Polyhedron_t* pph, ppl_const_Polyhedron_t ph, int complexity);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds an NNC polyhedron that is a copy of the C polyhedron \p ph;
+  writes a handle for the newly created polyhedron at address \p pph.
+*/
+int
+ppl_new_NNC_Polyhedron_from_C_Polyhedron(ppl_Polyhedron_t* pph,
+					 ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds an NNC polyhedron that approximates C_Polyhedron \p ph,
+  using an algorithm whose complexity does not exceed \p complexity;
+  writes a handle for the newly created polyhedron at address \p pph.
+
+  \note
+  The complexity argument, which can take values
+  \c PPL_COMPLEXITY_CLASS_POLYNOMIAL, \c PPL_COMPLEXITY_CLASS_SIMPLEX
+  and \c PPL_COMPLEXITY_CLASS_ANY, is ignored since the exact constructor
+  has polynomial complexity.
+*/
+int
+ppl_new_NNC_Polyhedron_from_C_Polyhedron_with_complexity
+(ppl_Polyhedron_t* pph, ppl_const_Polyhedron_t ph, int complexity);
+
+/*@}*/ /* Constructors Behaving as Conversion Operators */
+
+/*! \brief \name Destructor for (C or NNC) Polyhedra */
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Invalidates the handle \p ph: this makes sure the corresponding
+  resources will eventually be released.
+*/
+int
+ppl_delete_Polyhedron(ppl_const_Polyhedron_t ph);
+
+/*@}*/ /* Destructor for (C or NNC) Polyhedra */
+
+/*! \brief \name Functions that Do Not Modify the Polyhedron */
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes to \p m the dimension of the vector space enclosing \p ph.
+*/
+int
+ppl_Polyhedron_space_dimension
+(ppl_const_Polyhedron_t ph, ppl_dimension_type* m);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes to \p m the affine dimension of \p ph (not to be confused with the
+  dimension of its enclosing vector space) or 0, if \p ph is empty.
+*/
+int
+ppl_Polyhedron_affine_dimension
+(ppl_const_Polyhedron_t ph, ppl_dimension_type* m);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Checks the relation between the polyhedron \p ph and the constraint \p c.
+
+  If successful, returns a non-negative integer that is
+  obtained as the bitwise or of the bits (chosen among
+  PPL_POLY_CON_RELATION_IS_DISJOINT
+  PPL_POLY_CON_RELATION_STRICTLY_INTERSECTS,
+  PPL_POLY_CON_RELATION_IS_INCLUDED, and
+  PPL_POLY_CON_RELATION_SATURATES) that describe the relation between
+  \p ph and \p c.
+*/
+int
+ppl_Polyhedron_relation_with_Constraint
+(ppl_const_Polyhedron_t ph, ppl_const_Constraint_t c);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Checks the relation between the polyhedron \p ph and the generator \p g.
+
+  If successful, returns a non-negative integer that is
+  obtained as the bitwise or of the bits (only
+  PPL_POLY_GEN_RELATION_SUBSUMES, at present) that describe the
+  relation between \p ph and \p g.
+*/
+int
+ppl_Polyhedron_relation_with_Generator
+(ppl_const_Polyhedron_t ph, ppl_const_Generator_t g);
+
+int
+ppl_Polyhedron_relation_with_Congruence
+(ppl_const_Polyhedron_t ph, ppl_const_Congruence_t c);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes a const handle to the constraint system defining the
+  polyhedron \p ph at address \p pcs.
+*/
+int
+ppl_Polyhedron_get_constraints
+(ppl_const_Polyhedron_t ph, ppl_const_Constraint_System_t* pcs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes at address \p pcs a const handle to a system of congruences
+  approximating the polyhedron \p ph.
+*/
+int
+ppl_Polyhedron_get_congruences
+(ppl_const_Polyhedron_t ph, ppl_const_Congruence_System_t* pcs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes a const handle to the minimized constraint system defining the
+  polyhedron \p ph at address \p pcs.
+*/
+int
+ppl_Polyhedron_get_minimized_constraints
+(ppl_const_Polyhedron_t ph, ppl_const_Constraint_System_t* pcs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes at address \p pcs a const handle to a system of minimized
+  congruences approximating the polyhedron \p ph.
+*/
+int
+ppl_Polyhedron_get_minimized_congruences
+(ppl_const_Polyhedron_t ph, ppl_const_Congruence_System_t* pcs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph is empty; returns 0 if \p ph is
+  not empty.
+*/
+int
+ppl_Polyhedron_is_empty(ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph is a universe polyhedron;
+  returns 0 if it is not.
+*/
+int
+ppl_Polyhedron_is_universe(ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph is bounded; returns 0 if \p ph is
+  unbounded.
+*/
+int
+ppl_Polyhedron_is_bounded(ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph contains at least one integer
+  point; returns 0 otherwise.
+*/
+int
+ppl_Polyhedron_contains_integer_point(ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph is topologically closed;
+  returns 0 if \p ph is not topologically closed.
+*/
+int
+ppl_Polyhedron_is_topologically_closed(ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph is a discrete set;
+  returns 0 if \p ph is not a discrete set.
+*/
+int
+ppl_Polyhedron_is_discrete(ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph constrains \p var;
+  returns 0 if \p ph does not constrain \p var.
+*/
+int
+ppl_Polyhedron_constrains
+(ppl_Polyhedron_t ph, ppl_dimension_type var);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p le is bounded from above in \p ph;
+  returns 0 otherwise.
+*/
+int
+ppl_Polyhedron_bounds_from_above
+(ppl_const_Polyhedron_t ph, ppl_const_Linear_Expression_t le);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p le is bounded from below in \p ph;
+  returns 0 otherwise.
+*/
+int
+ppl_Polyhedron_bounds_from_below
+(ppl_const_Polyhedron_t ph, ppl_const_Linear_Expression_t le);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph is not empty
+  and \p le is bounded from above in \p ph, in which case
+  the supremum value and a point where \p le reaches it are computed.
+
+  \param ph
+  The polyhedron constraining \p le;
+
+  \param le
+  The linear expression to be maximized subject to \p ph;
+
+  \param sup_n
+  Will be assigned the numerator of the supremum value;
+
+  \param sup_d
+  Will be assigned the denominator of the supremum value;
+
+  \param pmaximum
+  Will store 1 in this location if the supremum is also the maximum,
+  will store 0 otherwise;
+
+  \param point
+  Will be assigned the point or closure point where \p le reaches the
+  extremum value.
+
+  If \p ph is empty or \p le is not bounded from above,
+  0 will be returned and \p sup_n, \p sup_d, \p *pmaximum and \p point
+  will be left untouched.
+*/
+int
+ppl_Polyhedron_maximize_with_point
+(ppl_const_Polyhedron_t ph,
+ ppl_const_Linear_Expression_t le,
+ ppl_Coefficient_t sup_n,
+ ppl_Coefficient_t sup_d,
+ int* pmaximum,
+ ppl_Generator_t point);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  The same as ppl_Polyhedron_maximize_with_point, but without the
+  output argument for the location where the supremum value is reached.
+*/
+int
+ppl_Polyhedron_maximize
+(ppl_const_Polyhedron_t ph,
+ ppl_const_Linear_Expression_t le,
+ ppl_Coefficient_t sup_n,
+ ppl_Coefficient_t sup_d,
+ int* pmaximum);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if  \p ph is not empty
+  and \p le is bounded from below in \p ph, in which case
+  the infimum value and a point where \p le reaches it are computed.
+
+  \param ph
+  The polyhedron constraining \p le;
+
+  \param le
+  The linear expression to be minimized subject to \p ph;
+
+  \param inf_n
+  Will be assigned the numerator of the infimum value;
+
+  \param inf_d
+  Will be assigned the denominator of the infimum value;
+
+  \param pminimum
+  Will store 1 in this location if the infimum is also the minimum,
+  will store 0 otherwise;
+
+  \param point
+  Will be assigned the point or closure point where \p le reaches the
+  extremum value.
+
+  If \p ph is empty or \p le is not bounded from below,
+  0 will be returned and \p sup_n, \p sup_d, \p *pmaximum and \p point
+  will be left untouched.
+*/
+int
+ppl_Polyhedron_minimize_with_point
+(ppl_const_Polyhedron_t ph,
+ ppl_const_Linear_Expression_t le,
+ ppl_Coefficient_t inf_n,
+ ppl_Coefficient_t inf_d,
+ int* pminimum,
+ ppl_Generator_t point);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  The same as ppl_Polyhedron_minimize_with_point, but without the
+  output argument for the location where the infimum value is reached.
+*/
+int
+ppl_Polyhedron_minimize_with_point
+(ppl_const_Polyhedron_t ph,
+ ppl_const_Linear_Expression_t le,
+ ppl_Coefficient_t inf_n,
+ ppl_Coefficient_t inf_d,
+ int* pminimum);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p x contains or is equal to \p y;
+  returns 0 if it does not.
+*/
+int
+ppl_Polyhedron_contains_Polyhedron
+(ppl_const_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p x strictly contains \p y; returns 0
+  if it does not.
+*/
+int
+ppl_Polyhedron_strictly_contains_Polyhedron
+(ppl_const_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p x and \p y are disjoint; returns 0
+  if they are not.
+*/
+int
+ppl_Polyhedron_is_disjoint_from_Polyhedron
+(ppl_const_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p x and \p y are the same polyhedron;
+  returns 0 if they are different.
+
+  Note that \p x and \p y may be topology- and/or dimension-incompatible
+  polyhedra: in those cases, the value 0 is returned.
+*/
+int
+ppl_Polyhedron_equals_Polyhedron
+(ppl_const_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Returns a positive integer if \p ph is well formed, i.e., if it
+  satisfies all its implementation invariants; returns 0 and perhaps
+  makes some noise if \p ph is broken.  Useful for debugging purposes.
+*/
+int
+ppl_Polyhedron_OK(ppl_const_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes to \p sz a lower bound to the size in bytes of the memory
+  managed by \p ph.
+*/
+int
+ppl_Polyhedron_external_memory_in_bytes
+(ppl_const_Polyhedron_t ph, size_t* sz);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes to \p sz a lower bound to the size in bytes of the memory
+  managed by \p ph.
+*/
+int
+ppl_Polyhedron_total_memory_in_bytes
+(ppl_const_Polyhedron_t ph, size_t* sz);
+
+/*@}*/ /* Functions that Do Not Modify the Polyhedron */
+
+
+/*! \brief \name Space Dimension Preserving Functions that May Modify the Polyhedron */
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds a copy of the constraint \p c to the system of constraints of \p ph.
+*/
+int
+ppl_Polyhedron_add_constraint
+(ppl_Polyhedron_t ph, ppl_const_Constraint_t c);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds a copy of the congruence \p c to polyhedron of \p ph.
+*/
+int
+ppl_Polyhedron_add_congruence
+(ppl_Polyhedron_t ph, ppl_const_Congruence_t c);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds a copy of the system of constraints \p cs to the system of
+  constraints of \p ph.
+*/
+int
+ppl_Polyhedron_add_constraints
+(ppl_Polyhedron_t ph, ppl_const_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds a copy of the system of congruences \p cs to the polyhedron \p ph.
+*/
+int
+ppl_Polyhedron_add_congruences
+(ppl_Polyhedron_t ph, ppl_const_Congruence_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds the system of constraints \p cs to the system of constraints of
+  \p ph.
+
+  \warning
+  This function modifies the constraint system referenced by \p cs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_Polyhedron_add_recycled_constraints
+(ppl_Polyhedron_t ph, ppl_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds the system of congruences \p cs to the polyhedron \p ph.
+
+  \warning
+  This function modifies the congruence system referenced by \p cs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_Polyhedron_add_recycled_congruences
+(ppl_Polyhedron_t ph, ppl_Congruence_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Refines \p ph using constraint \p c.
+*/
+int
+ppl_Polyhedron_refine_with_constraint
+(ppl_Polyhedron_t ph, ppl_const_Constraint_t c);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Refines \p ph using congruence \p c.
+*/
+int
+ppl_Polyhedron_refine_with_congruence
+(ppl_Polyhedron_t ph, ppl_const_Congruence_t c);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Refines \p ph using the constraints in \p cs.
+*/
+int
+ppl_Polyhedron_refine_with_constraints
+(ppl_Polyhedron_t ph, ppl_const_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Refines \p ph using the congruences in \p cs.
+*/
+int
+ppl_Polyhedron_refine_with_congruences
+(ppl_Polyhedron_t ph, ppl_const_Congruence_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Intersects \p x with polyhedron \p y and assigns the result to \p x.
+*/
+int
+ppl_Polyhedron_intersection_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p x an upper bound of \p x and \p y.
+
+  For the domain of polyhedra, this is the same as
+  <CODE>ppl_Polyhedron_poly_hull_assign(x, y)</CODE>.
+*/
+int
+ppl_Polyhedron_upper_bound_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Same as ppl_Polyhedron_poly_difference_assign(x, y).
+*/
+int
+ppl_Polyhedron_difference_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p x the
+  \extref{Meet_Preserving_Simplification, meet-preserving simplification}
+  of \p x with respect to context \p y. Returns a positive integer if
+  \p x and \p y have a nonempty intersection; returns \c 0 if they
+  are disjoint.
+*/
+int
+ppl_Polyhedron_simplify_using_context_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p x the \extref{Time_Elapse_Operator, time-elapse} between
+  the polyhedra \p x and \p y.
+*/
+int
+ppl_Polyhedron_time_elapse_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p ph its topological closure.
+*/
+int
+ppl_Polyhedron_topological_closure_assign(ppl_Polyhedron_t ph);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Modifies \p ph by \extref{Cylindrification, unconstraining}
+  the space dimension \p var.
+*/
+int
+ppl_Polyhedron_unconstrain_space_dimension
+(ppl_Polyhedron_t ph, ppl_dimension_type var);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Modifies \p ph by \extref{Cylindrification, unconstraining}
+  the space dimensions that are specified in the first \p n positions
+  of the array \p ds.
+  The presence of duplicates in \p ds is a waste but an innocuous one.
+*/
+int
+ppl_Polyhedron_unconstrain_space_dimensions
+(ppl_Polyhedron_t ph, ppl_dimension_type ds[], size_t n);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Transforms the polyhedron \p ph, assigning an affine expression
+  to the specified variable.
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param var
+  The variable to which the affine expression is assigned;
+
+  \param le
+  The numerator of the affine expression;
+
+  \param d
+  The denominator of the affine expression.
+*/
+int
+ppl_Polyhedron_affine_image
+(ppl_Polyhedron_t ph,
+ ppl_dimension_type var,
+ ppl_const_Linear_Expression_t le,
+ ppl_const_Coefficient_t d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Transforms the polyhedron \p ph, substituting an affine expression
+  to the specified variable.
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param var
+  The variable to which the affine expression is substituted;
+
+  \param le
+  The numerator of the affine expression;
+
+  \param d
+  The denominator of the affine expression.
+*/
+int
+ppl_Polyhedron_affine_preimage
+(ppl_Polyhedron_t ph,
+ ppl_dimension_type var,
+ ppl_const_Linear_Expression_t le,
+ ppl_const_Coefficient_t d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p ph the image of \p ph with respect to the
+  \extref{Generalized_Affine_Relations, generalized affine transfer relation}
+  \f$\frac{\mathrm{lb}}{\mathrm{d}}
+       \leq \mathrm{var}'
+         \leq \frac{\mathrm{ub}}{\mathrm{d}}\f$.
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param var
+  The variable bounded by the generalized affine transfer relation;
+
+  \param lb
+  The numerator of the lower bounding affine expression;
+
+  \param ub
+  The numerator of the upper bounding affine expression;
+
+  \param d
+  The (common) denominator of the lower and upper bounding affine expressions.
+*/
+int
+ppl_Polyhedron_bounded_affine_image
+(ppl_Polyhedron_t ph,
+ ppl_dimension_type var,
+ ppl_const_Linear_Expression_t lb,
+ ppl_const_Linear_Expression_t ub,
+ ppl_const_Coefficient_t d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p ph the preimage of \p ph with respect to the
+  \extref{Generalized_Affine_Relations, generalized affine transfer relation}
+  \f$\frac{\mathrm{lb}}{\mathrm{d}}
+       \leq \mathrm{var}'
+         \leq \frac{\mathrm{ub}}{\mathrm{d}}\f$.
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param var
+  The variable bounded by the generalized affine transfer relation;
+
+  \param lb
+  The numerator of the lower bounding affine expression;
+
+  \param ub
+  The numerator of the upper bounding affine expression;
+
+  \param d
+  The (common) denominator of the lower and upper bounding affine expressions.
+*/
+int
+ppl_Polyhedron_bounded_affine_preimage
+(ppl_Polyhedron_t ph,
+ ppl_dimension_type var,
+ ppl_const_Linear_Expression_t lb,
+ ppl_const_Linear_Expression_t ub,
+ ppl_const_Coefficient_t d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p ph the image of \p ph with respect to the
+  \extref{Generalized_Affine_Relations, generalized affine transfer relation}
+  \f$\mathrm{var}' \relsym \frac{\mathrm{le}}{\mathrm{d}}\f$,
+  where \f$\mathord{\relsym}\f$ is the relation symbol encoded
+  by \p relsym.
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param var
+  The left hand side variable of the generalized affine transfer relation;
+
+  \param relsym
+  The relation symbol;
+
+  \param le
+  The numerator of the right hand side affine expression;
+
+  \param d
+  The denominator of the right hand side affine expression.
+*/
+int
+ppl_Polyhedron_generalized_affine_image
+(ppl_Polyhedron_t ph,
+ ppl_dimension_type var,
+ enum ppl_enum_Constraint_Type relsym,
+ ppl_const_Linear_Expression_t le,
+ ppl_const_Coefficient_t d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p ph the preimage of \p ph with respect to the
+  \extref{Generalized_Affine_Relations, generalized affine transfer relation}
+  \f$\mathrm{var}' \relsym \frac{\mathrm{le}}{\mathrm{d}}\f$,
+  where \f$\mathord{\relsym}\f$ is the relation symbol encoded
+  by \p relsym.
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param var
+  The left hand side variable of the generalized affine transfer relation;
+
+  \param relsym
+  The relation symbol;
+
+  \param le
+  The numerator of the right hand side affine expression;
+
+  \param d
+  The denominator of the right hand side affine expression.
+*/
+int
+ppl_Polyhedron_generalized_affine_preimage
+(ppl_Polyhedron_t ph,
+ ppl_dimension_type var,
+ enum ppl_enum_Constraint_Type relsym,
+ ppl_const_Linear_Expression_t le,
+ ppl_const_Coefficient_t d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p ph the image of \p ph with respect to the
+  \extref{Generalized_Affine_Relations, generalized affine transfer relation}
+  \f$\mathrm{lhs}' \relsym \mathrm{rhs}\f$, where
+  \f$\mathord{\relsym}\f$ is the relation symbol encoded by \p relsym.
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param lhs
+  The left hand side affine expression;
+
+  \param relsym
+  The relation symbol;
+
+  \param rhs
+  The right hand side affine expression.
+*/
+int
+ppl_Polyhedron_generalized_affine_image_lhs_rhs
+(ppl_Polyhedron_t ph,
+ ppl_const_Linear_Expression_t lhs,
+ enum ppl_enum_Constraint_Type relsym,
+ ppl_const_Linear_Expression_t rhs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p ph the preimage of \p ph with respect to the
+  \extref{Generalized_Affine_Relations, generalized affine transfer relation}
+  \f$\mathrm{lhs}' \relsym \mathrm{rhs}\f$, where
+  \f$\mathord{\relsym}\f$ is the relation symbol encoded by \p relsym.
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param lhs
+  The left hand side affine expression;
+
+  \param relsym
+  The relation symbol;
+
+  \param rhs
+  The right hand side affine expression.
+*/
+int
+ppl_Polyhedron_generalized_affine_preimage_lhs_rhs
+(ppl_Polyhedron_t ph,
+ ppl_const_Linear_Expression_t lhs,
+ enum ppl_enum_Constraint_Type relsym,
+ ppl_const_Linear_Expression_t rhs);
+
+/*@}*/ /* Space Dimension Preserving Functions that May Modify [...] */
+
+
+/*! \brief \name Functions that May Modify the Dimension of the Vector Space */
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Seeing a polyhedron as a set of tuples (its points), assigns
+  to \p x all the tuples that can be obtained by concatenating,
+  in the order given, a tuple of \p x with a tuple of \p y.
+*/
+int
+ppl_Polyhedron_concatenate_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds \p d new dimensions to the space enclosing the polyhedron \p ph
+  and to \p ph itself.
+*/
+int
+ppl_Polyhedron_add_space_dimensions_and_embed
+(ppl_Polyhedron_t ph, ppl_dimension_type d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds \p d new dimensions to the space enclosing the polyhedron \p ph.
+*/
+int
+ppl_Polyhedron_add_space_dimensions_and_project
+(ppl_Polyhedron_t ph, ppl_dimension_type d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Removes from the vector space enclosing \p ph the space dimensions that
+  are specified in first \p n positions of the array \p ds.  The presence
+  of duplicates in \p ds is a waste but an innocuous one.
+*/
+int
+ppl_Polyhedron_remove_space_dimensions
+(ppl_Polyhedron_t ph, ppl_dimension_type ds[], size_t n);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Removes the higher dimensions from the vector space enclosing \p ph
+  so that, upon successful return, the new space dimension is \p d.
+*/
+int
+ppl_Polyhedron_remove_higher_space_dimensions
+(ppl_Polyhedron_t ph, ppl_dimension_type d);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Remaps the dimensions of the vector space according to a
+  \extref{Mapping_the_Dimensions_of_the_Vector_Space, partial function}.
+  This function is specified by means of the \p maps array,
+  which has \p n entries.
+
+  The partial function is defined on dimension <CODE>i</CODE>
+  if <CODE>i < n</CODE> and <CODE>maps[i] != ppl_not_a_dimension</CODE>;
+  otherwise it is undefined on dimension <CODE>i</CODE>.
+  If the function is defined on dimension <CODE>i</CODE>, then dimension
+  <CODE>i</CODE> is mapped onto dimension <CODE>maps[i]</CODE>.
+
+  The result is undefined if \p maps does not encode a partial
+  function with the properties described in the
+  \extref{Mapping_the_Dimensions_of_the_Vector_Space,
+          specification of the mapping operator}.
+*/
+int
+ppl_Polyhedron_map_space_dimensions
+(ppl_Polyhedron_t ph, ppl_dimension_type maps[], size_t n);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  \extref{expand_space_dimension, Expands} the \f$d\f$-th dimension of
+  the vector space enclosing \p ph to \p m new space dimensions.
+*/
+int
+ppl_Polyhedron_expand_space_dimension
+(ppl_Polyhedron_t ph, ppl_dimension_type d, ppl_dimension_type m);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Modifies \p ph by \extref{fold_space_dimensions, folding} the
+  space dimensions contained in the first \p n positions of the array \p ds
+  into dimension \p d.  The presence of duplicates in \p ds is a waste
+  but an innocuous one.
+*/
+int
+ppl_Polyhedron_fold_space_dimensions
+(ppl_Polyhedron_t ph,
+ ppl_dimension_type ds[],
+ size_t n,
+ ppl_dimension_type d);
+
+/*@}*/ /* Functions that May Modify the Dimension of the Vector Space */
+
+/*! \brief \name Input/Output Functions */
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag
+  \brief Prints \p x to \c stdout.
+*/
+int
+ppl_io_print_Polyhedron(ppl_const_Polyhedron_t x);
+
+/*! \relates ppl_Polyhedron_tag
+  \brief Prints \p x to the given output \p stream.
+*/
+int
+ppl_io_fprint_Polyhedron(FILE* stream, ppl_const_Polyhedron_t x);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Prints \p x to a malloc-allocated string, a pointer to which
+  is returned via \p strp.
+*/
+int
+ppl_io_asprint_Polyhedron(char** strp, ppl_const_Polyhedron_t x);
+
+/*! \relates ppl_Polyhedron_tag
+  \brief Dumps an ascii representation of \p x on \p stream.
+*/
+int
+ppl_Polyhedron_ascii_dump(ppl_const_Polyhedron_t x, FILE* stream);
+
+/*! \relates ppl_Polyhedron_tag
+  \brief Loads an ascii representation of \p x from \p stream.
+*/
+int
+ppl_Polyhedron_ascii_load(ppl_Polyhedron_t x, FILE* stream);
+
+/*@}*/ /* Input-Output Functions */
+
+
+/*! \name Ad Hoc Functions for (C or NNC) Polyhedra
+  The functions listed here below, being specific of the polyhedron domains,
+  do not have a correspondence in other semantic geometric descriptions.
+*/
+/*@{*/
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new C polyhedron from the system of generators
+  \p gs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p gs.
+*/
+int
+ppl_new_C_Polyhedron_from_Generator_System
+(ppl_Polyhedron_t* pph, ppl_const_Generator_System_t gs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new C polyhedron recycling the system of generators
+  \p gs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p gs.
+
+  \warning
+  This function modifies the generator system referenced by \p gs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_new_C_Polyhedron_recycle_Generator_System
+(ppl_Polyhedron_t* pph, ppl_Generator_System_t gs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new NNC polyhedron from the system of generators
+  \p gs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p gs.
+*/
+int
+ppl_new_NNC_Polyhedron_from_Generator_System
+(ppl_Polyhedron_t* pph, ppl_const_Generator_System_t gs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Builds a new NNC polyhedron recycling the system of generators
+  \p gs and writes a handle for the newly created polyhedron at
+  address \p pph.
+
+  The new polyhedron will inherit the space dimension of \p gs.
+
+  \warning
+  This function modifies the generator system referenced by \p gs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_new_NNC_Polyhedron_recycle_Generator_System
+(ppl_Polyhedron_t* pph, ppl_Generator_System_t gs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes a const handle to the generator system defining the
+  polyhedron \p ph at address \p pgs.
+*/
+int
+ppl_Polyhedron_get_generators
+(ppl_const_Polyhedron_t ph, ppl_const_Generator_System_t* pgs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Writes a const handle to the minimized generator system defining the
+  polyhedron \p ph at address \p pgs.
+*/
+int
+ppl_Polyhedron_get_minimized_generators
+(ppl_const_Polyhedron_t ph, ppl_const_Generator_System_t* pgs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds a copy of the generator \p g to the system of generators of \p ph.
+*/
+int
+ppl_Polyhedron_add_generator
+(ppl_Polyhedron_t ph, ppl_const_Generator_t g);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds a copy of the system of generators \p gs to the system of
+  generators of \p ph.
+*/
+int
+ppl_Polyhedron_add_generators
+(ppl_Polyhedron_t ph, ppl_const_Generator_System_t gs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Adds the system of generators \p gs to the system of generators of
+  \p ph.
+
+  \warning
+  This function modifies the generator system referenced by \p gs:
+  upon return, no assumption can be made on its value.
+*/
+int
+ppl_Polyhedron_add_recycled_generators
+(ppl_Polyhedron_t ph, ppl_Generator_System_t gs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p x the poly-hull of \p x and \p y.
+*/
+int
+ppl_Polyhedron_poly_hull_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p x the \extref{Convex_Polyhedral_Difference, poly-difference}
+  of \p x and \p y.
+*/
+int
+ppl_Polyhedron_poly_difference_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  Assigns to \p ph the polyhedron obtained from \p ph by "wrapping" the vector
+  space defined by the first \p n space dimensions in \p ds[].
+
+  \param ph
+  The polyhedron that is transformed;
+
+  \param ds[]
+  Specifies the space dimensions to be wrapped.
+
+  \param n
+  The first \p n space dimensions in the array \p ds[] will be wrapped.
+
+  \param w
+  The width of the bounded integer type corresponding to
+  all the dimensions to be wrapped.
+
+  \param r
+  The representation of the bounded integer type corresponding to
+  all the dimensions to be wrapped.
+
+  \param o
+  The overflow behavior of the bounded integer type corresponding to
+  all the dimensions to be wrapped.
+
+  \param pcs
+  Possibly null pointer to a constraint system whose space dimensions
+  are the first \p n dimensions in \p ds[]. If <CODE>*pcs</CODE>
+  depends on variables not in \p vars, the behavior is undefined.
+  When non-null, the constraint system is assumed to
+  represent the conditional or looping construct guard with respect
+  to which wrapping is performed.  Since wrapping requires the
+  computation of upper bounds and due to non-distributivity of
+  constraint refinement over upper bounds, passing a constraint
+  system in this way can be more precise than refining the result of
+  the wrapping operation with the constraints in <CODE>cs</CODE>.
+
+  \param complexity_threshold
+  A precision parameter where higher values result in possibly improved
+  precision.
+
+  \param wrap_individually
+  Non-zero if the dimensions should be wrapped individually
+  (something that results in much greater efficiency to the detriment of
+  precision).
+  */
+  int wrap_assign(ppl_Polyhedron_t ph,
+                  ppl_dimension_type ds[],
+                  size_t n,
+                  ppl_enum_Bounded_Integer_Type_Width w,
+                  ppl_enum_Bounded_Integer_Type_Representation r,
+                  ppl_enum_Bounded_Integer_Type_Overflow o,
+                  const ppl_const_Constraint_System_t* pcs,
+                  unsigned complexity_threshold,
+                  int wrap_individually);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{BHRZ03_widening, BHRZ03-widening} of
+  \p x and \p y.  If \p tp is not the null pointer, the
+  \extref{Widening_with_Tokens, widening with tokens} delay technique
+  is applied with <CODE>*tp</CODE> available tokens.
+*/
+int
+ppl_Polyhedron_BHRZ03_widening_assign_with_tokens
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y, unsigned* tp);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{H79_widening, H79-widening} of \p x
+  and \p y.  If \p tp is not the null pointer, the
+  \extref{Widening_with_Tokens, widening with tokens} delay technique is
+  applied with <CODE>*tp</CODE> available tokens.
+*/
+int
+ppl_Polyhedron_H79_widening_assign_with_tokens
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y, unsigned* tp);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{BHRZ03_widening, BHRZ03-widening} of
+  \p x and \p y.
+*/
+int
+ppl_Polyhedron_BHRZ03_widening_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{H79_widening, H79-widening} of \p x
+  and \p y.
+*/
+int
+ppl_Polyhedron_H79_widening_assign
+(ppl_Polyhedron_t x, ppl_const_Polyhedron_t y);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{BHRZ03_widening, BHRZ03-widening} of
+  \p x and \p y intersected with the constraints in \p cs that are
+  satisfied by all the points of \p x.  If \p tp is not the null pointer,
+  the \extref{Widening_with_Tokens, widening with tokens} delay technique
+  is applied with <CODE>*tp</CODE> available tokens.
+*/
+int
+ppl_Polyhedron_limited_BHRZ03_extrapolation_assign_with_tokens
+(ppl_Polyhedron_t x,
+ ppl_const_Polyhedron_t y,
+ ppl_const_Constraint_System_t cs,
+ unsigned* tp);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{H79_widening, H79-widening} of \p x
+  and \p y intersected with the constraints in \p cs that are
+  satisfied by all the points of \p x. If \p tp is not the null
+  pointer, the \extref{Widening_with_Tokens, widening with tokens} delay
+  technique is applied with <CODE>*tp</CODE> available tokens.
+*/
+int
+ppl_Polyhedron_limited_H79_extrapolation_assign_with_tokens
+(ppl_Polyhedron_t x,
+ ppl_const_Polyhedron_t y,
+ ppl_const_Constraint_System_t cs,
+ unsigned* tp);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{BHRZ03_widening, BHRZ03-widening} of
+  \p x and \p y intersected with the constraints in \p cs that are
+  satisfied by all the points of \p x.
+*/
+int
+ppl_Polyhedron_limited_BHRZ03_extrapolation_assign
+(ppl_Polyhedron_t x,
+ ppl_const_Polyhedron_t y,
+ ppl_const_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{H79_widening, H79-widening} of \p x
+  and \p y intersected with the constraints in \p cs that are
+  satisfied by all the points of \p x.
+*/
+int
+ppl_Polyhedron_limited_H79_extrapolation_assign
+(ppl_Polyhedron_t x,
+ ppl_const_Polyhedron_t y,
+ ppl_const_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{BHRZ03_widening, BHRZ03-widening} of
+  \p x and \p y intersected with the constraints in \p cs that are
+  satisfied by all the points of \p x, further intersected with all
+  the constraints of the form \f$\pm v \leq r\f$ and \f$\pm v < r\f$,
+  with \f$r \in \Qset\f$, that are satisfied by all the points of \p
+  x. If \p tp is not the null pointer,
+  the \extref{Widening_with_Tokens, widening with tokens} delay technique
+  is applied with <CODE>*tp</CODE> available tokens.
+*/
+int
+ppl_Polyhedron_bounded_BHRZ03_extrapolation_assign_with_tokens
+(ppl_Polyhedron_t x,
+ ppl_const_Polyhedron_t y,
+ ppl_const_Constraint_System_t cs,
+ unsigned* tp);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{H79_widening, H79-widening} of \p x
+  and \p y intersected with the constraints in \p cs that are
+  satisfied by all the points of \p x, further intersected with all
+  the constraints of the form \f$\pm v \leq r\f$ and \f$\pm v < r\f$,
+  with \f$r \in \Qset\f$, that are satisfied by all the points of \p x.
+  If \p tp is not the null pointer,
+  the \extref{Widening_with_Tokens, widening with tokens} delay technique
+  is applied with <CODE>*tp</CODE> available tokens.
+*/
+int
+ppl_Polyhedron_bounded_H79_extrapolation_assign_with_tokens
+(ppl_Polyhedron_t x,
+ ppl_const_Polyhedron_t y,
+ ppl_const_Constraint_System_t cs,
+ unsigned* tp);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{BHRZ03_widening, BHRZ03-widening} of
+  \p x and \p y intersected with the constraints in \p cs that are
+  satisfied by all the points of \p x, further intersected with all
+  the constraints of the form \f$\pm v \leq r\f$ and \f$\pm v < r\f$,
+  with \f$r \in \Qset\f$, that are satisfied by all the points of \p x.
+*/
+int
+ppl_Polyhedron_bounded_BHRZ03_extrapolation_assign
+(ppl_Polyhedron_t x,
+ ppl_const_Polyhedron_t y,
+ ppl_const_Constraint_System_t cs);
+
+/*! \relates ppl_Polyhedron_tag \brief
+  If the polyhedron \p y is contained in (or equal to) the polyhedron
+  \p x, assigns to \p x the \extref{H79_widening, H79-widening} of \p x
+  and \p y intersected with the constraints in \p cs that are
+  satisfied by all the points of \p x, further intersected with all
+  the constraints of the form \f$\pm v \leq r\f$ and \f$\pm v < r\f$,
+  with \f$r \in \Qset\f$, that are satisfied by all the points of \p x.
+*/
+int
+ppl_Polyhedron_bounded_H79_extrapolation_assign
+(ppl_Polyhedron_t x,
+ ppl_const_Polyhedron_t y,
+ ppl_const_Constraint_System_t cs);
+
+/*@}*/ /* Ad Hoc Functions for (C or NNC) Polyhedra */
+
+/*! \interface ppl_Pointset_Powerset_C_Polyhedron_tag
+  \brief
+  Types and functions for the Pointset_Powerset of C_Polyhedron objects.
+
+  The powerset domains can be instantiated by taking as a base domain
+  any fixed semantic geometric description
+  (C and NNC polyhedra, BD and octagonal shapes, boxes and grids).
+  An element of the powerset domain represents a disjunctive collection
+  of base objects (its disjuncts), all having the same space dimension.
+
+  Besides the functions that are available in all semantic geometric
+  descriptions (whose documentation is not repeated here),
+  the powerset domain also provides several ad hoc functions.
+  In particular, the iterator types allow for the examination and
+  manipulation of the collection of disjuncts.
+*/
+
+#if !defined(PPL_DOXYGEN_CONFIGURED_MANUAL)
+
+/*! \brief Opaque pointer \ingroup Datatypes */
+typedef struct ppl_Pointset_Powerset_C_Polyhedron_tag*
+        ppl_Pointset_Powerset_C_Polyhedron_t;
+
+/*! \brief Opaque pointer to const object \ingroup Datatypes */
+typedef struct ppl_Pointset_Powerset_C_Polyhedron_tag const*
+        ppl_const_Pointset_Powerset_C_Polyhedron_t;
+
+/*! \interface ppl_Pointset_Powerset_C_Polyhedron_iterator_tag
+  \brief
+  Types and functions for iterating on the disjuncts of a
+  ppl_Pointset_Powerset_C_Polyhedron_tag.
+*/
+
+/*! \brief Opaque pointer \ingroup Datatypes */
+typedef struct ppl_Pointset_Powerset_C_Polyhedron_iterator_tag*
+        ppl_Pointset_Powerset_C_Polyhedron_iterator_t;
+
+/*! \brief Opaque pointer to const object \ingroup Datatypes */
+typedef struct ppl_Pointset_Powerset_C_Polyhedron_iterator_tag const*
+        ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t;
+
+/*! \interface ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag
+  \brief
+  Types and functions for iterating on the disjuncts of a
+  const ppl_Pointset_Powerset_C_Polyhedron_tag.
+*/
+
+/*! \brief Opaque pointer \ingroup Datatypes */
+typedef struct ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag*
+        ppl_Pointset_Powerset_C_Polyhedron_const_iterator_t;
+
+/*! \brief Opaque pointer to const object \ingroup Datatypes */
+typedef struct ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag const*
+        ppl_const_Pointset_Powerset_C_Polyhedron_const_iterator_t;
+
+#endif /* !defined(PPL_DOXYGEN_CONFIGURED_MANUAL) */
+
+/*! \brief \name Construction, Initialization and Destruction */
+/*@{*/
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Builds a new `iterator' and writes a handle to it
+  at address \p pit.
+*/
+int
+ppl_new_Pointset_Powerset_C_Polyhedron_iterator
+(ppl_Pointset_Powerset_C_Polyhedron_iterator_t* pit);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Builds a copy of \p y and writes a handle to it at address \p pit.
+*/
+int
+ppl_new_Pointset_Powerset_C_Polyhedron_iterator_from_iterator
+(ppl_Pointset_Powerset_C_Polyhedron_iterator_t* pit,
+ ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t y);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Builds a new `const iterator' and writes a handle to it
+  at address \p pit.
+*/
+int
+ppl_new_Pointset_Powerset_C_Polyhedron_const_iterator
+(ppl_Pointset_Powerset_C_Polyhedron_const_iterator_t* pit);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Builds a copy of \p y and writes a handle to it at address \p pit.
+*/
+int
+ppl_new_Pointset_Powerset_C_Polyhedron_const_iterator_from_const_iterator
+(ppl_Pointset_Powerset_C_Polyhedron_const_iterator_t* pit,
+ ppl_const_Pointset_Powerset_C_Polyhedron_const_iterator_t y);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Assigns to \p psit an iterator "pointing" to the beginning of
+  the sequence of disjuncts of \p ps.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_iterator_begin
+(ppl_Pointset_Powerset_C_Polyhedron_t ps,
+ ppl_Pointset_Powerset_C_Polyhedron_iterator_t psit);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Assigns to \p psit a const iterator "pointing" to the beginning of
+  the sequence of disjuncts of \p ps.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_const_iterator_begin
+(ppl_const_Pointset_Powerset_C_Polyhedron_t ps,
+ ppl_Pointset_Powerset_C_Polyhedron_const_iterator_t psit);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Assigns to \p psit an iterator "pointing" past the end of
+  the sequence of disjuncts of \p ps.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_iterator_end
+(ppl_Pointset_Powerset_C_Polyhedron_t ps,
+ ppl_Pointset_Powerset_C_Polyhedron_iterator_t psit);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Assigns to \p psit a const iterator "pointing" past the end of
+  the sequence of disjuncts of \p ps.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_const_iterator_end
+(ppl_const_Pointset_Powerset_C_Polyhedron_t ps,
+ ppl_Pointset_Powerset_C_Polyhedron_const_iterator_t psit);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Invalidates the handle \p it: this makes sure the corresponding
+  resources will eventually be released.
+*/
+int
+ppl_delete_Pointset_Powerset_C_Polyhedron_iterator
+(ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t it);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Invalidates the handle \p it: this makes sure the corresponding
+  resources will eventually be released.
+*/
+int
+ppl_delete_Pointset_Powerset_C_Polyhedron_const_iterator
+(ppl_const_Pointset_Powerset_C_Polyhedron_const_iterator_t it);
+
+/*@}*/ /* Construction, Initialization and Destruction */
+
+/*! \brief \name Dereferencing, Increment, Decrement and Equality Testing */
+/*@{*/
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Dereferences \p it writing a const handle to the resulting disjunct
+  at address \p d.
+
+  \note
+  Even though \p it is an non-const iterator, dereferencing it results
+  in a handle to a \b const disjunct. This is because mutable iterators
+  are meant to allow for the modification of the sequence of disjuncts
+  (e.g., by dropping elements), while preventing direct modifications
+  of the disjuncts they point to.
+
+  \warning
+  On exit, the disjunct \p d is still owned by the powerset object:
+  any function call on the owning powerset object may invalidate it.
+  Moreover, \p d should \b not be deleted directly: its resources will
+  be released when deleting the owning powerset.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_iterator_dereference
+(ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t it,
+ ppl_const_Polyhedron_t* d);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Dereferences \p it writing a const handle to the resulting disjunct
+  at address \p d.
+
+  \warning
+  On exit, the disjunct \p d is still owned by the powerset object:
+  any function call on the owning powerset object may invalidate it.
+  Moreover, \p d should \b not be deleted directly: its resources will
+  be released when deleting the owning powerset.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_const_iterator_dereference
+(ppl_const_Pointset_Powerset_C_Polyhedron_const_iterator_t it,
+ ppl_const_Polyhedron_t* d);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Increments \p it so that it "points" to the next disjunct.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_iterator_increment
+(ppl_Pointset_Powerset_C_Polyhedron_iterator_t it);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Increments \p it so that it "points" to the next disjunct.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_const_iterator_increment
+(ppl_Pointset_Powerset_C_Polyhedron_const_iterator_t it);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Decrements \p it so that it "points" to the previous disjunct.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_iterator_decrement
+(ppl_Pointset_Powerset_C_Polyhedron_iterator_t it);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Decrements \p it so that it "points" to the previous disjunct.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_const_iterator_decrement
+(ppl_Pointset_Powerset_C_Polyhedron_const_iterator_t it);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_iterator_tag \brief
+  Returns a positive integer if the iterators corresponding to \p x and
+  \p y are equal; returns 0 if they are different.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_iterator_equal_test
+(ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t x,
+ ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t y);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_const_iterator_tag \brief
+  Returns a positive integer if the iterators corresponding to \p x and
+  \p y are equal; returns 0 if they are different.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_const_iterator_equal_test
+(ppl_const_Pointset_Powerset_C_Polyhedron_const_iterator_t x,
+ ppl_const_Pointset_Powerset_C_Polyhedron_const_iterator_t y);
+
+/*@}*/ /* Dereferencing, Increment, Decrement and Equality Testing */
+
+
+/*! \brief \name Ad Hoc Functions for Pointset_Powerset domains */
+/*@{*/
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_tag \brief
+  Drops from the sequence of disjuncts in \p ps all the
+  non-maximal elements so that \p ps is non-redundant.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_omega_reduce
+(ppl_const_Pointset_Powerset_C_Polyhedron_t ps);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_tag \brief
+  Writes to \p sz the number of disjuncts in \p ps.
+
+  \note
+  If present, Omega-redundant elements will be counted too.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_size
+(ppl_const_Pointset_Powerset_C_Polyhedron_t ps, size_t* sz);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_tag \brief
+  Returns a positive integer if powerset \p x geometrically covers
+  powerset \p y; returns 0 otherwise.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_geometrically_covers_Pointset_Powerset_C_Polyhedron
+(ppl_const_Pointset_Powerset_C_Polyhedron_t x,
+ ppl_const_Pointset_Powerset_C_Polyhedron_t y);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_tag \brief
+  Returns a positive integer if powerset \p x is geometrically
+  equal to powerset \p y; returns 0 otherwise.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_geometrically_equals_Pointset_Powerset_C_Polyhedron
+(ppl_const_Pointset_Powerset_C_Polyhedron_t x,
+ ppl_const_Pointset_Powerset_C_Polyhedron_t y);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_tag \brief
+  Adds to \p ps a copy of disjunct \p d.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_add_disjunct
+(ppl_Pointset_Powerset_C_Polyhedron_t ps, ppl_const_Polyhedron_t d);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_tag \brief
+  Drops from \p ps the disjunct pointed to by \p cit,
+  assigning to \p it an iterator to the disjunct following \p cit.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_drop_disjunct
+(ppl_Pointset_Powerset_C_Polyhedron_t ps,
+ ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t cit,
+ ppl_Pointset_Powerset_C_Polyhedron_iterator_t it);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_tag \brief
+  Drops from \p ps all the disjuncts from \p first to \p last (excluded).
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_drop_disjuncts
+(ppl_Pointset_Powerset_C_Polyhedron_t ps,
+ ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t first,
+ ppl_const_Pointset_Powerset_C_Polyhedron_iterator_t last);
+
+/*! \relates ppl_Pointset_Powerset_C_Polyhedron_tag \brief
+  Modifies \p ps by (recursively) merging together the pairs of
+  disjuncts whose upper-bound is the same as their set-theoretical union.
+*/
+int
+ppl_Pointset_Powerset_C_Polyhedron_pairwise_reduce
+(ppl_Pointset_Powerset_C_Polyhedron_t ps);
+
+/*@}*/ /* Ad Hoc Functions for Pointset_Powerset domains */