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

[Christoph Wintersteiger]

Martin: Speaking of which - did you/we plan to release a nice FPA SMT2 fuzzer type of tool? Maybe I should dust off that old generator...

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

> 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:
> https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2flevent
> erkok.github.io%2fsbv%2f.&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7cee762adfcd624b5fd7d108d2f65dd5fd%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=q3MRPwfXBmzrbhxnX8re5eQWwa%2f%2bH3Ku7bdCPlUgmDQ%3d For this use case, there's a function called 'compileToSMTLib' 'that does the trick:
> https://github.com/LeventErkok/sbv/blob/cc7a6f7017859c10f1c44111126017
> 66e835d9dc/Data/SBV/Provers/Prover.hs#L313
> )

If you want to use C then I can recommend CBMC, likewise for Ada I'd suggest SPARK.

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%7cee762adfcd624b5fd7d108d2f65dd5fd%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=wKZlEDufIMLcR8L%2by9FbmZKVFr50c9pDYyymC6qcisU%3d