[SMT-LIB] Feature request: nextUp and nextDown in FP

[Martin Brain]

On Mon, 2016-02-29 at 15:52 +0000, Florian Schanda wrote:
> Hi Martin, Cesare,
> 
> I would like to feature request (at low priority) nextUp and nextDown to 
> appear in the FP theory. They seem like a fairly obvious addition, and for 
> example in languages such as SPARK and Ada you do have access to them 
> directly.
> 
> Are there any difficulties I am missing?

That rather depends on what semantics you are intending them to have.  I
presume you want the IEEE-754 semantics:

<quote>
nextUp(x) is the least floating-point number in the format of x that
compares greater than x. If x is the negative number of least magnitude
in x’s format, nextUp(x) is −0. nextUp(±0) is the positive
number of least magnitude in x’s format. nextUp(+∞) is +∞, and
nextUp(−∞) is the finite negative number largest in magnitude. When x is
NaN, then the result is according to 6.2. nextUp(x) is quiet except for
sNaNs.  The preferred exponent is the least possible.  nextDown(x) is
−nextUp(−x).
</quote>

(where 6.2, for the purposes of SMT-LIB, says "it will return NaN")

Are there use cases for these beyond Ada?

Cheers,
 - Martin