[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Cesare Tinelli]

Hi all,

On 21 Apr 2017, at 10:06, Christoph Wintersteiger wrote:

> Hi Dan,
>
> Space is free,
>
That is, payed for by someone else :)  (The SMT-LIB coordinators, 
StarExec, etc.)

> 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.
>
Depending on how big the benchmark submission is, it may actually be 
necessary to create a selection for SMT-LIB, as opposed to just 
SMT-COMP.

We have moved the master copy of the SMT-LIB benchmarks to a GitLab 
server (at Iowa, with a mirror at INRIA, to be announced officially 
soon). While this is ultimately going to be more convenient for 
everybody, git does not work very well with very large repositories or 
very large files. So, although disk space is not necessarily a concern, 
the size of a repository is.

Perhaps Dan can still send all of his benchmarks to Christoph, and then 
we can work on a sample internally for SMT-LIB inclusion.


Cesare



> 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.
>
> Cheers,
> Christoph
>
> -----Original Message-----
> From: Delcypher [mailto:delcypher at gmail.com]
> Sent: 21 April 2017 02:20
> To: Clark Barrett <barrett at cs.stanford.edu>; Christoph Wintersteiger 
> <cwinter at microsoft.com>
> Cc: smt-comp at cs.nyu.edu
> Subject: Re: [SMT-COMP] Contribution of QF_FPBV and QF_FPABV 
> benchmarks
>
> Hi,
>
>
> On 23 March 2017 at 21:52, Clark Barrett <barrett at cs.stanford.edu> 
> wrote:
>> Hi Dan,
>>
>> Let me try to answer your questions.
>>
>> * Do I need to curate these benchmarks in some way. If so what
>> criteria should I use? E.g. Should I pick the longest running? I have
>> quite a few benchmarks (~ 8000) so having that many might not be
>> desirable.
>>
>> This is really up to you, but generally my hope would be a set of
>> benchmarks that does a good job of representing all the diversity of
>> the entire set of benchmarks.  If this means you can prune some,
>> great.  But you should be sure to include representatives from
>> different difficulty levels, different sizes, different statuses, 
>> different applications etc.
>
> I've now collected my initial queries from my tool (removing uses of 
> `fp.to_ieee_bv`). The numbers are
>
> QF_FPBV: 18110
> QF_FPABV: 19041
>
> This is rather a lot of queries.  My plan is to compute several 
> different distributions (e.g. distribution of execution times) and 
> semi-randomly sample from them to reduce the number. To do this I need 
> to know roughly how many queries I should be submitting. Any opinions 
> on this?
>
> Thanks,
> Dan.
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp