- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(ppl-0_11-branch): Version number bumped.
by Roberto Bagnara 03 Feb '11

03 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: e95046e63a0078b8cb39f6188af76bdc5812f402 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e95046e63a00… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Feb 3 07:52:21 2011 +0100 Version number bumped. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index cbc332a..cce80a9 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.11.1pre5], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [0.11.1pre6], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61)

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Do not use the deprecated function mpz_div_2exp.
by Roberto Bagnara 03 Feb '11

03 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: d4220bc1c8e9cc00d2e3ef3e4e675a0dc7fff51a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d4220bc1c8e9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Feb 3 07:51:31 2011 +0100 Do not use the deprecated function mpz_div_2exp. Use mpz_tdiv_q_2exp instead. --- src/checked_float.inlines.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 8f1fa76..f6077c1 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -887,7 +887,7 @@ assign_float_mpq(T& to, const mpq_class& from, Rounding_Dir dir) mpz_clear(r); if (bits == needed_bits + 1) { inexact = (inexact || mpz_odd_p(mantissa)); - mpz_div_2exp(mantissa, mantissa, 1); + mpz_tdiv_q_2exp(mantissa, mantissa, 1); } else --exponent;

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Specialize C_Integer<T> for plain char.
by Roberto Bagnara 03 Feb '11

03 Feb '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: 4771be9cdede70e06083ed22be72624063548c80 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4771be9cdede… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Feb 3 07:48:15 2011 +0100 Specialize C_Integer<T> for plain char. --- src/C_Integer.hh | 21 +++++++++++++++++++++ 1 files changed, 21 insertions(+), 0 deletions(-) diff --git a/src/C_Integer.hh b/src/C_Integer.hh index 8557a6b..c08156a 100644 --- a/src/C_Integer.hh +++ b/src/C_Integer.hh @@ -62,6 +62,27 @@ template <typename T> struct C_Integer : public False { }; template <> +struct C_Integer<char> : public True { + enum anonymous_enum { +#if PPL_CXX_PLAIN_CHAR_IS_SIGNED + is_signed = true +#else + is_signed = false +#endif + }; + typedef void smaller_type; + typedef void smaller_signed_type; + typedef void smaller_unsigned_type; +#if PPL_CXX_PLAIN_CHAR_IS_SIGNED + typedef unsigned char other_type; +#else + typedef signed char other_type; +#endif + static const char min = CHAR_MIN; + static const char max = CHAR_MAX; +}; + +template <> struct C_Integer<signed char> : public True { enum anonymous_enum { is_signed = true }; typedef void smaller_type;

1 0

[GIT] ppl/ppl(master): Do not use the deprecated function mpz_div_2exp.
by Fabio Bossi 02 Feb '11

02 Feb '11

Module: ppl/ppl Branch: master Commit: f14d56cb93cb6fffb3d68511b59237668f8de92c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f14d56cb93cb… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Feb 2 16:48:49 2011 +0100 Do not use the deprecated function mpz_div_2exp. Use mpz_tdiv_q_2exp instead. --- src/checked_float.inlines.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 8f1fa76..f6077c1 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -887,7 +887,7 @@ assign_float_mpq(T& to, const mpq_class& from, Rounding_Dir dir) mpz_clear(r); if (bits == needed_bits + 1) { inexact = (inexact || mpz_odd_p(mantissa)); - mpz_div_2exp(mantissa, mantissa, 1); + mpz_tdiv_q_2exp(mantissa, mantissa, 1); } else --exponent;

1 0

Re: [PPL-devel] Fwd: ppl_pips problems
by Albert Cohen 31 Jan '11

31 Jan '11

