[SMTCOMP] IMPORTANT: the infinite-precision issue

[Roberto Sebastiani]

Cesare,
I'm not sure I got the point.

On Tue, 13 Jun 2006, Cesare Tinelli wrote:

> (...)
>>> From a more principled perspective, I don't like the idea of customizing 
>>> tools for 
>> single instances, or of adopting tricks like
>> "if infty run mathsat_infty else if 32 run mathsat_32 else run mathsat_64".
>> 
> Fair enough. But I find it puzzling to hear this from a main MathSAT 
> developer. Isn't MathSAT's layered approach based exactly on the principle of 
> using the right (sub)solver for each specific input (sub)problem?

Yes, but the decision is taken internally by looking at the (atoms in) 
the formula, without exploiting any extra information provided as input.

> How would 
> this be different?


Sorry if my statement was not clear: here I meant avoiding customizations 
based *on the input flag information* "32,64,infty". If somebody wants to decide 
whether to use 32, 64, or infty precision on generical formulas in a layered manner, 
or whatever other technique, I'm perfectly at ease with that.

Roberto

>
> Cheers,
>
>
> Cesare
>
>
>
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>> On Tue, 6 Jun 2006, 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, 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.
>>> 
>>> 
>> 
>

-- 
------------------------------------------------------------------
Prof. ROBERTO SEBASTIANI
Dip. Informatica e Telecomunicazioni
Fac. Scienze M.F.N., Universita` di Trento    Tel: +39 0461 881514
Via Sommarive 14, I-38050, Trento, Italy      Fax: +39 0461 882093
roberto.sebastiani at dit.unitn.it     http://www.dit.unitn.it/~rseba
------------------------------------------------------------------