Merge branch 'master' into InsertionSort

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 <http://ece.uwaterloo.ca/~dwharder/NumericalAnalysis/02Numerics/Double/paper.pdf> as
 -- an excellent guide.

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.

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
+  error, called at ./Data/SBV/Provers/Prover.hs:264:27 in sbv-11.0-inplace:Data.SBV.Provers.Prover

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
+  error, called at ./Data/SBV/Provers/Prover.hs:611:33 in sbv-11.0-inplace:Data.SBV.Provers.Prover

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

SMTSolverVersions.md

@@ -33,7 +33,7 @@ report any issues you might see with newer releases.
       * Version 2.6.2 as downloaded from the above site on Apr 7, 2020
   * Z3:
       * http://github.com/Z3Prover/z3
-      * Version as downloaded from the above site on Sep 20th, 2024
+      * Version as downloaded from the above site on Sep 23rd, 2024
       * SBV typically relies on latest features of z3, so compiling directly
         from the sources is recommended. If that's not possible, you should
         always use their latest release.