如何摆脱 SBV 中 -0.0 的解决方案

Question

以下代码（使用 SBV）：

{-# LANGUAGE ScopedTypeVariables #-}
import Data.SBV
main :: IO ()
main = do
    res <- allSat zeros
    putStrLn $ show res

zeros :: Predicate
zeros = do
    z1 <- sDouble "Z1"
    constrain $ z1 .== 0.0
    return true

生成两种解决方案：

Solution #1:
  Z1 = 0.0 :: SDouble
Solution #2:
  Z1 = -0.0 :: SDouble
Found 2 different solutions.

如何消除无趣的-0.0 解决方案？我不能使用z1 ./= -0.0，因为当z1 是0.0 时也是如此。

Answer 1

[在 Hackage (http://hackage.haskell.org/package/sbv) 上发布 SBV 4.4 后更新，提供了适当的支持。]

假设您的 SBV >= 4.4，您现在可以这样做：

Prelude Data.SBV> allSat $ \z -> z .== (0::SDouble)
Solution #1:
  s0 = 0.0 :: Double
Solution #2:
  s0 = -0.0 :: Double
Found 2 different solutions.
Prelude Data.SBV> allSat $ \z -> z .== (0::SDouble) &&& bnot (isNegativeZeroFP z)
Solution #1:
  s0 = 0.0 :: Double
This is the only solution.

Answer 2

基于 cmets，以下代码仅产生一个解决方案：

zeros :: Predicate
zeros = do
    z1 <- sDouble "Z1"
    constrain $ z1 .== 0.0 &&& ((1 / z1) .> 0)
    return true

输出：

Solution #1:
  Z1 = 0.0 :: SDouble
This is the only solution.