[PPL-devel] Rational polyhedra

[Roberto Bagnara]

Hi Stefan.

On 11/23/2016 04:39 PM, Stefan Schupp wrote:
> I will give an example on how I understood the documentation - I
> might have missed something:
> 
> Assume I want to multiply some matrix A \in R^nxm with a single
> point p \in R^m. I would create some linear expression a_0
> reflecting the first row of the matrix to modify the first
> coordinate corresponding to some variable x_0.

The problem seems to be here: we are talking of C_Polyhedron,
which is a class for the representation and manipulation of
certain geometric ojects.  "Matrix", "row" and "first row"
do not make sense in this context.
Kind regards,

   Roberto

> Now if I use p.affine_image(x_0, a_0), my point p is modified, where
> the first coordinate is the result of my transformation. For the
> second row, I'd have to create a copy of that point (beforehand), as
> otherwise I use the updated value of the first coordinate for my
> follow-up transformation and so on, which would require me to create
> m copies of my point, which makes the whole task quite expensive and
> I am not sure on how to re-unite the results (for a point, sure, but
> in general).
> 
> I hope this clarifies my problem.
> 
> 
> On 23.11.2016 15:56, Roberto Bagnara wrote:
>> On 11/23/2016 09:14 AM, Stefan Schupp wrote:
>>> thanks for the answer. So, once I converted my coefficients for
>>> constraints or point coordinates to integer (in an
>>> over-approximating fashion), the library ensures overapproximation
>>> in any case, right?
>> Yes.  Note though that almost all operations on C_Polyhedron (and
>> NNC_Polyhedron) are exact, so that talking about "overapproximation"
>> might be misleading.  Refer to the documentation for the precise
>> semantics of each operation.
>>
>>> I already found the image and pre_image functions, but as they are
>>> not creating a new object (as far as I understood) but modify the
>>> current object, you cannot simply create a linear expression from
>>> each row and use the image function sequentially on your polyhedron.
>> I am not sure I follow: if you do not want to modify the current
>> object, you can make a copy and operate on the copy, can't you?
>> Kind regards,
>>
>>     Roberto
>>
>>> On 23.11.2016 08:18, Roberto Bagnara wrote:
>>>> Hello Stefan.
>>>>
>>>> On 11/22/2016 04:18 PM, Stefan Schupp wrote:
>>>>> I am using PPL for my project which is related to verification. In
>>>>> this context I require my computations to be exact or, if that is
>>>>> not possible, to be over-approximating. From what I read in the
>>>>> documentation, PPL ensures such an over-approximation, which is
>>>>> nice. I am using C_Polyhedron as my data type and currently
>>>>> interested in using rational arithmetic (mpq_class) in combination
>>>>> with that. From what I see, you can use the mpz_class type for
>>>>> C_Polyhedron, but not mpq_class directly. Is there a way intended to
>>>>> overcome this problem?
>>>> More than a problem, this is a precise design decision motivated by
>>>> efficiency reasons: conversion of coefficients of any kind to integer
>>>> coefficients is left to the application.  There are several examples
>>>> in the library on how to do that: possibly the simplest one given by
>>>> function normalize() in demos/ppl_lcdd/ppl_lcdd.cc .
>>>>
>>>>> In my current setup I use the double interface, but this requires
>>>>> conversion and most probably introduces rounding errors.
>>>> I am not sure I understand the first part of the sentence: which double
>>>> interface are you using?
>>>>
>>>>> Furthermore a usage question: Is there an intended way on how to
>>>>> compute a linear transformation of a polyhedron with a matrix?
>>>> Look for the string "image" in the manual.
>>>> Kind regards,
>>>>
>>>>      Roberto
>>>>
>>>
>>>
>>> _______________________________________________
>>> PPL-devel mailing list
>>> PPL-devel at cs.unipr.it
>>> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
>>>
>>
> 
> 
> 
> _______________________________________________
> PPL-devel mailing list
> PPL-devel at cs.unipr.it
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
> 


-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com