By the way, let me encourage you all to participate to the upcoming IMPACT and ACCA workshops associated with CGO: http://www.cgo.org/cgo2011/ http://www.cgo.org/cgo2011/workshops.php These are informal events in a nice environment, a good occasion to meet and present work in progress. Albert > -------- Original Message -------- > Subject: [PPL-devel] ppl_pips problems > Date: Mon, 31 Jan 2011 16:58:35 +0100 > From: Sven Verdoolaege <skimo-ppl(a)kotnet.org> > Reply-To: Sven Verdoolaege <skimo(a)kotnet.org> > To: ppl-devel(a)cs.unipr.it > CC: Albert Cohen <Albert.Cohen(a)inria.fr> > > I'm in the process of writing a paper about my improvements > to pip and I wanted to compare to the PPL implementation too. > (At least, I'd like to compare the execution times. I probably > won't be diving into source to find out which optimizations in > isl have also been implemented in PPL.) > > However, ppl_pips seems to produce incorrect results on some > test cases. I'm using version products_root-2871-gc02e988. > (The git repo does not appear to have any tags for the releases.) > > For bart-big.pip, ppl_pips returns > > Parameter N = (3*L + 64) div 256 > if N >= 1 and -3*L + 256*N >= 64 then > {-K + M ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - 2 ; M - 2 > ; M - N} > else > _|_ > > Which essentially means that it only found a solutions for > L = 64, while there should be a solution for every value of L > in the context. > > For bouleti.pip, ppl_pips returns > > _|_ > > That is, it claims that there is no solution, while isl_pip > and PipLib's exampleMP do find solutions. Here is one of them: > [p0, p1, p2, p3, p4, p5] -> { [1, 11, 4, 1, 2, 1, 2, 2, 1] : p3 = 1 and > p4 = 11 and p5 = 2 and p0 = 0 and p1 = 0 and p2 = 2 } > > The following iscc session demonstrates that this is indeed > a solution > > Q := > 24 17 > 1 0 0 0 -1 0 0 0 0 0 1 -1 1 0 0 0 0 > 1 0 0 0 0 0 0 -1 0 0 1 -1 1 0 0 0 0 > 1 0 0 0 0 -1 0 0 0 0 1 -1 1 0 0 0 0 > 1 0 0 0 0 0 0 0 -1 0 1 -1 1 0 0 0 0 > 1 0 0 0 0 0 1 0 0 0 -1 1 0 -1 0 0 0 > 1 -1 0 0 0 0 0 0 0 0 1 -1 0 1 0 0 0 > 1 0 -1 0 0 0 0 0 0 0 1 -1 0 0 1 0 0 > 1 0 0 1 0 0 0 0 0 0 -1 1 0 0 0 -1 -1 > 1 0 0 0 1 0 0 0 0 0 -1 0 0 0 0 0 -1 > 1 0 0 0 1 1 -1 0 0 0 -1 0 0 0 0 0 0 > 1 0 0 -1 0 0 0 2 0 0 -1 0 0 0 0 0 0 > 1 0 0 0 0 0 0 1 0 0 -1 0 0 0 0 0 -1 > 1 0 0 0 0 0 0 1 1 -1 -1 0 0 0 0 0 0 > 1 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 -1 > 1 0 0 0 0 0 0 0 1 0 -1 0 0 0 0 0 -1 > 1 0 0 0 0 0 1 0 0 0 -1 0 0 0 0 0 -1 > 1 0 0 0 0 0 0 0 0 1 -1 0 0 0 0 0 -1 > 1 1 1 0 0 0 0 0 0 0 -2 2 0 -1 -1 0 0 > 1 0 0 0 2 0 0 0 0 0 -2 1 0 0 0 -1 0 > 1 0 -1 0 0 0 0 0 4 3 -6 0 0 0 0 0 0 > 1 0 0 0 0 4 3 0 0 0 -7 1 0 0 -1 0 0 > 1 1 1 1 0 0 0 -2 -4 -4 7 0 0 0 0 0 0 > 1 0 0 0 -2 -4 -4 0 0 0 10 -3 0 1 1 1 0 > 1 -1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 > ; > {[1, 11, 4, 1, 2, 1, 2, 2, 1, 0, 0, 2, 1, 11, 2]} <= Q; > True > C := > 1 8 > 1 0 -1 1 0 0 0 -1 > ; > {[0, 0, 2, 1, 11, 2]} <= C; > True > > Also, I wonder if you have a parser for the output format of > ppl_pips so that I could compare the results produced by > ppl_pips with those produced by isl_pip. > > skimo >

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Added specializations for plain char.
by Roberto Bagnara 30 Jan '11

30 Jan '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: cc29a204ee6bb9f607360de08786b5c4b65f259b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cc29a204ee6b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Jan 30 22:11:01 2011 +0100 Added specializations for plain char. --- src/checked_int.inlines.hh | 179 ++++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 179 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=cc29a204…

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Version number bumped.
by Roberto Bagnara 30 Jan '11

