[PPL-devel] PPL and polyhedra comparisons

[Enea Zaffanella]

Hi Sebastian.

I am afraid I am not following your answer here below.

Sebastian Pop wrote:
> On Fri, Aug 22, 2008 at 11:23 AM, Roberto Bagnara <bagnara at cs.unipr.it> wrote:
>> This also remained unanswered (I guess that, on the way back from
>> holidays, you found zillions of messages pending... I know it is
>> not an easy situation).  If you can clarify the semantics of
>> the comparison operation you need, we will add it to the library.
> 
> Cool, thanks.
> 
>>  /* Compares P1 to P2: returns 0 when the polyhedra don't overlap,
>>    returns 1 when p1 >= p2, and returns -1 when p1 < p2.  The ">"
>>    relation is the "contains" relation.  */
>>
>> What should be returned if P1 and P2 do overlap and neither is
>> contained into the other?
>>
> 
> In that case,
> if p1 has constraints that are larger than p2, then 1, else -1.
> 
> i.e.
> 
> if p1 \ (p1 inter p2) is bigger than p2, then 1, else -1.

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).

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?

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

Ciao,
Enea.