Axel Simon wrote:
I am trying to describe how to analyze floating point calculations with polyhedra. It's a last-minute project for a VMCAI paper.
Great! There is no much time though ;-)
The only thing which could make the test fail is the fact that I retrieve the end iterator before I actually iterate through the constraint system.
That would not be a problem, provided nothing happens to the constraint system before you actually iterate. If you can reproduce the problem in C or C++ we would be more than happy to help with debugging.
The odd thing is that this function works 90% of the time. I would like to debug it but it is kind of hard since all interesting functions are in-line. It could be something with my binding to Haskell, but I just thought I ask if somebody has experienced the same problem with the C interface before going down that route.
No, we are not aware of any problem of this kind. You will find similar code, iterating through a generator system, at lines 667 and following of interfaces/C/lpenum/lpenum.c.
Do you need only the maximum value of the expression or also one or all vertices where the maximum is attained?
No, I would only be interested in the maximum (rational?) value. I think that is essential for analyzing non-linear expressions like x = e_1 *e_2 with \exists_x(P) \sqcup { x \leq \max(e_1,P)*e_1, x \leq \max(e_2,P)*e_1, x \geq \min(e_1,P)*e_2, x \geq \min(e_2,P)*e_1 } where \min(e_1,P) gives smallest value of the expression e_1 in P.
OK: we will try to add this functionality to the library in a couple of days or so. If this is too much time, you can look at the above mentioned lines 667 and following of interfaces/C/lpenum/lpenum.c: there, what is done is precisely to compute the rational maximum/minumum of a linear expression. Cheers
Roberto