CODEWITHSUNDEEP
haskellsmt
MichalAntkiew
MichalAntkiew

Reputation: 93

How to get rid of solutions with -0.0 in SBV

The following code (using 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

generates two solutions:

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

How do I eliminate the uninteresting -0.0 solution? I cannot use z1 ./= -0.0 because it is also true when z1 is 0.0.

Upvotes: 3

Views: 112

Answers (2)

alias
alias

Reputation: 30525

[Updated after SBV 4.4 release on Hackage (http://hackage.haskell.org/package/sbv), which provides proper support.]

Assuming you have SBV >= 4.4, you can now do:

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.

Upvotes: 3

MichalAntkiew
MichalAntkiew

Reputation: 93

Based on the comments, the following code produces only a single solution:

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

Output:

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

Upvotes: 1

Related Questions