Sven Verdoolaege wrote:
On Fri, Feb 06, 2004 at 07:48:42PM +0100, Roberto Bagnara wrote:
I am not sure I understand what you mean. The current version of the PPL is also based on GMP (even though we have a development branch to implement support for native integers and other kinds of coefficients, see http://www.cs.unipr.it/pipermail/ppl-devel/2004-February/004115.html).
Interesting. Have you performed any run time comparison ? A GMP-PolyLib is a lot slower than an integer-Polylib.
Not yet.
A quick glance at the documentation suggests that PPL only supports what Omega would call "set variables". Are there any plans for supporting parameters and/or existential variables ?
What do you mean by "existential variables"?
The usual. Existentially quantified variables. E.g., { x : \exists a : 4 a + 1 <= x <= 4a + 2 }
The variable `a' is bound to be an integer, right? Am I correct if I say that you are interested in systems of what, IIRC, Masdupuy calls "trapezoid congruences", i.e., things of the form
a1*x1 + ... an*xn in [l, u] (mod k),
which should mean
mod(a1*x1 + ... an*xn, k) belongs to the interval [l, u],
where a1, ..., an, l, u are rational numbers and k is a natural? You set above should then correspond to
x \in [1, 2] (mod 4).
These are in our list of the things we want to support.
@PhDThesis{Masdupuy93th, Author = "F. Masdupuy", Title = "Array Indices Relational Semantic Analysis Using Rational Cosets and Trapezoids", Type = "{Th`ese d'informatique}", School = "'Ecole Polytechnique", Address = "Palaiseau, France", Month = dec, Year = 1993 }
I think we will support parameterized polyhedra in the future. But this is something that will not happen tomorrow.
I'll see if I can get a student on it next year. I'm not holding my breath, though. Apparently, the word "polytope" scares people off.
Tell them that, for whoever does a nice job on the subject and is willing to give a seminar, there is a free trip to Parma to be won :-) All the best,
Roberto