[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Clark Barrett]

We have not really enforced such limits in the past, but since you asked...
:)

I think that a sample of no more than 1000 benchmarks in each of QF_FPBV
and QF_FPABV would be great!

-Clark

On Thu, Apr 20, 2017 at 6:19 PM, Delcypher <delcypher at gmail.com> wrote:

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