[SMT-LIB] A beginner's question about Wintersteiger's benchmark

[Levent Erkok]

On Thu, Nov 26, 2015 at 4:32 AM, Martin Brain <martin.brain at cs.ox.ac.uk>
wrote:

> On Wed, 2015-11-25 at 18:20 -0800, Levent Erkok wrote:
> > It'd be fairly easy to generate such benchmarks; but I don't know of the
> > top of my head if there's a "good" collection of them anywhere.
>
> As someone who has done this -- it's harder than you might think to
> create benchmarks that are meaningful, not too easy or too hard and in
> sufficient numbers / with sufficient variety that experiments using them
> are significant.


Absolutely! My "easy" remark was simply referring to the actual generation
of a file conforming to SMTLib2 from something that looks "mathematical."
Actually coming up with a good-benchmark idea, whether it merely involves
just constants or with symbolic variables thrown in, is a very difficult
task. It's at least as hard as coming up with good "test vectors," which is
a notoriously hard problem especially for floats.

But, as you also mentioned, once one has the idea of a benchmark problem,
higher-level tools like SBV or Spark or CBMC do simplify the actual
generation of files immensely; as SMTLib format is not particularly
programmer friendly; nor it was intended to be. It wasn't quite clear to me
whether the original-poster needed already generated good benchmarks, or
needed a way to create SMTLib2 compliant files for the problems he/she was
already thinking about.

-Levent.