[SMT-LIB] QF_BV and division by zero

[Christoph Wintersteiger]

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