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,
RobertoOn 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@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel