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

Florian Schanda florian.schanda at altran.com
Tue Mar 1 03:46:31 EST 2016


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.

	Florian


More information about the SMT-LIB mailing list