30 Jan '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: 5faf6eadd8ab521078afa63329c5ba542c502eed URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5faf6eadd8ab… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Jan 30 22:10:45 2011 +0100 Version number bumped. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index b8a32d2..cbc332a 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.11.1pre4], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [0.11.1pre5], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61)

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Copy-and-paste mistake fixed.
by Roberto Bagnara 30 Jan '11

30 Jan '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: 4c6e21f5fefa7333d31d79c7e8ee35352eb9d8b7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4c6e21f5fefa… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Jan 30 22:08:31 2011 +0100 Copy-and-paste mistake fixed. --- m4/ac_cxx_plain_char_is_signed.m4 | 2 -- 1 files changed, 0 insertions(+), 2 deletions(-) diff --git a/m4/ac_cxx_plain_char_is_signed.m4 b/m4/ac_cxx_plain_char_is_signed.m4 index bc0b086..51c2667 100644 --- a/m4/ac_cxx_plain_char_is_signed.m4 +++ b/m4/ac_cxx_plain_char_is_signed.m4 @@ -36,8 +36,6 @@ int foo[std::numeric_limits<char>::is_signed ? 1 : -1]; AC_MSG_RESULT(yes) ac_cxx_plain_char_is_signed=yes, AC_MSG_RESULT(no) - ac_cxx_plain_char_is_signed=no, - AC_MSG_RESULT(no) ac_cxx_plain_char_is_signed=no) if test x"$ac_cxx_plain_char_is_signed" = xyes

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Detect whether the plain char type is signed.
by Roberto Bagnara 30 Jan '11

30 Jan '11

Module: ppl/ppl Branch: ppl-0_11-branch Commit: 1af30643b88db3b1afafd25accaef1d1e479140d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1af30643b88d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Jan 30 20:06:05 2011 +0100 Detect whether the plain char type is signed. --- configure.ac | 3 ++ m4/Makefile.am | 1 + m4/ac_cxx_plain_char_is_signed.m4 | 55 +++++++++++++++++++++++++++++++++++++ 3 files changed, 59 insertions(+), 0 deletions(-) diff --git a/configure.ac b/configure.ac index 46c51ca..b8a32d2 100644 --- a/configure.ac +++ b/configure.ac @@ -666,6 +666,9 @@ AC_SEARCH_LIBS([sqrt], [m]) # Check for the possibility to control the FPU. AC_CHECK_FPU_CONTROL +# Check whether for the C++ compiler the plain char type is signed. +AC_CXX_PLAIN_CHAR_IS_SIGNED + # Check whether the C++ compiler provides proper long doubles. AC_CXX_PROVIDES_PROPER_LONG_DOUBLE diff --git a/m4/Makefile.am b/m4/Makefile.am index a69425f..313d28a 100644 --- a/m4/Makefile.am +++ b/m4/Makefile.am @@ -46,6 +46,7 @@ ac_cxx_ieee_inexact_flag.m4 \ ac_cxx_limit_memory.m4 \ ac_cxx_long_double_binary_format.m4 \ ac_cxx_long_double_exact_output.m4 \ +ac_cxx_plain_char_is_signed.m4 \ ac_cxx_proper_long_double.m4 \ ac_cxx_remainder_bug.m4 \ ac_prog_jar.m4 \ diff --git a/m4/ac_cxx_plain_char_is_signed.m4 b/m4/ac_cxx_plain_char_is_signed.m4 new file mode 100644 index 0000000..bc0b086 --- /dev/null +++ b/m4/ac_cxx_plain_char_is_signed.m4 @@ -0,0 +1,55 @@ +dnl A function to check whether the plain char type is signed. +dnl Copyright (C) 2001-2010 Roberto Bagnara <bagnara(a)cs.unipr.it> +dnl Copyright (C) 2010-2011 BUGSENG srl (http://bugseng.com) +dnl +dnl This file is part of the Parma Polyhedra Library (PPL). +dnl +dnl The PPL is free software; you can redistribute it and/or modify it +dnl under the terms of the GNU General Public License as published by the +dnl Free Software Foundation; either version 3 of the License, or (at your +dnl option) any later version. +dnl +dnl The PPL is distributed in the hope that it will be useful, but WITHOUT +dnl ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +dnl FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +dnl for more details. +dnl +dnl You should have received a copy of the GNU General Public License +dnl along with this program; if not, write to the Free Software Foundation, +dnl Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. +dnl +dnl For the most up-to-date information see the Parma Polyhedra Library +dnl site: http://www.cs.unipr.it/ppl/ . + +AC_DEFUN([AC_CXX_PLAIN_CHAR_IS_SIGNED], +[ +ac_save_CPPFLAGS="$CPPFLAGS" +ac_save_LIBS="$LIBS" +AC_LANG_PUSH(C++) + +AC_MSG_CHECKING([whether the plain char type is signed]) +AC_COMPILE_IFELSE([AC_LANG_SOURCE([[ +#include <limits> + +int foo[std::numeric_limits<char>::is_signed ? 1 : -1]; +]])], + AC_MSG_RESULT(yes) + ac_cxx_plain_char_is_signed=yes, + AC_MSG_RESULT(no) + ac_cxx_plain_char_is_signed=no, + AC_MSG_RESULT(no) + ac_cxx_plain_char_is_signed=no) + +if test x"$ac_cxx_plain_char_is_signed" = xyes +then + value=1 +else + value=0 +fi +AC_DEFINE_UNQUOTED(PPL_CXX_PLAIN_CHAR_IS_SIGNED, $value, + [Not zero if the the plain char type is signed.]) + +AC_LANG_POP(C++) +CPPFLAGS="$ac_save_CPPFLAGS" +LIBS="$ac_save_LIBS" +])

