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

[Martin Brain]

On Tue, 2016-03-01 at 08:46 +0000, Florian Schanda wrote:
> On Monday 29 Feb 2016 16:30:59 Martin Brain wrote:
> > That rather depends on what semantics you are intending them to have.  I
> > presume you want the IEEE-754 semantics:
> 
> Yes, indeed. I think asking for anything not IEEE-754 would not be helpful ;)
> 
> > Are there use cases for these beyond Ada?
> 
> If I remember right then math.h defines a nextafter that you can use to get to 
> this in a portable way, so there is some use-case in C/C++ as well.

As I understand it (I am not an / the authority here) the following
criteria need to be met for addition to the standard:

1. Are the functions / relations clearly additions to an existing theory
rather than needing a new one (at the risk of crossing threads : I think
cardinality constraints should be a new theory).

2. Is there a consensus agreement on the semantics?

3. Can the proposed function / relation be expressed using existing
ones?  If so, is there an advantage to having them as a distinct
function / relation (for example, allows better decision procedures to
be used).

4. Are there clear use-cases and users who want to pursue them?  Are
they willing to contribute non-trivial benchmarks including these to
SMT-LIB?

5. Are there solver authors who are willing to implement them.


In this case I think 1 and 2 are met.  I think there may be a way of
encoding these via an FMA  (v * 0x1.00002p-24 + v w/ RNE ?) plus some
ITEs but this introduces a lot of overhead for what could be a simple
operation, which means that 3 is met unless anyone else can come up with
a better encoding.  For 4. I can provide weak support for by saying that
CPROVER might add support for nextafter et al. in the C library if there
was end-user demand and we might support it like this.  Finally, 5., I
don't see a major problem with adding support to CVC4.

What do other people think?  SMT-LIB is a community consensus standard
and I really don't speak for everyone.

Cheers,
 - Martin