Floating Point Constraints in PPL
Hello,
My name is Radoslav Ivanov and I am a PhD student at the PRECISE lab at the University of Pennsylvania.
I am trying to perform some polyhedra operations using PPL (in C++). However, I am not sure if it is possible to encode constraints with non-integer values. Can you please tell me if this is possible and if yes, what type I should use?
Thanks, Rado
On 03/11/14 21:15, Radoslav Ivanov wrote:
My name is Radoslav Ivanov and I am a PhD student at the PRECISE lab at the University of Pennsylvania.
I am trying to perform some polyhedra operations using PPL (in C++). However, I am not sure if it is possible to encode constraints with non-integer values. Can you please tell me if this is possible and if yes, what type I should use?
Dear Radoslav,
it is always possible to encode constraints with non-integer coefficients into constraints with integer coefficients, which can then be treated with the PPL.
See ppl/demos/ppl_lcdd.cc as an example: the function normalize() takes an (input) vector of rational coefficients, an (output) vector of corresponding integer coefficients and an (input/output) accumulated denominator for the conversion.
If you tell us what are you trying to achieve, perhaps we can provide more useful advice. Kind regards,
Roberto
Thank you, Roberto! This function is exactly what I was looking for. I guess this mpq_class converts floats into pairs of numerators and denominators.
Regards, Rado
On Wed, Mar 12, 2014 at 3:25 AM, Roberto Bagnara bagnara@cs.unipr.itwrote:
On 03/11/14 21:15, Radoslav Ivanov wrote:
My name is Radoslav Ivanov and I am a PhD student at the PRECISE lab at the University of Pennsylvania.
I am trying to perform some polyhedra operations using PPL (in C++). However, I am not sure if it is possible to encode constraints with non-integer values. Can you please tell me if this is possible and if yes, what type I should use?
Dear Radoslav,
it is always possible to encode constraints with non-integer coefficients into constraints with integer coefficients, which can then be treated with the PPL.
See ppl/demos/ppl_lcdd.cc as an example: the function normalize() takes an (input) vector of rational coefficients, an (output) vector of corresponding integer coefficients and an (input/output) accumulated denominator for the conversion.
If you tell us what are you trying to achieve, perhaps we can provide more useful advice. Kind regards,
Roberto-- Prof. Roberto Bagnara
Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
participants (2)
-
Radoslav Ivanov -
Roberto Bagnara