Unsoundness with powers

[kunalsheth]

Correct case ($2^{-1074}$):

(declare-fun x () Real)
(assert (= x (^ 0.5 1074.0)))
(assert (> x 0))
(check-sat)

dReal v4.21.06.1 returns:

delta-sat with delta = 0.001
x : [4.9406564584124654e-324, 4.9406564584124654e-324]

Unsound case ($2^{-1075}$):

(declare-fun x () Real)
(assert (= x (^ 0.5 1075.0)))
(assert (> x 0))
(check-sat)

dReal v4.21.06.1 returns:

unsat

The threshold of 1075 (approx. 1024) reminds me of floating point FTZ/DAZ, I will look into that too.
z3 and cvc5 both return SAT, but their internal representation is as a rational of two integers.
dReal3 also has this issue, but the threshold is between 100 and 101.

EDIT:

1. 1075 makes sense for a FP FTZ/DAZ issue. See https://stackoverflow.com/questions/79359588/with-ieee-754-floating-point-numbers-is-underflow-still-better-than-overflow

[kunalsheth]

Definitely seems like FTZ/DAZ is enabled (the threshold is exactly 1023 when using RealConstant/interval bases), although fixing that alone just kicks the can down the road, still need to add special check for underflow with powers.

Probably a GAOL/FILIB issue?
pow function should never let the interval go to zero if the base was not zero to begin with.
I can add a check, and force the interval to always be at least the smallest possible non-zero width.

(set-logic QF_NRA)
(declare-fun x () Real)
(declare-fun y () Real [1.999999999, 2.000000001])
(assert (= x (^ y -1022.99999)))
(assert (> x 0))
(check-sat)
--------------------------------------------------
delta-sat with delta = 0.001
x : [4.9406564584124654e-324, 2.2250738585072014e-308]
y : [1.9999999989999999, 2.0000000010000001]

(set-logic QF_NRA)
(declare-fun x () Real)
(declare-fun y () Real [1.999999999, 2.000000001])
(assert (= x (^ y -1023.0)))
(assert (> x 0))
(check-sat)
--------------------------------------------------
unsat

Interestingly, both dReal3 and dReal4 have the exact same threshold (1023) when using interval bases, but different thresholds when using constant bases— there might be multiple separate-but-related bugs in both GAOL/FILIB and also the solvers' symbolic preprocessing evaluators.

[kunalsheth]

TODO: Look into how FTZ/DAZ and underflow may affect other computations. Interval libraries use fenv upward rounding modes to guarantee correctness, but FTZ/DAZ can cause things to round down.

TODO: Add underflow case check to GAOL/FILIB power operations.