[PPL-devel] PPL and polyhedra comparisons

[Enea Zaffanella]

Hi Sebastian (and colleagues).

I have a question regarding the cloog_domain_simplify operator.

I would like to know the result that should be expected
when simplifying the following domain,
having just a single polyhedron which is the two dimensional square
   [
     { 10 <= x <= 40,  10 <= y <= 40 }
   ]

with respect to the following domain context,
which is composed by four disjoint squares,
all having a proper intersection with the square above:
   [
     {  0 <= x <= 20,   0 <= y <= 20 },
     {  0 <= x <= 20,  30 <= y <= 50 },
     { 30 <= x <= 50,   0 <= y <= 20 },
     { 30 <= x <= 50,  30 <= y <= 50 }
   ]

If we encode the two unions above in PPL and run the 
simplify_using_context() on our Pointset_Powerset domain,
we will obtain no simplification at all, i.e., the result
is indeed the singleton input square.
This makes sense, as far as I can see, since no constraint
in the input polyhedron is redundant for all the disjuncts
of the context.

I am wondering if this is the expected result and, most importantly,
whether or not the algorithm that is currently implemented in cloog
(it is meant, by cloog when using the PPL)
provides the same result.
My wild guess is that the cloog algorithm is computing
something different ... and probably wrong.
It seems that it would add to the result a lot of polyhedra,
among which the universe polyhedron, which causes all of the other
polyhedra in the union to be simplified away. That is, it will
obtain a singleton union containing the universe polyhedron.

To my eyes, returning the universe domain is wrong, in that
it won't be preserving the intersection of the two input domains.

I would have run some test on cloog myself, but I can't
see how to (easily) feed in the specific input above.
So I am asking if you can help me in this respect.
Let us know, if possible, the result actually computed by cloog
on the example above, as well as comments on whether or not
the result computed by the PPL makes any sense.

Cheers,
Enea Zaffanella.