[PPL-announce] Parma Polyhedra Library 0.8
Roberto Bagnara
bagnara at cs.unipr.it
Fri Jan 20 19:24:51 CET 2006
After more than a year's hard work, we (the core development team) are
very pleased to announce the availability of PPL 0.8, a new release of
the Parma Polyhedra Library.
This release supports a new numerical abstraction: bounded difference
shapes. These are convex polyhedra that can be expressed by finite
sets of constraints of the form `x - y <= c', where `c' is a number.
Bounded difference shapes provide coarse but efficient-to-compute
approximations and can be crucial to deal with analysis problems with
lots of variables. Another premiere for this release is a class for
representing and solving linear programming problems; the solver is
based on a primal simplex algorithm using exact arithmetic.
The release includes dozens of other important improvements: usability
and portability (a new configuration program and Autoconf function
make it particularly easy to use the library), several new methods and
functions useful in the field of static analysis, new output methods
very useful for debugging applications using the library, improvements
to the C and Prolog interfaces, and (only!) half a dozen bug fixes.
See below for a (long) list of the main additions and changes.
For even more information, 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 at cs.unipr.it>
Patricia M. Hill <hill at comp.leeds.ac.uk>
Enea Zaffanella <zaffanella at cs.unipr.it>
New and Changed Features
========================
o The class template BD_Shape<T> provides an implementation of the
abstract domain of bounded difference shapes. The template type
parameter T specifies the basic type used for the inhomogeneous term
of bounded difference constraints; it can be instantiated to either
GMP's unbounded precision types (mpq_class, mpz_class), native
floating point types (float, double), or native integer types
(8, 16, 32 and 64 bits wide).
o New class LP_Problem provides an implementation of the
primal simplex algorithm using exact arithmetic.
o The new program `ppl-config' returns information about the
configuration and the installed components of the PPL.
This greatly simplifies the task of writing makefiles and
automatic configuration scripts. A manual page for `ppl-config'
has also been added.
o New Autoconf function
AM_PATH_PPL([MINIMUM-VERSION, [ACTION-IF-FOUND [, ACTION-IF-NOT-FOUND]]])
allows to test the existence and usability of particular versions of the
PPL, defining macros containing the required paths. The simple addition
of, e.g.,
AM_PATH_PPL(0.8)
to an application's configure.ac file is all that is needed in most
cases. Paths to the installed version of the PPL will be detected,
the version number will be checked to be at least the one
indicated, the variables PPL_CPPFLAGS and PPL_LDFLAGS will be set
accordingly and a quick sanity check of the PPL installation will
be performed. For more complex tasks, the AM_PATH_PPL function
defines the `--with-ppl-prefix' and `--with-ppl-exec-prefix'
configure options (useful when the PPL is installed into a
non-standard place or when multiple versions of the PPL are
installed). AM_PATH_PPL also defines the `--disable-ppltest'
configure option to disable the quick sanity check. When something
fails, AM_PATH_PPL provides accurate indications about what went
wrong and how to fix it. See the sources in m4/ppl.m4 for more
information.
o The browse and print versions of the PS and PDF formats of the user
manual have been merged into single documents: ppl-user-0.8.pdf and
ppl-user-0.8.ps.gz. The equivalent developer reference documents
have also been merged.
o One of the possible values for the configuration option
`--enable-coefficients' has been renamed from `gmp' to `mpz'.
o New configuration option `--enable-interfaces' allows some or all of
the Prolog and C interfaces to be selectively enabled.
o Portability has been further improved.
o Added to C_Polyhedron (resp., NNC_Polyhedron) new method
bool poly_hull_assign_if_exact(const C_Polyhedron&)
(resp. bool poly_hull_assign_if_exact(const NNC_Polyhedron&))
and its synonym
bool upper_bound_assign_if_exact(const C_Polyhedron&)
(resp. bool upper_bound_assign_if_exact(const NNC_Polyhedron&)).
o Added new typedef `element_type' to template Polyhedra_Powerset,
which corresponds to the type of the underlying numeric domain.
o Output operators have been added for Generator::Type and
Constraint::Type.
o Class Bounding_Box has new method
Constraint_System Bounding_Box::constraints() const,
which returns the system of constraints.
o Class Bounding_Box has new widening methods
Bounding_Box::CC76_widening_assign(const Bounding_Box& y)
and
template <typename Iterator>
Bounding_Box::CC76_widening_assign(const Bounding_Box& y,
Iterator first,
Iterator last).
o All methods in class Determinate that are specific to the Polyhedra
template parameter have been dropped. If needed, they can still be
invoked through element().
o Method
bool Constraint_System::has_strict_inequalities() const
is now publicly accessible.
o Added Polyhedron methods difference_assign() and join_assign(),
behaving as poly_difference_assign() and poly_hull_assign(),
so as to have more uniform interfaces.
o The helper function widen_fun_ref() building a limited widening
function is now templatic even on the second argument (i.e., the
limiting constraint system). The templatic widening method
Polyhedra_Powerset<PH>::BHZ03_widening_assign()
no longer has a default value for the certificate parameter.
o The signatures of Polyhedron methods maximize() and minimize()
have been greatly simplified.
o The function template
template <typename PH>
bool check_containment(const PH&, const Polyhedra_Powerset<PH>&)
now works whenever there exists a lossless conversion mapping an
object of type PH into an NNC_Polyhedron (e.g., when PH = BD_Shape).
The same holds for methods
bool Polyhedra_Powerset<PH>::geometrically_covers()
and
bool Polyhedra_Powerset<PH>::geometrically_equals().
o Disjuncts can be added to an instance of Polyhedra_Powerset with
the new method
void add_disjunct(const PH& ph).
o The two generalized_affine_image() methods of class Polyhedron
are now matched by corresponding methods for computing preimages
of affine relations.
o Added to class Polyhedron the method
void bounded_affine_image(Variable v,
const Linear_Expression& lb,
const Linear_Expression& ub,
Coefficient_traits::const_reference d
= Coefficient_one())
computing the image of the polyhedron according to the
transfer relation lb/d <= v' <= ub/d.
Also added the corresponding method for computing preimages.
o The enumeration
Polyhedron::Degenerate_Kind
has been placed outside of class Polyhedron and renamed as
Degenerate_Element.
o New output operators in namespace IO_Operators:
std::ostream& operator<<(std::ostream&, const Constraint::Type&)
and
std::ostream& operator<<(std::ostream&, const Generator::Type&).
o Added to class Constraint the methods
bool is_tautological() const
and
bool is_inconsistent() const
returning true when the constraint is always or never satisfied,
respectively.
o Added to classes Constraint (resp., Generator) the method
bool is_equivalent_to(const Constraint& y) const
(resp., bool is_equivalent_to(const Generator& y) const)
which check for semantic equivalence of corresponding class
instances. Also made available the (semantic) comparison operators
`==' and `!='.
o The swap() methods of classes Linear_Expression, Constraint, Generator,
Constraint_System and Generator_System are now publicly accessible.
o Added to classes Constraint and Generator the methods
void ascii_dump(std::ostream& s) const
and
void ascii_load(std::istream& s) const.
o In classes Poly_Con_Relation and Poly_Gen_Relation the methods
void ascii_dump(std::ostream& s) const
and
void ascii_load(std::istream& s) const
are now publicly accessible.
o All classes which provide the method
void ascii_dump(std::ostream& s) const
now also provide the methods
void ascii_dump() const
and
void print() const.
These methods print to std::cerr the textual and user-level
representation (resp.) of the given object. This enables the
output of such object representations in GDB.
o New functions added to the C interface:
int ppl_Coefficient_is_bounded(void),
int ppl_Coefficient_min(mpz_t min),
int ppl_Coefficient_max(mpz_t max)
allow C applications to obtain information about the Coefficient
integer numerical type.
The new Prolog interface predicates ppl_Coeffient_is_bounded/0,
ppl_Coefficient_max/1 and ppl_Coefficient_min/1 provide the same
functionality.
o All predicates in the Prolog interface that require an input list
as an argument will now throw an exception if that argument is not
a list. Before, some predicates, such as
ppl_Polyhedron_remove_space_dimensions/2, would fail.
o In the Prolog interface, the names and arities of the "with_token"
widening and extrapolation predicates have been revised to
"with_tokens" with an extra argument and the functionality has been
revised to match more closely the corresponding C++ interface
operators.
o In the Prolog interface, the names and arities of the predicates
that create handles for new polyhedra have been revised to match
more closely the corresponding C and C++ interface operators. That
is, instead of having "c" and/or "nnc" as arguments to indicate the
topology of the polyhedron, the topologies are now part of the
names of the predicates.
o The SWI-Prolog interface allows now the exchange of unbounded numbers
between the PPL and Prolog applications. This requires SWI-Prolog
version 5.6.0 or later version. Previous versions of SWI-Prolog
are no longer supported.
o The YAP interface allows now the exchange of unbounded numbers
between the PPL and Prolog applications. This requires YAP
version 5.1.0 or later version. Previous versions of YAP
are no longer supported.
o The `ppl_lpsol' demo has now two more options: with `--enumerate' it
solves the given linear programming problem by vertex/point
enumeration; with `--simplex' (the default) it uses our simplex
implementation with exact arithmetic. The `ppl_lpsol' program,
which is only built if a suitable version of GLPK is available, is
installed into the directory (selectable at configuration time) for
user executables.
o Manual pages have been added for the ppl_lpsol and ppl_lcdd
programs.
o The new class BD_Shape<T> as well as the "checked" native
coefficients selectable with the `--enable-coefficients' configure
options, are based on a very general and powerful notion of "number
family with a policy". This is made available to the users of the
PPL via the wrapper template class Checked_Number<T, P>, where T is
the underlying numeric type (native integer or float of any width,
unbounded integer or rational) and `P' is a policy specifying
things such as whether to check for overflows and other
"exceptional" conditions and what to do in such cases. The policy
also specifies whether T should be extended with representations
for infinities or NAN (Not A Number) and default rounding modes.
A complete set of arithmetic functions and operators are provided:
they either use the default rounding mode or accept a rounding mode
as an extra parameter and, depending on the policy, may return a result
that indicates the relation that exists between the true mathematical
result and the (possibly approximate) computed result. Input/output
functions with the same properties (controlled rounding and indications
of the approximations) are also provided.
Bugfixes
========
o Fixed a bug in Polyhedra_Powerset<PH>::concatenate_assign() whereby
a temporary Polyhedra_Powerset object was created with the wrong
dimension.
o Corrected a memory leak bug in the demo ppl_lpsol.
o Corrected a bug in method
NNC_Polyhedron::minimized_constraints()
whereby an internal assertion might have been violated.
o Fixed a bug whereby calling the methods
Polyhedron::generalized_affine_image()
on an empty polyhedron could have resulted in an exception thrown.
o Fixed a bug whereby the occurrence of an `out of memory' error during
the allocation of a row of integer coefficients could have resulted
in a memory leak.
o Fixed a bug affecting the specialized constructors
Polyhedra_Powerset<NNC_Polyhedron>::
Polyhedra_Powerset(const Polyhedra_Powerset<C_Polyhedron>& y)
and
Polyhedra_Powerset<C_Polyhedron>::
Polyhedra_Powerset(const Polyhedra_Powerset<C_Polyhedron>& y)
whereby the newly built Polyhedra_Powerset object could have been
flagged as non-redundant even though it was containing redundant
disjuncts. Fixed a similar bug in generic constructor
Polyhedra_Powerset(const Constraint_System& cs)
that manifests when `cs' is denoting an empty polyhedron.
--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it
More information about the PPL-announce
mailing list