Ber Past wrote:

Looking at the library documentation, it seems it fits exactly my needs. I have only one question (probably stupid, but my knowledge of the library is not yet very good): is there any operator/function that allows to calculate the complement of a Polyhedron?

Thanks for your help.

Dear Ber,

I am not sure I understand what you need, so I will give you two alternatives.

Our library (PPL) provides an operation called "poly-difference" that yields the smallest convex polyhedron containing the set-theoretic difference of its two arguments. Computing the poly-difference of the universe polyhedron and a polyhedron ph gives an upper approximation of the complement. This approximation can of course be extremely coarse unless your application generates only a very restricted class of polyhedra.

Alternatively, the PPL can represent the genuine complement of a given convex polyhedron by a (finite) set of convex polyhedra. Sets of polyhedra are fully supported by version 0.6 of the library, which has just been released. Here is a small program to give you an idea of what you can do:

-------------------------------- %< %< %< -------------------------------- #include <ppl.hh>

using namespace std; using namespace Parma_Polyhedra_Library; using namespace Parma_Polyhedra_Library::IO_Operators;

template <typename PH> Polyhedra_PowerSet<NNC_Polyhedron> complement(const PH& ph) { pair<PH, Polyhedra_PowerSet<NNC_Polyhedron> > partition = linear_partition(ph, PH(ph.space_dimension(), Polyhedron::UNIVERSE)); return partition.second; }

int main() { Variable x(0); Variable y(1);

C_Polyhedron p(2, Polyhedron::EMPTY); p.add_generator(point(x)); p.add_generator(point(y)); p.add_generator(point(-x)); p.add_generator(point(-y));

cout << "p = " << p << endl;

Polyhedra_PowerSet<NNC_Polyhedron> p_c = complement(p);

cout << "complement(p) = " << p_c << endl;

C_Polyhedron q(2); q.add_constraint(x >= -1); q.add_constraint(x <= 1); q.add_constraint(y >= 1); q.add_constraint(y <= 3);

cout << "q = " << q << endl;

Polyhedra_PowerSet<NNC_Polyhedron> q_c = complement(q);

cout << "complement(q) = " << q_c << endl;

return 0; } -------------------------------- %< %< %< --------------------------------

And here is the output of the program (newlines added for readability):

p = -A - B >= -1, -A + B >= -1, A - B >= -1, A + B >= -1 complement(p) = { { A + B > 1 }, { -A - B >= -1, A - B > 1 }, { -A - B >= -1, -A + B > 1 }, { -A - B > 1, -A + B >= -1, A - B >= -1 } } q = -A >= -1, -B >= -3, B >= 1, A >= -1 complement(q) = { { A > 1 }, { -A >= -1, B > 3 }, { -A >= -1, -B > -1 }, { -A > 1, -B >= -3, B >= 1 } }

Notice that, in general, there are several possible representations of the complement of a polyhedron as a set of polyhedra. This implementation guarantees that the resulting set is a partition of the complement of the given polyhedron (i.e., that the members of the set are pairwise disjoint). It should also be possible to prove that the partition returned has a reasonable number of elements (such as the number of facets of the argument). I hope this helps. Please do not hesitate to come back to us in case it doesn't. All the best,

Roberto

...

From: Roberto Bagnara bagnara@cs.unipr.it To: BerPast berpast@hotmail.com Subject: Re: Help with alias analysis framework Date: Sat, 14 Aug 2004 09:30:12 +0200

BerPast wrote:

...

In the paper "Interprocedural may-alias analysis for pointers: beyond k-limiting", the author presents a parametric framework for the analysis of pointer aliases. The framework is parametrised by a numeric lattice V#. The lattice has to have some abstract operators; the 4th are 5th are for me the most complex: 4) resolution of a linear system: given a system S, I need to compute a member of the lattice which is an upper approximation of the integer solutions to S; 5) intersection with a linear system: if S is a system of linear equations and K is a member of the lattice, I need to compute an upper approximation of the solutions to S that are also in K (no empty intersection with K I guess).

I need to implement the lattice operators, but I have no idea of how to do this. Probably using Fourier-Motzkin projection I can solve the problem for the lattice obtained by the smash product of the interval lattice (any other, more efficient method?), but how can this problem be solved for a generic lattice? Can someone point out to me some documentation and (if available code implemenation) explaining how to solve this problem for a generic lattice?

I am not sure I understand what you mean by "[solving] this problem [...] for a generic lattice." All the numerical abstractions provided by the Parma Polyhedra Library (http://www.cs.unipr.it/ppl/) come with the operations that a numeric lattice must possess in Alain Deutsch's framework. All the best,

Roberto Bagnara

-- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it