[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Christoph Wintersteiger]

Hi Dan, Clark, all,

Thanks Clark for the detailed answer! 

In addition to what Clark said, it may be helpful to know that benchmarks without status annotation won't be used in the SMT competition (afaik), so if you are reasonably confident of the status, please do add it. 

Regarding Z3's fp.to_ieee_bv, here is what the FP theory definition says:

:note
 "There is no function for converting from (_ FloatingPoint eb sb) to the
  corresponding IEEE 754-2008 binary format, as a bit vector (_ BitVec m) with 
  m = eb + sb, because (_ NaN eb sb) has multiple, well-defined representations.
  Instead, an encoding of the kind below is recommended, where f is a term
  of sort (_ FloatingPoint eb sb):

   (declare-fun b () (_ BitVec m))
   (assert (= ((_ to_fp eb sb) b) f))
 "

So, a quick dirty hack is to simply replace all occurrrences of fp.to_ieee_bv with new, uninterpreted functions. If your infrastructure makes it easy to add the additional assertions/constraints on them you could add those too. Of course, semantics for NaNs may be different, but that may not be important in the context of SMTLIB. 

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | https://www.microsoft.com/en-us/research/people/cwinter/


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-comp-bounces at cs.nyu.edu [mailto:smt-comp-bounces at cs.nyu.edu] On Behalf Of Clark Barrett
Sent: 23 March 2017 21:53
To: Delcypher <delcypher at gmail.com>
Cc: smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

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
_______________________________________________
SMT-COMP mailing list
SMT-COMP at cs.nyu.edu
http://cs.nyu.edu/mailman/listinfo/smt-comp