[PPL-announce] Parma Polyhedra Library 0.10
Roberto Bagnara
bagnara at cs.unipr.it
Tue Nov 4 17:17:53 CET 2008
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 at cs.unipr.it>
Patricia M. Hill <hill at comp.leeds.ac.uk>
Enea Zaffanella <zaffanella at 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 at cs.unipr.it
More information about the PPL-announce
mailing list