From 4b78c12c0670f57e4fa0eec6befd9aff75cdaefd Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 20 Nov 2023 13:50:19 -0800 Subject: [PATCH] Revert "Revert "Match new z3 output"" This reverts commit 18d849ce61dad1560b3b7299db5a05161e1b5219. --- Data/SBV/List.hs | 2 +- Data/SBV/RegExp.hs | 2 +- Documentation/SBV/Examples/Existentials/CRCPolynomial.hs | 2 +- Documentation/SBV/Examples/Misc/Floating.hs | 6 +++--- Documentation/SBV/Examples/Uninterpreted/Multiply.hs | 6 +++--- Documentation/SBV/Examples/WeakestPreconditions/Sum.hs | 4 ++-- 6 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs index 21b25e7d2..519adb0c3 100644 --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -148,7 +148,7 @@ singleton = lift1 SeqUnit (Just (: [])) -- Q.E.D. -- >>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1) -- Satisfiable. Model: --- s0 = [0,16] :: [Word16] +-- s0 = [0,64] :: [Word16] listToListAt :: SymVal a => SList a -> SInteger -> SList a listToListAt s offset = subList s offset 1 diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs index 580410750..28bbc02a3 100644 --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -87,7 +87,7 @@ import Data.SBV.Char -- >>> let phone = pre * "-" * post -- >>> sat $ \s -> (s :: SString) `match` phone -- Satisfiable. Model: --- s0 = "200-8000" :: String +-- s0 = "800-8000" :: String class RegExpMatchable a where -- | @`match` s r@ checks whether @s@ is in the language generated by @r@. match :: a -> RegExp -> SBool diff --git a/Documentation/SBV/Examples/Existentials/CRCPolynomial.hs b/Documentation/SBV/Examples/Existentials/CRCPolynomial.hs index 9e9bc9ad9..f39b2d47c 100644 --- a/Documentation/SBV/Examples/Existentials/CRCPolynomial.hs +++ b/Documentation/SBV/Examples/Existentials/CRCPolynomial.hs @@ -69,7 +69,7 @@ genPoly hd maxCnt = do res <- allSatWith defaultSMTCfg{allSatMaxModelCount = Jus -- We have: -- -- >>> findHD4Polynomials 2 --- Polynomial #1. x^16 + x^6 + x^3 + 1 +-- Polynomial #1. x^16 + x^3 + x^2 + 1 -- Polynomial #2. x^16 + x^2 + x + 1 -- Found: 2 polynomial(s). -- diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs index fed73b671..1d22a2233 100644 --- a/Documentation/SBV/Examples/Misc/Floating.hs +++ b/Documentation/SBV/Examples/Misc/Floating.hs @@ -129,13 +129,13 @@ nonZeroAddition = prove $ do [a, b] <- sFloats ["a", "b"] -- -- >>> multInverse -- Falsifiable. Counter-example: --- a = -1.7414917e38 :: Float +-- a = 7.156233e-24 :: Float -- -- Indeed, we have: -- --- >>> let a = -1.7414917e38 :: Float +-- >>> let a = 7.156233e-24 :: Float -- >>> a * (1/a) --- 0.9999999 +-- 0.99999994 multInverse :: IO ThmResult multInverse = prove $ do a <- sFloat "a" constrain $ fpIsPoint a diff --git a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs index 5b96bf498..4c6dc8cbc 100644 --- a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs +++ b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs @@ -47,8 +47,8 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo) -- >>> sat synthMul22 -- Satisfiable. Model: -- mul22_hi :: Bool -> Bool -> Bool -> Bool -> Bool --- mul22_hi False True True True = True -- mul22_hi True True False True = True +-- mul22_hi False True True True = True -- mul22_hi True False False True = True -- mul22_hi False True True False = True -- mul22_hi True True True False = True @@ -67,8 +67,8 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo) -- -- >>> :{ -- mul22_hi :: (SBool, SBool, SBool, SBool) -> SBool --- mul22_hi params = params `sElem` [ (sFalse, sTrue, sTrue, sTrue) --- , (sTrue, sTrue, sFalse, sTrue) +-- mul22_hi params = params `sElem` [ (sTrue, sTrue, sFalse, sTrue) +-- , (sFalse, sTrue, sTrue, sTrue) -- , (sTrue, sFalse, sFalse, sTrue) -- , (sFalse, sTrue, sTrue, sFalse) -- , (sTrue, sTrue, sTrue, sFalse) diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs index 0c56c6fea..21b779b5a 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs @@ -205,8 +205,8 @@ is an example: Following proof obligation failed: ================================== Invariant for loop "i < n" is not maintained by the body: - Before: SumS {n = 2, i = 1, s = 1} - After : SumS {n = 2, i = 2, s = 3} + Before: SumS {n = 3, i = 1, s = 1} + After : SumS {n = 3, i = 2, s = 3} Here, we posed the extra incorrect invariant that @s <= i@ must be maintained, and SBV found us a reachable state that violates the invariant. The /before/ state indeed satisfies @s <= i@, but the /after/ state does not. Note that the proof fails in this case not because the program