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

[Levent Erkok]

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.

Incidentally, the benchmark you suggested has the trivial solution of "0";
I'm guessing you had something more interesting in mind. In any case, I
generated the attached benchmark for it using the SBV-library for Haskell;
see attached.

(Using higher-level languages instead of SMT-Lib makes generating such
queries much easier. There are bindings from many languages. If Haskell is
your choice then more info on SBV is available here:
http://leventerkok.github.io/sbv/. For this use case, there's a function
called 'compileToSMTLib' 'that does the trick:
https://github.com/LeventErkok/sbv/blob/cc7a6f7017859c10f1c4411112601766e835d9dc/Data/SBV/Provers/Prover.hs#L313
)

-Levent.


On Wed, Nov 25, 2015 at 3:55 PM, Zhoulai <zell08v at gmail.com> wrote:

> Thanks. It seems most of Wintersteiger's benchmarks  are in the style of
> unit-test as you said. Then, is there  any floating point benchmarks in
> SMT-LIB that seems more interesting,  e.g.,  x*x + 2*x + 1 <=1 where 'x' is
> an unknown FP number (rather than a real)?
>
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bench.smt2
Type: application/octet-stream
Size: 956 bytes
Desc: not available
URL: </pipermail/smt-lib/attachments/20151125/858ebd84/attachment.obj>