[PPL-devel] Rational polyhedra

[Stefan Schupp]

Hello Roberto,

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?

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.

Best regards,
Stefan


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
>

-- 
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/32a1c250/attachment.bin>