[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

Fri Apr 7 07:39:18 EDT 2017

Hi,

> 1. Are there any file naming conventions that I need to follow?

No hard constraints there. Pick something that makes it easy to remember where the benchmarks came from so that it's easy to get a rough guess of what's in them. 

> 2. What directory structure should I use? Currently I have
> QF_*/<source_benchmark>/query_DDDD.smt2

I like QF_*/surname/project-or-paper-name (like in QF_FP). 

I'm not sure there's a :description field; it's usually :source, e.g.:

(set-info :source |Name <email> These are the benchmarks for our ... paper.|)

Regarding unsat annotations: I think in the past the strategy was to label only those benchmarks with sat/unsat if we are reasonably sure that this is what they actually are. I personally don't fully agree with that policy either (for the same reason as you do), but I'm not sure everybody is ok with relaxing that rule ��

Regarding actual submission: Either; wait for an account or just send them to me via e-mail or make them available for download somewhere. I'll take care of the rest then. (I'm assuming I'll be responsible for those repositories.) 

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 Delcypher
Sent: 07 April 2017 11:39
To: Clark Barrett <barrett at cs.stanford.edu>
Cc: smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

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 "unknown1" 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://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fclc-g
> itlab.cs.uiowa.edu%3A2443%2FSMT-LIB-benchmarks-tmp%2Fbenchmarks-pendin
> g&data=02%7C01%7Ccwinter%40microsoft.com%7C3b3add4bd3b84455bfcb08d47da
> 28d5b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636271584509173947&
> sdata=mxprSFIXoxdjtivYjBf4nItFaBIMBE%2FAqamr92UWc40%3D&reserved=0

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.
_______________________________________________
SMT-COMP mailing list
SMT-COMP at cs.nyu.edu
https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fcs.nyu.edu%2Fmailman%2Flistinfo%2Fsmt-comp&data=02%7C01%7Ccwinter%40microsoft.com%7C3b3add4bd3b84455bfcb08d47da28d5b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636271584509173947&sdata=d8YEmk4FA1ux4vZXelvTlcNwVP6%2FpxRuU2FowgFzqCc%3D&reserved=0