[PPL-devel] a Bug, a Beg and a Binding

[Roberto Bagnara]

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 at cs.unipr.it