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
The PPL development team:
Roberto Bagnara bagnara@cs.unipr.it Patricia M. Hill hill@comp.leeds.ac.uk Elisa Ricci ericci@cs.unipr.it Enea Zaffanella zaffanella@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.
participants (1)
-
Roberto Bagnara