The core development team is very pleased to announce the availability of PPL 0.11, a new release of the Parma Polyhedra Library.
This release has many new features, among which:
- a class PIP_Problem that provides a Parametric Integer Programming problem solver;
- "deterministic" timeout computation facilities;
- support for termination analysis via the automatic synthesis of linear ranking functions;
- support for approximating computations involving (bounded) machine integers.
This release includes several other enhancements, speed improvements 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
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 Patricia M. Hill Enea Zaffanella
Applied Formal Methods Laboratory Department of Mathematics University of Parma, Italy
-------------------------------------------------------------------------- NEWS for version 0.11 (released on August 2, 2010) --------------------------------------------------------------------------
New and Changed Features ========================
o New class PIP_Problem provides a Parametric Integer Programming (PIP) problem solver (mainly based on P. Feautrier's specification). The implementation combines a parametric dual simplex algorithm using exact arithmetic with Gomory's cut generation.
o New "deterministic" timeout computation facilities: it is now possible to set computational bounds (on the library calls taking exponential time) that do not depend on the actual elapsed time and hence are independent from the actual computation environment (CPU, operating system, etc.).
o New support for termination analysis via the automatic synthesis of linear ranking functions. Given a sound approximation of a loop, the PPL provides methods to decide whether that approximation admits a linear ranking function (possibly obtaining one as a witness for termination) and to compute the space of all such functions. In addition, methods are provided to obtain the space of all linear quasi-ranking functions, for use in conditional termination analysis.
o New support for approximating computations involving (bounded) machine integers. A general wrapping operator is provided that is parametric with respect to the set of space dimensions (variables) to be wrapped, the width, representation and overflow behavior of all these variables. An optional constraint system can, when given, improve the precision.
o All the PPL semantic objects provide new methods
void drop_some_non_integer_points(Complexity_Class) void drop_some_non_integer_points(const Variables_Set&, Complexity_Class)
which possibly tighten the object by dropping some points with non-integer coordinates (for the space dimensions corresponding to `vars'), within a certain computational complexity bound.
o New Linear_Expression methods
bool is_zero() const bool all_homogeneous_terms_are_zero() const
return true if and only if `*this' is 0, and if and only if all the homogeneous terms of `*this' are 0, respectively.
o New Linear_Expression methods
void add_mul_assign(Coefficient_traits::const_reference c, Variable v) void sub_mul_assign(Coefficient_traits::const_reference c, Variable v)
assign linear expression *this + c * v (resp., *this - c * v) to *this, while avoiding the allocation of a temporary Linear_Expression.
o For the PPL semantic objects, other than the Pointset_Powerset and Partially_Reduced Product, there is a new method:
bool frequency(const Linear_Expression& expr, Coefficient& freq_n, Coefficient& freq_d, Coefficient& val_n, Coefficient& val_d)
This operator computes both the "frequency" (f = freq_n/freq_d) and a value (v = val_n/val_d) closest to zero so that every point in the object satisfies the congruence (expr %= v) / f.
o New reduction operator "Shape_Preserving_Reduction" has been added to the Partially_Reduced_Product abstraction. This operator is aimed at the product of a grid and a shape domain, allowing the bounds of the shape to shrink to touch the points of the grid, such that the new bounds are parallel to the old bounds.
o The Java interface has to be explicitly initialized before use by calling static method Parma_Polyhedra_Library.initialize_library(). Initialization makes more explicit the exact point where PPL floating point rounding mode is set; it also allows for the caching of Java classes and field/method IDs, thereby reducing the overhead of native method callbacks.
o The C and Java interfaces now support timeout computation facilities.
o Implementation of general (C and NNC) polyhedra speeded up.
o Implementation of the MIP solver speeded up.
o When the PPL has been configured with CPPFLAGS="-DPPL_ARM_CAN_CONTROL_FPU=1", the library initialization procedure checks that the FPU can indeed be controlled and fails if that is not the case.
o New configure option --with-gmp-prefix supersedes the (now removed) options --with-libgmp-prefix and --with-libgmpxx-prefix.
o New configuration option `--with-gmp-build=DIR' allows to use a non-installed build of GMP in DIR.
Deprecated and Removed Methods ==============================
o All methods having a name ending in `_and_minimize' (e.g., add_constraints_and_minimize, poly_hull_assign_and_minimize, ...) have been removed (they were deprecated in version 0.10).
Bugfixes ========
o Corrected a bug in maximize and mininimize optimization methods of class template Pointset_Powerset, whereby the Boolean value true (indicating successful optimization) was returned for empty powersets.
o Corrected a bug in method bool NNC_Polyhedron::poly_hull_assign_if_exact(const NNC_Polyhedron&); whereby some inexact NNC hulls were incorrectly flagged as exact.