[PPL-devel] Closed versus NNC polyhedra

[Roberto Bagnara]

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 at 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

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