[PPL-devel] Rational polyhedra

[Roberto Bagnara]

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

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