[SMTCOMP] IMPORTANT: the infinite-precision issue

[Cesare Tinelli]

Hi all,

Leonardo de Moura wrote:
> 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, 
 >
It looks like it is needed in some problems.
According to Domagoj Babic who has looked at the QF_LIA problems in 
depth, at least one of the *64*.msat.smt problems in 
http://goedel.cs.uiowa.edu/smtlib/smtlib/benchmarks/QF_LIA/CIRC
use numerals that *will* go out or range on 32bit machines.


> 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.
> 
Domagoj had this suggestion: how about annotating each benchmark with an 
indication of what kind of precision it needs?
This could be easily done in our open format by adding an additional 
field. Domagoj was suggesting something of the form

:max_range {infty | u64 | s32 | ... }

specifying the minimum range required (u64 - 64bit unsigned, s32 - 32bit 
signed, ...) to solve the benchmark correctly.

The problem of course would be to figure out the smallest safest range 
for the existing benchmarks and future ones when it is not explicitly 
provided by the benchmarks' creator.

What do you think?



Cesare


>> 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.
> 
> 
>