[PPL-devel] Closed versus NNC polyhedra

[Michael Classen]

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.

I also intend to follow the graphite telephone conference call this
Wednesday at 3pm.

greetings,
Michael Classen

On Fri, Jul 10, 2009 at 6:05 PM, Roberto Bagnara<bagnara at cs.unipr.it> wrote:
> Michael Classen wrote:
>>
>> Hello Roberto,
>>
>> this is basically what I was referring to:
>
> Hi Michael,
>
> thanks for clarifying.  I need to understand more about what you
> mean by:
>
>>> I basically just want to know if I can get correct integer results
>>> when using this combination of datatypes. I want to use operations
>>> like union, intersection, projection, basically most standard
>>> operations you want to use on polytopes.
>
> What do you mean by "correct integer results"?
>
> What I am worried about is that you may believe the PPL supports
> the computation of the integer hull of a convex rational polyhedron
> (i.e., the smallest polyhedron containing only the integer points
> of the given rational polyhedron).  The PPL does not provide an
> algorithm to solve this (difficult!) problem.
>
> What the PPL provides is:
>
> 1) the C_Polyhedron class that you know;
> 2) the Grid class that is able, in particular, to express
>   the integer lattice;
> 3) a generic Partially_Reduced_Product class that allows
>   to combine two domains, given a reduction procedure
>   that propagates _some_ information from one to the
>   other.  I am wondering if this is the same notion
>   of "combination" you use above.
>
> In point (3) the key words are "partially" and "some".
> If _all_ the information was propagated from the Grid
> component to the C_Polyhedron component, we would be
> able to compute the integer hull, but this is not the
> case.
>
> Going back to the expression "correct integer results",
> a Partially_Reduced_Product among a C_Polyhedron and
> a Grid encoding the integer lattice provides (as far as
> we know) correct, but possibly (and often) imprecise
> results.
> 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
>