[SMT-LIB] QF_BV and division by zero

[Martin Brain]

On Thu, 2015-10-15 at 11:38 +0000, 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. 

In the case of fp.min/fp.max I believe it to be possible to create a
bitwise implementation that supports the (current) partially specified
semantics [ create four non-deterministic bits at "global" level and use
them for the sign of the output in the four min / max (-0,+0) / (+0,-0)
cases].  Then if you want to make it configurable, you can do so at the
'user' / encoder level by adding:

(assert (= (fp.min (_ +zero 8 24) (_ -zero 8 24)) (_ -zero 8 24) ))
; etc.

If you're feeling particularly swanky you can even have a small program
that runs on your target platform (with the right compiler, etc.
options) that prints out the four asserts so you can min and max like
your target platform.  In fact I'm half way tempted to write on for C...

> 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,

I'm unhappy with fp.min/fp.max as well and I am one of the people
directly responsible!  IMHO both should clearly be symmetric and fp.max
should give +0 and min -0 on the case of mixed sign zeros.  HOWEVER
that's not what IEEE-754 says and one of our goals was that any IEEE-754
implementation should be a model of the theory, so we have to live with
this annoying corner case.


>  but it's the only proper FPA function that is partially unspecified (except the conversion terms to other theories). 

This is an important point IMHO.  Bit-vector division and fp.max/fp.min
can be "fixed" but there are always going to be awkward cases, such as
the conversions, that are not well defined.  It will not be possible to
fix all of these, thus this should be (and so far, is) a conversation
about fixing particular cases.

Cheers,
 - Martin