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

[Christoph Wintersteiger]

Hi all,

Exactly, just like the others said, those are randomly generated test cases. I spent a bit of effort on the generator some years ago, so that particular percentages of corner/nan/inf cases appear in them, and I automatically compared them to the results from various FPUs (x87/SSE2/Itanium, various precisions) so I think for the purpose of testing they should be alright. There's always one benchmark that tests whether a benchmark has any solution at all and then there's a second benchmark that checks that the solution has to be the same as what the FPU said. 

They are not interesting for performance testing of course, as pretty much everything is easy (except for the remainder operation perhaps). 

Alberto Griggio's benchmarks contain some randomly generated systems of polynomials, those may be a better starting point for you I think. 

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Martin Brain
Sent: 26 November 2015 12:01
To: smt-lib at cs.nyu.edu
Subject: Re: [SMT-LIB] A beginner's question about Wintersteiger's benchmark

On Wed, 2015-11-25 at 15:55 -0800, Zhoulai wrote:
> Thanks. It seems most of Wintersteiger's benchmarks  are in the style 
> of unit-test as you said.

Yes.  Floating-point is notoriously detailed and has lots of awkward edge cases.  Christoph kindly wrote and released a set of unit-test style benchmarks to help everyone catch these.

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

Have a look in QF_BVFP/, QF_FP/schanda and QF_FP/griggio.

Cheers,
 - Martin


_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.cs.nyu.edu%2fmailman%2flistinfo%2fsmt-lib&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7caadf74602bd24b89e10f08d2f65974ab%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=Aqaz05viBeyNG7KOZBC9G%2bHukI7QkeRfN5jP%2fxGyetE%3d