[SMTCOMP] IMPORTANT: the infinite-precision issue

[Paulo J. Matos]

Hi all,

On 07/06/06, Cesare Tinelli <tinelli at cs.uiowa.edu> wrote:
> 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 | ... }

This will not solve Sebastiani's the problem, right? Since, even if
you annotate it, you have to build your solver against GMP in case
max_range is infty. Unless, you can decide during runtime which type
of precision to use, this doesn't solve it. Obviously, you can define
an interface and two math engines, one based on processor 'precision'
and other based on 'GMP' and then load one of them once you know which
kind of precision to use but it's not a simple solution.

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

You mean the maximum precision?

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

If you decide to go through this path then, every non-unspecified
benchmark against max_range should be considered to be infty,
probably. That is if we prefer correctness and completeness to
efficiency.

On the other hand, I don't think removing benchmarks with infty
precision requirements is a solution since there may be solvers using
languages, which by default have infty precision and are then already
paying a price. Removing these benchmarks are unfair to them. As I see
it, the solver should return unknown if it cannot solve benchmarks
with infty precision and it detects some overflow, as it was already
mentioned by Leonardo. By doing this, you'll leave the weight of the
decision on the authors which should decide what to do.

There are always solutions which authors might take, like trying to
solve using limited precision and shifting to a GMP interface during
runtime if overflow is detected. Solver is more complex but solves the
issue.

Cheers,

Paulo Matos

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


-- 
Paulo Jorge Matos - pocm at sat inesc-id pt
Web: http://sat.inesc-id.pt/~pocm
Computer and Software Engineering
INESC-ID - SAT Group