- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Completed `ppl_config_SOURCES'.
by Roberto Bagnara 26 Feb '12

26 Feb '12

Module: ppl/ppl Branch: master Commit: 5238b268632f21366a5ba79816bf742fbb8ebc71 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5238b268632f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 26 09:24:01 2012 +0100 Completed `ppl_config_SOURCES'. --- src/Makefile.am | 3 +++ 1 files changed, 3 insertions(+), 0 deletions(-) diff --git a/src/Makefile.am b/src/Makefile.am index 8d12e35..ed490f0 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -72,8 +72,11 @@ lib_LTLIBRARIES = libppl.la bin_PROGRAMS = ppl-config ppl_config_SOURCES = \ +BUGS.hh \ BUGS.cc \ +COPYING.hh \ COPYING.cc \ +CREDITS.hh \ CREDITS.cc nodist_ppl_config_SOURCES = \

1 0

[GIT] ppl/ppl(master): Cater for platforms where no floating-point type is supported.
by Roberto Bagnara 26 Feb '12

26 Feb '12

Module: ppl/ppl Branch: master Commit: 81b598e7484f1d4b0d3323bafb30578c17149b1d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=81b598e7484f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Feb 26 08:21:32 2012 +0100 Cater for platforms where no floating-point type is supported. --- configure.ac | 22 ++++++++---------- tests/Concrete_Expression/Makefile.am | 38 +++++++++++++------------------- 2 files changed, 26 insertions(+), 34 deletions(-) diff --git a/configure.ac b/configure.ac index 45acdca..e78909e 100644 --- a/configure.ac +++ b/configure.ac @@ -762,17 +762,15 @@ AC_CXX_DOUBLE_BINARY_FORMAT # Detect the binary format used by C++ long doubles. AC_CXX_LONG_DOUBLE_BINARY_FORMAT -# Check whether the C++ run-time systems provides exact output for -# floats. -#AC_CXX_FLOAT_EXACT_OUTPUT - -# Check whether the C++ run-time systems provides exact output for -# doubles. -#AC_CXX_DOUBLE_EXACT_OUTPUT - -# Check whether the C++ run-time systems provides exact output for -# long doubles. -#AC_CXX_LONG_DOUBLE_EXACT_OUTPUT +# Test if some floating-point type is supported. +if test $ac_supported_float = 1 \ +|| test $ac_supported_double = 1 \ +|| test $ac_supported_long_double = 1 +then + supported_some_floating_point_type=yes +fi +AM_CONDITIONAL(SUPPORTED_SOME_FLOATING_POINT_TYPE, + test x$supported_some_floating_point_type = xyes) # Check whether the C++ compiler supports zero-length arrays. AC_CXX_SUPPORTS_ZERO_LENGTH_ARRAYS @@ -1222,7 +1220,7 @@ fi AM_CONDITIONAL(BUILD_YAP_PROLOG_INTERFACE, test x$build_yap_prolog_interface = xyes) -# Test if *any* Prolog system has to be built. +# Test if some Prolog interfaces have to be built. if test x$build_ciao_prolog_interface = xyes \ || test x$build_gnu_prolog_interface = xyes \ || test x$build_sicstus_prolog_interface = xyes \ diff --git a/tests/Concrete_Expression/Makefile.am b/tests/Concrete_Expression/Makefile.am index 3a79ec1..54b1af8 100644 --- a/tests/Concrete_Expression/Makefile.am +++ b/tests/Concrete_Expression/Makefile.am @@ -52,7 +52,7 @@ $(top_builddir)/tests/libppl_tests.a \ $(top_builddir)/src/libppl.la \ @extra_libraries@ -ORIGINAL_TESTS = \ +ALL_TESTS = \ C_Expr \ linearform1 \ linearize \ @@ -64,9 +64,19 @@ octagonalshape2 \ polyhedron1 \ polyhedron2 -DERIVED_TESTS = +BUGS = + +EXTRA_DIST = $(ALL_TESTS) $(BUGS) + +# There are platforms where no floating-point type is supported. +if SUPPORTED_SOME_FLOATING_POINT_TYPE + +check_PROGRAMS = $(ALL_TESTS) $(BUGS) + +TESTS = run_tests.stamp + +endif SUPPORTED_SOME_FLOATING_POINT_TYPE -ALL_TESTS = $(ORIGINAL_TESTS) $(DERIVED_TESTS) # This will be overridden by the `run_tests' script. if SUPPORTED_FLOAT @@ -83,12 +93,11 @@ LONG_DOUBLE_FLAGS = \ endif endif endif + TEST_CPPFLAGS = $(FLOAT_FLAGS) $(DOUBLE_FLAGS) $(LONG_DOUBLE_FLAGS) dist_check_SCRIPTS = run_tests -TESTS = run_tests.stamp - .PHONY: run_tests.stamp run_tests.stamp: run_tests +MAKE="$(MAKE)" $(srcdir)/run_tests @@ -152,30 +161,15 @@ polyhedron1_SOURCES = polyhedron1.cc polyhedron2_SOURCES = polyhedron2.cc -# -# Sources and compilation flags for the derived check programs -# - -DERIVED_CXXFLAGS = -DDERIVED_TEST $(AM_CXXFLAGS) - -#nnc_frompolyhedron1_SOURCES = frompolyhedron1.cc -#nnc_frompolyhedron1_CXXFLAGS = $(DERIVED_CXXFLAGS) - -BUGS = - -check_PROGRAMS = $(ALL_TESTS) $(BUGS) - -#EXTRA_DIST = $(refinewithconstraints2_SRCS) - -#MOSTLYCLEANFILES = \ -#ascii_dump_load1.dat CLEANFILES = \ run_tests.stamp + DISTCLEANFILES = \ dirty_marker + $(top_builddir)/utils/libppl_utils.a: $(MAKE) $(AM_MAKEFLAGS) -C $(top_builddir)/utils libppl_utils.a

