[SMTCOMP] IMPORTANT: the infinite-precision issue

[Aaron Stump]

[ responding to Cesare: ]

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

I think this sounds like a good idea.  Obtaining a rough estimate of the
smallest safe annotation could maybe be done (by someone with their
fingers in the code of a solver built with a bignum package) by
instrumenting the solver to track how large the integers used during
solving are.  A more mathematical definition of the smallest safe
annotation might be challenging to come up with, and challenging to
compute (is it the annotation needed for a run of a particular published
algorithm? the one needed for the shortest proof in some theory?).

Aaron