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@cs.unipr.it
We announce the availability of PPL 0.10.2, a new release of the Parma
Polyhedra Library fixing a few bugs affecting PPL 0.10.1.
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/
The core development team,
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.2 (released on April 18, 2009)
--------------------------------------------------------------------------
Bugfixes
========
o Correctly detect GMP 4.3.0.
o Fixed the C interface library version information.
o Test program tests/Polyhedron/memory1 disabled on the zSeries s390x
platform.
o Makefiles fixed so as to avoid failure of `make -n check'.
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
We are pleased to announce the availability of PPL 0.10.1, a new release
of the Parma Polyhedra Library.
This release includes several important improvements to PPL 0.10,
among which is better portability (including the support for
cross-compilation), increased robustness, better packaging and several
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 contributors 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.1 (released on April 14, 2009)
--------------------------------------------------------------------------
New and Changed Features
========================
o Added support for cross compilation.
o The configuration script now explicitly checks that a recent enough
version of GNU M4 is available if at least one non-C++ interface is
enabled (in previous versions this check was not performed and
building the library could fail in a mysterious way).
o Robustness improved.
o Some packaging issues have been fixed.
o New macro PPL_DIRTY_TEMP_COEFFICIENT allows users of the C++
interface to decrease memory allocation overhead and to improve
locality whenever they need a temporary variable of type
`Coefficient'.
o The C++, C, Java and OCaml interfaces now provide utility functions
to format the textual representations of constraints, congruences
and so on. This makes it easy to code debugging prints with line
indentation and wrapping.
o The C interface now provides functions of the form
int ppl_io_asprint_Polyhedron(char** strp, P x)
where `P' is any opaque pointer to a const PPL object. These
functions print `x' to a malloc-allocated string, a pointer to
which is returned via `strp'.
o The OCaml interface can now be compiled to native code using ocamlopt.
o New configuration option `--with-mlgmp=DIR' allows to specify the
installation directory of the ML GMP package.
o The OCaml interface now supports timeout computation facilities
through functions ppl_set_timeout and ppl_reset_timeout. Moreover,
new functions ppl_Coefficient_is_bounded, ppl_Coefficient_min,
ppl_Coefficient_max and ppl_max_space_dimension have been added.
o The Prolog interfaces are no longer enabled by default in the
release tarballs (they are enabled by default in the Git versions).
Bugfixes
========
o Fixed a bug whereby `make check' was failing when the library was
configured with the `--disable-watchdog' option.
o Fixed a bug in method
bool Polyhedron::contains_integer_point() const;
whereby, under very specific conditions, an empty polyhedron is
incorrectly said to contain an integer point.
o Fixed a bug in method
Partially_Reduced_Product<D1, D2, R>::time_elase_assign(y)
whereby, if the product y was not already reduced, the operation could
lose precision.
o Fixed a bug in the OCaml interface, which was affecting functions
ppl_Grid_generalized_affine_image_with_congruence
and
ppl_Grid_generalized_affine_preimage_with_congruence.
o Fixed a bug in the Grid class that affected the methods
Grid::bounds_from_above(), Grid::bounds_from_below(),
Grid::maximize() and Grid::minimize();
causing all of them to wrongly return true in certain cases where
the grid generators were not minimized.
o Fixed a bug whereby big-endian architectures were not properly
recognized by the configuration script.
o Fixed a bug in the Java/OCaml/Prolog interfaces, whereby
the method/function/predicate for dropping a disjunct from a
Pointset_Powerset object were returning an invalid iterator.
o Fixed a bug in method Octagonal_Shape<T>::affine_image(var, expr)
whereby a wrong result was computed under specific conditions.
o Fixed a bug in the OCaml interface, whereby functions of form
ppl_..._widening_assign_with_tokens
and
ppl_..._extrapolation_assign_with_tokens
could return a wrong number of tokens.
o Fixed a bug in the OCaml interface, whereby functions that returned
an OCaml 'unit' type were returning the wrong value.
o Fixed several garbage collection related bugs in the OCaml interface.
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
We have uploaded the first PPL 0.10.1 release candidate to
ftp://ftp.cs.unipr.it/pub/ppl/snapshots/
You can check the NEWS file via Gitweb:
http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=blob_plain;f=NEWS;hb=…
If all goes well, the release of PPL 0.10.1 will happen on April 14, 2009.
In case problems arise, the above mentioned snapshot will be replaced by
a new one and only announced on ppl-devel(a)cs.unipr.it (of course the real
release will be properly announced).
Please report any problem you may encounter to ppl-devel(a)cs.unipr.it
Beta-testing is especially important on this occasion because PPL 0.10.1
will be the last release in the PPL 0.10 series. The following release
will be PPL 0.11.
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
Next week-end we will say goodbye to CVS and pass all the PPL
repositories to git (http://git-scm.com/). Abramo has worked
hard to make the transition as smooth as possible, so I think
no one should worry.
Sometimes during the weekend, the CVS repository will be frozen
(it will remain at its place, but in read-only mode). A few
hours later the new git repository will appear: I will send
an explanatory message to the lists when this happens.
All the best,
Roberto
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
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
Dear All,
we have uploaded the first PPL 0.10 release candidate (0.10pre36)
to
ftp://ftp.cs.unipr.it/pub/ppl/snapshots/
You can check the NEWS file via ViewVC:
http://www.cs.unipr.it/cgi-bin/viewvc/viewvc.cgi/ppl/NEWS?view=co
If all goes well, the release of PPL 0.10 will happen on November 4, 2008.
In case problems arise, 0.10pre36 will be substituted by 0.10pre37, and so
forth, without further announcements (of course the real release will
be properly announced).
Please report any problem you may encounter to ppl-devel(a)cs.unipr.it
All the best,
Roberto Bagnara Patricia M. Hill Enea Zaffanella
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
The core development team is very pleased to announce the availability
of PPL 0.9 in Fedora 7. This is part of an ongoing effort to make the
Parma Polyhedra Library available (also in binary form) on the major
software platforms [1]. Special thanks are due to Michael Schwendt
and Mamoru Tasaka for all the assistance they gave us. The (more than
obsolete) RPM packages available from the PPL download page will soon
be removed. We hope to release PPL 0.10 (with lots of new interesting
features) by the end of the year.
All the best,
Roberto Bagnara <bagnara(a)cs.unipr.it>
Patricia M. Hill <hill(a)comp.leeds.ac.uk>
Enea Zaffanella <zaffanella(a)cs.unipr.it>
[1] If there are platforms you care more than others, please let us know.
If you have expertise in building packages for platforms other than
Fedora 7 and would like to share your knowledge with us, please get in touch.
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
The core development team is delighted to announce the availability of
a new paper on the PPL. "The Parma Polyhedra Library: Toward a
Complete Set of Numerical Abstractions for the Analysis and
Verification of Hardware and Software Systems" is the first published
paper that covers, though not in depth, all the main features of the
PPL. It is a very recommended reading for anyone using or considering
to use the library. Besides listing several important features that
---we suspect--- most users are unaware of, it illustrates the current
development plans for the library and reviews some of the applications
using it.
Roberto Bagnara <bagnara(a)cs.unipr.it>
Patricia M. Hill <hill(a)comp.leeds.ac.uk>
Enea Zaffanella <zaffanella(a)cs.unipr.it>
[1] http://www.cs.unipr.it/ppl/Documentation/bibliography#BagnaraHZ06TR
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
The core development team is very pleased to announce the
availability of PPL 0.9, a new release of the Parma Polyhedra Library.
The key feature of this release is complete support for the domain of
rational grids. Roughly speaking, a grid is the solution of a finite
system of congruence relations such as `x + y - 2*z = 3 (mod 6)'.
Grids can encode information about the patterns of distribution of the
values that program variables can take. The implementation offered in
PPL 0.9 is, as far as we know, the first published one that is
functionally complete (i.e., providing all the required operations,
including a provably correct widening) for the purposes of program
analysis and verification.
The release includes also many portability improvement and a couple
of 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>
New and Changed Features
========================
o The class Grid provides a complete implementation of the relational
domain of rational grids. This can represent all sets that can
be expressed by the conjunction of a finite number of congruence
relations. Operations provided include everything that is needed
in the field of static analysis and verification, including affine
images, preimages and their generalizations, grid-difference and
widening operators. This is the first time such a complete domain
is made freely available to the community.
o Several important portability improvements. Among other things,
it is now possible to build only the static libraries or only
the shared libraries. (Notice that some interfaces depend on
the availability of the shared libraries: these will not be built
when shared libraries are disabled.)
Bugfixes
========
o Fixed a bug whereby the SICStus Prolog interface could not be built
on x86_64.
o Fixed a bug in an internal method that, under some circumstances,
could cause a wrong result to be computed.
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it