1 0

[GIT] ppl/ppl(master): Added several missing \relates and \ingroup Doxygen commands.
by Enea Zaffanella 26 Feb '12

26 Feb '12

Module: ppl/ppl Branch: master Commit: fa1aba6cae22ad32a1f520cb2fce421d0259c3a8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fa1aba6cae22… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Feb 26 00:27:51 2012 +0100 Added several missing \relates and \ingroup Doxygen commands. --- src/Checked_Number.defs.hh | 8 +++++++ src/Float.defs.hh | 46 ++++++++++++++++++++----------------------- src/Interval.defs.hh | 1 + src/Linear_Form.defs.hh | 2 +- src/PIP_Tree.defs.hh | 2 +- src/termination.defs.hh | 28 +++++++++++++------------- 6 files changed, 46 insertions(+), 41 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=fa1aba6c…

1 0

[GIT] ppl/ppl(master): Remove docs for a few implementation classes from the user manual.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 609f96793392774847c032d06ac3898e62995d4f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=609f96793392… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 23:55:53 2012 +0100 Remove docs for a few implementation classes from the user manual. --- src/CO_Tree.defs.hh | 6 +++--- src/Checked_Number.defs.hh | 6 ++++++ src/Dense_Row.defs.hh | 4 ++++ src/Sparse_Matrix.defs.hh | 4 +++- src/Sparse_Row.defs.hh | 8 ++++++-- src/Sparse_Row.inlines.hh | 3 +++ src/intervals.defs.hh | 2 -- 7 files changed, 25 insertions(+), 8 deletions(-) diff --git a/src/CO_Tree.defs.hh b/src/CO_Tree.defs.hh index 61c8556..0a84211 100644 --- a/src/CO_Tree.defs.hh +++ b/src/CO_Tree.defs.hh @@ -52,11 +52,11 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { //! A cache-oblivious binary search tree of pairs. -/*! +/*! \ingroup PPL_CXX_interface This class implements a binary search tree with keys of dimension_type type and data of Coefficient type, laid out in a dynamically-sized array. - The array-based layout saves calls to new/delete (to insert n elements + The array-based layout saves calls to new/delete (to insert \f$n\f$ elements only \f$O(\log n)\f$ allocations are performed) and, more importantly, is much more cache-friendly than a standard (pointer-based) tree, because the elements are stored sequentially in memory (leaving some holes to allow @@ -94,7 +94,7 @@ namespace Parma_Polyhedra_Library { The indexes and values are stored in different arrays to reduce cache-misses during key queries. - The tree can store up to (-(dimension_type)1)/100 elements. + The tree can store up to \f$(-(dimension_type)1)/100\f$ elements. This limit allows faster density computations, but can be removed if needed. */ class CO_Tree { diff --git a/src/Checked_Number.defs.hh b/src/Checked_Number.defs.hh index d7bad52..390f7f6 100644 --- a/src/Checked_Number.defs.hh +++ b/src/Checked_Number.defs.hh @@ -139,15 +139,21 @@ struct Native_Checked_To_Wrapper<Checked_Number<T, P> > { } }; +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \ingroup PPL_CXX_interface */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) template <typename T> struct Is_Checked : public False { }; +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \ingroup PPL_CXX_interface */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) template <typename T, typename P> struct Is_Checked<Checked_Number<T, P> > : public True { }; +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \ingroup PPL_CXX_interface */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) template <typename T> struct Is_Native_Or_Checked : public Bool<Is_Native<T>::value || Is_Checked<T>::value> { }; diff --git a/src/Dense_Row.defs.hh b/src/Dense_Row.defs.hh index 0bcbd50..0e95e77 100644 --- a/src/Dense_Row.defs.hh +++ b/src/Dense_Row.defs.hh @@ -504,12 +504,16 @@ void swap(Dense_Row& x, Dense_Row& y); void iter_swap(std::vector<Dense_Row>::iterator x, std::vector<Dense_Row>::iterator y); +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Returns <CODE>true</CODE> if and only if \p x and \p y are equal. /*! \relates Dense_Row */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) bool operator==(const Dense_Row& x, const Dense_Row& y); +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Returns <CODE>true</CODE> if and only if \p x and \p y are different. /*! \relates Dense_Row */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) bool operator!=(const Dense_Row& x, const Dense_Row& y); } // namespace Parma_Polyhedra_Library diff --git a/src/Sparse_Matrix.defs.hh b/src/Sparse_Matrix.defs.hh index a8dc341..310f95f 100644 --- a/src/Sparse_Matrix.defs.hh +++ b/src/Sparse_Matrix.defs.hh @@ -29,8 +29,9 @@ site: http://bugseng.com/products/ppl/ . */ #include "globals.types.hh" #include <vector> +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! A sparse matrix of Coefficient. -/*! +/*! \ingroup PPL_CXX_interface This class is a drop-in replacement of Dense_Matrix, meaning that code using Dense_Matrix can be ported to Sparse_Matrix changing only references to Dense_Matrix and Dense_Row into references to Sparse_Matrix and @@ -52,6 +53,7 @@ site: http://bugseng.com/products/ppl/ . */ \see Sparse_Row */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) class Parma_Polyhedra_Library::Sparse_Matrix { public: diff --git a/src/Sparse_Row.defs.hh b/src/Sparse_Row.defs.hh index 555bf4b..180a2d1 100644 --- a/src/Sparse_Row.defs.hh +++ b/src/Sparse_Row.defs.hh @@ -34,7 +34,7 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { //! A finite sparse sequence of coefficients. -/*! +/*! \ingroup PPL_CXX_interface This class is implemented using a CO_Tree. See the documentation of CO_Tree for details on the implementation and the performance. @@ -75,7 +75,7 @@ public: \see CO_Tree::const_iterator */ typedef CO_Tree::const_iterator const_iterator; - + explicit Sparse_Row(Flags flags); //! Constructs a row with the specified size. @@ -821,12 +821,16 @@ namespace Parma_Polyhedra_Library { #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) void swap(Sparse_Row& x, Sparse_Row& y); +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Returns <CODE>true</CODE> if and only if \p x and \p y are equal. /*! \relates Sparse_Row */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) bool operator==(const Sparse_Row& x, const Sparse_Row& y); +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Returns <CODE>true</CODE> if and only if \p x and \p y are different. /*! \relates Sparse_Row */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) bool operator!=(const Sparse_Row& x, const Sparse_Row& y); } // namespace Parma_Polyhedra_Library diff --git a/src/Sparse_Row.inlines.hh b/src/Sparse_Row.inlines.hh index 703cf0b..0e076f1 100644 --- a/src/Sparse_Row.inlines.hh +++ b/src/Sparse_Row.inlines.hh @@ -371,6 +371,9 @@ Sparse_Row::total_memory_in_bytes(dimension_type /* capacity */) const { return total_memory_in_bytes(); } +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +/*! \relates Sparse_Row */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) inline void swap(Sparse_Row& x, Sparse_Row& y) { x.m_swap(y); diff --git a/src/intervals.defs.hh b/src/intervals.defs.hh index b9193b4..50993d8 100644 --- a/src/intervals.defs.hh +++ b/src/intervals.defs.hh @@ -31,10 +31,8 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { -#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! The result of an operation on intervals. /*! \ingroup PPL_CXX_interface */ -#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) enum I_Result { //! \hideinitializer Result may be empty. I_EMPTY = 1U,

1 0

[GIT] ppl/ppl(master): Properly terminate Doxygen comments.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: f9163fbd8bc14a1ab5a466b4d058925803caaca0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f9163fbd8bc1… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 22:55:33 2012 +0100 Properly terminate Doxygen comments. --- src/intervals.defs.hh | 26 +++++++++++++------------- 1 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/intervals.defs.hh b/src/intervals.defs.hh index 92b7693..b9193b4 100644 --- a/src/intervals.defs.hh +++ b/src/intervals.defs.hh @@ -36,33 +36,33 @@ namespace Parma_Polyhedra_Library { /*! \ingroup PPL_CXX_interface */ #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) enum I_Result { - //! \hideinitializer Result may be empty + //! \hideinitializer Result may be empty. I_EMPTY = 1U, - //! \hideinitializer Result may have only one value + //! \hideinitializer Result may have only one value. I_SINGLETON = 2U, /*! \brief \hideinitializer - Result may have more than one value, but it is not the domain universe + Result may have more than one value, but it is not the domain universe. */ I_SOME = 4U, - //! \hideinitializer Result may be the domain universe + //! \hideinitializer Result may be the domain universe. I_UNIVERSE = 8U, - //! \hideinitializer Result is not empty + //! \hideinitializer Result is not empty. I_NOT_EMPTY = I_SINGLETON | I_SOME | I_UNIVERSE, - //! \hideinitializer Result may be empty or not empty + //! \hideinitializer Result may be empty or not empty. I_ANY = I_EMPTY | I_NOT_EMPTY, - //! \hideinitializer Result may be empty or not empty + //! \hideinitializer Result may be empty or not empty. I_NOT_UNIVERSE = I_EMPTY | I_SINGLETON | I_SOME, - //! \hideinitializer Result is neither empty nor the domain universe + //! \hideinitializer Result is neither empty nor the domain universe. I_NOT_DEGENERATE = I_SINGLETON | I_SOME, - //! \hideinitializer Result is definitely exact + //! \hideinitializer Result is definitely exact. I_EXACT = 16, - //! \hideinitializer Result is definitely inexact + //! \hideinitializer Result is definitely inexact. I_INEXACT = 32, - //! \hideinitializer Operation has definitely changed the set + //! \hideinitializer Operation has definitely changed the set. I_CHANGED = 64, - //! \hideinitializer Operation has left the set definitely unchanged + //! \hideinitializer Operation has left the set definitely unchanged. I_UNCHANGED = 128, - //! \hideinitializer Operation is undefined for some combination of values + //! \hideinitializer Operation is undefined for some combination of values. I_SINGULARITIES = 256 };

1 0

[GIT] ppl/ppl(master): Wrong guard fixed.
by Roberto Bagnara 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 637df0294f81d71e4f00d55063be06cf34adf4c4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=637df0294f81… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Feb 25 18:22:24 2012 +0100 Wrong guard fixed. --- demos/ppl_lpsol/ppl_lpsol.c | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/demos/ppl_lpsol/ppl_lpsol.c b/demos/ppl_lpsol/ppl_lpsol.c index 9a72e40..8c62b94 100644 --- a/demos/ppl_lpsol/ppl_lpsol.c +++ b/demos/ppl_lpsol/ppl_lpsol.c @@ -326,7 +326,7 @@ process_options(int argc, char* argv[]) { my_exit(0); break; -#ifdef PPL_LPSOL_SUPPORTS_TIMINGS +#ifdef PPL_LPSOL_SUPPORTS_LIMIT_ON_CPU_TIME case 'C': l = strtol(optarg, &endptr, 10);

1 0

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

25 Feb '12

Module: ppl/ppl Branch: master Commit: e87943772e7901e7b5c0e550d89742423b7fe225 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e87943772e79… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Feb 25 18:16:44 2012 +0100 Updated. --- CREDITS | 28 +++++++++++++++------------- NEWS | 2 +- README | 17 ++++++++++++----- ppl.lsm.in | 36 +++++++++++++++++++++++++----------- 4 files changed, 53 insertions(+), 30 deletions(-) diff --git a/CREDITS b/CREDITS index a34375e..99aa556 100644 --- a/CREDITS +++ b/CREDITS @@ -88,9 +88,9 @@ Past Contributors: algorithms for rational grids and products of grids and polyhedra. - Giordano Fracasso (University of Parma) wrote the initial version - of the support for native and checked integer - coefficients. + Giordano Fracasso (former student of the University of Parma) wrote + the initial version of the support for native + and checked integer coefficients. Francois Galea [5] (University of Versailles) worked at the implementation of the Parametric Integer @@ -100,11 +100,12 @@ Past Contributors: helped a little to improve the documentation for bounded differences. - Elena Mazzi (University of Parma) worked on our implementation - of bounded differences and octagons. She also - participated in the theoretical and practical - work concerning widening operators for weakly - relational domains. + Elena Mazzi (former student of the University of Parma) worked + on our implementation of bounded differences + and octagons. She also participated in the + theoretical and practical work concerning + widening operators for weakly relational + domains. David Merchat (formerly at the University of Parma) helped us with the generation of the library's documentation @@ -129,11 +130,12 @@ Past Contributors: Angela Stazzone (former student of the University of Parma) worked on the library's documentation. - Fabio Trabucchi (University of Parma) worked on a development - branch where he added serializers for all the - objects of the PPL. Support for serialization - based on Fabio's work will be available in a - future release of the library. + Fabio Trabucchi (former student of the University of Parma) worked + on a development branch where he added + serializers for all the objects of the PPL. + Support for serialization based on Fabio's + work will be available in a future release of + the library. Claudio Trento (former student of the University of Pisa) did a small amount of work on an experimental OCaml diff --git a/NEWS b/NEWS index 5807807..7de2386 100644 --- a/NEWS +++ b/NEWS @@ -10,7 +10,7 @@ Parma Polyhedra Library NEWS -- history of user-visible changes -------------------------------------------------------------------------- -NEWS for version 0.12 (release date to be decided) +NEWS for version 0.12 (released on February 27, 2012) -------------------------------------------------------------------------- New and Changed Features diff --git a/README b/README index 785214b..079e65a 100644 --- a/README +++ b/README @@ -17,17 +17,24 @@ To be more precise, the Parma Polyhedra Library (PPL) can handle: by an equality or a (strict or non-strict) inequality with rational coefficients; - + convex polyhedra defined by systems of bounded differences with - a wide choice of integer, rational or floating point coefficients; + + some special classes of polyhedra shapes that offer interesting + complexity/precision tradeoffs: boxes, bounded difference shapes + and octagonal shapes defined over a wide choice of integer, + rational or floating point coefficients; - + all grids (or, equivalently, lattices); a grid is defined by a set + + all grids (or, equivalently, lattices): a grid is defined by a set of congruence relations with rational coefficients and consists of the set of all points that satisfy these relations; - + finite powersets of the above; + + finite powersets and products of the above; + linear programming problems, solved with an implementation of the - primal simplex algorithm using exact arithmetic. + primal simplex algorithm using exact arithmetic; + + + parametric integer programming problems; + + + termination analysis problems, via the automatic synthesis of + linear ranking functions. The Parma Polyhedra Library is: diff --git a/ppl.lsm.in b/ppl.lsm.in index 6f20d00..0e01b58 100644 --- a/ppl.lsm.in +++ b/ppl.lsm.in @@ -4,24 +4,38 @@ Version: @VERSION@ Entered-date: @ISODATE@ Description: The Parma Polyhedra Library (PPL) is a C++ library for the manipulation of numerical abstractions. -Keywords: C++ library convex polyhedra -Author: Roberto Bagnara (bagnara(a)cs.unipr.it) - Patricia M. Hill (hill(a)comp.leeds.ac.uk) - Enea Zaffanella (zaffanella(a)cs.unipr.it) - Abramo Bagnara (Opera Unica) - Andrea Cimino (University of Parma) - Giordano Fracasso (University of Parma) - Elena Mazzi (University of Parma) - Matthew Mundell (University of Leeds) - Barbara Quartieri (University of Parma) +Keywords: C++ library convex polyhedra verification +Author: Roberto Bagnara (BUGSENG srl and University of Parma) + Patricia M. Hill (BUGSENG srl and University of Leeds) + Enea Zaffanella (BUGSENG srl and University of Parma) + Abramo Bagnara (BUGSENG srl) Elisa Ricci (former student of the University of Parma) + Marco Poletti (student of the University of Bologna) + Alessandro Zaccagnini (University of Parma) + Roberto Amadini (former student of the University of Parma) + Irene Bacchi (former student of the University of Parma) + Fabio Biselli (student of the University of Parma) + Fabio Bossi (former student of the University of Parma) + Danilo Bonardi (former student of the University of Parma) Sara Bonini (former student of the University of Parma) + Andrea Cimino (former student of the University of Parma) + Katy Dobson (former student of the University of Leeds) + Giordano Fracasso (former student of the University of Parma) + Francois Galea (University of Versailles) + Maximiliano Marchesi (former student of the University of Parma) + Elena Mazzi (former student of the University of Parma) + David Merchat (formerly at the University of Parma) + Matthew Mundell (formerly at the University of Leeds) Andrea Pescetti (former student of the University of Parma) + Barbara Quartieri (former student of the University of Parma) + Enric Rodriguez Carbonell (Technical University of Catalonia) Angela Stazzone (former student of the University of Parma) + Fabio Trabucchi (University of Parma) + Claudio Trento (former student of the University of Pisa) Tatiana Zolo (former student of the University of Parma) Maintained-by: ppl-devel(a)cs.unipr.it (PPL developers) Primary-site: metlab.unc.edu /pub/linux/libs - 5850k ppl-@VERSION@.tar.gz + 16788k ppl-@VERSION@.tar.gz 800 ppl.lsm Alternate-site: Original-site: http://bugseng.com/products/ppl/

1 0

[GIT] ppl/ppl(master): Hide enum initializers from docs.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: bbc3deda4d9ee21af4609396779e4ab1bde16d5b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bbc3deda4d9e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 18:09:09 2012 +0100 Hide enum initializers from docs. Remove I_Result enumeration form user manual. --- src/intervals.defs.hh | 45 ++++++++++++++++++++++++++++----------------- 1 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/intervals.defs.hh b/src/intervals.defs.hh index a4f3754..92b7693 100644 --- a/src/intervals.defs.hh +++ b/src/intervals.defs.hh @@ -31,46 +31,55 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +//! The result of an operation on intervals. +/*! \ingroup PPL_CXX_interface */ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) enum I_Result { - //! The resulting set may be empty + //! \hideinitializer Result may be empty I_EMPTY = 1U, - //! The resulting set may have only one value + //! \hideinitializer Result may have only one value I_SINGLETON = 2U, - //! The resulting set may have more than one value and to be not the domain universe + /*! \brief \hideinitializer + Result may have more than one value, but it is not the domain universe + */ I_SOME = 4U, - //! The resulting set may be the domain universe + //! \hideinitializer Result may be the domain universe I_UNIVERSE = 8U, - //! The resulting set is not empty + //! \hideinitializer Result is not empty I_NOT_EMPTY = I_SINGLETON | I_SOME | I_UNIVERSE, - //! The resulting set may be empty or not empty + //! \hideinitializer Result may be empty or not empty I_ANY = I_EMPTY | I_NOT_EMPTY, - //! The resulting set may be empty or not empty + //! \hideinitializer Result may be empty or not empty I_NOT_UNIVERSE = I_EMPTY | I_SINGLETON | I_SOME, - //! The resulting set can'be empty or the domain universe + //! \hideinitializer Result is neither empty nor the domain universe I_NOT_DEGENERATE = I_SINGLETON | I_SOME, - //! The resulting set is definitely exact + //! \hideinitializer Result is definitely exact I_EXACT = 16, - //! The resulting set is definitely inexact + //! \hideinitializer Result is definitely inexact I_INEXACT = 32, - //! The operation has definitely changed the set + //! \hideinitializer Operation has definitely changed the set I_CHANGED = 64, - //! The operation has left the set definitely unchanged + //! \hideinitializer Operation has left the set definitely unchanged I_UNCHANGED = 128, - //! The operation is undefined for some combination of values + //! \hideinitializer Operation is undefined for some combination of values I_SINGULARITIES = 256 }; -inline I_Result operator|(I_Result a, I_Result b) { +inline I_Result +operator|(I_Result a, I_Result b) { return static_cast<I_Result>(static_cast<unsigned>(a) | static_cast<unsigned>(b)); } -inline I_Result operator&(I_Result a, I_Result b) { +inline I_Result +operator&(I_Result a, I_Result b) { return static_cast<I_Result>(static_cast<unsigned>(a) & static_cast<unsigned>(b)); } -inline I_Result operator-(I_Result a, I_Result b) { +inline I_Result +operator-(I_Result a, I_Result b) { return static_cast<I_Result>(static_cast<unsigned>(a) & ~static_cast<unsigned>(b)); } @@ -352,7 +361,9 @@ struct I_Constraint_Rel { template <typename T, typename Val_Or_Ref_Criteria = Use_Slow_Copy, bool extended = false> -class I_Constraint : public I_Constraint_Common<I_Constraint<T, Val_Or_Ref_Criteria, extended> > { +class I_Constraint + : public I_Constraint_Common<I_Constraint<T, Val_Or_Ref_Criteria, + extended> > { typedef Val_Or_Ref<T, Val_Or_Ref_Criteria> Val_Ref; typedef typename Val_Ref::Arg_Type Arg_Type; typedef typename Val_Ref::Return_Type Return_Type;

1 0

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

25 Feb '12

Module: ppl/ppl Branch: master Commit: fcbdfeab44225f1b03243f11bd32e999828c0b4c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fcbdfeab4422… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Feb 25 17:06:00 2012 +0100 Updated. --- CREDITS | 60 +++++++++++++++++++++++++++--------------------------------- 1 files changed, 27 insertions(+), 33 deletions(-) diff --git a/CREDITS b/CREDITS index 7c799d7..a34375e 100644 --- a/CREDITS +++ b/CREDITS @@ -10,9 +10,10 @@ people: Core Development Team: ---------------------- - Roberto Bagnara [1] (University of Parma) - Patricia M. Hill [2] (University of Leeds) - Enea Zaffanella [3] (University of Parma) + Roberto Bagnara [1] (BUGSENG srl and University of Parma) + Patricia M. Hill [2] (BUGSENG srl and University of Leeds) + Enea Zaffanella [3] (BUGSENG srl and University of Parma) + Abramo Bagnara (BUGSENG srl) Former Members of the Core Development Team: @@ -28,21 +29,6 @@ Former Members of the Core Development Team: Current Contributors: --------------------- - Abramo Bagnara (Opera Unica) rewrote and generalized the - support for checked coefficients. He also - wrote the support for extended numbers and is - currently writing a new implementation of - intervals. He also helps on several other - design and implementation issues. - - Fabio Bossi (student of the University of Parma) - is working on the PPL support for the approximation - of floating point computations. - - Francois Galea [*] (University of Versailles) is working - at the implementation of the Parametric Integer - Programming solver. - 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 @@ -51,10 +37,7 @@ Current Contributors: on improving the PPL's memory footprint and on other improvements to the library. - Enric Rodriguez Carbonell [4] (Technical University of Catalonia) is - working on the implementation of polynomial spaces. - - Alessandro Zaccagnini [5] (University of Parma) has helped with + Alessandro Zaccagnini [4] (University of Parma) has helped with the efficient implementation of GCD and LCM for checked numbers. He is now working on the definitions of interval arithmetic operations. @@ -65,7 +48,7 @@ Current Contributors: Past Contributors: ------------------ - Roberto Amadini (student of the University of Parma) + Roberto Amadini (former student of the University of Parma) did some work on the PPL support for the approximation of floating point computations. @@ -79,6 +62,10 @@ Past Contributors: did some work on the PPL support for the approximation of floating point computations. + Fabio Bossi (former student of the University of Parma) + worked on the PPL support for the approximation + of floating point computations. + Danilo Bonardi (former student of the University of Parma) worked on a development branch where he experimented with the use of metaprogramming techniques @@ -96,7 +83,7 @@ Past Contributors: solver, and also most of the Java and OCaml interfaces. - Katy Dobson [6] (former student of the University of Leeds) + Katy Dobson (former student of the University of Leeds) worked on the formalization and definition of algorithms for rational grids and products of grids and polyhedra. @@ -105,6 +92,10 @@ Past Contributors: of the support for native and checked integer coefficients. + Francois Galea [5] (University of Versailles) worked + at the implementation of the Parametric Integer + Programming solver. + Maximiliano Marchesi (former student of the University of Parma) helped a little to improve the documentation for bounded differences. @@ -119,18 +110,22 @@ Past Contributors: with the generation of the library's documentation using Doxygen. - Matthew Mundell [7] (formerly at the University of Leeds) worked + Matthew Mundell [6] (formerly at the University of Leeds) worked on the implementation of rational grids. He has also helped on other implementation issues. - Andrea Pescetti (University of Parma) was one of the four students - with which the PPL project started. Later, he - helped a little with the library's documentation. + Andrea Pescetti (former student of the University of Parma) was one + of the four students with which the PPL + project started. Later, he helped a little + with the library's documentation. Barbara Quartieri (former student of the University of Parma) worked on our implementation of bounded differences and octagons. + Enric Rodriguez Carbonell [7] (Technical University of Catalonia) + worked at the implementation of polynomial spaces. + Angela Stazzone (former student of the University of Parma) worked on the library's documentation. @@ -369,11 +364,10 @@ projects and organizations: [1] http://www.cs.unipr.it/~bagnara/ [2] http://www.comp.leeds.ac.uk/hill/ [3] http://www.cs.unipr.it/~zaffanella/ - [*] http://www.prism.uvsq.fr/~fgalea/ - [4] http://www.lsi.upc.edu/~erodri/ - [5] http://www.math.unipr.it/~zaccagni/ - [6] http://www.comp.leeds.ac.uk/katyd/ - [7] http://www.mundell.ukfsn.org/ + [4] http://www.math.unipr.it/~zaccagni/ + [5] http://www.prism.uvsq.fr/~fgalea/ + [6] http://www.mundell.ukfsn.org/ + [7] http://www.lsi.upc.edu/~erodri/ [8] http://www.irisa.fr/lande/fbesson/fbesson.html [9] http://www.cs.ucsb.edu/~bultan/ [10] http://www.clip.dia.fi.upm.es/~boris/

1 0

[GIT] ppl/ppl(master): For code clarity purposes, better distinguish signed /unsigned operations.
by Enea Zaffanella 25 Feb '12

25 Feb '12

Module: ppl/ppl Branch: master Commit: 5ac71293891dbc160c066a80738a4bd27b93a450 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5ac71293891d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Feb 25 16:12:58 2012 +0100 For code clarity purposes, better distinguish signed/unsigned operations. Detected by ECLAIR service utypflag. --- src/Bit_Row.cc | 6 ++++-- src/CO_Tree.cc | 9 +++++---- src/checked_float.inlines.hh | 19 +++++++++++-------- 3 files changed, 20 insertions(+), 14 deletions(-) diff --git a/src/Bit_Row.cc b/src/Bit_Row.cc index c303fae..d250197 100644 --- a/src/Bit_Row.cc +++ b/src/Bit_Row.cc @@ -55,7 +55,8 @@ PPL::Bit_Row::next(unsigned long position) const { // return (r == C_Integer<unsigned long>::max) ? -1 : r; // </CODE> - mp_size_t li = static_cast<mp_size_t>(position / PPL_BITS_PER_GMP_LIMB); + const unsigned long uli = position / PPL_BITS_PER_GMP_LIMB; + mp_size_t li = static_cast<mp_size_t>(uli); const mp_size_t vec_size = vec->_mp_size; PPL_ASSERT(vec_size >= 0); if (li >= vec_size) @@ -104,7 +105,8 @@ PPL::Bit_Row::prev(unsigned long position) const { const mp_size_t vec_size = vec->_mp_size; PPL_ASSERT(vec_size > 0); - mp_size_t li = static_cast<mp_size_t>(position / PPL_BITS_PER_GMP_LIMB); + const unsigned long uli = position / PPL_BITS_PER_GMP_LIMB; + mp_size_t li = static_cast<mp_size_t>(uli); mp_limb_t limb; mp_srcptr p = vec->_mp_d; diff --git a/src/CO_Tree.cc b/src/CO_Tree.cc index 4a70f04..0b388a1 100644 --- a/src/CO_Tree.cc +++ b/src/CO_Tree.cc @@ -893,8 +893,9 @@ PPL::CO_Tree --subtree_size; } - PPL_ASSERT(first_unused_index >= indexes); - return static_cast<dimension_type>(first_unused_index - indexes); + ptrdiff_t distance = first_unused_index - indexes; + PPL_ASSERT(distance >= 0); + return static_cast<dimension_type>(distance); } void @@ -907,8 +908,8 @@ PPL::CO_Tree::redistribute_elements_in_subtree( bool add_element) { // This is static and with static allocation, to improve performance. - // sizeof_to_bits(sizeof(dimension_type)) is the maximum k such that 2^k-1 is a - // dimension_type, so it is the maximum tree height. + // sizeof_to_bits(sizeof(dimension_type)) is the maximum k such that + // 2^k-1 is a dimension_type, so it is the maximum tree height. // For each node level, the stack may contain up to two element (one for the // subtree rooted at the right son of a node of that level, and one for the // node itself). An additional element can be at the top of the tree. diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 79166c0..08b7251 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -885,14 +885,17 @@ assign_float_mpq(T& to, const mpq_class& from, Rounding_Dir dir) { - exponent); mpz_t mantissa; mpz_init(mantissa); - long shift = static_cast<long>(needed_bits) - exponent; - if (shift > 0) { - mpz_mul_2exp(mantissa, numer_z, static_cast<unsigned long>(shift)); - numer_z = mantissa; - } - else if (shift < 0) { - mpz_mul_2exp(mantissa, denom_z, static_cast<unsigned long>(-shift)); - denom_z = mantissa; + { + long shift = static_cast<long>(needed_bits) - exponent; + if (shift > 0) { + mpz_mul_2exp(mantissa, numer_z, static_cast<unsigned long>(shift)); + numer_z = mantissa; + } + else if (shift < 0) { + shift = -shift; + mpz_mul_2exp(mantissa, denom_z, static_cast<unsigned long>(shift)); + denom_z = mantissa; + } } mpz_t r; mpz_init(r);

1 0