[SMT-LIB] QF_BV and division by zero

[Aina Niemetz]

Configurable does not only require both implementations, it also is more
error prone as the user has to be aware of the fact that both options
exist and which option the solver chooses by default.

Even though we (the Boolector team) could unfortunately not participate
in the discussion at this year's SMT workshop, as you might already
know, we're strong supporters of the proposed solution.
Hence, another +1 from me :D

Aina


On 10/15/2015 01:38 PM, Christoph Wintersteiger wrote:
> Configurable is even worse, it requires both implementations :)
> 
> At some time in the past I suggested to add a mandatory option so
> that users who don't specify anything will get a warning message
> prompting them to choose one of the semantics, some of which can be
> left unsupported by solver developers.
> 
> I'm also unhappy with fp.min/fp.max. It's the same issue, but in that
> case the decision went toward unspecified results in the end, but
> it's the only proper FPA function that is partially unspecified
> (except the conversion terms to other theories).
> 
> Uninterpreted functions can always be wrapped around the terms
> division terms, so if solvers support UFs, users can customize to
> whatever semantics they prefer. As long as the theory definition is
> clear about that, there shouldn't be any problem with that.
> 
> 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-lib-bounces at cs.nyu.edu
> [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Florian Schanda 
> Sent: 15 October 2015 11:22 To: smt-lib at cs.nyu.edu Subject: Re:
> [SMT-LIB] QF_BV and division by zero
> 
> On Wednesday 14 Oct 2015 22:08:01 Clark Barrett wrote:
>> We've had many discussions about the semantics of division by zero
>> in the bit-vector theory.  After the most recent discussion at the
>> SMT workshop, it became clear that the arguments for fixing an 
>> interpretation seem to outweigh the arguments for the current 
>> semantics.  So, we are proposing to change the semantics of
>> bit-vector division so that division by zero produces a vector of
>> all 1's.  The rationale is:
> 
> Hm, not sure I am totally convinced, I've always been more happy with
> the current "uninterpreted function" behaviour. But I do certainly
> see *why* solver writers might prefer the fixed interpretation.
> 
> This issue is very similar to the fp.min and fp.max issue to me;
> could we not use a similar solution (i.e. make it configurable)?
> 
> Florian _______________________________________________ SMT-LIB
> mailing list SMT-LIB at cs.nyu.edu 
> https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.cs.nyu.edu%2fmailman%2flistinfo%2fsmt-lib&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7ce4c9c4580229436a315808d2d54abd6a%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=fG5LMaAb6YhRrehLP2B%2fTWh3GjJ3gPSFrW%2bEd2hfztk%3d
>
> 
_______________________________________________
> SMT-LIB mailing list SMT-LIB at cs.nyu.edu 
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-lib/attachments/20151015/4c44edb4/attachment.asc>