[SMTCOMP] IMPORTANT: the infinite-precision issue

[Leonardo de Moura]

Hi Roberto,

This is a good point.

> there is an important question about SMT-COMP which apparently  
> nobody asked so far: do we explicitly require infinite precision  
> from SMT solvers on arithmetic-related theories? (I.e., RDL/IDL/LAR/ 
> LAI and combinations.)

I believe one needs to use multi precision arithmetic for solving  
some problems in
LRA and LIA, but I agree with you that the benchmarks in RDL and IDL  
do not
require infinite precision.

I'm not sure if we should force/require people to use multi precision  
arithmetic.
I think it is perfectly ok to use fixed precision, and return "unknown"
when an overflow/underflow is detected.

I also believe it is perfectly ok to enter an incomplete solver, and  
return
"unknown" for formulas you know your solver is incomplete.
For example, Aaron Stump did that last year. CVC is not complete
for integers, and he returned "unknown" for potential "sat" instances.

Anyway, I really interested in knowing what the rest of the SMT  
community
thinks about this issue.

> On the one hand, infinite precision prevents an SMT tool from
> giving wrong answers on some problems. On the other hand, using  
> infinite precision significantly slows down the performances  
> (around a 3 factor in our experience).

In my experiments, I noticed a 1.4 factor. I'm using GMP  
(www.swox.com/gmp/)
for infinite precision. I guess you are using it too. :-)
We found that memory management can be expensive with GMP, and a good  
trick
is to create a pool of GMP numbers and reuse them for intermediate  
computations.

Cheers,
Leonardo.