[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Christoph Wintersteiger]

Yes, I downloaded them (old and new) but haven't committed them to the repository yet. I'll run the latest Z3 over them as well, just to make sure everything's in order.

Just a minor point: Rafael Z?hl's name doesn't render right (when I open the file in emacs). Should I change it to Zaehl?

Cheers,
Christoph


Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | https://www.microsoft.com/en-us/research/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: Delcypher [mailto:delcypher at gmail.com] 
Sent: 28 April 2017 13:55
To: Christoph Wintersteiger <cwinter at microsoft.com>
Cc: Clark Barrett <barrett at cs.stanford.edu>; smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

Hi,

On 23 April 2017 at 20:29, Delcypher <delcypher at gmail.com> wrote:
> Hi,
>
> On 21 April 2017 at 16:06, Christoph Wintersteiger 
> <cwinter at microsoft.com> wrote:
>> Hi Dan,
>>
>> Space is free, submit them all! If it turns out there are too many of them, we can let others (e.g. the competition organizers) do the sub-sampling themselves and by their own criteria.
>>
>> In other parts of the library it turned out that we had a bunch of duplicates with different file names (e.g. QF_BV/sage2 if I remember correctly). If there's an easy way for you to filter those, that would be nice.
>
> Finally! I have the first version of the benchmarks for consideration.
> I'm sorry that this took so long. I had a lot of false starts.
>
> Good call on asking me to remove duplicates (I used the fdupes tool 
> for this). This found a bug in my tool because it is supposed to cache 
> query results so for a single run of my tool there should have been no 
> duplicates but it turns out were some!
>
> They are available at
> https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fwww.doc
> .ic.ac.uk%2F~dsl11%2Fassets%2Fqf_fpabv_qf_fpbv_liew_v0.tar.xz&data=02%
> 7C01%7Ccwinter%40microsoft.com%7C6934291fa4e5474895b508d48e35c074%7C72
> f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C636289808891405673&sdata=zwV1
> %2BZ7AfrReAAP12IMRTNyx9Xw9WS25FrZMhrn44mw%3D&reserved=0
>
> These have been annotated with
>
> * The logic
> * Satisfiability if known. This was determined by running Z3 and
> Mathsat5 on the benchmarks before doing any annotation. I suspect the 
> `QF_FPABV` logic annotation might confuse the solvers but I've not 
> tried. I allowed at most 30 minutes per query
> * A note regarding a corresponding equisatisfiable query if it exists
>
> A few statistics:
>
> Number of benchmarks by logic:
> QF_FPABV: 18033 benchmarks
> QF_FPBV: 17156 benchmarks
>
> Number of benchmarks by satisfiability:
> 28099 sat benchmarks
> 7070 unsat benchmarks
> 20 unknown benchmarks
>
> Please take a look and let me know if you find any problems. If you or 
> others wish to remove benchmarks please discuss this with me first.
> Doing so without care will breaks the comments in the benchmarks 
> noting about corresponding equisatisfiable benchmarks in the other 
> logic.

I don't know if you've had a chance to look yet but I noticed I didn't attribute all the authors of the benchmarks that I should have.
I've produced a revised version which fixes this which is available at the link below.

https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fwww.doc.ic.ac.uk%2F~dsl11%2Fassets%2Fqf_fpabv_qf_fpbv_liew_v1.tar.xz&data=02%7C01%7Ccwinter%40microsoft.com%7C6934291fa4e5474895b508d48e35c074%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C636289808891405673&sdata=qI3vCqNa%2FQgkuN7pAjptm%2FHV7UQaxMgGqnJiKSr1tMA%3D&reserved=0

I'm keen to get feedback on this so please take a look. Again if you'd like me to trim down the number of benchmarks I'm happy to do this but I need to the okay from Christoph because he will become the owner of these benchmarks.

Thanks,
Dan.