[SMT-COMP] [SMT-LIB] SMT-COMP 2016: Draft Rules and Timeline Available

[Christoph Wintersteiger]

I agree, reducing the entry barrier is the most important reason I think. We had discussion about that in the past, but somehow they always end 50/50%. 

In my opinion, any undefined behavior can always be encoded into UFs or quantifiers (if your solver of choice supports it) and in pretty much all of those instances, the undefined behavior has been put in place for the very reason that we can't make that choice for the user. I think that forcing users to put those UFs where they need it is a good idea, as they need to be aware of those details, and internally I suppose most solvers do exactly the same anyways.  

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 Dejan Jovanovic
Sent: 17 May 2016 03:44
To: smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] [SMT-LIB] SMT-COMP 2016: Draft Rules and Timeline Available

Ok, I'll take it that handling division as in the standard is to be expected then.

It would be nice to have a discussion about this in the wider context of SMTLIB and undefined behavior. I see it less about the current solvers giving correct answers, and more about consistency and reducing the barrier to entry. As with bit-vectors it's not clear that this semantics for division are ideal. Also, we'd like to encourage people to do develop new solvers and participate, and addition of UF can be quite a burden if the solver doesn't already support it.

Does anyone else have an opinion on this?

Cheers, Dejan

On Sun, May 15, 2016 at 10:07 AM Tjark Weber <tjark.weber at it.uu.se> wrote:

> Dejan,
>
> On Sun, 2016-05-15 at 15:56 +0000, Dejan Jovanović wrote:
> > The issue is basically the same as in bit-vectors, i.e. to properly 
> > support it one has to involve extra reasoning with uninterpreted 
> > functions. Since the issue is the same as in bit-vectors, my 
> > thinking is that it would be best to use the same policy for 
> > inclusion in the competition.
>
> I understand the similarity with bit-vector division. However, 
> considering that these benchmarks have been used in past competitions 
> without apparent problems, I would be reluctant to exclude benchmarks 
> that use integer/real number division just on similarity grounds, and 
> without a wider discussion. (Also, it is not clear to me that we could 
> easily distinguish between guarded and unguarded use.)
>
> Are there solvers that handle unguarded (integer/real number) division 
> incorrectly, or SMT-LIB benchmarks that have been assigned an 
> incorrect status?
>
> > There was lots of discussion about it so I don't remember anymore, 
> > are bit-vector benchmarks with unguarded division included in the 
> > competition?
>
> Not in 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%7cca07bf3c2a2c4faf6cad08d37dff5911%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=zCD76BpKyWzBGdsuVNwYeRV1t%2bzYbK9diV298qKcHrA%3d