Roberto Bagnara wrote:
Axel Simon wrote:
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.
Hi Axel, there is now a snapshot of the PPL 0.6 development branch in http://www.cs.unipr.it/ppl/Download/ftp/snapshots/ppl-0.6pre2.tar.bz2 In the C interface you will find the function ppl_Polyhedron_maximize() that does what you need (and more). Beware: this new code is almost untested. Please let us know how it goes. Cheers Roberto P.S. Any progress in debugging the ConSys iteration problem? -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it