[SMTCOMP] The infinite-precision issue again

[Aaron Stump]

Hi, Albert.  Clark, Leonardo, and I have been discussing the concerns
you raised about having benchmarks crafted to test soundness when
working with large numerals (I suggest calling these "artificial bignum
benchmarks").  As Leonardo mentioned, we concluded the original
discussion (sparked by Roberto Sebastiani) by saying that we would
indeed include artifical bignum benchmarks in all arithmetic divisions.
So we would really need to stay with that decision at this point, since
we had no complaints and the competition is coming up soon.

But addressing the issues you raised more directly, I would offer the
following argument for why there should be no issue in including
artificial bignum benchmarks.  Solvers using machine arithmetic only
(let's call these "32-bit solvers"), without a bignum package, are
presumably doing so because their implementors believe this will confer
a speed advantage.  If that is correct, there should be benchmarks that
can be solved within whatever time limit by 32-bit solvers, but not by
similar solvers using a bignum package ("bignum solvers").  In that
case, any points a 32-bit solver loses due to inability to perform
arithmetic on large numerals should be recovered on benchmarks where the
cost of arithmetic on numerals is decisive for solving or not solving
the benchmark.

Now the reality is, no one seems to have any such benchmarks, where the
cost of arithmetic on numerals is the deciding factor.  Certainly no one
has provided them to SMT-COMP.  So for competition, bignum solvers may
indeed have an advantage.  The burden is, in my opinion, on the
proponent of 32-bit solvers to provide benchmarks where using native
arithmetic is essential to solve the benchmark in time.  

Of course, if it is true that 32-bit arithmetic confers a significant
advantage, more robust solutions are to use 32-bit arithmetic and fail
over to bignum arithmetic if overflow/underflow is detected; or
possibly conservatively analyze the benchmark to decide which arithmetic
package to use (though this may not be trivial to determine).  

Finally, even if the jury is still out on whether native arithmetic
confers a crucial advantage on benchmarks of interest, supporting
arbitrary precision numerals is more robust, and hence requiring such
support seems like a reasonable default position in the absence of
more evidence.

Aaron, attempting to summarize the position also of Clark and Leonardo