[PPL-announce] Parma Polyhedra Library 1.0

Roberto Bagnara bagnara at cs.unipr.it
Thu Jun 28 22:51:41 CEST 2012


The core development team is very pleased to announce the availability
of PPL 1.0, a new release of the Parma Polyhedra Library.

This release includes support for the optimized representation of
sparse vectors of coefficients, achieving significant performance
improvements, e.g., when dealing with constraint systems describing
weakly relational abstractions such as boxes and octagonal shapes.

The precise list of user-visible changes is below.
For more information, please come and visit the new PPL web site at

        http://bugseng.com/products/ppl

On behalf of all the past and present developers listed at
http://bugseng.com/products/ppl/credits and in the file CREDITS,

   Roberto Bagnara  Patricia M. Hill  Enea Zaffanella  Abramo Bagnara

                              BUGSENG srl
                          (http://bugseng.com)


--------------------------------------------------------------------------
NEWS for version 1.0  (released on June 28, 2012)
--------------------------------------------------------------------------

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

o  Significant improvements have been obtained in both time and space
    resource usage by the definition of data structures and algorithms
    for the case of "sparse rows", i.e., sequences of coefficients
    where most of the values are zero.

o  The library fully supports two different representations for rows:
    the "dense" representation is an array-like representation tailored
    to sequences having most of their coefficients different from zero;
    the "sparse" representation saves memory space (as well as CPU
    cycles) when most of the coefficients in the sequence are zero.

o  A generic interface allows for a seamless interaction between the
    dense and the sparse row representation. Most library entities
    (linear expressions, constraints, generators, congruences, and
    their systems) can be built using either representation, specified
    as a constructor's argument.

o  As a by-product of this sparse/dense refactoring work, efficiency
    improvements have been obtained even for those computations that
    are still based on the dense row representation.

o  Reasonable default values for the row representation are provided
    for each library entity, automatically leading to significant
    memory space savings even in old client/library code, e.g., when
    dealing with constraint systems describing weakly relational
    abstractions such as boxes and octagonal shapes.

o  If desired, these default values can be customized to user's needs
    by changing just a few lines of library code.  For instance, the
    constraint systems stored inside C_Polyhedron and NNC_Polyhedron
    objects can be made to use the sparse representation by just
    changing the following line in Polyhedron.defs.hh:

      static const Representation default_con_sys_repr = DENSE;

    to become

      static const Representation default_con_sys_repr = SPARSE;


Bugfixes
========

o  Fixed a bug affecting methods

      bool BD_Shape<T>::contains(const BD_Shape& y) const;
      bool Octagonal_Shape<T>::contains(const Octagonal_Shape& y) const;

    whereby the wrong result was obtained when *this is an empty
    weakly-relational shape and y is not empty.

o  Fixed a bug affecting the PIP solver whereby a wrong result could have
    been obtained if the input constraint system contained multiple linear
    equality constraints.

-- 
      Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                               BUGSENG srl - http://bugseng.com
                               mailto:roberto.bagnara at bugseng.com


More information about the PPL-announce mailing list