[SMT-COMP] 回复：SMT-COMP Digest, Vol 78, Issue 2

[简简单单]

TD

---原始邮件---
发件人:"smt-comp-request"<smt-comp-request at cs.nyu.edu>
发送时间:2017年3月18日 星期六 上午0:2
收件人:"smt-comp"<smt-comp at cs.nyu.edu>
主题:SMT-COMP Digest, Vol 78, Issue 2
Send SMT-COMP mailing list submissions to
smt-comp at cs.nyu.edu
To subscribe or unsubscribe via the World Wide Web, visit
http://cs.nyu.edu/mailman/listinfo/smt-comp
or, via email, send a message with subject or body 'help' to
smt-comp-request at cs.nyu.edu
You can reach the person managing the list at
smt-comp-owner at cs.nyu.edu
When replying, please edit your Subject line so it is more specific
than "Re: Contents of SMT-COMP digest..."
Today's Topics:
1. Contribution of QF_FPBV and QF_FPABV benchmarks (Delcypher)
----------------------------------------------------------------------
Message: 1
Date: Fri, 17 Mar 2017 13:39:00 +0000
From: Delcypher <delcypher at gmail.com>
To: "smt-comp at cs.nyu.edu" <smt-comp at cs.nyu.edu>
Subject: [SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks
Message-ID:
<CANNJ_zjAGB0uY3Dh8-t+JHxUzDWLCrY2fW9R7r2Q_ohPSDJXpA at mail.gmail.com>
Content-Type: text/plain; charset=UTF-8
Hi,
I just saw the call for benchmarks.
I'd like to state I intend to contribute a set of benchmarks
* Some QF_FPBV benchmarks
* A new category that I suggested some time ago that mixes the
theories of quantifier free floating point and arrays of bitvectors. I
suggest the name QF_FPABV
I should have preliminary version of these benchmarks available in the
next few days.
A few 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.
* Some benchmarks may use Z3's non-standard fp.to_ieee_bv function. Is
that a problem?
* 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?
* Many benchmarks do not have a known answer. Is that a problem?
* 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?).
Thanks,
Dan.
------------------------------
_______________________________________________
SMT-COMP mailing list
SMT-COMP at cs.nyu.edu
http://cs.nyu.edu/mailman/listinfo/smt-comp
End of SMT-COMP Digest, Vol 78, Issue 2
***************************************