On Friday, Aug 22, 2003, at 22:45 Europe/Paris, Roberto Bagnara wrote:
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.
Ok, thanks, I'll give it a go.
P.S. Any progress in debugging the ConSys iteration problem?
No, not yet. There reason might be that Haskell uses a pre-installed gmp package which is version 4.0.1. I compiled PPL against 4.2.1. Thus PPL used the headers and gmpxx.a of the newer version while the gmp.a is from Haskell. I know that it's asking for trouble, but the binary representation of mpz's haven't changed and I don't get any link errors. I'll try to build PPL against version 4.0.1 now. Is that possible?
Axel.