[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Clark Barrett]

Good point.  I will modify the instructions.

-Clark

On Thu, Mar 23, 2017 at 5:44 PM, Bruno Dutertre <bruno.dutertre at sri.com>
wrote:

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