Michael Classen wrote:
Hi Roberto,
basicall, what I need Z-polytopes for is a problem like the following:
Assume we have a certain loop-nest with some statements that access a certain array:
for(i=0; i<n; i++) { for(j=0; j<n; j++) { A[2*i][2*j] = ... A[i][i] = ... } }
(in general, array accesses can be arbitrary affine functions of loop variables and structural parameters)
What I want to analyze is the array elements that are accessed by this program. I want to count the number of array elements that are needed during this computation. Unfortunately, the resulting sets are not always convex polytopes, e.g. in this case, the first array access function yields a set of points with only even numbers for coordinate entries.
So I have to use Z-polytopes to describe this set and count the number of points it contains. For this purpose, I have to calculate a disjoint union of the two Z-polytopes resulting from mapping each array access function (2i,2j) and (i,i) on the index space of each statement. Then, I can use the Barvinok algorithm to count the number of elements for each set in the resulting (disjoint) union.
I have implemented this method using the PolyLib, but unfortunately there seem to be fundamental problems with the implementation of Z-polytopes. So I was hoping that I could use PPL to achieve something equivalent.
I hope this will clear up a few of the misunderstandings? But feel free to ask further questions.
[Copying here my reply to another message to ppl-devel@cs.unipr.it]
I propose you to start from the beginning. But this time, let us avoid anything that is not precisely defined.
My understanding is that you are interested in Z-polytopes. A polytope is a bounded, convex polyhedron, right?
And a Z-polytope is the intersection between a polytope and an integer lattice, right? (Note: in the PPL "integer lattices" are called "integral grids".)
The PPL provides a way to "combine" a Grid (which can represent any integer lattice), with a C_Polyhedron (which can represent any polytope). But the combination is loose, because the tight integration is computationally intractable.
Now, what operations do you require? I guess you need to know if a Z-polytope is empty, right? This requires to answer, for a given polytope P in R^n described by a system of constraints with rational coefficients, the question:
Is P intersected with Z^n empty?
We currently use a standard, branch-and-bound mixed integer programming optimizer: it may fail to terminate, it may be ridiculously expensive. Can we do better? We got in touch with three leading experts in the field. Two did not bother to reply. *The* leading expert told us that "[Lenstra's algorithm, the algorithm of Gr"otschel, Lov'asz and Schrijver, and the algorithm of Lov'asz and Scarf] are essentially theoretical. I don't know of any implementations." If you know the algorithm we should use, please share.
If we want the tight integration between C_Polyhedron and Grid, we also need to compute a representation of the "integer hull" of P, that is, the convex polyhedral hull of P intersected with Z^n. Which cutting plane algorithm(s) should we use? So far, we got no answer from the experts we contacted. Do you know the answer?
Perhaps I have misunderstood what you mean by a "precise way of dealing with something like Z-polytopes"? Please let us know. Cheers,
Roberto