[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Delcypher]

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.