- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Added a missing project and updated a broken link.
by Roberto Bagnara 28 Feb '12

28 Feb '12

Module: ppl/ppl Branch: master Commit: acadcd82f6c200e12723630c950ac7c279f4ceca URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=acadcd82f6c2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Feb 28 11:46:39 2012 +0100 Added a missing project and updated a broken link. --- CREDITS | 16 ++++++++++------ 1 files changed, 10 insertions(+), 6 deletions(-) diff --git a/CREDITS b/CREDITS index fe664a0..82b9bf7 100644 --- a/CREDITS +++ b/CREDITS @@ -350,17 +350,20 @@ projects and organizations: - PRIN project ``AIDA 2007 - Abstract Interpretation: Design and Applications'' [62]; +- Integrated Action Italy-Spain 2001-2002 ``Advanced Development Environments + for Logic Programs'' [63]; + - Royal Society Joint project 2004/R1-EU (UK-Italy) ``Automatic Detection of Unstable Numerical Computations''; - EPSRC (UK) project EP/C520726/1 - ``Numerical Domains for Software Analysis'' [63]; + ``Numerical Domains for Software Analysis'' [64]; - Royal Society International Outgoing Short Visit 2007/R4 - ``Finding and Verifying the Absence of Bugs in Imperative Programs'' [64]; + ``Finding and Verifying the Absence of Bugs in Imperative Programs'' [65]; - EPSRC (UK) project EP/G025177/1 - ``Geometric Abstractions for Scalable Program Analyzers'' [64]. + ``Geometric Abstractions for Scalable Program Analyzers'' [65]. -------- @@ -368,7 +371,7 @@ projects and organizations: [2] http://www.comp.leeds.ac.uk/hill/ [3] http://www.cs.unipr.it/~zaffanella/ [4] http://www.math.unipr.it/~zaccagni/ - [5] http://www.prism.uvsq.fr/~fgalea/ + [5] http://fgalea.free.fr/ [6] http://www.mundell.ukfsn.org/ [7] http://www.lsi.upc.edu/~erodri/ [8] http://www.irisa.fr/lande/fbesson/fbesson.html @@ -426,5 +429,6 @@ projects and organizations: [60] http://www.disi.unige.it/person/DelzannoG/cover/ [61] http://www.cs.unipr.it/Projects/AIDA/ [62] http://www.cs.unipr.it/Projects/AIDA2007/ -[63] http://www.comp.leeds.ac.uk/hill/chiara/WWW/linda.html -[64] http://www.comp.leeds.ac.uk/hill/chiara/WWW/projects.html +[63] http://www.cs.unipr.it/Projects/AzInt2001-2002Sp +[64] http://www.comp.leeds.ac.uk/hill/chiara/WWW/linda.html +[65] http://www.comp.leeds.ac.uk/hill/chiara/WWW/projects.html

1 0

Parma Polyhedra Library 0.12
by Roberto Bagnara 27 Feb '12

27 Feb '12

The core development team is very pleased to announce the availability of PPL 0.12, a new release of the Parma Polyhedra Library. This release includes portability improvements, a few bug fixes, and performance improvements for the MIP and PIP solvers. and PIP solvers. Configurability has also been improved, especially as far as the detection of GMP is concerned. ECLAIR (http://bugseng.com/products/eclair) has been introduced into the development workflow to bring the PPL into conformance with the applicable rules in MISRA, CERT, NASA/JPL, ESA/BSSC and other widely-used coding standards. The precise list of user-visible changes is below. For more information, please come and visit the new PPL web site at http://bugseng.com/products/ppl On behalf of all the past and present developers listed at http://bugseng.com/products/ppl/credits and in the file CREDITS, Roberto Bagnara Patricia M. Hill Enea Zaffanella Abramo Bagnara BUGSENG srl (http://bugseng.com) -------------------------------------------------------------------------- NEWS for version 0.12 (released on February 27, 2012) -------------------------------------------------------------------------- New and Changed Features ======================== o New configure options `--with-gmp=DIR', `--with-gmp-include=DIR' and `--with-gmp-lib=DIR' supersede the (now removed) option `--with-gmp-prefix'. (The old option never really worked; hopefully this is the last change in this area.) o New configuration option `--disable-documentation'. When specified no new documentation is built: only the documentation already present in the source tree is installed upon `make install'. o The resolution process for PIP_Problem now better exploits the integrality of parameters to simplify the newly generated tautological constraints, the splitting constraints of decision nodes, and the expressions defining artificial parameters. o The implementations of the MIP and PIP solvers are based on a new data structure leading to significant space and time savings when the tableau matrix is sparse; the benchmarks of the ppl_lpsol demo show an improvement on the average case, that grows when the toughest tests in the benchmark suite are considered. o When the `--check' option is used, the input data for demo ppl_lpsol is perturbed the same way as GLPK does, thereby allowing for a meaningful comparison of the results obtained. o The input routine for PPL numeric datatypes has been extended to accept the ISO9899 (C99) hexadecimal floating constant syntax. o The Parma Watchdog Library has been merged into the Parma Polyhedra Library. Bugfixes ======== o Corrected a precision bug in methods Box<ITV>::upper_bound_assign(const Box&) Box<ITV>::upper_bound_assign_if_exact(const Box&) whereby, provided any argument is an empty box and under other rather specific conditions, the computed result was correct but unnecessarily imprecise. o Corrected a bug in method Grid::relation_with(const Constraint&) const whereby, under specific conditions, the method was creating invalid Grid_Generator objects and providing an incorrect result. -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Update version.
by Roberto Bagnara 27 Feb '12

27 Feb '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: 0a918b0eee08c0d4edf422843568c36f3006b93e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0a918b0eee08… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Feb 27 17:30:24 2012 +0100 Update version. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index e78909e..fa8dbba 100644 --- a/configure.ac +++ b/configure.ac @@ -24,7 +24,7 @@ # Process this file with Autoconf to produce a configure script. # Every other copy of the package version number gets its value from here. -AC_INIT([the Parma Polyhedra Library], [0.12pre7], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [0.12], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61)

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Mark ChangeLog.
by Roberto Bagnara 27 Feb '12

27 Feb '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: c3cc90d21be881f2242ca94233d503ba70cc5c24 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c3cc90d21be8… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Feb 27 17:30:24 2012 +0100 Mark ChangeLog. --- ChangeLog | 4 ++++ 1 files changed, 4 insertions(+), 0 deletions(-) diff --git a/ChangeLog b/ChangeLog index b33555c..a791115 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2012-02-27 Roberto Bagnara <bagnara(a)cs.unipr.it> + * PPL 0.12 released. + +2012-02-27 Roberto Bagnara <bagnara(a)cs.unipr.it> + * CREDITS, TODO: Updated. 2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it>

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Updated.
by Roberto Bagnara 27 Feb '12

27 Feb '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: 00cbfdb30e8e8a7e5c7fe20f63c53a27370a7905 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=00cbfdb30e8e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Feb 27 17:24:27 2012 +0100 Updated. --- ChangeLog | 167 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 167 insertions(+), 0 deletions(-) diff --git a/ChangeLog b/ChangeLog index 46ae1f2..b33555c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,170 @@ +2012-02-27 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * CREDITS, TODO: Updated. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Concrete_Expression.defs.hh, src/Concrete_Expression.types.hh: + Let classes in Concrete_Expression.defs.hh appear in the user + manual. + +2012-02-27 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * src/globals.types.hh: Documented the enumerated values of enum + Floating_Point_Format. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/intervals.defs.hh: Let the docs for the I_Result enum appear + on the devref manual only. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/OR_Matrix.inlines.hh, src/globals.defs.hh: Mark some docs for + the devref manual only. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/fpu.defs.hh: Group together documentation of functions + controlling FPU. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/linearize.hh: Fixed documentation for linearize and added + \relates directive. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/termination.defs.hh: Grouped together docs for the + linear-ranking functions. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/CO_Tree.defs.hh, src/Sparse_Row.defs.hh: CO_Tree and + Sparse_Row should only appear in the devref manual. + +2012-02-26 Abramo Bagnara <abramo.bagnara(a)gmail.com> + + * src/Row_Flags.cc: Fixed missing namespace. + +2012-02-26 Abramo Bagnara <abramo.bagnara(a)gmail.com> + + * src/Checked_Number.templates.hh, src/Interval.templates.hh, + src/Interval_Info.inlines.hh, src/Row_Flags.cc: Fixed and uniformed + iomanip uses. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/wrap_string.cc: Avoid mixing plain character data with numeric + data. Detected by ECLAIR service utypflag. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * doc/devref.doxyconf-html.in, doc/devref.doxyconf-latex.in: Removed + references to an obsolete file. + +2012-02-26 Abramo Bagnara <abramo.bagnara(a)gmail.com> + + * src/CO_Tree.defs.hh, src/MIP_Problem.cc: Removed redundant and + unused stuff. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Checked_Number.defs.hh, src/Ptr_Iterator.defs.hh: Use the same + typenames in function declarations/definitions. Detected by ECLAIR + service funtypes. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Interval_Info.defs.hh, src/Pointset_Powerset.templates.hh, + src/checked_int.inlines.hh: Avoid mixing boolean and arithmetic + values. Detected by ECLAIR service utypflag. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/GMP_Integer.defs.hh: Get rid of redundant declarations of a + couple of functions. Detected by ECLAIR service funtypes. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Interval_Info.inlines.hh: Simplified + Interval_Info::ascii_load(). Resettting format flags does not + change the istream status, which was previously tested and is known + to be good: hence, return true. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * demos/ppl_lcdd/ppl_lcdd.cc, demos/ppl_pips/ppl_pips.cc, + fedora/ppl.hh, fedora/ppl_c.h, fedora/pwl.hh, + src/BDS_Status.idefs.hh, src/Box_Status.idefs.hh, + src/Float.defs.hh, src/Grid_Status.idefs.hh, + src/Og_Status.idefs.hh, src/Ph_Status.idefs.hh, src/fpu.defs.hh: + `#error' messages made consistent. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * src/compiler.hh: Variable names fixed. + +2012-02-26 Abramo Bagnara <abramo.bagnara(a)gmail.com> + + * interfaces/C/ppl_c_implementation_common.cc, + interfaces/Java/jni/ppl_java_common.defs.hh, + interfaces/Java/jni/ppl_java_common.inlines.hh, + src/BD_Shape.templates.hh, src/Box.templates.hh, + src/Grid_public.cc, src/Octagonal_Shape.templates.hh, + src/Polyhedron_public.cc, src/Variable.cc, src/Variable.defs.hh, + src/Variables_Set.cc, src/Variables_Set.defs.hh, + src/Variables_Set.inlines.hh, src/termination.templates.hh, + src/wrap_assign.hh, tests/Polyhedron/affineimage2.cc, + tests/Polyhedron/bgp99extrapolation1.cc, + tests/Polyhedron/bhz03widening1.cc, + tests/Polyhedron/boundedbhrz03extrapolation1.cc, + tests/Polyhedron/writevariable1.cc, tests/ppl_test.cc, + tests/ppl_test.hh: Avoid to use Variable references. Uniformed + Variable creations. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * src/compiler.hh: Types fixed. Useless if-then-else removed. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * m4/ac_check_gmp.m4: Use `libtool' to test linking with GMP only if + the option `--with-gmp-build' was given. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Congruence_System.cc, src/Interval_Info.defs.hh, + src/Ph_Status.inlines.hh: Prefer explicit tests against zero. Avoid + using boolean values as integer values. Detected by ECLAIR service + utypflag. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Linear_Form.templates.hh, src/OR_Matrix.inlines.hh, + src/checked_float.inlines.hh: Improved implementation of + OR_Matrix<T>::any_row_iterator<U>::operator+=(). Increased + readability: - separated explicit type conversions from code performing + arithmetic operations (on non-mixed typed values); - added a few redundant parentheses. Similar improvement applied + to a couple of other functions. Detected by ECLAIR service + utypflag. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/globals.defs.hh, src/version.hh.in: Provide a named group for + all library version control functions. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * interfaces/C/ppl_c_implementation_common.cc, + src/DB_Row.inlines.hh, src/Interval_Info.inlines.hh, + src/ppl-config.cc.in: Prefer explicit tests against zero. Detected + by ECLAIR service utypflag. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * ChangeLog: Updated. + 2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> * tests/Makefile.am: Added `Watchdog' to `SUBDIRS'.

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Updated.
by Roberto Bagnara 27 Feb '12

27 Feb '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: 143fc5c5b4fdc0a6c24271d60f515214937ee39b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=143fc5c5b4fd… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Feb 27 17:22:59 2012 +0100 Updated. --- CREDITS | 11 ++++++----- TODO | 8 ++------ 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/CREDITS b/CREDITS index 99aa556..fe664a0 100644 --- a/CREDITS +++ b/CREDITS @@ -29,6 +29,12 @@ Former Members of the Core Development Team: Current Contributors: --------------------- + Andrea Cimino (former student of the University of Parma) + wrote most of the mixed integer programming + solver, and also most of the Java and OCaml + interfaces. He keeps helping us, especially + with the web site. + Marco Poletti (student of the University of Bologna) implemented the sparse matrices that are used in the MIP and PIP solvers of the PPL; he also @@ -78,11 +84,6 @@ Past Contributors: one of the four students with which the PPL project started. - Andrea Cimino (former student of the University of Parma) - wrote most of the mixed integer programming - solver, and also most of the Java and OCaml - interfaces. - Katy Dobson (former student of the University of Leeds) worked on the formalization and definition of algorithms for rational grids and products diff --git a/TODO b/TODO index 271fb42..75b2e0d 100644 --- a/TODO +++ b/TODO @@ -1,11 +1,10 @@ -Enhancements for PPL 0.12 or later versions +Enhancements for PPL 0.13 or later versions =========================================== - Make all the *affine*image() methods uniform as far as the specification is concerned. - Add the domains of bounded integers and affine spaces. -- Finish the domain of intervals. - Intervals are best instantiated with checked numbers with particular policies: review all the interfaced boxes, augment the testsuite, and update the documentation. @@ -66,7 +65,7 @@ Enhancements for PPL 0.12 or later versions - Any_Pointset domain: check the interface for lacking or useless methods. -Enhancements for PPL 0.13 or later versions +Enhancements for PPL 0.14 or later versions =========================================== - Find a way to let the GMP and checked-int versions of the PPL coexist @@ -108,8 +107,5 @@ Efficiency Issues - There must be a more efficient way to implement bool Polyhedron::is_disjoint_from(const Polyhedron&). - There must be a more efficient way to compute convex differences. -- We are being rather careless about the creation of temporaries - as far as the classes Linear_Expression, Constraint and Generator - are concerned. - Provide a better implementation of computing squares in MIP_Problem's steepest-edge to avoid big numbers.

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 27 Feb '12

27 Feb '12

Module: ppl/ppl Branch: master Commit: 00cbfdb30e8e8a7e5c7fe20f63c53a27370a7905 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=00cbfdb30e8e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Feb 27 17:24:27 2012 +0100 Updated. --- ChangeLog | 167 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 167 insertions(+), 0 deletions(-) diff --git a/ChangeLog b/ChangeLog index 46ae1f2..b33555c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,170 @@ +2012-02-27 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * CREDITS, TODO: Updated. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Concrete_Expression.defs.hh, src/Concrete_Expression.types.hh: + Let classes in Concrete_Expression.defs.hh appear in the user + manual. + +2012-02-27 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * src/globals.types.hh: Documented the enumerated values of enum + Floating_Point_Format. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/intervals.defs.hh: Let the docs for the I_Result enum appear + on the devref manual only. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/OR_Matrix.inlines.hh, src/globals.defs.hh: Mark some docs for + the devref manual only. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/fpu.defs.hh: Group together documentation of functions + controlling FPU. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/linearize.hh: Fixed documentation for linearize and added + \relates directive. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/termination.defs.hh: Grouped together docs for the + linear-ranking functions. + +2012-02-27 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/CO_Tree.defs.hh, src/Sparse_Row.defs.hh: CO_Tree and + Sparse_Row should only appear in the devref manual. + +2012-02-26 Abramo Bagnara <abramo.bagnara(a)gmail.com> + + * src/Row_Flags.cc: Fixed missing namespace. + +2012-02-26 Abramo Bagnara <abramo.bagnara(a)gmail.com> + + * src/Checked_Number.templates.hh, src/Interval.templates.hh, + src/Interval_Info.inlines.hh, src/Row_Flags.cc: Fixed and uniformed + iomanip uses. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/wrap_string.cc: Avoid mixing plain character data with numeric + data. Detected by ECLAIR service utypflag. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * doc/devref.doxyconf-html.in, doc/devref.doxyconf-latex.in: Removed + references to an obsolete file. + +2012-02-26 Abramo Bagnara <abramo.bagnara(a)gmail.com> + + * src/CO_Tree.defs.hh, src/MIP_Problem.cc: Removed redundant and + unused stuff. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Checked_Number.defs.hh, src/Ptr_Iterator.defs.hh: Use the same + typenames in function declarations/definitions. Detected by ECLAIR + service funtypes. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Interval_Info.defs.hh, src/Pointset_Powerset.templates.hh, + src/checked_int.inlines.hh: Avoid mixing boolean and arithmetic + values. Detected by ECLAIR service utypflag. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/GMP_Integer.defs.hh: Get rid of redundant declarations of a + couple of functions. Detected by ECLAIR service funtypes. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Interval_Info.inlines.hh: Simplified + Interval_Info::ascii_load(). Resettting format flags does not + change the istream status, which was previously tested and is known + to be good: hence, return true. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * demos/ppl_lcdd/ppl_lcdd.cc, demos/ppl_pips/ppl_pips.cc, + fedora/ppl.hh, fedora/ppl_c.h, fedora/pwl.hh, + src/BDS_Status.idefs.hh, src/Box_Status.idefs.hh, + src/Float.defs.hh, src/Grid_Status.idefs.hh, + src/Og_Status.idefs.hh, src/Ph_Status.idefs.hh, src/fpu.defs.hh: + `#error' messages made consistent. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * src/compiler.hh: Variable names fixed. + +2012-02-26 Abramo Bagnara <abramo.bagnara(a)gmail.com> + + * interfaces/C/ppl_c_implementation_common.cc, + interfaces/Java/jni/ppl_java_common.defs.hh, + interfaces/Java/jni/ppl_java_common.inlines.hh, + src/BD_Shape.templates.hh, src/Box.templates.hh, + src/Grid_public.cc, src/Octagonal_Shape.templates.hh, + src/Polyhedron_public.cc, src/Variable.cc, src/Variable.defs.hh, + src/Variables_Set.cc, src/Variables_Set.defs.hh, + src/Variables_Set.inlines.hh, src/termination.templates.hh, + src/wrap_assign.hh, tests/Polyhedron/affineimage2.cc, + tests/Polyhedron/bgp99extrapolation1.cc, + tests/Polyhedron/bhz03widening1.cc, + tests/Polyhedron/boundedbhrz03extrapolation1.cc, + tests/Polyhedron/writevariable1.cc, tests/ppl_test.cc, + tests/ppl_test.hh: Avoid to use Variable references. Uniformed + Variable creations. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * src/compiler.hh: Types fixed. Useless if-then-else removed. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * m4/ac_check_gmp.m4: Use `libtool' to test linking with GMP only if + the option `--with-gmp-build' was given. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Congruence_System.cc, src/Interval_Info.defs.hh, + src/Ph_Status.inlines.hh: Prefer explicit tests against zero. Avoid + using boolean values as integer values. Detected by ECLAIR service + utypflag. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/Linear_Form.templates.hh, src/OR_Matrix.inlines.hh, + src/checked_float.inlines.hh: Improved implementation of + OR_Matrix<T>::any_row_iterator<U>::operator+=(). Increased + readability: - separated explicit type conversions from code performing + arithmetic operations (on non-mixed typed values); - added a few redundant parentheses. Similar improvement applied + to a couple of other functions. Detected by ECLAIR service + utypflag. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * src/globals.defs.hh, src/version.hh.in: Provide a named group for + all library version control functions. + +2012-02-26 Enea Zaffanella <zaffanella(a)cs.unipr.it> + + * interfaces/C/ppl_c_implementation_common.cc, + src/DB_Row.inlines.hh, src/Interval_Info.inlines.hh, + src/ppl-config.cc.in: Prefer explicit tests against zero. Detected + by ECLAIR service utypflag. + +2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> + + * ChangeLog: Updated. + 2012-02-26 Roberto Bagnara <bagnara(a)cs.unipr.it> * tests/Makefile.am: Added `Watchdog' to `SUBDIRS'.

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 27 Feb '12

27 Feb '12

Module: ppl/ppl Branch: master Commit: 143fc5c5b4fdc0a6c24271d60f515214937ee39b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=143fc5c5b4fd… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Feb 27 17:22:59 2012 +0100 Updated. --- CREDITS | 11 ++++++----- TODO | 8 ++------ 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/CREDITS b/CREDITS index 99aa556..fe664a0 100644 --- a/CREDITS +++ b/CREDITS @@ -29,6 +29,12 @@ Former Members of the Core Development Team: Current Contributors: --------------------- + Andrea Cimino (former student of the University of Parma) + wrote most of the mixed integer programming + solver, and also most of the Java and OCaml + interfaces. He keeps helping us, especially + with the web site. + Marco Poletti (student of the University of Bologna) implemented the sparse matrices that are used in the MIP and PIP solvers of the PPL; he also @@ -78,11 +84,6 @@ Past Contributors: one of the four students with which the PPL project started. - Andrea Cimino (former student of the University of Parma) - wrote most of the mixed integer programming - solver, and also most of the Java and OCaml - interfaces. - Katy Dobson (former student of the University of Leeds) worked on the formalization and definition of algorithms for rational grids and products diff --git a/TODO b/TODO index 271fb42..75b2e0d 100644 --- a/TODO +++ b/TODO @@ -1,11 +1,10 @@ -Enhancements for PPL 0.12 or later versions +Enhancements for PPL 0.13 or later versions =========================================== - Make all the *affine*image() methods uniform as far as the specification is concerned. - Add the domains of bounded integers and affine spaces. -- Finish the domain of intervals. - Intervals are best instantiated with checked numbers with particular policies: review all the interfaced boxes, augment the testsuite, and update the documentation. @@ -66,7 +65,7 @@ Enhancements for PPL 0.12 or later versions - Any_Pointset domain: check the interface for lacking or useless methods. -Enhancements for PPL 0.13 or later versions +Enhancements for PPL 0.14 or later versions =========================================== - Find a way to let the GMP and checked-int versions of the PPL coexist @@ -108,8 +107,5 @@ Efficiency Issues - There must be a more efficient way to implement bool Polyhedron::is_disjoint_from(const Polyhedron&). - There must be a more efficient way to compute convex differences. -- We are being rather careless about the creation of temporaries - as far as the classes Linear_Expression, Constraint and Generator - are concerned. - Provide a better implementation of computing squares in MIP_Problem's steepest-edge to avoid big numbers.

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Let classes in Concrete_Expression.defs. hh appear in the user manual.
by Enea Zaffanella 27 Feb '12

27 Feb '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: 7d19a65f547bc4224622dbf70df1c43b792a194f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d19a65f547b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Feb 27 15:57:45 2012 +0100 Let classes in Concrete_Expression.defs.hh appear in the user manual. --- src/Concrete_Expression.defs.hh | 8 ++++++++ src/Concrete_Expression.types.hh | 3 +-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/Concrete_Expression.defs.hh b/src/Concrete_Expression.defs.hh index 655e119..0f30e57 100644 --- a/src/Concrete_Expression.defs.hh +++ b/src/Concrete_Expression.defs.hh @@ -30,6 +30,7 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { +//! The type of a concrete expression. class Concrete_Expression_Type { public: /*! \brief @@ -116,6 +117,7 @@ private: Implementation impl; }; +//! Base class for all concrete expressions. template <typename Target> class Concrete_Expression_Common { public: @@ -145,6 +147,7 @@ public: }; +//! Base class for binary operator applied to two concrete expressions. template <typename Target> class Binary_Operator_Common { public: @@ -158,6 +161,7 @@ public: const Concrete_Expression<Target>* right_hand_side() const; }; +//! Base class for unary operator applied to one concrete expression. template <typename Target> class Unary_Operator_Common { public: @@ -168,20 +172,24 @@ public: const Concrete_Expression<Target>* argument() const; }; +//! Base class for cast operator concrete expressions. template <typename Target> class Cast_Operator_Common { //! Returns the casted expression. const Concrete_Expression<Target>* argument() const; }; +//! Base class for integer constant concrete expressions. template <typename Target> class Integer_Constant_Common { }; +//! Base class for floating-point constant concrete expression. template <typename Target> class Floating_Point_Constant_Common { }; +//! Base class for references to some approximable. template <typename Target> class Approximable_Reference_Common { }; diff --git a/src/Concrete_Expression.types.hh b/src/Concrete_Expression.types.hh index 7a3c7e7..999ff41 100644 --- a/src/Concrete_Expression.types.hh +++ b/src/Concrete_Expression.types.hh @@ -27,7 +27,7 @@ class Binary_Operator; template <typename Target> class Unary_Operator; -//! A cast operator applied converting one concrete expression to some type. +//! A cast operator converting one concrete expression to some type. template <typename Target> class Cast_Operator; @@ -43,7 +43,6 @@ class Floating_Point_Constant; template <typename Target> class Approximable_Reference; -//! The type of a concrete expression. class Concrete_Expression_Type; /*! \brief

1 0

[GIT] ppl/ppl(master): Let classes in Concrete_Expression.defs. hh appear in the user manual.
by Enea Zaffanella 27 Feb '12

27 Feb '12

Module: ppl/ppl Branch: master Commit: 7d19a65f547bc4224622dbf70df1c43b792a194f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d19a65f547b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Feb 27 15:57:45 2012 +0100 Let classes in Concrete_Expression.defs.hh appear in the user manual. --- src/Concrete_Expression.defs.hh | 8 ++++++++ src/Concrete_Expression.types.hh | 3 +-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/Concrete_Expression.defs.hh b/src/Concrete_Expression.defs.hh index 655e119..0f30e57 100644 --- a/src/Concrete_Expression.defs.hh +++ b/src/Concrete_Expression.defs.hh @@ -30,6 +30,7 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { +//! The type of a concrete expression. class Concrete_Expression_Type { public: /*! \brief @@ -116,6 +117,7 @@ private: Implementation impl; }; +//! Base class for all concrete expressions. template <typename Target> class Concrete_Expression_Common { public: @@ -145,6 +147,7 @@ public: }; +//! Base class for binary operator applied to two concrete expressions. template <typename Target> class Binary_Operator_Common { public: @@ -158,6 +161,7 @@ public: const Concrete_Expression<Target>* right_hand_side() const; }; +//! Base class for unary operator applied to one concrete expression. template <typename Target> class Unary_Operator_Common { public: @@ -168,20 +172,24 @@ public: const Concrete_Expression<Target>* argument() const; }; +//! Base class for cast operator concrete expressions. template <typename Target> class Cast_Operator_Common { //! Returns the casted expression. const Concrete_Expression<Target>* argument() const; }; +//! Base class for integer constant concrete expressions. template <typename Target> class Integer_Constant_Common { }; +//! Base class for floating-point constant concrete expression. template <typename Target> class Floating_Point_Constant_Common { }; +//! Base class for references to some approximable. template <typename Target> class Approximable_Reference_Common { }; diff --git a/src/Concrete_Expression.types.hh b/src/Concrete_Expression.types.hh index 7a3c7e7..999ff41 100644 --- a/src/Concrete_Expression.types.hh +++ b/src/Concrete_Expression.types.hh @@ -27,7 +27,7 @@ class Binary_Operator; template <typename Target> class Unary_Operator; -//! A cast operator applied converting one concrete expression to some type. +//! A cast operator converting one concrete expression to some type. template <typename Target> class Cast_Operator; @@ -43,7 +43,6 @@ class Floating_Point_Constant; template <typename Target> class Approximable_Reference; -//! The type of a concrete expression. class Concrete_Expression_Type; /*! \brief

1 0