Any plans for `int_64` coefficients or, ideally, `mpz_t` coefficients?

[jmct]

Hello,

Unless I'm misunderstanding ELINA currently supports 32-bit integers for its coefficients but no larger (i.e. there is no elina_coeff_set_interval_int that works with long long int). It seems that ELINA is using long long ints for the coefficients of its linear constraint arrays, but only internally, is that correct?

I was just curious as to whether there were any plans on expanding the possible size of coefficient values. PPL is able to support mpz_t coefficients, is this feasible for ELINA? We'd prefer to use ELINA for its automatic decomposition, etc.

Thanks so much for your work!

-Jose

[GgnDpSngh]

Hi Jose,

Thanks for your interest in ELINA. You can encode larger coefficients by creating object(s) of type "elina_scalar_t" with mpq_t using the function "elina_scalar_set_mpq". The resulting scalar(s) can be used to encode large coefficients with "elina_coeff_set_interval_scalar" or "elina_coeff_set_scalar" methods. Since ELINA uses long long int internally, if your encoded number exceeds the limit, then there would be an overflow which we try to handle soundly while minimizing the loss of precision. For this, we set the associated decomposed Polyhedra to the top. Let me know if it works or if you have any more questions.

Cheers, Gagan

[jmct]

Hey Gagan, thanks for your quick response.

To give you a bit more detail, we are actually already reaching these limits (i.e. we are getting the exception from opt_pk_vector.c, line 569. This is even with just using 32-bit coefficients (we're encoding very big spaces!). The PPL version of this code does not overflow because we're using PPL that's configured to use mpz_ts internally. We're wanting to move away from that codebase for various reasons.

I know that using mpz_ts internally would make us lose some of the benefits of ELINA!, but we're still hoping to make up for the performance losses with the automatic decomposition. If it would help you we could provide you with example code.

Any thoughts?

Cheers,

Jose

[GgnDpSngh]

Hi Jose,

Thanks for your feedback. Sure, depending on the analysis, the Polyhedra coefficients can grow large very quickly even starting from a very small integer, e.g. 5. Besides performance issues, ELINA does not use mpz_t because based on my experience the Polyhedra widening tends to get rid of constraints with large coefficients. I would look into extending the support for mpz_t in ELINA and let you know (I am not sure if its trivial and it may take a while :)).

Cheers, Gagan

[jmct]

Hey again,

Yeah, our use case is definitely not normal!

I would definitely be willing to help or even lead the development of any such feature if you think it's something you're willing to have in ELINA.

My gut says that the least painful way to do something like this would be to use the convention that PolyLib uses. They define a value type (similar in nature to your elina_int_t) with that type resolving to different underlying types depending on build-time flags. See here. They have many possible choices, which complicates the matter, but perhaps we could do just long long int and mpz_t. The upside to doing everything via C pre-processor macros is that it will still let you have everything unboxed and immediate when it's possible, only falling back to indirections when mpz_t is used. However, there are some downsides to this approach, of course. One is that all arithmetic operations must be done via macros (ugly) and the other is that care must be taken to ensure the library is never assuming a specific underlying implementation outside of the macro definitions.

Cheers,

Jose

[GgnDpSngh]

Hi Jose,

I would be fine if you want to work on adding mpz_t support in ELINA (I am having few deadlines so would not be able to do it right away), I would be happy to help if you encounter any issues. I agree that defining a generic value type that takes different number types based on build time flags is the easiest option (We already do it for compatibility with APRON).

Cheers, Gagan