[PPL-announce] Parma Polyhedra Library 0.11

[Roberto Bagnara]

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

        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    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.

-- 
Prof. Roberto Bagnara
Applied Formal Methods Laboratory
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it