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

Axel Simon a.simon at kent.ac.uk
Sun Aug 24 17:53:26 CEST 2003


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.




More information about the PPL-devel mailing list