-
Notifications
You must be signed in to change notification settings - Fork 54
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Any plans for int_64
coefficients or, ideally, mpz_t
coefficients?
#26
Comments
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, |
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 I know that using Any thoughts? Cheers, Jose |
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, |
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 Cheers, Jose |
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, |
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 withlong long int
). It seems that ELINA is usinglong long int
s 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
The text was updated successfully, but these errors were encountered: