- PPL-announce - BUGSENG Mailman

Parma Polyhedra Library 0.8
by Roberto Bagnara 20 Jan '06

20 Jan '06

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(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 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@cs.unipr.it

1 0

New research position in Parma involving work on/with the PPL
by Roberto Bagnara 23 Feb '05

23 Feb '05

The position is available for a fixed term of two years to join the Formal Methods research team led by Prof. Roberto Bagnara [1] in the Department of Mathematics [2], University of Parma [3], Italy. A substantial part of the job concerns the research and development of analysis and verification techniques and tools based on the Parma Polyhedra Library and on PURRS [4], a system providing sophisticated computer algebra services required by automatic complexity analysis. Enhancements to both the PPL and PURRS are among the results that are expected from this line of work. See the official advert [5] for more information (the deadline for applications is March 18th, 2004). [1] http://www.cs.unipr.it/~bagnara/ [2] http://www.math.unipr.it/ [3] http://www.unipr.it/ [4] http://www.cs.unipr.it/purrs/ [5] http://www.unipr.it/arpa/setpersd/050217-BANDO3ASS-SCIENZE.htm -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Parma Polyhedra Library 0.7
by Roberto Bagnara 24 Dec '04

24 Dec '04

We are very happy to announce the availability of PPL 0.7, the latest release of the Parma Polyhedra Library. The main focus of this release is a new configuration option that enables the choice of different kinds of coefficients. As an alternative to the unbounded integer coefficients provided by the GMP library, the user can now configure the PPL to use checked native integers (8, 16, 32 or 64 bits wide). The checked integer coefficients apply systematic and efficient overflow detection, raising an exception if the computed value cannot be represented by the underlying type. When the numerical coefficients involved are likely to be small, the user can obtain significant efficiency improvements while being sure that, if no exception is thrown, the results are reliable. This release also includes other important improvements ranging from major efficiency gains (for all configurations) to usability and portability. Several bugs have been fixed and a more consistent naming scheme for the library types has been adopted: as a result users willing to upgrade will have to do a little renaming work on their applications. But it is worth the effort. For more information, see below the list of main additions and changes and visit the PPL web site at http://www.cs.unipr.it/ppl/ The core PPL 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> New and Changed Features ======================== o The new configuration option `--enable-coefficients' allows for the use of alternative (integral) coefficient types. Besides GMP integers, the user can now use checked native integers (8, 16, 32 or 64 bits wide). The use of such native coefficients is completely safe, since systematic (yet efficient) overflow detection is performed and, in case of overflow, an exception is raised. GMP coefficients are used by default. o Significant efficiency improvements have been achieved everywhere. o We now require GMP 4.1.3 or higher. o The following classes have been renamed as indicated: AskTell -> Ask_Tell BoundingBox -> Bounding_Box ConSys -> Constraint_System GenSys -> Generator_System Integer -> Coefficient LinExpression -> Linear_Expression Polyhedra_PowerSet -> Polyhedra_Powerset PowerSet -> Powerset SatMatrix -> Saturation_Matrix SatRow -> Saturation_Row o The helper function `widen_fun' has been renamed `widen_fun_ref'. o New assignment operators allowing to obtain an NNC_Polyhedron from a C_Polyhedron and the other way around. In the latter case, the topological closure of the argument polyhedron is computed. o New explicit constructors and assignment operators allowing to obtain a Polyhedra_Powerset<NNC_Polyhedron> from a Polyhedra_Powerset<C_Polyhedron> and the other way around. In the latter case, the topological closure of the element polyhedra is computed. o New explicit constructor Powerset<CS>::Powerset(const CS& d): if `d' is not bottom, builds a powerset containing only `d'; builds the empty powerset otherwise. o New explicit constructor Polyhedra_Powerset<CS>::Polyhedra_Powerset(const PH& ph): if `ph' is not empty, builds a powerset containing only `ph'; builds the empty powerset otherwise. o New method Polyhedra_Powerset::poly_difference_assign(const Polyhedra_Powerset& y) assigns to `*this' the poly-difference of `*this' and `y'. o All the public classes of the library have been endowed with methods memory_size_type total_memory_in_bytes() const and memory_size_type external_memory_in_bytes() const returning (lower bounds for) the total size in bytes of the memory occupied by *this and of the memory managed by *this, respectively. The type `memory_size_type' is a newly added unsigned integral type suitable to the representation of such information. o New method dimension_type Polyhedron::affine_dimension() returns the affine dimension of *this (not to be confused with the dimension of its enclosing vector space) or 0, if *this is empty. o All the methods changing (i.e., adding, removing, mapping, etc.) the dimensions of the vector space have been renamed so as to avoid any possible ambiguity with the affine dimension of the modified object. For instance, Polyhedron::add_dimensions_and_embed(dimension_type m); has been renamed as Polyhedron::add_space_dimensions_and_embed(dimension_type m); o The constructor C_Polyhedron(const NNC_Polyhedron& y) no longer throws an exception if `y' is not topologically closed. Rather, it constructs a C_Polyhedron representing the topological closure of `y'. o The following constructors have been made explicit: Constraint_System::Constraint_System(const Constraint& c), Generator_System::Generator_System(const Generator& g), C_Polyhedron::C_Polyhedron(const Constraint_System& cs), C_Polyhedron::C_Polyhedron(const Generator_System& cs), C_Polyhedron::C_Polyhedron(Constraint_System& cs), C_Polyhedron::C_Polyhedron(Generator_System& cs), NNC_Polyhedron::NNC_Polyhedron(const Constraint_System& cs), NNC_Polyhedron::NNC_Polyhedron(const Generator_System& cs), NNC_Polyhedron::NNC_Polyhedron(Constraint_System& cs), NNC_Polyhedron::NNC_Polyhedron(Generator_System& cs). Polyhedra_Powerset<PH>::Polyhedra_Powerset(const Constraint_System& cs). o Functions in the C interface that compute (space) dimensions no longer return their result. The caller is now required to pass, as an extra argument, a pointer to a memory area where the result will be written. All the C interface functions now use the return value to signal the success or failure of the requested operation. o Now `make check' runs a number of tests with `ppl_lcdd', comparing the results to expected ones. o The `ppl_lcdd' demo is now able to parse problems produced by lrs, i.e., where the number of rows of the matrix is omitted and replaced by "*****" (five asterisks). o The enumeration values of enum Complexity_Class have been renamed POLYNOMIAL_COMPLEXITY, SIMPLEX_COMPLEXITY and ANY_COMPLEXITY. o In the Prolog interface, the predicates ppl_new_polyhedron_from_dimension/3 and ppl_new_polyhedron_empty_from_dimension/3 have been replaced by a single predicate ppl_new_polyhedron_from_space_dimension/4 where the (extra) third argument indicates whether the polyhedron to be created should be the universe or the empty polyhedron. o As the unary plus operator is not in standard Prolog, '+'/1 in linear expressions is no longer supported by the Prolog interface. Bugfixes ======== o Fixed a bug that was causing an unwanted exception to be thrown when adding to a C_Polyhedron some generators obtained from an NNC_Polyhedron (even though no closure point was being added). o Fixed a bug in the handling of empty generator systems having a strictly positive space dimension. o Fixed a bug that was affecting Polyhedra_PowerSet::geometrically_covers() and Polyhedra_PowerSet::geometrically_equals(). o Method C_Polyhedron::H79_widening_assign() now widens the polyhedron itself instead of the homogenized polyhedral cone representing it. o Fixed a bug that was affecting Polyhedron::H79_widening_assign() as well as all the limited and bounded extrapolation operators. o Fixed a bug in Polyhedron::map_space_dimensions() that could manifest itself when used with a partial function encoding permutation. o Fixed a bug in the C interface function ppl_new_Linear_Expression_with_dimension(). o Fixed a bug in the `ppl_lpsol' demo. o Fixed a bug in Polyhedron::is_universe() that could manifest itself when the polyhedron is described by a generator system that is not in minimal form. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

PPL position available
by Roberto Bagnara 15 Nov '04

15 Nov '04

The post is available for a fixed term of one year, in the first instance, to join the Software Analysis research team led by Dr Patricia M. Hill [1] in the School of Computing [2], University of Leeds [3], UK. A substantial part of the job concerns the development and maintenance of the Parma Polyhedra Library, a library for the manipulation of numerical abstraction used in static program analysis and automated program verification. The ideal candidate should have a good degree in Computer Science or related subject with excellent programming skills and some expertise in C++. Some knowledge about static program analysis and convex polyhedra would also be useful. See the official advert [4] for more information. [1] http://www.comp.leeds.ac.uk/hill/ [2] http://www.comp.leeds.ac.uk/ [3] http://www.leeds.ac.uk/ [4] http://wwwnotes2.leeds.ac.uk/jobs/unijob.nsf/756c9c2f13a3c88780256cce0043e7… -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Parma Polyhedra Library 0.6.1
by Roberto Bagnara 20 Aug '04

20 Aug '04

We have just released PPL 0.6.1. This release fixes some packaging and documentation issues that were present in PPL 0.6. For more information, visit the PPL web site at http://www.cs.unipr.it/ppl/ The PPL 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> New and Changed Features ======================== o Some packaging issues have been fixed. o The documentation has been completed and improved. o The methods Polyhedra_PowerSet::semantically_contains(const Polyhedra_PowerSet&) and Polyhedra_PowerSet::semantically_equals(const Polyhedra_PowerSet&) have been renamed Polyhedra_PowerSet::geometrically_covers(const Polyhedra_PowerSet&) and Polyhedra_PowerSet::geometrically_equals(const Polyhedra_PowerSet& y), respectively. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Parma Polyhedra Library 0.6
by Roberto Bagnara 18 Aug '04

18 Aug '04

We are very happy to announce the availability of PPL 0.6, the latest release of the Parma Polyhedra Library. More than a year has passed since the previous release. During this period we have been doing a considerable amount of research and development work and this release, which is the first of a series of official versions that we hope to publish in the very near future, incorporates some of this work. The main focus of this release is on complete support for powersets of polyhedra. This includes the customizable framework for the definition of widening operators we have proposed at this year's VMCAI conference. Then there is support for summary dimensions as proposed by Denis Gopan and colleagues in their TACAS 2004 paper. We have started adding demo programs to the library. One of them, `ppl_lcdd', is actually useful and is competitive with similar programs available out there. Many other improvements have been performed: documentation, performance, portability and the configuration machinery have all been improved. A handful of bugfixes complete the picture: see below for more details. For more information, visit the PPL web site at http://www.cs.unipr.it/ppl/ The PPL 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> New and Changed Features ======================== o New templatic classes Determinate, PowerSet, and Polyhedra_PowerSet. The first two classes realize, in a completely generic way, the determinate and powerset constructions described by Roberto Bagnara in his 1998, Science of Computer Programming paper. The third class is a specialization of the powerset construction on polyhedra. The powerset construction comes with the generic widening technique proposed by Roberto Bagnara, Patricia Hill and Enea Zaffanella in their VMCAI 2004 paper. Actually, the Polyhedra_PowerSet class provides the first genuine, non-trivial widening ever proposed (let alone made available) on a domain of sets of convex polyhedra. o New methods void Polyhedron::expand_dimension(Variable, dimension_type) and void Polyhedron::fold_dimensions(const Variables_Set&, Variable) allow the easy realization of summary dimensions as proposed by Denis Gopan and colleagues in their TACAS 2004 paper. o A new `demos' directory has been added. In the `ppl_lcdd' subdirectory, this contains a sort of clone of the cddlib test program `lcdd', written using the PPL's C++ interface, together with several example polyhedra in the formats that the program can handle. The `ppl_lpsol' subdirectory contains another demo program that solves linear programming problems by vertex/point enumeration. This is written using the PPL's C interface and comes with several example problems in the Mathematical Programming System (MPS) format. In order to read MPS files, `ppl_lpsol' uses the GNU Linear Programming Kit (GLPK); thus `ppl_lpsol' is only compiled if a suitable version of GLPK is available. o New macro PPL_VERSION expands to the version string of the library. o New file README.configure provides additional information about the configuration and compilation of the library. o The documentation has been improved in various ways. o The documentation for users, in PostScript, PDF and HTML formats, is now installed in a standard place by `make install'. o The variable `abandon_exponential_computations' has been renamed `abandon_expensive_computations'. o The methods void Polyhedron::add_constraints(ConSys& cs), void Polyhedron::add_generators(GenSys& gs), bool Polyhedron::add_constraints_and_minimize(ConSys& cs), and bool Polyhedron::add_generators_and_minimize(GenSys& gs) have been renamed void Polyhedron::add_recycled_constraints(ConSys& cs), void Polyhedron::add_recycled_generators(GenSys& gs), bool Polyhedron::add_recycled_constraints_and_minimize(ConSys& cs), and bool Polyhedron::add_recycled_generators_and_minimize(GenSys& gs), respectively. At the same time, the methods void Polyhedron::add_constraints(const ConSys& cs), void Polyhedron::add_generators(const GenSys& gs), bool Polyhedron::add_constraints_and_minimize(const ConSys& cs), and bool Polyhedron::add_generators_and_minimize(const GenSys& gs) have been added. Corresponding changes have been made to the C and Prolog interfaces. o New methods Polyhedron::maximize() and Polyhedron::minimize() for maximizing and minimizing a linear expression subject to the polyhedron. o New output operator in namespace IO_Operators: std::ostream& operator<<(std::ostream&, const LinExpression&). o The method Polyhedron::map_dimensions(const PartialFunction& pfunc) has been significantly optimized for the case when `pfunc' is a permutation. A simple "renaming" of the dimensions is now extremely cheap. o The function Parma_Polyhedra_Library::max_space_dimension() has been given a new semantics and destiny: it returns the maximum space dimension that _all_ the abstractions provided by the library can handle. Each individual abstraction provides its versions of this function. Thus, e.g., NNC_Polyhedron::max_space_dimension() gives the maximum space dimensions an NNC_Polyhedron can handle. o The type of output functions for the class Variable, `Variable::Output_Function_Type', has been renamed `Variable::output_function_type' and is now defined as void output_function_type(std::ostream& s, const Variable& v). In other words, `v' is now passed by const reference and not by value. o Thanks to Bruno Haible, it is now possible to use versions of the GMP library installed into nonstandard places. The new configure options --with-libgmp-prefix[=DIR] and --with-libgmpxx-prefix[=DIR] substitute the old (and not really working) options --with-gmp-includes=DIR and --with-gmp-dir=DIR. Bugfixes ======== o Fixed a bug in the C interface function ppl_Polyhedron_map_dimensions() whereby a wrong result was computed. o Fixed a bug in Polyhedron::poly_difference_assign(const Polyhedron&) whereby a wrong result was computed. o Fixed a bug in the Prolog interface predicate ppl_Polyhedron_get_bounding_box/3 whereby a wrong result was sometimes computed in the case of an empty polyhedron. o Fixed a bug in the Prolog interface predicate ppl_new_Polyhedron_from_bounding_box/3 whereby the predicate was failing when given an empty bounding box. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

A cycle of seminars on convex polyhedra and applications
by Roberto Bagnara 04 Nov '03

04 Nov '03

In the coming months, we will have a very interesting cycle of seminars on convex polyhedra for the analysis and verification of hardware and software systems. This will be a nice occasion to get (prospective) developers and (potential) users together and to discuss the current and future developments. If you are interested, please bookmark the page http://www.cs.unipr.it/ppl/seminars_2003_2004 which will be used to communicate all the details and updates (no further messages on this subject will be sent to the PPL mailing lists). All the best, Roberto Bagnara -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Parma Polyhedra Library 0.5
by Roberto Bagnara 28 Apr '03

28 Apr '03

We are happy to announce the availability of PPL 0.5, the latest release of the Parma Polyhedra Library. This innovative release is packed with new features. We now have the most precise widening operator on Earth. Still concerning widenings, there is now support for "widening with tokens": a new and original improvement over the traditional widening delay technique. Several new operations on polyhedra have been added. The C and Prolog interfaces have been extended and the Prolog interface now supports six different Prolog systems. Many efficiency, usability and portability improvements have been made and, of course, a number of bugs have been fixed. Even though there is no compatibility of any kind with previous versions of the library, we believe that the interfaces are stabilizing and will not change much in the future. Starting from this release, the library provides macros and functions that allow the client applications to adapt to different versions of the library. For more information, visit the PPL web site at http://www.cs.unipr.it/ppl/ The PPL development team: Roberto Bagnara <bagnara(a)cs.unipr.it> Patricia M. Hill <hill(a)comp.leeds.ac.uk> Elisa Ricci <ericci(a)cs.unipr.it> Enea Zaffanella <zaffanella(a)cs.unipr.it> New and Changed Features ======================== o New methods Polyhedron::BHRZ03_widening_assign() and Polyhedron::BHRZ03_limited_extrapolation_assign(). The BHRZ03 widening is a novel widening that is always more precise than the one, by now standard, we call H79. o The novel "widening with tokens" technique improves on the good old widening delay technique by refraining from widening only when necessary. Precision is thus increased still guaranteeing convergence. All widening operators can now be supplied with an optional argument, recording the number of available tokens, which is decremented when tokens are used. o Two new methods have been defined that compute the image of a polyhedron under an affine relation. The first method, Polyhedron::generalized_affine_image(var, relsym, expr, denom), generalizes the classical Polyhedron::affine_image() method by allowing `relsym' to denote any of the relations <, <=, =, >=, >. The second method, Polyhedron::generalized_affine_image(lhs, relsym, rhs), is a variant where an arbitrary linear expression `lhs' is allowed to occur on the left-hand side of the affine relation. o New constructors to build polyhedra from read-only constraint and generator systems: C_Polyhedron(const ConSys&), C_Polyhedron(const GenSys&), NNC_Polyhedron(const ConSys&), and NNC_Polyhedron(const GenSys&). In the C interface the functions taking non-const arguments named ppl_new_<T>_from_<S> have been renamed ppl_new_<T>_recycle_<S>, where <T> is either "C" or "NNC", and <S> is either "ConSys" or "GenSys". The old names have been given to the new const functions. o New function LinExpression& operator*=(LinExpression&, const Integer&) to multiply (in place) an expression by a scalar. o The methods Polyhedron::check_empty() and Polyhedron::check_universe() have been renamed is_empty() and is_universe(), respectively. o New method bool Polyhedron::is_disjoint_from(const Polyhedron& y) returning true if and only `*this' and `y' are disjoint. o New methods bool Polyhedron::add_constraint_and_minimize(const Constraint&) and bool Polyhedron::add_generator_and_minimize(const Generator&) to add a constraint or a generator and minimizing the result at the same time. o New method: template <typename PartialFunction> void Polyhedron::map_dimensions(const PartialFunction&). This allows to rename the dimensions of a polyhedron according to a partial function mapping dimensions to dimensions. o New function LinExpression operator+(const LinExpression&): previously an expressions like `+x2-x3-x4 <= 0' could not constitute valid syntax for a constraint. o New type `dimension_type': an unsigned integral type for representing space dimensions. o New function dimension_type max_space_dimension(): returns the maximum space dimension this library can handle. o New function dimension_type not_a_dimension(): returns a value that does not designate a valid dimension. o The method Polyhedron::add_dimensions_and_constraints(ConSys&) has gone. A similar functionality is provided by the new method Polyhedron::concatenate_assign(const Polyhedron&). The same change has, of course, been performed on all the PPL interfaces. o New macros PPL_VERSION_MAJOR, PPL_VERSION_MINOR, PPL_VERSION_REVISION, and PPL_VERSION_BETA allow the client application to adapt to different versions of the library. o New function const char* version() returns a character string containing the PPL version. o New function const char* banner() returns a character string containing information about the PPL version, the licensing, the lack of any warranty whatsoever, the C++ compiler used to build the library, where to report bugs and where to look for further information. o The Prolog interface now supports also Ciao Prolog and XSB. o The C and Prolog interfaces have been extended so as to make more of the library's functionality available to Prolog and C users. o Timeout computation facilities have been added to the Prolog interfaces: new predicates ppl_set_timeout_exception_atom/1, ppl_timeout_exception_atom/1, ppl_set_timeout/1, ppl_reset_timeout/0. o Many efficiency improvements have been achieved. Part of these have been obtained by increasing the degree of "lazyness" of the library. o Many portability and standard-conformance improvements: the library can now be compiled with GNU g++, Intel C++ Compiler 7.0 for Linux, and Comeau C/C++ 4.3.0.1 Compiler Front-End; the library has also been tested on a variety of platforms. o The functions Polyhedron::operator<=(const Polyhedron&, const Polyhedron&), Polyhedron::operator>=(const Polyhedron&, const Polyhedron&), Polyhedron::operator<(const Polyhedron&, const Polyhedron&), and Polyhedron::operator>(const Polyhedron&, const Polyhedron&) have been removed. The methods Polyhedron::contains(const Polyhedron&) and Polyhedron::strictly_contains(const Polyhedron&) provide the same functionality. o The method Polyhedron::limited_H79_widening_assign() has been renamed Polyhedron::limited_H79_extrapolation_assign(). From now on, the name `widening' is reserved for operators that come with a convergence guarantee (i.e., with the ability of turning infinite chains to finite ones). Upper bound operators without such a guarantee contain the word `extrapolation' in their name. o The renamed method Polyhedron::limited_H79_extrapolation_assign() takes the constraint system argument by const reference (in the old Polyhedron::limited_H79_widening_assign() that argument was passed by non-const reference). o We now require GMP 4.1.2 or higher. o In conformance with the C++ standard [17.4.3.1.2], in all the identifiers exported by the C interface, any occurrence of "__" (double underscore) has been replaced by "_" (underscore). o Added a parameter to Polyhedron::shrink_bounding_box(): this specifies the complexity class of the algorithm to be used. o All the input/output operators have been confined into namespace Parma_Polyhedra_Library::IO_Operators. This way they do not conflict with the operators the user might want to define. o The operator Constraint operator>>(const Constraint&, unsigned int) has been removed. o The method Polyhedron::poly_difference_assign_and_minimize(const Polyhedron&) has been removed. Bugfixes ======== o Fixed a bug in operator-=(LinExpression&, const LinExpression&) whereby we computed a wrong result in some circumstances. o Fixed a bug in method Polyhedron::minimized_constraints() that, under some circumstances, could cause a wrong result or a program crash. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Parma Polyhedra Library 0.4.2
by Roberto Bagnara 04 Oct '02

04 Oct '02

We have the pleasure to announce the release 0.4.2 of the Parma Polyhedra Library, a minor bugfix release. Most of the bugs fixed in this release were discovered thanks to the ongoing effort to extend the PPL test suite so as to cover 100% of the library's code. For more information, visit the PPL web site at http://www.cs.unipr.it/ppl/ The PPL development team: Roberto Bagnara <bagnara(a)cs.unipr.it> Patricia M. Hill <hill(a)comp.leeds.ac.uk> Elisa Ricci <ericci(a)cs.unipr.it> Enea Zaffanella <zaffanella(a)cs.unipr.it> Bugfixes ======== o Fixed a bug in method Polyhedron::add_generator(const Generator&) whereby we were not adding the corresponding closure point when adding a point to an empty NNC polyhedron. o Fixed a bug in method GenSys::insert(const Generator&) whereby the insertion of a generator into an empty generator system might be mishandled. o Fixed a bug in method Polyhedron::operator<=(const Polyehdron&) whereby the lines of the polyhedron were handled improperly. o Fixed a bug in a private method used to implement public method Polyhedron::relation_with(const Generator& g), whereby a wrong result was obtained when `g' was a line. o Fixed a bug in methods Polyhedron::affine_image() and Polyhedron::affine_preimage(), whereby a wrong result could be obtained when using a negative denominator for the affine expression. o Fixed a bug in methods Polyhedron::minimized_constraints() and Polyhedron::minimized_generators(), whereby a library invariant was violated when calling these methods on a zero-dimensional space universe NNC polyhedron. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Parma Polyhedra Library 0.4.1
by Roberto Bagnara 30 Jul '02

30 Jul '02

We have the pleasure to announce the release 0.4.1 of the Parma Polyhedra Library, a minor bugfix release. For more information, visit the PPL web site at http://www.cs.unipr.it/ppl/ The PPL development team: Roberto Bagnara <bagnara(a)cs.unipr.it> Patricia M. Hill <hill(a)comp.leeds.ac.uk> Elisa Ricci <ericci(a)cs.unipr.it> Enea Zaffanella <zaffanella(a)cs.unipr.it> Bugfixes ======== o Fixed a bug in Polyhedron::poly_difference_assign(const Polyhedron& y) whereby the equality constraints of `y' were ignored (the bug was affecting both C and NNC computations). o Fixed a bug in Polyhedron::operator=(const Polyhedron& y). This bug, which is triggered in some cases when `y' is empty, should only affect versions of the library obtained with the `--enable-assertions' configuration flag. o Fixed a bug in Polyhedron::check_universe(), which was returning the wrong result when called on a zero-dim universe polyhedron. o Fixed a bug in NNC_Polyhedron::NNC_Polyhedron(ConSys& cs) whereby an invariant was violated in case `cs' was empty. This bug should only affect versions of the library obtained with the `--enable-assertions' configuration flag. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0