[PPL-devel] PPL and polyhedra comparisons

[Sebastian Pop]

On Sat, Aug 23, 2008 at 5:48 AM, Enea Zaffanella <zaffanella at cs.unipr.it> wrote:
> In the current sources of cloog_ppl, we have the following:
>
> static int
> cloog_domain_polyhedron_compare (CloogMatrix *m1, CloogMatrix *m2,
>                                 int level, int nb_par, int dimension)
>
> I can guess (please correct me if I am wrong) that:
>
>  a) `m1' and `m2' are the constraints describing polyhedra p1 and p2;
>
>  b) the two polyhedra have space dimension `dimension';
>
>  c) `nb_par' should be the number of parameters and it must satisfy the
> precondition 0 <= nb_par <= dimension;
>
>  d) `level' seems to identify a dimension of the polyhedron and, according
> to a comment to the corresponding code in polylib, it must satisfy the
> precondition
>      1 <= level <= dimension
> However, from the way it is used, it seems to me (but I am not sure about
> it) that it should also satisfy the stronger precondition
>      1 <= level <= dimension - nb_par
> (as a side note, this stronger property would imply dimension > 0).
>

Yes, all this is correct.

> Now, looking at the code for the cloog function above I see this formal
> parameter `level' playing a non-trivial role, so that it seems strange to me
> that it is not mentioned at all in the comment quoted by Roberto.
>
> Can you please clarify its meaning?
>

A little more detail of what nb_par and level are: nb_par represents
the number of variables that are not known at compile time but that do
not vary in the loop nest that is considered.  For example, parameters
can be loop bounds.  The first dimensions in a polyhedron represent
iteration domains: 1 <= level <= dimension - nb_par, and level is one
of these loop iterators.  Polyhedra are sorted following the value of
their constraints in dimension "level".

> Note that any strengthening of the preconditions above
> (e.g., replacing a non-strict inequality <= by a strict inequality <)
> will be really helpful.

Remember that in PolyLib format, the first column of a constraint
matrix represents the {eq, ineq} boolean for the row.  In PPL format:
0 <= level < dimension - nb_par
dimension - nb_par <= parameter < dimension

Does this help?

Sebastian