[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Clark Barrett]

Thanks for the answers Christoph.  See additional thoughts from me inline
below.

On Fri, Apr 7, 2017 at 4:39 AM, Christoph Wintersteiger <
cwinter at microsoft.com> wrote:

> Hi,
>
> > 1. Are there any file naming conventions that I need to follow?
>
> No hard constraints there. Pick something that makes it easy to remember
> where the benchmarks came from so that it's easy to get a rough guess of
> what's in them.
>

Agreed.


> > 2. What directory structure should I use? Currently I have
> > QF_*/<source_benchmark>/query_DDDD.smt2
>
> I like QF_*/surname/project-or-paper-name (like in QF_FP).
>

The directory structure you propose is fine, as is the one proposed by
Christoph.  Documentation should be within the :source field of the
benchmark, so it's not required for the directory structure to document
that in a particular way.


> I'm not sure there's a :description field; it's usually :source, e.g.:
>
> (set-info :source |Name <email> These are the benchmarks for our ...
> paper.|)
>

That's right.  The ":source" field should include all of the information
requested on the benchmarks-pending page here:
https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-tmp/benchmarks-pending
This is also the place to include any additional comments (such as the
correspondence between two different encodings of the same problem).
Basically, treat this field as the full documentation for the benchmark.


> Regarding unsat annotations: I think in the past the strategy was to label
> only those benchmarks with sat/unsat if we are reasonably sure that this is
> what they actually are. I personally don't fully agree with that policy
> either (for the same reason as you do), but I'm not sure everybody is ok
> with relaxing that rule ��
>

As mentioned elsewhere, a status annotation other than "unknown" should
only be included if you are *very* confident.  Our goal for SMT-LIB is to
have 100% accuracy in status attributes.  Any "speculations" on the status
can be included as a comment in the source annotation.


> Regarding actual submission: Either; wait for an account or just send them
> to me via e-mail or make them available for download somewhere. I'll take
> care of the rest then. (I'm assuming I'll be responsible for those
> repositories.)
>

Right now, we don't plan on giving write-access accounts to anyone except
the benchmark maintainers (partly because benchmark repositories can get
really big, so pull requests are not a great mechanism).  Sending them to a
maintainer or making them available for download are both good options.

-Clark