Should I build with GMP for performance?

[roastduck]

Hi,

I see Z3 supports both GMP and internal implementation on multi-precision. I am wondering which one yields better performance. In other words, if I am OK about GMP's GPL license, should I prefer GMP?

Thanks in advance.

[NikolajBjorner]

I don't think there was a sufficiently noticeable difference between GMP and z3's native MP bindings. I never use GMP bindings for evaluation. Note that MP does have significant overhead in some arithmetic (QF_LRA, QF_LIA) benchmarks. The big issue is not really whether to use one MP library or the other, the big issue there is to rewrite the solvers entirely to not use MP at all and use fixed-precision (64 bit integers) or floats. These rewrites are beyond the current scope of plans given that the use cases for QF_LRA and similar are not prolific and using MIP solvers for such cases makes more sense.

[roastduck]

Actually the problems that I concern are to prove inequalities of integer expressions involving linear operations and integer-division-by-constants, which I think belongs to QF_LIA. How do I run the benchmarks for QF_LIA? I can run a comparison between the two MP libraries.

As for rewriting the solvers to entirely use fixed-precision at all, I see it is not in the plan, but I am curious about how to do it in principle? Since we do not know the user input in advance, do we have to check each integer's value at run time, so as to decide with to hold it with MP or fixed integers? Besides, if we use rationals in the solver, their denominators can get quite large, especially when the coefficients are mutually prime. How can we avoid this case?