- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(bounded_arithmetic): Modified declaration and implementation of bitwise operator on intervals.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 5f6685859cdee87fa71b14c1cc8d8a27b03fce25 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5f6685859cde… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:16:05 2011 +0200 Modified declaration and implementation of bitwise operator on intervals. --- src/Interval.defs.hh | 89 ++- src/Interval.inlines.hh | 1437 +++++++++++++++++------------------------------ 2 files changed, 584 insertions(+), 942 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=5f668585…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Adjusted documentation about bitwise operator.
by Alberto Gioia 27 Aug '11

27 Aug '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 0663324f51238dc36d88909734de6e7063ba4b73 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0663324f5123… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sat Aug 27 17:12:43 2011 +0200 Adjusted documentation about bitwise operator. --- doc/definitions.dox | 92 ++++++++++++++++++++++++-------------------------- 1 files changed, 44 insertions(+), 48 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index ba80d9f..e48e010 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2821,9 +2821,10 @@ The interval bitwise operators are defined as follow: \begin{cases} \bigl[0, \min(b, b')\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[0, \max(b, b')\bigr], - & \text{if $a \geq 0$ and $b' < 0$, - or $b < 0$ and $a' \geq 0$}; \\ + \bigl[0, b\bigr], + & \text{if $a \geq 0$ and $b' < 0$}; \\ + \bigl[0, b'\bigr], + & \text{if $b < 0$ and $a' \geq 0$}; \\ \bigl[a + a', \min(b,b')\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} @@ -2834,9 +2835,10 @@ The interval bitwise operators are defined as follow: \begin{cases} \bigl[\max(a,a'), b + b'\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[\min(a,a'),-1\bigr], - & \text{if $a \geq 0$ and $b' < 0$, - or $b < 0$ and $a' \geq 0$}; \\ + \bigl[a',-1\bigr], + & \text{if $a \geq 0$ and $b' < 0$}; \\ + \bigl[a,-1\bigr], + & \text{if $b < 0$ and $a' \geq 0$}; \\ \bigl[\max(a,a'),-1\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} @@ -2845,25 +2847,31 @@ The interval bitwise operators are defined as follow: \f[ [a,b] \bxorii [a',b'] \approx \begin{cases} - \bigl[0,|b + b'|\bigr], - & \text{if $a \geq 0$ and $a' \geq 0$, - or $b < 0$ and $b' < 0$}; \\ - \bigl[-(|a| + |a'|),-1\bigr], - & \text{if $a \geq 0$ and $b' < 0$, - or $b < 0$ and $a' \geq 0$}. \\ + \bigl[0,b + b'\bigr], + & \text{if $a \geq 0$ and $a' \geq 0$}; \\ + \bigl[(-a + a'),-1\bigr], + & \text{if $a \geq 0$ and $b' < 0$}; \\ + \bigl[(a - a'),-1\bigr], + & \text{if $b < 0$ and $a' \geq 0$}; \\ + \bigl[0, |b + b'|\bigr], + & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} \f] \f[ [a,b] \olessthan ^{\#} [a',b'] \approx \begin{cases} - \bigl[0, \bigl(b \times 2^{b'}\bigr)\bigr], + \bigl[\bigl(a \times 2^{a'}\bigr), + \bigl(b \times 2^{b'}\bigr)\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[0, \bigl(b / 2^{\left|b'\right|}\bigr)\bigr], + \bigl[\bigl(a / 2^{\left|a'\right|}\bigr, + \bigl(b / 2^{\left|b'\right|}\bigr)\bigr], & \text{if $a \geq 0$ and $b' < 0$}; \\ - \bigl[\bigl(a \times 2^{a'}\bigr), 0\bigr], + \bigl[\bigl(a \times 2^{a'}\bigr), + \bigl(b \times 2^{b'}\bigr)\bigr], & \text{if $b < 0$ and $a' \geq 0$}; \\ - \bigl[\bigl(a / 2^{\left|a'\right|}\bigr), 0\bigr], + \bigl[\bigl(a / 2^{\left|a'\right|}\bigr), + \bigl(b / 2^{\left|b'\right|}\bigr)\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} \f] @@ -2871,13 +2879,17 @@ The interval bitwise operators are defined as follow: \f[ [a,b] \ogreaterthan ^{\#} [a',b'] \approx \begin{cases} - \bigl[0, \bigl(b / 2^{b'}\bigr)\bigr], + \bigl[\bigl(a / 2^{a'}\bigr), + \bigl(b / 2^{b'}\bigr)\bigr], & \text{if $a \geq 0$ and $a' \geq 0$}; \\ - \bigl[0, \bigl(b \times 2^{\left|b'\right|}\bigr)\bigr], + \bigl[\bigl(a \times 2^{\left|a'\right|}\bigr), + \bigl(b \times 2^{\left|b'\right|}\bigr)\bigr], & \text{if $a \geq 0$ and $b' < 0$}; \\ - \bigl[\bigl(a / 2^{a'}\bigr), 0\bigr], + \bigl[\bigl(a / 2^{a'}\bigr), + \bigl(b / 2^{b'}\bigr)\bigr], & \text{if $b < 0$ and $a' \geq 0$}; \\ - \bigl[\bigl(a \times 2^{\left|a'\right|}\bigr), 0\bigr], + \bigl[\bigl(a \times 2^{\left|a'\right|}\bigr), + \bigl(b \times 2^{\left|b'\right|}\bigr)\bigr], & \text{if $b < 0$ and $b' < 0$}. \\ \end{cases} @@ -3060,10 +3072,8 @@ both greater than or equal zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ - 0 - \leq \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} @@ -3074,10 +3084,8 @@ have discordand signs, with the first greater than or equal zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ - 0 - \leq \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} @@ -3088,26 +3096,22 @@ have discordand signs, with the first less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ + \left(k + \sum_{v \in \cV}k_{v}v \right) + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} - \leq - \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq - 0 \f] Finally, if \f$i + \sum_{v \in V}i_{v}v\f$ and \f$i' + \sum_{v \in V}i'_{v}v\f$ are both less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ + \left(k + \sum_{v \in \cV}k_{v}v \right) + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} - \leq - \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq - 0 \f] \subsubsection bitwise_right_shift Bitwise RIGHT SHIFT @@ -3125,10 +3129,8 @@ both greater than or equal zero then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ - 0 - \leq \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} @@ -3139,10 +3141,8 @@ have discordand signs, with the first greater than or equal zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ - 0 - \leq \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} @@ -3153,26 +3153,22 @@ have discordand signs, with the first less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ + \left(k + \sum_{v \in \cV}k_{v}v \right) + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} - \leq - \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq - 0 \f] Finally, if \f$i + \sum_{v \in V}i_{v}v\f$ and \f$i' + \sum_{v \in V}i'_{v}v\f$ are both less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \f[ + \left(k + \sum_{v \in \cV}k_{v}v \right) + \approx \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} - \leq - \left(k + \sum_{v \in \cV}k_{v}v \right) - \leq - 0 \f] Where \f$\asifp, \adifp, \amifp,\f$ and \f$\adivifp\f$ are the corresponding

1 0

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