[PPL-announce] Parma Polyhedra Library 0.4

[Roberto Bagnara]

After months of hard work, we have the pleasure to announce the
release 0.4 of the Parma Polyhedra Library.

This revolutionary release is a big step toward functional
completeness of the library.  We now have the best available support
for Not Necessarily Closed (NNC) polyhedra (that is, polyhedra that
can be expressed by a mixture of equalities and strict and non-strict
inequalities).  A complete C interface has been added and the Prolog
interface has been extended and generalized (now supporting GNU
Prolog, SICStus Prolog, SWI-Prolog and YAP).  Support has been added
for timeout-guarded operations.  Portability has also been greatly
improved: the library should now be completely written in standard
C/C++, compiles cleanly under three major C++ compilers and has been
roughly tested on a handful of different computing platforms.  Besides
that, almost everything has been improved and changed (forget about
any kind of compatibility with release 0.3).

For more information, visit the PPL web site at

       http://www.cs.unipr.it/ppl/

The PPL development team:

      Roberto Bagnara  <bagnara at cs.unipr.it>
      Patricia M. Hill <hill at comp.leeds.ac.uk>
      Elisa Ricci      <ericci at cs.unipr.it>
      Enea Zaffanella  <zaffanella at cs.unipr.it>


New and Changed Features
========================

o  Added full support for Not Necessarily Closed (NNC) polyhedra:
    - creation of strict inequality constraints and mixed constraint
      systems;
    - creation of closure points and extended generator systems;
    - added classes C_Polyhedron (for the representation of Closed
      polyhedra) and NNC_Polyhedron (the user no longer can create
      Polyhedron objects);
    - added topology compatibility checks to avoid mixing objects of
      the two kinds;
    - added explicit constructors to create a polyhedron of a given
      topology kind starting from a polyhedron of the other kind;
    - added methods Polyhedron::is_topologically_closed() and
      Polyhedron::topological_closure_assign();
    - implemented methods Polyhedron::minimized_constraints() and
      Polyhedron::minimized_generators() to obtain minimal
      descriptions, both for closed and for NNC polyhedra.

o  New method Polyhedron::time_elapse_assign(const Polyhedron&):
    it computes the time-elapse operation defined in

      N. Halbwachs, Y.-E. Proy, and P. Roumanoff.
      Verification of real-time systems using linear relation analysis.
      Formal Methods in System Design, 11(2):157-185, 1997.

o  New method Polyhedron::is_bounded(): it returns true if and only
    if the polyhedron is bounded, i.e., finite.

o  New methods Polyhedron::bounds_from_above(const LinExpression& e)
    and Polyhedron::bounds_from_below(const LinExpression& e): they
    return true if and only if the linear expression `e' is bounded
    from above/below in the polyhedron.

o  New, complete C interface.  As a demo, a toy solver for pure linear
    programming problems has been implemented using this interface.
    Notice that solving linear programming problems is completely
    outside the scope of the library.  As a consequence the toy provided
    as a demo is only a toy provided as a demo.

o  Revised and completed Prolog interface:
    - now supporting GNU Prolog, SICStus Prolog, SWI Prolog and YAP.
    - all predicates have been renamed to match their intended
      semantics;
    - arguments have been reordered where necessary so as to follow the
      rule "input arguments before output arguments";
    - predicates added so that all the public methods for Polyhedra in
      the C++ library are available as Prolog predicates;
    - the interface has been extended to allow for closed and not
      necessarily closed polyhedra.

o  Added support for timeout-guarded operations.  It is now possible
    for client applications to safely interrupt any exponential
    computation paths in the library and get control back in a time
    that is a linear function of the space dimension of the object
    (polyhedron, system of constraints or generators) of highest
    dimension on which the library is operating upon.

o  The methods named convex_hull_* and convex_difference_*
    have been renamed poly_hull_* and poly_difference_*.

o  All methods named *_and_minimize() now return a boolean
    flag that is false if the result is empty.

o  All method and variable names containing the word "vertex"
    have been replaced by names containing the word "point"
    (some previous uses of the word "vertex" were not formally correct).

o  The methods Polyhedron::includes(const Generator&) and
    Polyhedron::satisfies(const Constraint&) have been removed,
    as well as the enumeration GenSys_Con_Rel.
    They have been replaced by the new methods
    Polyhedron::relation_with(const Generator&) and
    Polyhedron::relation_with(const Constraint&),
    which return values of the new enumeration types
    Relation_Poly_Gen and Relation_Poly_Con, respectively.

o  The method Constraint::coefficient(void) has been renamed
    to Constraint::inhomogeneous_term(void).

o  The methods Polyhedron::widening_assign() and
    Polyhedron::limited_widening_assign() have been renamed
    Polyhedron::H79_widening_assign() and
    Polyhedron::limited_H79_widening_assign(), respectively.
    This emphasizes the fact that they implement extensions
    of the widenings introduced in

      N. Halbwachs.
      Détermination Automatique de Relations Linéaires
      Vérifiées par les Variables d'un Programme.
      Thèse de 3ème cicle d'informatique,
      Université scientifique et médicale de Grenoble,
      Grenoble, France, March 1979.

    and described in

      N. Halbwachs, Y.-E. Proy, and P. Roumanoff.
      Verification of real-time systems using linear relation analysis.
      Formal Methods in System Design, 11(2):157-185, 1997.

o  The library no longer calls abort(): appropriate exceptions
    are always thrown instead.


Bugfixes
========

o  Fixed a bug whereby creating a point with a negative denominator
    caused the library to misbehave.

o  Fixed a bug in Polyhedron::add_constraints(ConSys&) whereby
    we could have created constraint systems having rows with
    different capacities.

o  Several other bugs have been fixed.


-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it