Comments (5)
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
from elina.
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_t
s internally. We're wanting to move away from that codebase for various reasons.
I know that using mpz_t
s 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
from elina.
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
from elina.
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
from elina.
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
from elina.
Related Issues (20)
- Segfault when creating a polyhedra using a tcons_array HOT 1
- Broken ELINA after 9c99c4d177c691f98f2031657c18fe6fbe4c7571 HOT 1
- Adding a new variable and interval to Poly HOT 4
- Meet/Join with different dims? HOT 5
- Makefile in fppoly references non-existant sign_approx.o HOT 1
- Wrong CDD_PREFIX after ./configure --cdd-prefix HOT 4
- Memory leaks (Valgrind) in elina_poly HOT 7
- OSError: libfppoly.so: cannot open shared object file: No such file or directory HOT 4
- error: ‘AP_SCALAR_MPFR’ undeclared (first use in this function); did you mean ‘ELINA_SCALAR_MPFR’? HOT 2
- error when executing make in ELINA HOT 2
- Get relative bounds for dimensions HOT 2
- SEGFAULT when joining bottom HOT 4
- Portability issue with the `funptr` array HOT 7
- -march=native and -DTIMING not supported in Apple M1 HOT 3
- Missing MPFR_LIB_FLAG and GMP_LIB_FLAG in Makefile HOT 2
- How to tune the clam options to reproduce ELINA paper results HOT 14
- Does ELINA support the join and meet operators in case of the NNC Polyhedra? HOT 11
- No bound_texpr support for polyhedra domain
- Octagon overflow during assignment not handled correctly? HOT 1
- Unexpected bottom after meeting constraints using elina_poly HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from elina.