[PPL-devel] Rational polyhedra

[Stefan Schupp]

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. 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
>>
>

-- 
Stefan Schupp M.Sc.
RWTH Aachen University
Computer Science Department, Informatik 2
D-52056 Aachen, Germany
http://ths.rwth-aachen.de/people/stefan-schupp/
Tel.: +49 241 80 21244


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4807 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://www.cs.unipr.it/pipermail/ppl-devel/attachments/20161123/f05f1423/attachment.bin>