[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Delcypher]

Hi Clark,

Thanks for the detailed answers :)

> * Some benchmarks may use Z3's non-standard fp.to_ieee_bv function. Is
> that a problem?
>
> This is definitely a problem for including them in SMT-LIB.  You either need
> to make a case for extending the standard, find a way to encode the
> benchmarks with this construct in a different way, or we will have to
> exclude the benchmarks with this operator.

I may try to convert a few by hand but I guess I'll have to drop a whole bunch.

I'd really like to see some sort of `fp.to_ieee_bv` partial function
in SMT-LIB but I'll write up a separate post on this.

> * The QF_FPBV and QF_FPABV benchmarks will be very similar because
> they come from the same source (the QF_FPBV benchmarks are QF_FPABV
> benchmarks where we have been able to remove arrays using knowledge of
> our problem domain). Is this a problem?
>
> No - in fact it's often interesting to include the same benchmarks using
> different encodings.  Each set of benchmarks should explain that they come
> from the same source though, so people understand the relationship.

How would you like me to express this relationship? I guess I should
write something in the `:description` field.

> * Many benchmarks do not have a known answer. Is that a problem?
>
> We encourage you to set the status if it is known, but you can also submit
> benchmarks with unknown status.

Is it okay to put these "unknown" benchmarks as "unsat"? I really want
them included in the competition so solver
writers are encouraged to try improve performance on these difficult
benchmarks. If putting them as "unknown"
means they won't be used in the competition I'd rather just label them
as "unsat" and note in the description that
this has not been confirmed.

> * Are there any requirements about what needs to be in the pre-amble
> of the smt2 file? (.e.g Does the logic need to be stated?).
>
> Yes.  We recently set up a repository for benchmark submissions which
> includes instructions about the pre-amble.  Please refer to those
> instructions which are here:
> https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-tmp/benchmarks-pending

Thanks for this. It looks very helpful. I have a few other questions
that are not addressed by this document.

1. Are there any file naming conventions that I need to follow?
2. What directory structure should I use? Currently I have

QF_FPBV/<source_benchmark>/query_DDDD.smt2
QF_FPABV/<source_benchmark>/query_DDDD.smt2

where `<source_benchmark>` is some name that reflects the C program
that the constraints came from and `DDDD` is some integer. If there is
a `QF_FPABV` query that we managed to represent in `QF_FPBV` then
`DDDD` will be the same integer. The number `DDDD` does not necessary
increase in steps of 1 because the number is query number issued by my
tool and I will be cherry picking queries produced by my tool.

3. How do I perform the submission? Will you give me an account on
your gitlab instance so I can commit to your `benchmarks-pending`
repository?

Thanks,
Dan.