[SMT-LIB] Idea: fp.to_ieee_bv as extension to FloatingPoint theory

[Delcypher]

Hi,

This follows on from a discussion on the smt-comp mailing list [1].
This is a proposal to add a function `fp.to_ieee_bv` to the
FloatingPoint theory [2].

# TL;DR

`fp.to_ieee_bv` is a total function (based on Z3's `fp.to_ieee_bv`)
that takes a floating point sort and as output gives the binary
IEEE-754 encoding of that floating point sort as bitvector.

# Why do I want this?

The reason for wanting this function is in my tool I have to handle
bitcasts in C programs. In these programs bitcasts between integers
(i.e. BitVector sort) and floating point variables may occur. An
example is the `signbit()` function that examines the sign bit of the
floating point variable.

The FloatingPoint theory standard currently suggests to handle this by
introducing a fresh bitvector variable and an additional assertion
that the fresh bitvector converted to a floating point sort is equal
to the expression that I wish to convert to Bitvector sort.

I find this rather cumbersome. It makes queries harder to read and write.

# fp.to_ieee_bv

The function `fp.to_ieee_bv` converts a floating point sort to a
bitvector sort using the IEEE-754 binary encoding. To be a total
function if the argument to the function is a NaN it picks the
encoding of a quiet NaN (from IEEE-754 2008) with the following
additional constraints

- The sign bit is 0
- In the trailing significand field only the most significant bit is
set 1, the rest are set to zero.

This choice is arbitrary and I'd happy for it to be something else
provided there are good reasons.

Although we could make `fp.to_ieee_bv` a partial function (i.e. have
it undefined for NaN inputs) I worry we'd hit issues like we have with
`bvudiv` (i.e. division by zero).

This function provides a convenient way to do conversion that works
well provided the user is willing to accept only a single encoding for
NaN is considered. If the user wants multiple encodings to be
considered they would need to use the fresh variable approach
suggested in [2].

# Final thoughts

I don't feel that strongly about this idea so I won't fight for it but
I think it would be good to discuss it.


[1] http://cs.nyu.edu/pipermail/smt-comp/2017/000436.html
[2] http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml

Thanks,
Dan