From 245e2ed3e72da7d0b8c86487b8a4a854ecb22ae2 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Sep 2024 07:52:48 -0700 Subject: [PATCH 1/2] Update z3 tested date --- SMTSolverVersions.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SMTSolverVersions.md b/SMTSolverVersions.md index 0f4bc11d7..72877c322 100644 --- a/SMTSolverVersions.md +++ b/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. From bca37e9970036a91d8089785f0db9bb55acb8546 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Sep 2024 07:53:18 -0700 Subject: [PATCH 2/2] Match new z3 output --- Documentation/SBV/Examples/Misc/Floating.hs | 54 ++++++++++----------- SBVTestSuite/GoldFiles/allSat6.gold | 8 +-- SBVTestSuite/GoldFiles/noOpt1.gold | 2 +- SBVTestSuite/GoldFiles/noOpt2.gold | 2 +- SBVTestSuite/GoldFiles/validate_2.gold | 8 +-- 5 files changed, 36 insertions(+), 38 deletions(-) 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