1 0

[GIT] ppl/ppl(master): AC_PROG_OCAML only sets OCAMLOPT if OCAMLC is different from "no".
by Roberto Bagnara 29 Jan '11

29 Jan '11

Module: ppl/ppl Branch: master Commit: c02e988b645f656169f037794797bcbb45f57f2e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c02e988b645f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Jan 29 19:45:52 2011 +0100 AC_PROG_OCAML only sets OCAMLOPT if OCAMLC is different from "no". --- configure.ac | 50 +++++++++++++++++++++++++------------------------- 1 files changed, 25 insertions(+), 25 deletions(-) diff --git a/configure.ac b/configure.ac index 0dc74ba..68934ec 100644 --- a/configure.ac +++ b/configure.ac @@ -1018,32 +1018,32 @@ then AC_PROG_OCAML if test x"$OCAMLC" != xno then - # Check for the bytecode version of ML GMP. - AC_MSG_CHECKING([for ML GMP bytecode module gmp.cma]) - if ( test ${mlgmp_dir} = +gmp && test -f ${OCAMLLIB}/gmp/gmp.cma ) \ - || test -f ${mlgmp_dir}/gmp.cma; - then - AC_MSG_RESULT(yes) - ocamlc_gmp="yes" - else - AC_MSG_RESULT(no) - ocamlc_gmp="no" - fi - fi - if test x"$OCAMLOPT" != xno - then - ocamlopt_root=`${OCAMLOPT} -where` - # Check for the native version of ML GMP. - AC_MSG_CHECKING([for ML GMP native module gmp.cmxa]) - if ( test ${mlgmp_dir} = +gmp && test -f ${ocamlopt_root}/gmp/gmp.cmxa ) \ + # Check for the bytecode version of ML GMP. + AC_MSG_CHECKING([for ML GMP bytecode module gmp.cma]) + if ( test ${mlgmp_dir} = +gmp && test -f ${OCAMLLIB}/gmp/gmp.cma ) \ + || test -f ${mlgmp_dir}/gmp.cma; + then + AC_MSG_RESULT(yes) + ocamlc_gmp="yes" + else + AC_MSG_RESULT(no) + ocamlc_gmp="no" + fi + if test x"$OCAMLOPT" != xno + then + ocamlopt_root=`${OCAMLOPT} -where` + # Check for the native version of ML GMP. + AC_MSG_CHECKING([for ML GMP native module gmp.cmxa]) + if ( test ${mlgmp_dir} = +gmp && test -f ${ocamlopt_root}/gmp/gmp.cmxa ) \ || test -f ${mlgmp_dir}/gmp.cmxa; - then - AC_MSG_RESULT(yes) - ocamlopt_gmp="yes" - else - AC_MSG_RESULT(no) - ocamlopt_gmp="no" - fi + then + AC_MSG_RESULT(yes) + ocamlopt_gmp="yes" + else + AC_MSG_RESULT(no) + ocamlopt_gmp="no" + fi + fi fi fi AM_CONDITIONAL(HAVE_OCAMLC, test x$ocamlc_gmp = xyes)

1 0