Implementing the sign of NaN?

[aqjune]

Currently, Alive2 does not distinguish between +NaN and -NaN:

https://alive2.llvm.org/ce/z/8TB3fv

I found that there are a few library functions in C that safely deals with the sign of NaN:

• signbit: https://en.cppreference.com/w/cpp/numeric/math/signbit
• copysign: https://en.cppreference.com/w/cpp/numeric/math/copysign

Z3 does not seem to support signed NaNs (maybe all SMT solvers don't?); would there be an efficient way to implement them in Alive2?

[nunoplopes]

Is this any useful in practice? i.e., does any optimization require it?

[aqjune]

I briefly looked through InstCombine and it had a few optimizations on copysign.
But, defining copysign(NaN) to nondeterministically return either +1 or -1 was sufficient to explain them.
Their validities were not affected by the signlessness of Alive2 NaN.

So maybe for doing translation validation the abstraction is fine, but it is just my guess.