[PPL-devel] Closed versus NNC polyhedra

[Michael Classen]

Hello Roberto,

this is basically what I was referring to:

---------- Forwarded message ----------
From: P M Hill <hill at comp.leeds.ac.uk>
Date: Wed, Jul 8, 2009 at 9:52 PM
Subject: Re: [PPL-devel] integer versus rational solutions
To: Michael Classen <michael.classen at uni-passau.de>
Cc: ppl-devel at cs.unipr.it, "gcc-graphite at googlegroups.com"
<gcc-graphite at googlegroups.com>


On Wed, 8 Jul 2009, Michael Classen wrote:

>> HTH. Let me know if you have further queries wrt this domain, we will glad
>> to help.
>>
>> Pat
>
> Hi Pat,
>
> I basically just want to know if I can get correct integer results
> when using this combination of datatypes. I want to use operations
> like union, intersection, projection, basically most standard
> operations you want to use on polytopes.

Yes. These are already available in the latest release, but the best
version of the product domain is in the products branch of the GIT
repository. I would recommend you to use that if possible.

Sorry, I did not reply sooner to your previous email. I did try and
see what could be done to help solve the problem you described. (i.e.,
transforming a grid x polyhedron product to one where the grid is the
integer lattice). In fact, I have a proposal for adding a method to
the product domain that I hope would be sufficient for what you need
while, from the point of view of the PPL, fits into the existing
structures. In particular, I am believe that the implementation work
would be small!

That is:
In the product domain, (assuming for this explanation that the first
domain is a grid and the second a C polyhedron) there would be a
method such as:

bool
Partially_Reduced_Product<Grid, C_Polyhedron, R>
::affine_lattice_transform(const Grid& gr1)

that assigns to *this = <gr, ph> the product <gr1, ph1> such that
there is an affine function (ie a sequence of affine image mappings)
T, T(gr) = gr1 and T(ph) = ph1.

If there is no invertible affine function T such that T(gr) = gr1,
then the method could return false and otherwise true.

If you call the method with gr1 = integral lattice, and gr as a full
dimensional discrete grid you will get the polyhedron transformed to
one where the integral points correspond to the grid points and you
can use whatever tools you like to count the number of integer points.
By calling the same method with this* = <gr1, ph1> with the argument
gr, you will
be able to invert the operation.

I can try and implement something like this next week (while away at a
conference) as I think this would be useful anyway for other
applications.

Best wishes,
 Pat



On Fri, Jul 10, 2009 at 4:43 PM, Roberto Bagnara<bagnara at cs.unipr.it> wrote:
> Tobias Grosser wrote:
>>
>> On Thu, 2009-07-09 at 16:52 +0200, Michael Classen wrote:
>>>>
>>>> They do not. However at the moment we are working on R^n. We should move
>>>> to integral polyhedron.
>>>>
>>>> Tobi
>>>
>>> You say that as if it is very easy... is there already a simple way of
>>> dealing with integral polyhedrons in PPL? If so, I should maybe tell
>>> Patricia that she shouldn't work too hard on this new datatype...?
>>
>> No. I am waiting for Patricia's work. I think this is the way to go.
>
> Hi there.
>
> Can you please explain what you mean by "integral polyhedron",
> "new datatype" and "Patricia's work"?  Please do not be afraid
> to (re)state the obvious: I am sure there is one or more
> misunderstandings here.
> Cheers,
>
>    Roberto
>
> --
> Prof. Roberto Bagnara
> Computer Science Group
> Department of Mathematics, University of Parma, Italy
> http://www.cs.unipr.it/~bagnara/
> mailto:bagnara at cs.unipr.it
>