[SMT-COMP] SMT-COMP 2016: Benchmarks in 2.0 and 2.5 Formats

[Giles Reger]

We would also appreciate a final word from the organisers on this topic.

By the way, I support Dejan’s previous suggestion as did some others e.g.

> Basically we have benchmarks that the establishment can solve and there is
> some consensus that the solutions are correct. But, since we have the
> computational power and time, there is no reason not to run the competition
> on all benchmarks, even those with status unknown. It should be possible to
> compute for each solver the number of solved problems:
> 
> N1 = form the "known" set,
> N2 = from the "unknown" set where also all other successful solvers
> concur,
> N3 = from the "unknown" set where no other solver concurs.
> 
> This gives a choice scoring over N1 (conservative), N1+N2 (moderate), or
> N1+N2+N3 (liberal).
> 
> I don't see any reason not to use the moderate scoring. Although the
> liberal score is appealing, and I would support it, it's hard to see a
> viable path to nomination in 2016. But, I would still like to see it at
> least presented in the competition results.


This will obviously require more time but if it is available then this approach seems to make the most sense to me.

Best,
Giles

> On 26 May 2016, at 18:47, Dejan Jovanović <dejan.jovanovic at sri.com> wrote:
> 
> Tjark,
> 
> There are thousands of new benchmarks, particularly in the bit-vector
> category (e.g QF_BV/Sage2 17471 benchmarks) . As far as we saw they are
> marked as "unknown".
> 
> You haven't really responded to the "unknown" status issue. This is
> important. From the discussion and talking with people it's clear that
> relying on "known" benchmarks only is detrimental to competition.
> 
> Can you please give the final word on this. Will only the "known"
> benchmarks be used in the competition?
> 
> Best, Dejan
> 
> On Wed, May 25, 2016 at 3:03 PM Tjark Weber <tjark.weber at it.uu.se> wrote:
> 
>> On Wed, 2016-05-25 at 13:41 -0700, Clark Barrett wrote:
>>> I think the situation is actually much better than advertised.  I
>>> believe that the *only* feature of smt-lib 2.5 (versus 2.0) being
>>> used is representing quotes-within-quotes as "" instead of \" and
>>> this only happens in a few benchmarks and only in their source
>>> attribute.
>>> 
>>> So, if the SMT-COMP scrambler strips the source attribute, then *all*
>>> benchmarks should be fully smt-lib 2.0 compliant.  Please do let me
>>> know if anyone finds a counter-example to this claim, but if it is
>>> true, then I think there should not be an version issue for the
>>> competition.
>> 
>> As far as I can see after grepping over the entire SMT-LIB, this
>> accurately describes the current situation. Moreover, version 2.0
>> escape sequences \" and \\ do not seem to appear anywhere.
>> 
>> The competition scrambler (which is now available at
>> http://smtcomp.sourceforge.net/2016/tools.shtml) has been revised to
>> support "" within strings. Since the scrambler strips the :source
>> attribute, solvers should never see "" as an escape sequence. Thus,
>> this difference between 2.0 and 2.5 should be immaterial for the
>> competition.
>> 
>> Please let me know if your own testing reveals any related issues.
>> 
>> Best,
>> Tjark
>> _______________________________________________
>> SMT-COMP mailing list
>> SMT-COMP at cs.nyu.edu
>> http://cs.nyu.edu/mailman/listinfo/smt-comp
>> 
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp