antoinemine / apron

Apron Numerical Abstract Domain Library
Other
114 stars 33 forks source link

Apron wrapper for PPLite 0.12. #105

Closed ezaffanella closed 6 months ago

ezaffanella commented 7 months ago

PPLite version 0.12 no longer depends on gmpxx (the C++ interface of GMP).

Note: we also applied a minor renaming to newpolka matrix* type and functions (adding prefix "pk") so as to avoid a few name clashes with version 3 of the FLINT library, which is a required dependency of PPLite. Both newpolka and FLINT v.3 have functions named "matrix_clear" and "matrix_equal", thereby preventing static linking of Apron and PPLite when using the newer version of FLINT. Fix contributed by Michele Spotti.

antoinemine commented 6 months ago

Thanks for the PR!

I tried it although I still havePPLite 0.11 (not 0.12) and I get errors in pplite_user.hh:

In file included from pplite_user.cc:16:
pplite_user.hh: In function 'void pplite::apron::to_scalar(ap_scalar_t*, const pplite::Integer&)':
pplite_user.hh:50:5: error: 'const pplite::Integer' {aka 'const class pplite::FLINT_Integer'} has no member named 'get_mpz'
   50 |   i.get_mpz(mpq_numref(s->val.mpq));
      |     ^~~~~~~
pplite_user.hh: In function 'void pplite::apron::to_scalar(ap_scalar_t*, const pplite::Integer&, const pplite::Integer&)':
pplite_user.hh:59:5: error: 'const pplite::Integer' {aka 'const class pplite::FLINT_Integer'} has no member named 'get_mpz'
   59 |   n.get_mpz(mpq_numref(s->val.mpq));
      |     ^~~~~~~
pplite_user.hh:60:5: error: 'const pplite::Integer' {aka 'const class pplite::FLINT_Integer'} has no member named 'get_mpz'
   60 |   d.get_mpz(mpq_denref(s->val.mpq));
      |     ^~~~~~~
pplite_user.hh: In function 'void pplite::apron::to_scalar(ap_scalar_t*, const pplite::Rational&)':
pplite_user.hh:68:5: error: 'const pplite::Rational' {aka 'const class pplite::FLINT_Rational'} has no member named 'get_mpq'
   68 |   r.get_mpq(s->val.mpq);
      |     ^~~~~~~

Is this expected? Do you have a plan so that the binding works with both versions 0.11and 0.12, or would it be unadvisable?

ezaffanella commented 6 months ago

It was expected, as the PPLite's interface has changed. But you are right: we should detect the PPLite's version at configuration time and add a few (conditionally compiled) helpers to make it work for both 0.11 and 0.12. We will provide an updated PR.

antoinemine commented 6 months ago

Thanks, that'd be perfect! Alternatively, if it makes more sense to make it work only for 0.12, it's also OK, but the configure should nevertheless check the PPLite version and disable PPLite support if an earlier version is detected.

antoinemine commented 6 months ago

Thanks! In get_pplite_version, I think that you need to change $cxx into $cxx $cxxflags $deps (both time).

antoinemine commented 6 months ago

Sorry, another thing: I think that PPLITE_PREFIX should be pplite_prefix in get_pplite_version, as it is the output of checkprefix (which may contain PPLITE_PREFIX if specified, but might discover another working prefix even if PPLITE_PREFIX is empty).

ezaffanella commented 6 months ago

Done, thank you.

antoinemine commented 6 months ago

Thank you very much! I think this is ready to be merged.