[PPL-devel] Rational polyhedra

[Roberto Bagnara]

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
> 


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