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

[Clark Barrett]

Hi all,

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.

-Clark

On Wed, May 25, 2016 at 8:08 AM, Christoph Wintersteiger <
cwinter at microsoft.com> wrote:

> Hi all,
>
> I think for the purpose of the competition this little detail really
> doesn't make much of a difference. We could simply sed "s/\"/_/g" all of
> them before passing them to the solvers. Or, perhaps even easier, just
> strip the whole (set-info :source ...) command. I'm not aware of any such
> issues in other commands, at least not in the SMTLIB benchmarks.
>
> Cheers,
> Christoph
>
> Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44
> 1223 479999 | research.microsoft.com/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 Tjark Weber
> Sent: 25 May 2016 15:25
> To: David Deharbe <david.deharbe at clearsy.com>; Bruno Dutertre <
> bruno.dutertre at sri.com>
> Cc: Sylvain Conchon <Sylvain.Conchon at lri.fr>; smt-comp at cs.nyu.edu
> Subject: Re: [SMT-COMP] SMT-COMP 2016: Benchmarks in 2.0 and 2.5 Formats
>
> On Wed, 2016-05-25 at 09:50 +0200, David Deharbe wrote:
> > This request sounds perfectly reasonable and poses a problem.
> >
> > In my opinion the changes should be coordinated with the SMT-LIB
> > maintainers. [...]
>
> The situation is even more convoluted. The SMT-COMP benchmark scrambler
> currently does not pass 'set-info' commands to the solver. At least in the
> case of the :source and :status attributes, this is for good reason.
>
> The scrambler could be modified to pass on 'set-info :smt-lib-version'
> commands only; but the SMT-COMP rules postulate that set-option and
> set-logic commands come first in benchmarks.
>
> I will investigate whether it would be feasible to provide all benchmarks
> in a form that is compatible with both 2.0 and 2.5.
> Otherwise, we may have to declare benchmarks that cause parsing
> problems/ambiguities ineligible for SMT-COMP 2016.
>
> Best,
> Tjark
>
> _______________________________________________
> 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=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c9ae01be1f0ab4322a1ef08d384a8706a%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=rJWHljdQidHS0rYSLyschomHj%2bpkaCgYbMrOH3ZVy08%3d
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>