August 2011 - PPL-devel - BUGSENG Mailman

FW: Fwd: ppl 0.11.2 vs llvm
by Freeh Sophia 26 Aug '11

26 Aug '11

Freeh Sophia Marketing GmbH Emanuelstr. 3, 10317 Berlin Deutschland Telefon: +49 (33) 5310967 Email: freehsophia(a)gmail.com Site: http://flug.airego.de/

1 0

Fwd: Re: Linear constraint solving example with floating point co-efficients
by Roberto Bagnara 24 Aug '11

24 Aug '11

-------- Original Message -------- Subject: Re: [PPL-devel] Linear constraint solving example with floating point co-efficients Date: Wed, 24 Aug 2011 02:55:32 -0400 From: Mahesh Nanjundappa <knmahesh(a)vt.edu> To: Roberto Bagnara <bagnara(a)cs.unipr.it> Hello Dr. Bagnara, Sorry if I bothered you and thanks for getting back to me despite your busy schedule. I've been going through the documentation and the sample examples from past 2 days. My purpose is more than the solving the linear system. But frankly speaking, I've not been to get any simple example compiled with floating point coefficients. I was looking for a pointer to any example which is solved with floating point coefficients. Again, thanks for getting back to me. Regards, Mahesh On Wed, Aug 24, 2011 at 2:34 AM, Roberto Bagnara <bagnara(a)cs.unipr.it <mailto:bagnara@cs.unipr.it>> wrote: On 08/23/11 15:31, Mahesh Nanjundappa wrote: Hi all, Please don't feel annoyed by this request. I did try for looking for examples in the folder I downloaded and in the manual. But couldnt find what I was looking for. I'm looking for a simple example where a linear constraint system with floating point coefficients (variables can also take floating point values) is solved and output is printed to either file or stdout. I don't have strict requirement to number of decimal points it has to be accurately computed. I'm fine with just 2 decimal points. The system can be as simple as this, 1.2*x + 2.3y <= 8.2 2.2*x + 1.4*y <= 7.1 This one example I tried out but with integer coefficients. #include <ppl.hh> #include "ppl_c.h" using namespace Parma_Polyhedra_Library; int main() { Variable x(0); Variable y(1); Constraint_System CS; Linear_Expression LE1 = 1*x + 2*y; Linear_Expression LE2 = 2*x + 1*y; CS.insert(LE1 <= 7); CS.insert(LE2 <= 5); C_Polyhedron P(CS); return 0; } It would be great if someone can help me out with this by providing an example or code for the system I described earlier. Thanks in advance, Mahesh Hi Mahesh. There is really no way you can use the PPL without even looking at its documentation. Good luck, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~__bagnara/ <http://www.cs.unipr.it/~bagnara/> mailto:bagnara@cs.unipr.it <mailto:bagnara@cs.unipr.it>

1 0

Linear constraint solving example with floating point co-efficients
by Mahesh Nanjundappa 24 Aug '11

24 Aug '11

Hi all, Please don't feel annoyed by this request. I did try for looking for examples in the folder I downloaded and in the manual. But couldnt find what I was looking for. I'm looking for a simple example where a linear constraint system with floating point coefficients (variables can also take floating point values) is solved and output is printed to either file or stdout. I don't have strict requirement to number of decimal points it has to be accurately computed. I'm fine with just 2 decimal points. The system can be as simple as this, 1.2*x + 2.3y <= 8.2 2.2*x + 1.4*y <= 7.1 This one example I tried out but with integer coefficients. #include <ppl.hh> #include "ppl_c.h" using namespace Parma_Polyhedra_Library; int main() { Variable x(0); Variable y(1); Constraint_System CS; Linear_Expression LE1 = 1*x + 2*y; Linear_Expression LE2 = 2*x + 1*y; CS.insert(LE1 <= 7); CS.insert(LE2 <= 5); C_Polyhedron P(CS); return 0; } It would be great if someone can help me out with this by providing an example or code for the system I described earlier. Thanks in advance, Mahesh

2 1

[GIT] ppl/ppl(master): Improved portability to Solaris.
by Roberto Bagnara 21 Aug '11

21 Aug '11

Module: ppl/ppl Branch: master Commit: 4006d8772e751993e6e9b099116296614e9508ab URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4006d8772e75… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Aug 21 08:14:36 2011 +0200 Improved portability to Solaris. (Thanks to Dagobert Michelsen and Maciej Blizinski.) --- interfaces/Java/jni/ppl_java_globals.cc | 10 ++++++++++ tests/Box/refinewithconstraints1.cc | 8 ++++++++ 2 files changed, 18 insertions(+), 0 deletions(-) diff --git a/interfaces/Java/jni/ppl_java_globals.cc b/interfaces/Java/jni/ppl_java_globals.cc index 019d02f..57b7fb8 100644 --- a/interfaces/Java/jni/ppl_java_globals.cc +++ b/interfaces/Java/jni/ppl_java_globals.cc @@ -735,7 +735,17 @@ Java_parma_1polyhedra_1library_Parma_1Polyhedra_1Library_version_1beta JNIEXPORT jstring JNICALL Java_parma_1polyhedra_1library_Parma_1Polyhedra_1Library_version (JNIEnv* env, jclass) { +#if defined(__sun) || defined(__sun__) + + // Some versions of Solaris declare a version() function that causes + // the following function call to be ambiguous. + return env->NewStringUTF(Parma_Polyhedra_Library::version()); + +#else // !(defined(__sun) || defined(__sun__)) + return env->NewStringUTF(version()); + +#endif // !(defined(__sun) || defined(__sun__)) } JNIEXPORT jstring JNICALL diff --git a/tests/Box/refinewithconstraints1.cc b/tests/Box/refinewithconstraints1.cc index ac4c91f..b1ba961 100644 --- a/tests/Box/refinewithconstraints1.cc +++ b/tests/Box/refinewithconstraints1.cc @@ -23,6 +23,14 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" +#if defined(__sun) || defined(__sun__) + +// Some versions of Solaris define R1 in /usr/include/ia32/sys/reg.h. +// This conflicts with the use or R1 being made in this proram. +# undef R1 + +#endif // defined(__sun) || defined(__sun__) + namespace { bool

1 0

[GIT] ppl/ppl(master): Item revised.
by Roberto Bagnara 19 Aug '11

19 Aug '11

Module: ppl/ppl Branch: master Commit: af093875852581a53d324323c4dad09206cc71cf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=af0938758525… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Aug 19 12:22:10 2011 +0200 Item revised. --- TODO | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/TODO b/TODO index 0023df5..134fea1 100644 --- a/TODO +++ b/TODO @@ -12,8 +12,8 @@ Enhancements for PPL 0.12 or later versions - Make the library thread-safe. - Modify the Makefile.am's to extend silent mode to our own rules. - Reduce the number of FIXMEs to no more than 20. -- Consider switching to MLGMPIDL for the OCaml interface - (see https://bugzilla.redhat.com/show_bug.cgi?id=491712). +- Base the OCaml interface on Zarith + (http://forge.ocamlcore.org/projects/zarith/) instead of MLGMP. - Improve the OCaml interface by supporting dynamic loading. - Enhance the support for systems not providing support for the IEEE inexact flag.

1 0

A compilation issue on Solaris 10, amd64
by Maciej Bliziński 19 Aug '11

19 Aug '11

Hello, At OpenCSW, we're working on a Solaris port of PPL. Dagobert Michelsen has identified two issues, which are specific to compiling on i386 or amd64. One is that there's a macro called "R1" defined on Solaris, and the second is that an existing version() function (from headers present on Solaris) results in an ambiguity which breaks compilation. Patches are available at [1]. There's one more issue, this time specific to amd64 (i386 compilation completes fine): /opt/csw/gcc4/bin/g++ -DHAVE_CONFIG_H -I. -I../.. -DBOX_INSTANCE=rt_r_oc -I../../src -I../../src -I../../tests -I../../utils -DNDEBUG=1 -I/opt/csw/include -g -O2 -frounding-math -O2 -pipe -m64 -march=opteron -W -Wall -MT max_min1.o -MD -MP -MF .deps/max_min1.Tpo -c -o max_min1.o max_min1.cc interval1.cc: In function 'bool<unnamed>::test01() [with F = float]': interval1.cc:195: instantiated from here interval1.cc:77: error: no matching function for call to 'Parma_Polyhedra_Library::Interval<float, Parma_Polyhedra_Library::Interval_Restriction_None<Parma_Polyhedra_Library::Interval_Info_Bitset<unsigned int, <unnamed>::My_Interval<float>::Floating_Point_Real_Interval_Info_Policy> > >::join_assign(double)' interval1.cc:195: instantiated from here interval1.cc:90: error: no matching function for call to 'Parma_Polyhedra_Library::Interval<float, Parma_Polyhedra_Library::Interval_Restriction_None<Parma_Polyhedra_Library::Interval_Info_Bitset<unsigned int, <unnamed>::My_Interval<float>::Floating_Point_Real_Interval_Info_Policy> > >::is_disjoint_from(double)' interval1.cc:90: error: no matching function for call to 'Parma_Polyhedra_Library::Interval<float, Parma_Polyhedra_Library::Interval_Restriction_None<Parma_Polyhedra_Library::Interval_Info_Bitset<unsigned int, <unnamed>::My_Interval<float>::Floating_Point_Real_Interval_Info_Policy> > >::is_disjoint_from(double)' ../../src/Interval.defs.hh: In constructor 'Parma_Polyhedra_Library::Interval<Boundary, Info>::Interval(const T&) [with T = double, Boundary = float, Info = Parma_Polyhedra_Library::Interval_Restriction_None<Parma_Polyhedra_Library::Interval_Info_Bitset<unsigned int, <unnamed>::My_Interval<float>::Floating_Point_Real_Interval_Info_Policy> >]': interval1.cc:76: instantiated from 'bool<unnamed>::test01() [with F = float]' interval1.cc:195: instantiated from here ../../src/Interval.defs.hh:657: error: no matching function for call to 'Parma_Polyhedra_Library::Interval<float, Parma_Polyhedra_Library::Interval_Restriction_None<Parma_Polyhedra_Library::Interval_Info_Bitset<unsigned int, <unnamed>::My_Interval<float>::Floating_Point_Real_Interval_Info_Policy> > >::assign(const double&)' ../../src/Interval.defs.hh:374: note: candidates are: Parma_Polyhedra_Library::I_Result Parma_Polyhedra_Library::Interval<Boundary, Info>::assign(Parma_Polyhedra_Library::Degenerate_Element) [with Boundary = float, Info = Parma_Polyhedra_Library::Interval_Restriction_None<Parma_Polyhedra_Library::Interval_Info_Bitset<unsigned int, <unnamed>::My_Interval<float>::Floating_Point_Real_Interval_Info_Policy> >] gmake[4]: *** [interval1.o] Error 1 gmake[4]: *** Waiting for unfinished jobs.... mv -f .deps/generalizedaffinepreimage1.Tpo .deps/generalizedaffinepreimage1.Po mv -f .deps/limitedcc76extrapolation1.Tpo .deps/limitedcc76extrapolation1.Po mv -f .deps/max_min1.Tpo .deps/max_min1.Po mv -f .deps/mapspacedims1.Tpo .deps/mapspacedims1.Po gmake[4]: Leaving directory `/home/maciej/src/opencsw/pkg/ppl/trunk/work/solaris9-i386/build-isa-amd64/ppl-0.11.2/tests/Box' The compiler version is: maciej@unstable10x [unstable10x]:~ > /opt/csw/gcc4/bin/g++ --version g++ (GCC) 4.3.3 Copyright (C) 2008 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. Do you have any advice regarding this issue? Maciej [1] https://gar.svn.sourceforge.net/svnroot/gar/csw/mgar/pkg/ppl/trunk/files/

2 2

Sage and PPL
by Volker Braun 19 Aug '11

19 Aug '11

Dear PPL-developers, I'm happy to announce that the Parma Polyhedra Library is now used in Sage-4.7.1 (www.sagemath.org) for polyhedral computations. This includes a Python/Cython interface http://www.sagemath.org/doc/reference/sage/libs/ppl.html on which Sage's polyhedral objects are based (or being transitioned to). Thank you for your hard work and quick response to bug reports! Volker Braun

2 1

[GIT] ppl/w3ppl(master): Added link to Sage.
by Roberto Bagnara 19 Aug '11

19 Aug '11

Module: ppl/w3ppl Branch: master Commit: 79cbc4d4552e6137e368818127e1183e022a3895 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=79cbc4d455… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Aug 19 08:57:30 2011 +0200 Added link to Sage. --- htdocs/Applications/Applications.raw | 9 +++++++++ 1 files changed, 9 insertions(+), 0 deletions(-) diff --git a/htdocs/Applications/Applications.raw b/htdocs/Applications/Applications.raw index 00c429c..67129b0 100644 --- a/htdocs/Applications/Applications.raw +++ b/htdocs/Applications/Applications.raw @@ -10,10 +10,19 @@ Here are the ones we are aware of. <UL> <LI> + The <A HREF="http://www.sagemath.org/">Sage</A> + mathematics software system uses the Parma Polyhedra Library + for polyhedral computations. This includes a + <A HREF="http://www.sagemath.org/doc/reference/sage/libs/ppl.html">Python/Cython interface</A> + on which Sage's polyhedral objects are based. + </LI> +<P> + <LI> The <A HREF="http://spaceex.imag.fr/">SpaceEx</A> tool platform facilitates the implementation of algorithms related to reachability and safety verification. </LI> +<P> <LI> <A HREF="http://gcc.gnu.org/wiki/Graphite">Graphite</A> (Gimple Represented as Polyhedra), a framework for high-level

1 0

[GIT] ppl/w3ppl(master): Added link to SpaceEx.
by Roberto Bagnara 19 Aug '11

19 Aug '11

Module: ppl/w3ppl Branch: master Commit: 7b8df5899045579e4d9e24594a48d66f46452ce0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=7b8df58990… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Aug 19 08:45:14 2011 +0200 Added link to SpaceEx. --- htdocs/Applications/Applications.raw | 5 +++++ 1 files changed, 5 insertions(+), 0 deletions(-) diff --git a/htdocs/Applications/Applications.raw b/htdocs/Applications/Applications.raw index 3980cb9..00c429c 100644 --- a/htdocs/Applications/Applications.raw +++ b/htdocs/Applications/Applications.raw @@ -10,6 +10,11 @@ Here are the ones we are aware of. <UL> <LI> + The <A HREF="http://spaceex.imag.fr/">SpaceEx</A> tool platform + facilitates the implementation of algorithms related to reachability + and safety verification. + </LI> + <LI> <A HREF="http://gcc.gnu.org/wiki/Graphite">Graphite</A> (Gimple Represented as Polyhedra), a framework for high-level loop optimizations that is now part of

1 0

Re: [PPL-devel] Fwd: PPL and FPU rounding mode
by Roberto Bagnara 13 Aug '11

13 Aug '11

On 08/10/11 21:18, Benjamin Hiller wrote: > Dear Prof. Roberto, > > thank you very much for your quick reply. > > Am 10.08.2011 18:38, schrieb Roberto Bagnara: >> If you call restore_pre_PPL_rounding() reset the rounding mode to its >> default (typically round-to-nearest) AND you use a PPL abstraction >> based on floating point numbers without first calling >> set_rounding_for_PPL() then the result computed by PPL will be bogus. >> For example, you may have a non-empty box be mistaken for empty. Of >> course, you may be lucky, but I would not count on that. > > Our data should be such that each polyhedron is far from being > degenerated so I don't think they will become empty due to rounding. > >> Which PPL classes are you using? Many PPL classes are not based on >> floating point numbers. If you only use those, then there is no problem >> at all, whatever rounding mode is in effect. > > So far we are using the classes Variable, Variable_Set, > Generator_System, Linear_Expression, Generator, C_Polytope, > Constraint_System, Constraint. I'm not sure whether this is the > information you need. As far as I know (I did not do the > implementation myself), we scale everything such that we have > integer points/constraint coefficients. If by C_Polytope you mean C_Polyhedron and if the list of classes above is otherwise complete, then your usage of the PPL does not depend on the floating point rounding mode in effect. So you should not worry. > In any case, it is only slightly more inconvenient to turn on the > appropriate rounding mode for PPL before using it so we might better > do that. This might be a wise thing if there is the danger that someone, one day, may use other PPL abstractions based on machine floating-point numbers. > Best regards, > > Benjamin Cheers, Roberto P.S. Please direct all messages concerning the PPL to ppl-devel(a)cs.unipr.it -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 2