diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs index f7564dff3..dea0ae32d 100644 --- a/Documentation/SBV/Examples/Misc/Floating.hs +++ b/Documentation/SBV/Examples/Misc/Floating.hs @@ -69,21 +69,21 @@ assocPlus x y z = x + (y + z) .== (x + y) + z -- -- >>> assocPlusRegular -- Falsifiable. Counter-example: --- x = -1.7478492e-21 :: Float --- y = 9.693523e-27 :: Float --- z = 5.595795e-20 :: Float +-- x = 4.4272205e21 :: Float +-- y = 2.9514347e20 :: Float +-- z = 4.4676022e15 :: Float -- -- Indeed, we have: -- --- >>> let x = -1.7478492e-21 :: Float --- >>> let y = 9.693523e-27 :: Float --- >>> let z = 5.595795e-20 :: Float +-- >>> let x = 4.4272205e21 :: Float +-- >>> let y = 2.9514347e20 :: Float +-- >>> let z = 4.4676022e15 :: Float -- >>> x + (y + z) --- 5.4210105e-20 +-- 4.722369e21 -- >>> (x + y) + z --- 5.421011e-20 +-- 4.722368e21 -- --- Note the difference in the results! +-- Note the significant difference in the results! assocPlusRegular :: IO ThmResult assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"] let lhs = x+(y+z) @@ -103,13 +103,13 @@ assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"] -- -- >>> nonZeroAddition -- Falsifiable. Counter-example: --- a = 7.135861e-8 :: Float --- b = 8.57579e-39 :: Float +-- a = 2.9670994e34 :: Float +-- b = -7.208359e-5 :: Float -- -- Indeed, we have: -- --- >>> let a = 7.135861e-8 :: Float --- >>> let b = 8.57579e-39 :: Float +-- >>> let a = 2.9670994e34 :: Float +-- >>> let b = -7.208359e-5 :: Float -- >>> a + b == a -- True -- >>> b == 0 @@ -158,30 +158,28 @@ multInverse = prove $ do a <- sFloat "a" -- -- >>> roundingAdd -- Satisfiable. Model: --- rm = RoundTowardZero :: RoundingMode --- x = 1.7499695 :: Float --- y = 1.2539366 :: Float +-- rm = RoundTowardPositive :: RoundingMode +-- x = -4.0039067 :: Float +-- y = 131076.0 :: Float -- -- (Note that depending on your version of Z3, you might get a different result.) -- Unfortunately Haskell floats do not allow computation with arbitrary rounding modes, but SBV's -- 'SFloatingPoint' type does. We have: -- --- >>> sat $ \x -> x .== (fpAdd sRoundTowardZero 1.7499695 1.2539366 :: SFloat) +-- >>> sat $ \x -> x .== (fpAdd sRoundTowardPositive (-4.0039067) 131076.0 :: SFloat) -- Satisfiable. Model: --- s0 = 3.003906 :: Float --- >>> sat $ \x -> x .== (fpAdd sRoundNearestTiesToEven 1.7499695 1.2539366 :: SFloat) --- Satisfiable. Model: --- s0 = 3.0039063 :: Float +-- s0 = 131072.0 :: Float +-- >>> (-4.0039067) + 131076.0 :: Float +-- 131071.99 -- --- We can see why these two results are indeed different: The 'RoundTowardZero' --- (which rounds towards the origin) produces a smaller result, closer to 0. Indeed, if we treat these numbers --- as 'Double' values, we get: +-- We can see why these two results are indeed different: The 'RoundTowardPositive +-- (which rounds towards positive infinity) produces a larger result. -- --- >>> 1.7499695 + 1.2539366 :: Double --- 3.0039061 +-- >>> (-4.0039067) + 131076.0 :: Double +-- 131071.9960933 -- --- we see that the "more precise" result is smaller than what the 'Float' value is, justifying the --- smaller value with 'RoundTowardZero. A more detailed study is beyond our current scope, so we'll +-- we see that the "more precise" result is larger than what the 'Float' value is, justifying the +-- larger value with 'RoundTowardPositive. A more detailed study is beyond our current scope, so we'll -- merely note that floating point representation and semantics is indeed a thorny -- subject, and point to as -- an excellent guide. diff --git a/SBVTestSuite/GoldFiles/allSat6.gold b/SBVTestSuite/GoldFiles/allSat6.gold index a8b19fb02..78593e0ce 100644 --- a/SBVTestSuite/GoldFiles/allSat6.gold +++ b/SBVTestSuite/GoldFiles/allSat6.gold @@ -1,10 +1,10 @@ Solution #1: - x = 1 :: Word8 - y = 2 :: Word8 -Solution #2: x = 0 :: Word8 y = 2 :: Word8 -Solution #3: +Solution #2: x = 0 :: Word8 y = 1 :: Word8 +Solution #3: + x = 1 :: Word8 + y = 2 :: Word8 Found 3 different solutions. \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/noOpt1.gold b/SBVTestSuite/GoldFiles/noOpt1.gold index 209bbd709..cf06ae25a 100644 --- a/SBVTestSuite/GoldFiles/noOpt1.gold +++ b/SBVTestSuite/GoldFiles/noOpt1.gold @@ -28,4 +28,4 @@ *** Use "sat" for plain satisfaction CallStack (from HasCallStack): - error, called at ./Data/SBV/Provers/Prover.hs:263:27 in sbv-11.0-inplace:Data.SBV.Provers.Prover \ No newline at end of file + error, called at ./Data/SBV/Provers/Prover.hs:264:27 in sbv-11.0-inplace:Data.SBV.Provers.Prover \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/noOpt2.gold b/SBVTestSuite/GoldFiles/noOpt2.gold index 36f659fe7..924b10b75 100644 --- a/SBVTestSuite/GoldFiles/noOpt2.gold +++ b/SBVTestSuite/GoldFiles/noOpt2.gold @@ -30,4 +30,4 @@ *** Use "optimize"/"optimizeWith" to calculate optimal satisfaction! CallStack (from HasCallStack): - error, called at ./Data/SBV/Provers/Prover.hs:610:33 in sbv-11.0-inplace:Data.SBV.Provers.Prover \ No newline at end of file + error, called at ./Data/SBV/Provers/Prover.hs:611:33 in sbv-11.0-inplace:Data.SBV.Provers.Prover \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/validate_2.gold b/SBVTestSuite/GoldFiles/validate_2.gold index cc6a1b5f8..760457b35 100644 --- a/SBVTestSuite/GoldFiles/validate_2.gold +++ b/SBVTestSuite/GoldFiles/validate_2.gold @@ -26,11 +26,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (_ +zero 8 24))) +[RECV] ((s0 (fp #b0 #x00 #b00000001001110100110010))) *** Solver : Z3 *** Exit code: ExitSuccess [VALIDATE] Validating the model. Assignment: -[VALIDATE] x = 0.0 :: Float +[VALIDATE] x = 5.6391e-41 :: Float [VALIDATE] There are no constraints to check. [VALIDATE] Validating outputs. @@ -39,7 +39,7 @@ FINAL OUTPUT: *** *** Assignment: *** -*** x = 0.0 :: Float +*** x = 5.6391e-41 :: Float *** *** Floating point FMA operation is not supported concretely. *** @@ -49,4 +49,4 @@ FINAL OUTPUT: *** Alleged model: *** *** Satisfiable. Model: -*** x = 0.0 :: Float +*** x = 5.6391e-41 :: Float