PPL-announce

Download

ppl-announce@bugseng.com

November 2008

1 participants
1 discussions

Parma Polyhedra Library 0.10
by Roberto Bagnara 04 Nov '08

04 Nov '08

The core development team is very pleased to announce the availability of PPL 0.10, a new release, under the terms of the GNU General Public License version 3 (or later), of the Parma Polyhedra Library. This release has many new features. There are several new abstractions, among which: - An implementation of the domain of "octagonal shapes", an element of which may be seen as the solution of a finite system of constraints such as `x +/- y <= 3' (so that in 2D, it will have at most 8 sides). - An implementation of a domain of "boxes", which represents (geometrically speaking) a not necessarily closed, iso-oriented hyperrectangle. This can also be viewed as the smash product of `n' not necessarily closed and possibly unbounded intervals, where `n' is the space dimension of the box. The class LP_Problem has been renamed MIP_Problem and now supports the solution of Mixed Integer (Linear) Programming problems. The PPL semantic object Polyhedra_Powerset has been replaced by a templatic domain Pointset_Powerset that can take any (simple) PPL semantic object for the domain of its disjuncts. The language interfaces of the libraries now include OCaml and Java. Thus the PPL now has interfaces to C++, C, Java, OCaml, Ciao Prolog, GNU Prolog, SICStus, SWI-Prolog, XSB and YAP. Most of the domains provided by the C++ interface and almost all the public methods for these domains are also supported by the other language interfaces. The release also includes improvements to the documentation, many new configuration options, and some bug fixes. The precise list of user-visible changes is below. For more information, please come and visit the PPL web site at http://www.cs.unipr.it/ppl/ On behalf of all the past and present developers listed at http://www.cs.unipr.it/ppl/Credits/ and in the file CREDITS, Roberto Bagnara <bagnara(a)cs.unipr.it> Patricia M. Hill <hill(a)comp.leeds.ac.uk> Enea Zaffanella <zaffanella(a)cs.unipr.it> -------------------------------------------------------------------------- NEWS for version 0.10 (released on November 4, 2008) -------------------------------------------------------------------------- New and Changed Features ======================== The license ----------- o The Parma Polyhedra Library is now released under the terms of the version 3 (or later) of the GNU General Public License. New and renamed classes ----------------------- o The new class Octagonal_Shape provides an implementation of the domain of octagonal shapes (including optimized algorithms and a provably correct widening) as proposed by Roberto Bagnara, Patricia Hill, Elena Mazzi and Enea Zaffanella in their SAS 2005 paper. o A new abstraction called Box has been added. Geometrically speaking, a Box represents a not necessarily closed, iso-oriented hyperrectangle. This can also be seen as the smash product of `n' not necessarily closed and possibly unbounded intervals, where `n' is the space dimension of the box. The Box template class is parametric with respect to a class of intervals. o A generic implementation of intervals has been added. The template class Interval is parametric on the type used to represent the interval boundaries (all native integer and floating point types are supported as well as unbounded integers and rational numbers provided by GMP). Another class template type parameter allows for the control of a number of other features of the class (such as the ability to represent: open as well as closed boundaries, empty intervals in addition to nonempty ones, intervals of extended number families that contain positive and negative infinities, plain intervals of real numbers and intervals of integer numbers). The Interval class still needs a lot of work and both its implementation and its interface are likely to change significantly: it is released now because it is needed for the Box class and as a kind of technology preview. o The class LP_Problem has been renamed MIP_Problem and now supports the solution of Mixed Integer (Linear) Programming problems. Support has been added for the incremental solution of MIP problems: it is now possible to add new space dimensions or new constraints to the feasible region, as well as change the objective function and the optimization mode, while still exploiting some of the computational work done before these changes. Support has also been added to change control parameters for the pricing method. This allows a choice between the steepest edge pricing method, either implemented with floating point numbers (default) or with integer coefficients, and the textbook pricing method. o The PPL semantic object Polyhedra_Powerset has been replaced by the templatic object template <typename PS> Pointset_Powerset that can take any (simple) PPL semantic object for the domain of its disjuncts. In addition to the methods common to all the PPL semantic objects, methods specific to this domain include: void add_disjunct(const PS&), void pairwise_reduce(), void omega_reduce() const, bool geometrically_covers(const Pointset_Powerset&) const, bool geometrically_equals(const Pointset_Powerset&) const, and bool simplify_using_context_assign(const Pointset_Powerset&). o A new abstraction called Partially_Reduced_Product (PRP) has been added. A PRP is a pair of two PPL semantic objects that is parametric on the component domains and on a reduction operator. The PPL currently provides three reduction operators and hence, three different kinds of products: - a Direct_Product where the reduction operator is the identity; - a Smash_Product where the reduction operator shares emptiness information between the components; and - a Constraints_Product where the reduction operator refines each component with the constraints satisfied by the other component. The PRP class still needs a lot of work and both its implementation and its interface are likely to change significantly: it is released now as a kind of technology preview and any feedback is welcome. New and renamed methods ----------------------- o All PPL semantic objects can now be constructed from other simple PPL semantic objects. All these constructors have an optional complexity argument with default value allowing algorithms with any complexity to be used. o New methods void restore_pre_PPL_rounding() and void set_rounding_for_PPL() allow the FPU rounding mode to be set to what it was before the initialization of the PPL, and to set it (again) so that the PPL abstractions based on floating point numbers work correctly, respectively. o All PPL semantic objects now provide methods void refine_with_constraint(const Constraint&), void refine_with_congruence(const Congruence&), void refine_with_constraints(const Constraint_System&), and void refine_with_congruences(const Congruence_System&). These methods are similar to the corresponding `add_' methods. The difference is in the reaction policy when the argument constraint/congruence is not optimally supported by the semantic domain: while the `add_' methods will throw an exception, the `refine_with_' methods will apply an upward approximation semantics. o Default widening operators of the form: void widening_assign(const ABSTRACTION&, unsigned*) are now provided for all abstractions except for the Pointset_Powerset abstractions. o All PPL semantic objects now provide the method int32_t hash_code() const returning a 32-bit hash code for *this. If x and y are such that x == y evaluates to true, so does x.hash_code() == y.hash_code(). o All PPL semantic objects now provide the methods memory_size_type total_memory_in_bytes() const memory_size_type external_memory_in_bytes() const returning, respectively, the total size in bytes of the memory occupied by the PPL object and the size in bytes of the memory managed by the PPL object. o For all the PPL semantic objects there are new methods: static bool can_recycle_constraint_systems() and static bool can_recycle_congruence_systems() that indicate whether or not a PPL semantic object is able to recycle constraints and congruences, respectively. o For all PPL semantic objects there is a new method: bool contains_integer_point() const which checks if a PPL semantic object contains an integer point; Note that this is not currently provided for the Partially_Reduced_Product classes. o For all PPL semantic objects there is a new method: bool constrains(Variable) const which checks if a dimension is constrained by a PPL semantic object; o For all PPL semantic objects there are new methods: void unconstrain(Variable) void unconstrain(const Variables_Set&) which assign, to a PPL semantic object, the cylindrification of the object with respect to one (resp., a set) of its dimensions, as defined by L. Henkin, J. D. Monk, and A. Tarski in Cylindric Algebras: Part I (published by North-Holland in 1971). o Several methods bool is_topologically_closed() const void topological_closure_assign() that were provided for just some of the PPL semantic objects are now uniformly available for all the objects. o Methods using the Congruence and Congruence_System classes such as Congruence_System congruences() const, Congruence_System minimized_congruences() const, void add_congruence(const Congruence&), void add_congruences(const Congruence_System&), void add_recycled_congruences(const Congruence_System&), and Poly_Con_Relation relation_with(const Congruence&). that were just provided for the Grid domain are now provided for all the PPL semantic objects. o For the Grid class, as it is not always possible to obtain a Pointset_Powerset<Grid> object that is a finite linear partition of the difference of two grids, we have added the method: std::pair<Grid, Pointset_Powerset<Grid> > approximate_partition(const Grid&, const Grid&, bool&) where the third argument is set to false if there is no finite linear partition. o In the Congruence class, for consistency with the Constraint class, the methods is_trivial_true() and is_trivial_false() have been renamed as is_tautological() and is_inconsistent(), respectively. o The methods bool Constraint_System::empty() const, bool Generator_System::empty() const, bool Congruence_System::empty() const, and bool Grid_Generator_System::empty() const return true if and only if the system in question is empty (i.e., it has no constraints, generators, congruences or grid-generators, respectively). Deprecated and removed methods ------------------------------ o As all PPL semantic objects can now be constructed from boxes, the constructors template <typename Box> C_Polyhedron(const Box&, From_Bounding_Box), template <typename Box> NNC_Polyhedron(const Box&, From_Bounding_Box), template <typename Box> Grid(const Box&, From_Bounding_Box) have been removed. Similarly, as boxes can be constructed from other PPL semantic objects, the method template <typename Box> void shrink_bounding_box(Box&, Complexity_Class) const has been removed from all the classes. o The use of methods having a name ending in `_and_minimize' (e.g., add_constraints_and_minimize, poly_hull_assign_and_minimize, ...) is now deprecated (see the core library documentation for an explanation); their complete removal is planned for version 0.11. o Class BD_Shape and Grid no longer provide methods such as bds_hull_*, join_*, bds_difference_* and grid_difference_*. The uniformly named methods upper_bound_* and difference_assign should be used instead. For (C and NNC) polyhedra, the poly_hull_* and poly_difference_assign methods have been kept for backward compatibility (users should anyway prefer adopting the uniformly named variants). o For Grids, the PPL no longer supports covering boxes; hence the constructor template <typename Box> Grid(const Box&, From_Covering_Box) and also the method template <typename Box> void get_covering_box(Box&) const have been removed. Other changes for the C++ interface ----------------------------------- o All identifiers containing the strings `less_than_or_equal' or `greater_than_or_equal', any case, have been renamed so as to contain `less_or_equal' or `greater_or_equal', respectively. A similar change also applies to the C interface (see below). o The `ppl.hh' header file no longer defines macros not prefixed by "PPL_". o Users of the C++ interface of the library can now decide to disable the automatic initialization mechanism of the PPL. To do so, the preprocessor symbol PPL_NO_AUTOMATIC_INITIALIZATION should be defined before including the <ppl.hh> header file. When automatic initialization is disabled it is imperative to explicitly call the new function void Parma_Polyhedra_Library::initialize() before using the library. The new function void Parma_Polyhedra_Library::finalize() and should also be called (to release a small amount of memory) when done with the library. Changes to the other language interfaces ---------------------------------------- o Support for language interfaces has been expanded to include OCaml and Java. Thus the PPL now supports interfaces to C++, C, Java, OCaml, Ciao Prolog, GNU Prolog, SICStus Prolog, SWI Prolog, XSB Prolog and YAP Prolog. o Most of the PPL semantic objects provided by the C++ interface are also supported by all the non-C++ language interfaces. A few domains (in particular, many of the possible Box instantiations) are only available via the C++ interface. o Almost all the public methods for the PPL semantic objects are provided as methods/functions/predicates in the non-C++ language interfaces with a uniform naming policy. In particular: * in the C interface, the methods named ppl_Polyhedron_{constraints,generators,congruences} ppl_Polyhedron_minimized_{constraints,generators,congruences} have been renamed ppl_Polyhedron_get_{constraints,generators,congruences} ppl_Polyhedron_get_minimized_{constraints,generators,congruences}, respectively; * in the Prolog interfaces, the predicates ppl_Grid_generalized_image_lhs_rhs/5 and ppl_Grid_generalized_preimage_lhs_rhs/5 ppl_Grid_generalized_image/6 and ppl_Grid_generalized_preimage/6 have been renamed as ppl_Grid_generalized_image_lhs_rhs_with_congruence/5 ppl_Grid_generalized_preimage_lhs_rhs_with_congruence/5 ppl_Grid_generalized_image_with_congruence/6 ppl_Grid_generalized_preimage_with_congruence/6 respectively, so as to allow for /4 and /5, resp., versions. o As already reported for the C++ interface, in the C interface, all identifiers containing the strings `less_than_or_equal' or `greater_than_or_equal', any case, have been renamed so as to contain `less_or_equal' or `greater_or_equal', respectively. o In the C interface it is no longer an error to call ppl_initialize() or ppl_finalize() multiple times (this matches the behavior of the other non-C++ language interfaces). Documentation changes --------------------- o The documentation for the library has been deeply reorganized and split into several documents: besides the user and developer manuals for the core library and its C++ interface, we now provide separate user and developer manuals for each one of the other available language interfaces (namely, C, Java, OCaml, and Prolog). It is also possible to produce "configuration dependent" variants of the non-C++ language interface manuals, where the contents of the manual take into account the value of configuration option `--enable-instantiations'. All the manuals are provided in HTML, PDF and PostScript formats. o New man pages libppl(3) and libppl_c(3) have been added. These give short overviews on how to use the PPL in C++ and C programs, respectively, on Unix-like operating systems. Configuration changes --------------------- o Several options have been added to the configuration script. These allow to control the generated language interfaces, the floating point instruction set to be used, the use of Valgrind during `make check', the exclusion of some PPL-based programs from the build. The README.configure file has been updated consequently. Bugfixes ======== o Fixed bugs that prevented building the library on systems not supported by the Parma Watchdog Library or when the `--disable-watchdog' configure was used. o Fixed a bug in Grid::constraints() and Grid::minimized_constraints() that caused an internal assertion to fail when the grid had 0 space dimensions. o Fixed a bug in Linear_System::insert(const Linear_Row&) whereby a wrong result could have been obtained when inserting a not necessarily closed constraint/generator in an empty system having a higher space dimension. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0