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.