[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Bruno Dutertre]

On 03/23/2017 02:52 PM, Clark Barrett 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.
>
> * 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.
>
> * 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.
>
> * 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.
>
> * 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
>

Clark,

These instructions require pre-amble:

(set-logic <logic>)
(set-info :source |<description>|)
(set-info :smt-lib-version <version>)
(set-info :category <category>)
(set-info :status <status>)

The version information should come earlier because it affects parsing of
|<description>|. SMT-LIB 2.0 was pure ASCII and SMT-LIB 2.5 is not. What's
allowed in a |<description>| by version 2.5 is not the same as what's
allowed in 2.0.

Bruno



> -Clark
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4049 bytes
Desc: S/MIME Cryptographic Signature
URL: </pipermail/smt-comp/attachments/20170323/205ca1ad/attachment.p7s>