[PPL-devel] simplify_using_context() vs. cloog_domain_simplify()

[Enea Zaffanella]

Resending (with apologies) after correcting the subject line.

Enea Zaffanella wrote:
> 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.