[SMT-LIB] QF_BV and division by zero

[Viktor Kuncak]

A clarification question: does IEEE FP standard enforce that multiple
executions with same arguments always yield the same result, even for the
cases where the result of the operation is unspecified?

Thanks,
  Viktor

On Tue, Oct 20, 2015 at 12:52 PM Martin Brain <martin.brain at cs.ox.ac.uk>
wrote:

> 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
>
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>