sbv 12.0 → 12.1
raw patch · 26 files changed
+355/−226 lines, 26 files
Files
- CHANGES.md +11/−0
- Data/SBV/Compilers/C.hs +2/−1
- Data/SBV/Core/Data.hs +3/−0
- Data/SBV/Core/Kind.hs +12/−7
- Data/SBV/Core/Model.hs +28/−13
- Data/SBV/Core/Operations.hs +70/−34
- Data/SBV/Core/Symbolic.hs +4/−4
- Data/SBV/List.hs +13/−0
- Data/SBV/SMT/SMTLib2.hs +12/−7
- Data/SBV/TP/List.hs +14/−6
- Data/SBV/TP/TP.hs +9/−9
- Documentation/SBV/Examples/Queries/CaseSplit.hs +1/−1
- Documentation/SBV/Examples/TP/SumReverse.hs +9/−3
- SBVTestSuite/GoldFiles/array_misc_32.gold +0/−34
- SBVTestSuite/GoldFiles/array_misc_33.gold +0/−34
- SBVTestSuite/GoldFiles/array_misc_34.gold +0/−34
- SBVTestSuite/GoldFiles/lambda08.gold +27/−27
- SBVTestSuite/GoldFiles/listFloat1.gold +18/−0
- SBVTestSuite/GoldFiles/listFloat2.gold +56/−0
- SBVTestSuite/GoldFiles/listFloat3.gold +34/−0
- SBVTestSuite/GoldFiles/tuple_enum.gold +4/−4
- SBVTestSuite/TestSuite/Arrays/InitVals.hs +0/−3
- SBVTestSuite/TestSuite/Basics/Lambda.hs +1/−1
- SBVTestSuite/TestSuite/Basics/List.hs +23/−0
- SBVTestSuite/TestSuite/Basics/Tuple.hs +3/−3
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,6 +1,17 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 12.1, 2025-07-11++ * Add missing instances for strong-equality, extending it to lists/Maybe etc. (Only impacts floats and structures+ that contain floats.)++ * Be more careful about applications of equality when floats are involved. Previously, we were using regular SMTLib+ equality for structures. (i.e., lists of values or any other container that have a float element stored somewhere.)+ Unfortunately the IEEE-754 semantics for equality does not correspond to SMTLib's notion of equality in these+ cases, causing semantic differences. Now we are more careful, and we also warn the user about performance+ implications and ask them to use custom-functions instead.+ ### Version 12.0, 2025-07-04 * [BACKWARDS COMPATIBILITY] Renamed KnuckleDragger to TP, for theorem-proving. The original name was confusing, and
Data/SBV/Compilers/C.hs view
@@ -746,7 +746,8 @@ rtc = cgRTC cfg cBinOps = [ (Plus, "+"), (Times, "*"), (Minus, "-")- , (Equal, "=="), (NotEqual, "!="), (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=")+ , (Equal False, "==") -- no strong equality!+ , (NotEqual, "!="), (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=") , (And, "&"), (Or, "|"), (XOr, "^") ]
Data/SBV/Core/Data.hs view
@@ -709,8 +709,10 @@ class EqSymbolic a where -- | Symbolic equality. (.==) :: a -> a -> SBool+ -- | Symbolic inequality. (./=) :: a -> a -> SBool+ -- | Strong equality. On floats ('SFloat'/'SDouble'), strong equality is object equality; that -- is @NaN == NaN@ holds, but @+0 == -0@ doesn't. On other types, (.===) is simply (.==). -- Note that (.==) is the /right/ notion of equality for floats per IEEE754 specs, since by@@ -721,6 +723,7 @@ -- -- NB. If you do not care about or work with floats, simply use (.==) and (./=). (.===) :: a -> a -> SBool+ -- | Negation of strong equality. Equaivalent to negation of (.===) on all types. (./==) :: a -> a -> SBool
Data/SBV/Core/Kind.hs view
@@ -30,7 +30,7 @@ Kind(..), HasKind(..), constructUKind, smtType, hasUninterpretedSorts , BVIsNonZero, ValidFloat, intOfProxy , showBaseKind, needsFlattening, RoundingMode(..), smtRoundingMode- , eqCheckIsObjectEq, expandKinds+ , eqCheckIsObjectEq, containsFloats, isSomeKindOfFloat, expandKinds ) where import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields)@@ -374,14 +374,19 @@ r = fromEnum iv -- | Is this a type we can safely do equality on? Essentially it avoids floats (@NaN@ /= @NaN@, @+0 = -0@), and reals (due--- to the possible presence of non-exact rationals.+-- to the possible presence of non-exact rationals. In short, this will return True if there are no floats/reals under the hood. eqCheckIsObjectEq :: Kind -> Bool eqCheckIsObjectEq = not . any bad . expandKinds- where bad KFloat = True- bad KDouble = True- bad KFP{} = True- bad KReal = True- bad _ = False+ where bad KReal = True+ bad k = isSomeKindOfFloat k++-- | Same as above, except only for floats+containsFloats :: Kind -> Bool+containsFloats = any isSomeKindOfFloat . expandKinds++-- | Is some sort of a float?+isSomeKindOfFloat :: Kind -> Bool+isSomeKindOfFloat k = isFloat k || isDouble k || isFP k -- | Do we have a completely uninterpreted sort lying around anywhere? hasUninterpretedSorts :: Kind -> Bool
Data/SBV/Core/Model.hs view
@@ -1062,10 +1062,14 @@ -- Lists instance EqSymbolic a => EqSymbolic [a] where- [] .== [] = sTrue- (x:xs) .== (y:ys) = x .== y .&& xs .== ys- _ .== _ = sFalse+ [] .== [] = sTrue+ (x:xs) .== (y:ys) = x .== y .&& xs .== ys+ _ .== _ = sFalse + [] .=== [] = sTrue+ (x:xs) .=== (y:ys) = x .=== y .&& xs .=== ys+ _ .=== _ = sFalse+ instance OrdSymbolic a => OrdSymbolic [a] where [] .< [] = sFalse [] .< _ = sTrue@@ -1074,7 +1078,8 @@ -- NonEmpty instance EqSymbolic a => EqSymbolic (NonEmpty a) where- (x :| xs) .== (y :| ys) = x : xs .== y : ys+ (x :| xs) .== (y :| ys) = x : xs .== y : ys+ (x :| xs) .=== (y :| ys) = x : xs .=== y : ys instance OrdSymbolic a => OrdSymbolic (NonEmpty a) where (x :| xs) .< (y :| ys) = x : xs .< y : ys@@ -1093,10 +1098,14 @@ -- Either instance (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) where- Left a .== Left b = a .== b- Right a .== Right b = a .== b- _ .== _ = sFalse+ Left a .== Left b = a .== b+ Right a .== Right b = a .== b+ _ .== _ = sFalse + Left a .=== Left b = a .=== b+ Right a .=== Right b = a .=== b+ _ .=== _ = sFalse+ instance (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) where Left a .< Left b = a .< b Left _ .< Right _ = sTrue@@ -1105,35 +1114,40 @@ -- 2-Tuple instance (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) where- (a0, b0) .== (a1, b1) = a0 .== a1 .&& b0 .== b1+ (a0, b0) .== (a1, b1) = a0 .== a1 .&& b0 .== b1+ (a0, b0) .=== (a1, b1) = a0 .=== a1 .&& b0 .=== b1 instance (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) where (a0, b0) .< (a1, b1) = a0 .< a1 .|| (a0 .== a1 .&& b0 .< b1) -- 3-Tuple instance (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) where- (a0, b0, c0) .== (a1, b1, c1) = (a0, b0) .== (a1, b1) .&& c0 .== c1+ (a0, b0, c0) .== (a1, b1, c1) = (a0, b0) .== (a1, b1) .&& c0 .== c1+ (a0, b0, c0) .=== (a1, b1, c1) = (a0, b0) .=== (a1, b1) .&& c0 .=== c1 instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) where (a0, b0, c0) .< (a1, b1, c1) = (a0, b0) .< (a1, b1) .|| ((a0, b0) .== (a1, b1) .&& c0 .< c1) -- 4-Tuple instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) where- (a0, b0, c0, d0) .== (a1, b1, c1, d1) = (a0, b0, c0) .== (a1, b1, c1) .&& d0 .== d1+ (a0, b0, c0, d0) .== (a1, b1, c1, d1) = (a0, b0, c0) .== (a1, b1, c1) .&& d0 .== d1+ (a0, b0, c0, d0) .=== (a1, b1, c1, d1) = (a0, b0, c0) .=== (a1, b1, c1) .&& d0 .=== d1 instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) where (a0, b0, c0, d0) .< (a1, b1, c1, d1) = (a0, b0, c0) .< (a1, b1, c1) .|| ((a0, b0, c0) .== (a1, b1, c1) .&& d0 .< d1) -- 5-Tuple instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) where- (a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .== (a1, b1, c1, d1) .&& e0 .== e1+ (a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .== (a1, b1, c1, d1) .&& e0 .== e1+ (a0, b0, c0, d0, e0) .=== (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .=== (a1, b1, c1, d1) .&& e0 .=== e1 instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) where (a0, b0, c0, d0, e0) .< (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .< (a1, b1, c1, d1) .|| ((a0, b0, c0, d0) .== (a1, b1, c1, d1) .&& e0 .< e1) -- 6-Tuple instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) where- (a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) .&& f0 .== f1+ (a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) .&& f0 .== f1+ (a0, b0, c0, d0, e0, f0) .=== (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .=== (a1, b1, c1, d1, e1) .&& f0 .=== f1 instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) where (a0, b0, c0, d0, e0, f0) .< (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .< (a1, b1, c1, d1, e1)@@ -1141,7 +1155,8 @@ -- 7-Tuple instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) where- (a0, b0, c0, d0, e0, f0, g0) .== (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) .&& g0 .== g1+ (a0, b0, c0, d0, e0, f0, g0) .== (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) .&& g0 .== g1+ (a0, b0, c0, d0, e0, f0, g0) .=== (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .=== (a1, b1, c1, d1, e1, f1) .&& g0 .=== g1 instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) where (a0, b0, c0, d0, e0, f0, g0) .< (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .< (a1, b1, c1, d1, e1, f1)
Data/SBV/Core/Operations.hs view
@@ -324,7 +324,7 @@ | isDouble x, Just f1 <- getD x, Just f2 <- getD y = svBool $ f1 `fpIsEqualObjectH` f2 | isFP x, Just f1 <- getFP x, Just f2 <- getFP y = svBool $ f1 `fpIsEqualObjectH` f2 | isFloat x || isDouble x || isFP x = SVal KBool $ Right $ cache r- | True = svEqual x y+ | True = compareSV (Equal True) x y where getF (SVal _ (Left (CV _ (CFloat f)))) = Just f getF _ = Nothing @@ -342,15 +342,18 @@ compareSV :: Op -> SVal -> SVal -> SVal compareSV op x y -- Make sure we don't get anything we can't handle or expect- | op `notElem` [Equal, NotEqual, LessThan, GreaterThan, LessEq, GreaterEq] = error $ "Unexpected call to compareSV: " ++ show (op, x, y)- | kx /= ky = error $ "Mismatched kinds in call to compareSV:" ++ show (op, x, kindOf x, kindOf y)- | (isSet kx || isArray ky) && op `notElem` [Equal, NotEqual] = error $ "Unexpected Set/Array not-equal comparison: " ++ show (op, x, k)+ | op `notElem` [Equal True, Equal False, NotEqual, LessThan, GreaterThan, LessEq, GreaterEq]+ = error $ "Unexpected call to compareSV: " ++ show (op, x, y)+ | kx /= ky+ = error $ "Mismatched kinds in call to compareSV:" ++ show (op, x, kindOf x, kindOf y)+ | (isSet kx || isArray ky) && op `notElem` [Equal True, Equal False, NotEqual]+ = error $ "Unexpected Set/Array not-equal comparison: " ++ show (op, x, k) -- Boolean equality optimizations- | k == KBool, op == Equal, SVal _ (Left xv) <- x, xv == trueCV = y -- true .== y --> y- | k == KBool, op == Equal, SVal _ (Left yv) <- y, yv == trueCV = x -- x .== true --> x- | k == KBool, op == Equal, SVal _ (Left xv) <- x, xv == falseCV = svNot y -- false .== y --> svNot y- | k == KBool, op == Equal, SVal _ (Left yv) <- y, yv == falseCV = svNot x -- x .== false --> svNot x+ | k == KBool, Equal{} <- op, SVal _ (Left xv) <- x, xv == trueCV = y -- true .== y --> y+ | k == KBool, Equal{} <- op, SVal _ (Left yv) <- y, yv == trueCV = x -- x .== true --> x+ | k == KBool, Equal{} <- op, SVal _ (Left xv) <- x, xv == falseCV = svNot y -- false .== y --> svNot y+ | k == KBool, Equal{} <- op, SVal _ (Left yv) <- y, yv == falseCV = svNot x -- x .== false --> svNot x | k == KBool, op == NotEqual, SVal _ (Left xv) <- x, xv == trueCV = svNot y -- true ./= y --> svNot y | k == KBool, op == NotEqual, SVal _ (Left yv) <- y, yv == trueCV = svNot x -- x ./= true --> svNot x@@ -376,12 +379,12 @@ Nothing -> -- cCompare is conservative on floats. Give those one more chance, only at the top-level. -- (i.e., if stored under a Maybe/Either/List etc., we'll resort to a symbolic result.) case (k, cvVal xv, cvVal yv) of- (KFloat, CFloat a, CFloat b) -> svBool (a `cOp` b)- (KDouble, CDouble a, CDouble b) -> svBool (a `cOp` b)- (KFP{} , CFP a, CFP b) -> svBool (a `cOp` b)- _ -> symResult+ (KFloat, CFloat a, CFloat b) -> svBool (a `cFPOp` b)+ (KDouble, CDouble a, CDouble b) -> svBool (a `cFPOp` b)+ (KFP{} , CFP a, CFP b) -> svBool (a `cFPOp` b)+ _ -> symResult Just r -> svBool $ case op of- Equal -> r == EQ+ Equal _ -> r == EQ NotEqual -> r /= EQ LessThan -> r == LT GreaterThan -> r == GT@@ -396,17 +399,23 @@ ky = kindOf y k = kx -- only used after we ensured kx == ky - symResult = SVal KBool $ Right $ cache res+ -- Are there any floats embedded down from here? if so, we have to be careful due to presence of NaN+ safeEq = op == Equal True -- strong equality ok+ || isSomeKindOfFloat k -- top level OK+ || not (containsFloats k) -- has floats somewhere: not ok++ symResult+ | safeEq = symResultSafe+ | True = symResultFP++ -- This will go down to SMTLib's =. So only use it if we're safe to do so!+ symResultSafe = SVal KBool $ Right $ cache res where res st = do svx :: SV <- svToSV st x svy :: SV <- svToSV st y - -- We might be able to further optimize if we- -- know these are the same nodes, provided we- -- don't have a float case. (Recall that NaN doesn't- -- compare equal to itself, so avoid that.)- if svx == svy && not (isFloat k || isDouble k || isFP k)+ if svx == svy && eqCheckIsObjectEq k then case op of- Equal -> pure trueSV+ Equal{} -> pure trueSV LessEq -> pure trueSV GreaterEq -> pure trueSV NotEqual -> pure falseSV@@ -415,15 +424,42 @@ _ -> error $ "Unexpected call to compareSV, equal SV case: " ++ show (op, svx) else newExpr st KBool (SBVApp op [svx, svy]) - a `cOp` b = case op of- Equal -> a == b- NotEqual -> a /= b- LessThan -> a < b- GreaterThan -> a > b- LessEq -> a <= b- GreaterEq -> a >= b- _ -> error $ "Unexpected call to cOp: " ++ show op+ a `cFPOp` b = case op of+ Equal False -> a == b+ Equal True -> a `fpIsEqualObjectH` b+ NotEqual -> a /= b+ LessThan -> a < b+ GreaterThan -> a > b+ LessEq -> a <= b+ GreaterEq -> a >= b+ _ -> error $ "Unexpected call to cFPOp: " ++ show op + -- OK, we have a result that has floats embedded in it. So comparison is problematic.+ -- Certain subsets of this is supported elsewhere. Here, we simply bail out.+ symResultFP = error $ unlines $ [ ""+ , "*** Data.SBV: Unsupported complicated comparison:"+ , "***"+ , "*** Op : " ++ show op+ , "*** Type: " ++ show k+ , "***"+ , "*** Due to the presence of NaN, comparisons over this type require"+ , "*** special support in SMTLib. And in general this can lead to"+ , "*** performance issues since the comparison is no longer a natively"+ , "*** supported operation in the logic."+ , "***"+ , "*** NB. If you want the semantics NaN == NaN, and +0 /= -0, then you can use .=== instead."+ , "***"+ ]+ ++ case alternative of+ Nothing -> ["*** Please report this as a feature request."]+ Just a -> [ "*** For this case, please use: " ++ a+ , "*** but beware of performance/decidability implications."+ ]++ where alternative = case (op, k) of+ (Equal False, KList f) | isFloat f || isDouble f || isFP f -> Just "Data.SBV.List.listEq"+ _ -> Nothing+ -- Compare two CVals; if we can. We're being conservative here and deferring to a symbolic result if we get something complicated. cCompare :: Kind -> Op -> CVal -> CVal -> Maybe Ordering cCompare k op x y =@@ -485,23 +521,23 @@ -- Arrays and sets only support equality/inequality. And they have object-equality semantics. So -- if there are any floats or non-exact-rationals down in the index or element kinds, we bail- (CSet a, CSet b) | op `elem` [Equal, NotEqual]+ (CSet a, CSet b) | op `elem` [Equal True, Equal False, NotEqual] , KSet ke <- k -> case svSetEqual ke a b of Nothing -> Nothing -- We don't know Just True -> Just EQ -- They're equal- Just False -> Just $ if op == Equal+ Just False -> Just $ if op `elem` [Equal True, Equal False] then GT -- Pick GT, So equality test will fail else EQ -- Pick EQ, So in-equality test will fail | True -> error $ "cCompare: Received unexpected set comparison: " ++ show (op, k) - (CArray a, CArray b) | op `elem` [Equal, NotEqual]+ (CArray a, CArray b) | op `elem` [Equal True, Equal False, NotEqual] , KArray k1 k2 <- k -> case svArrEqual k1 k2 a b of Nothing -> Nothing -- We don't know Just True -> Just EQ -- They're equal- Just False -> Just $ if op == Equal+ Just False -> Just $ if op `elem` [Equal True, Equal False] then GT -- Pick GT, So equality test will fail else EQ -- Pick EQ, So in-equality test will fail | True@@ -565,9 +601,9 @@ (True, False, True) -> Just True -- keys match, but defs don't. But we keys are complete, so def mismatch is OK _ -> Nothing -- otherwise, we don't really know. So, remain symbolic. --- | Equality.+-- | Equality. This is SMT object equality. svEqual :: SVal -> SVal -> SVal-svEqual = compareSV Equal+svEqual = compareSV (Equal False) -- | Inequality. svNotEqual :: SVal -> SVal -> SVal
Data/SBV/Core/Symbolic.hs view
@@ -210,7 +210,7 @@ | Abs | Quot | Rem- | Equal+ | Equal Bool -- ^ If bool is True then this is strong (i.e., object equality). Matters for floats or structures containing them. | Implies | NotEqual | LessThan@@ -630,7 +630,7 @@ where syms = [ (Plus, "+"), (Times, "*"), (Minus, "-"), (UNeg, "-"), (Abs, "abs") , (Quot, "quot") , (Rem, "rem")- , (Equal, "=="), (NotEqual, "/="), (Implies, "=>")+ , (Equal True, "==="), (Equal False, "=="), (NotEqual, "/="), (Implies, "=>") , (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=") , (Ite, "if_then_else") , (And, "&"), (Or, "|"), (XOr, "^"), (Not, "~")@@ -674,7 +674,7 @@ SBVApp op [a, b] | isCommutative op && a > b -> SBVApp op [b, a] _ -> s where isCommutative :: Op -> Bool- isCommutative o = o `elem` [Plus, Times, Equal, NotEqual, And, Or, XOr]+ isCommutative o = o `elem` [Plus, Times, Equal True, Equal False, NotEqual, And, Or, XOr] -- Show instance for 'SBVExpr'. Again, only for debugging purposes. instance Show SBVExpr where@@ -693,7 +693,7 @@ showOpInfix :: Op -> Bool showOpInfix = (`elem` infixOps) where infixOps = [ Plus, Times, Minus, Quot, Rem, Implies- , Equal, NotEqual, LessThan, GreaterThan, LessEq, GreaterEq+ , Equal True, Equal False, NotEqual, LessThan, GreaterThan, LessEq, GreaterEq , And, Or, XOr, Join ]
Data/SBV/List.hs view
@@ -40,6 +40,9 @@ -- * Containment , elem, notElem, isInfixOf, isSuffixOf, isPrefixOf + -- * List equality+ , listEq+ -- * Sublists , take, drop, splitAt, subList, replace, indexOf, offsetIndexOf @@ -369,6 +372,16 @@ = literal True | True = lift2 True (SeqPrefixOf (kindOf (Proxy @a))) (Just L.isPrefixOf) pre l++-- | @listEq@ is a variant of equality that you can use for lists of floats. It respects @NaN /= NaN@. The reason+-- we do not do this automatically is that it complicates proof objectives usually, as it does not simply resolve to+-- the native equality check.+listEq :: forall a. SymVal a => SList a -> SList a -> SBool+listEq+ | containsFloats (kindOf (Proxy @a))+ = smtFunction "listEq" $ \xs ys -> ite (null xs) (null ys) (head xs .== head ys .&& listEq (tail xs) (tail ys))+ | True+ = (.==) -- | @`isSuffixOf` suf l@. Is @suf@ a suffix of @l@? --
Data/SBV/SMT/SMTLib2.hs view
@@ -1027,7 +1027,8 @@ , (Abs, liftAbs) , (Quot, lift2S "bvudiv" "bvsdiv") , (Rem, lift2S "bvurem" "bvsrem")- , (Equal, eqBV)+ , (Equal True, eqBV)+ , (Equal False, eqBV) , (NotEqual, neqBV) , (LessThan, lift2S "bvult" "bvslt") , (GreaterThan, lift2S "bvugt" "bvsgt")@@ -1065,7 +1066,8 @@ , (Times, lift2WM "*" "fp.mul") , (UNeg, lift1FP "-" "fp.neg") , (Abs, liftAbs)- , (Equal, equal)+ , (Equal True, equal)+ , (Equal False, equal) , (NotEqual, notEqual) , (LessThan, lift2Cmp "<" "fp.lt") , (GreaterThan, lift2Cmp ">" "fp.gt")@@ -1078,7 +1080,8 @@ , (Times, lift2Rat "sbv.rat.times") , (UNeg, liftRat "sbv.rat.uneg") , (Abs, liftRat "sbv.rat.abs")- , (Equal, lift2Rat "sbv.rat.eq")+ , (Equal True, lift2Rat "sbv.rat.eq")+ , (Equal False, lift2Rat "sbv.rat.eq") , (NotEqual, lift2Rat "sbv.rat.notEq") , (LessThan, lift2Rat "sbv.rat.lt") , (GreaterThan, lift2Rat "sbv.rat.lt" . swap)@@ -1093,7 +1096,8 @@ swap sbvs = error $ "SBV.SMTLib2.sh.swap: Unexpected arguments: " ++ show sbvs -- equality and comparisons are the only thing that works on uninterpreted sorts and pretty much everything else- uninterpretedTable = [ (Equal, lift2S "=" "=" True)+ uninterpretedTable = [ (Equal True, lift2S "=" "=" True)+ , (Equal False, lift2S "=" "=" True) , (NotEqual, liftNS "distinct" "distinct" True) , (LessThan, unintComp "<") , (GreaterThan, unintComp ">")@@ -1102,7 +1106,8 @@ ] -- For strings, equality and comparisons are the only operators- smtStringTable = [ (Equal, lift2S "=" "=" True)+ smtStringTable = [ (Equal True, lift2S "=" "=" True)+ , (Equal False, lift2S "=" "=" True) , (NotEqual, liftNS "distinct" "distinct" True) , (LessThan, stringCmp False "str.<") , (GreaterThan, stringCmp True "str.<")@@ -1110,9 +1115,9 @@ , (GreaterEq, stringCmp True "str.<=") ] - -- For lists, equality is really the only operator+ -- For lists, equality is really the only operator. Also, not strong-equality due to lists of floats. -- Likewise here, things might change for comparisons- smtListTable = [ (Equal, lift2S "=" "=" True)+ smtListTable = [ (Equal False, lift2S "=" "=" True) , (NotEqual, liftNS "distinct" "distinct" True) , (LessThan, seqCmp False "seq.<") , (GreaterThan, seqCmp True "seq.<")
Data/SBV/TP/List.hs view
@@ -611,6 +611,7 @@ -- Step: 2 Q.E.D. -- Step: 3 Q.E.D. -- Step: 4 Q.E.D.+-- Step: 5 Q.E.D. -- Result: Q.E.D. -- [Proven] mapCompose :: Ɐxs ∷ [Integer] → Bool mapCompose :: forall a b c. (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> (SBV b -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))@@ -621,6 +622,7 @@ =: map g (f x .: map f xs) =: g (f x) .: map g (map f xs) ?? ih+ =: g (f x) .: map (g . f) xs =: (g . f) x .: map (g . f) xs =: map (g . f) (x .: xs) =: qed@@ -864,7 +866,7 @@ -- Step: 5 Q.E.D. -- Result: Q.E.D. -- [Proven] foldrFoldl :: Ɐxs ∷ [Integer] → Bool-foldrFoldl :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> (SBV b -> SBV a -> SBV b) -> SBV b-> TP (Proof (Forall "xs" [a] -> SBool))+foldrFoldl :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> (SBV b -> SBV a -> SBV b) -> SBV b -> TP (Proof (Forall "xs" [a] -> SBool)) foldrFoldl (<+>) (<*>) e = do -- Assumptions about the operators let -- (x <+> y) <*> z == x <+> (y <*> z)@@ -1380,7 +1382,7 @@ -- | @take n (map f xs) == map f (take n xs)@ ----- >>> runTP $ take_map @Integer @Float (uninterpret "f")+-- >>> runTP $ take_map @Integer @Integer (uninterpret "f") -- Lemma: take_cons Q.E.D. -- Lemma: map1 Q.E.D. -- Lemma: take_map.n <= 0 Q.E.D.@@ -1392,7 +1394,9 @@ -- Step: 4 Q.E.D. -- Step: 5 Q.E.D. -- Result: Q.E.D.--- Lemma: take_map Q.E.D.+-- Lemma: take_map+-- Step: 1 Q.E.D.+-- Result: Q.E.D. -- [Proven] take_map :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool take_map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) take_map f = do@@ -1419,9 +1423,13 @@ =: map f (take n (x .: xs)) =: qed - lemma "take_map"- (\(Forall n) (Forall xs) -> take n (map f xs) .== map f (take n xs))- [proofOf h1, proofOf h2]+ calc "take_map"+ (\(Forall n) (Forall xs) -> take n (map f xs) .== map f (take n xs)) $+ \n xs -> [] |- take n (map f xs)+ ?? h1+ ?? h2+ =: map f (take n xs)+ =: qed -- | @n .> 0 ==> drop n (x .: xs) == drop (n - 1) xs@ --
Data/SBV/TP/TP.hs view
@@ -390,8 +390,8 @@ -- | Turn a raw (i.e., as written by the user) proof tree to a tree where the successive equalities are made explicit.-mkProofTree :: SymVal a => (SBV a -> SBV a -> c) -> TPProofRaw (SBV a) -> TPProofGen c [String] SBool-mkProofTree symEq = go (CalcStart [])+mkProofTree :: SymVal a => (SBV a -> SBV a -> c, SBV a -> SBV a -> SBool) -> TPProofRaw (SBV a) -> TPProofGen c [String] SBool+mkProofTree (symTraceEq, symEq) = go (CalcStart []) where -- End of the proof; tie the begin and end go step (ProofEnd () hs) = case step of -- It's tempting to error out if we're at the start and already reached the end@@ -399,7 +399,7 @@ -- general case, it's quite valid in a case-split; where one of the case-splits -- might be easy enough for the solver to deduce so the user simply says "just derive it for me." CalcStart hs' -> ProofEnd sTrue (hs' ++ hs) -- Nothing proven!- CalcStep begin end hs' -> ProofEnd (begin .== end) (hs' ++ hs)+ CalcStep begin end hs' -> ProofEnd (begin `symEq` end) (hs' ++ hs) -- Branch: Just push it down. We use the hints from previous step, and pass the current ones down. go step (ProofBranch c hs ps) = ProofBranch c (getHelperText hs) [(bc, go step' p) | (bc, p) <- ps]@@ -409,20 +409,20 @@ -- Step: go (CalcStart hs) (ProofStep cur hs' p) = go (CalcStep cur cur (hs' ++ hs)) p- go (CalcStep first prev hs) (ProofStep cur hs' p) = ProofStep (symEq prev cur) hs (go (CalcStep first cur hs') p)+ go (CalcStep first prev hs) (ProofStep cur hs' p) = ProofStep (prev `symTraceEq` cur) hs (go (CalcStep first cur hs') p) -- | Turn a sequence of steps into a chain of equalities mkCalcSteps :: SymVal a => (SBool, TPProofRaw (SBV a)) -> ([Int] -> Symbolic SBool) -> Symbolic CalcStrategy mkCalcSteps (intros, tpp) qcInstance = do pure $ CalcStrategy { calcIntros = intros- , calcProofTree = mkProofTree (.==) tpp+ , calcProofTree = mkProofTree ((.===), (.===)) tpp , calcQCInstance = qcInstance } -- | Given initial hypothesis, and a raw proof tree, build the quick-check walk over this tree for the step that's marked as such. qcRun :: SymVal a => [Int] -> (SBool, TPProofRaw (SBV a)) -> Symbolic SBool qcRun checkedLabel (intros, tpp) = do- results <- runTree sTrue 1 ([1], mkProofTree (\a b -> (a, b, a .== b)) tpp)+ results <- runTree sTrue 1 ([1], mkProofTree (\a b -> (a, b, a .=== b), (.==)) tpp) case [b | (l, b) <- results, l == checkedLabel] of [(caseCond, b)] -> do constrain $ intros .&& caseCond pure b@@ -1457,7 +1457,7 @@ split xs empty cons = ProofBranch False [] [(cnil, empty), (ccons, cons h t)] where cnil = SL.null xs (h, t) = SL.uncons xs- ccons = sNot cnil .&& xs .== h SL..: t+ ccons = sNot cnil .&& xs .=== h SL..: t -- | Case splitting over two lists; empty and full cases for each split2 :: (SymVal a, SymVal b)@@ -1476,11 +1476,11 @@ ] where xnil = SL.null xs (hx, tx) = SL.uncons xs- xcons = sNot xnil .&& xs .== hx SL..: tx+ xcons = sNot xnil .&& xs .=== hx SL..: tx ynil = SL.null ys (hy, ty) = SL.uncons ys- ycons = sNot ynil .&& ys .== hy SL..: ty+ ycons = sNot ynil .&& ys .=== hy SL..: ty -- | A quick-check step, taking number of tests. qc :: Int -> Helper
Documentation/SBV/Examples/Queries/CaseSplit.hs view
@@ -41,7 +41,7 @@ x <- sFloat "x" - constrain $ x ./= x -- yes, in the FP land, this does hold+ constrain $ x ./= x -- yes, in the FP land, this is satisfiable by NaN query $ do mbR <- caseSplit True [ ("fpIsNegativeZero", fpIsNegativeZero x) , ("fpIsPositiveZero", fpIsPositiveZero x)
Documentation/SBV/Examples/TP/SumReverse.hs view
@@ -42,14 +42,16 @@ -- Step: 1 Q.E.D. -- Step: 2 Q.E.D. -- Step: 3 Q.E.D.--- Step: 4 Q.E.D.+-- Step: 4 (associativity) Q.E.D.+-- Step: 5 Q.E.D. -- Result: Q.E.D. -- Inductive lemma: sumReverse -- Step: Base Q.E.D. -- Step: 1 Q.E.D. -- Step: 2 Q.E.D. -- Step: 3 Q.E.D.--- Step: 4 Q.E.D.+-- Step: 4 (commutativity) Q.E.D.+-- Step: 5 Q.E.D. -- Result: Q.E.D. -- [Proven] sumReverse :: Ɐxs ∷ [Integer] → Bool revSum :: forall a. (SymVal a, Num (SBV a)) => IO (Proof (Forall "xs" [a] -> SBool))@@ -62,7 +64,9 @@ =: sum (x .: (xs ++ ys)) =: x + sum (xs ++ ys) ?? ih- =: x + sum xs + sum ys+ =: x + (sum xs + sum ys)+ ?? "associativity"+ =: (x + sum xs) + sum ys =: sum (x .: xs) + sum ys =: qed @@ -75,5 +79,7 @@ =: sum (reverse xs) + sum [x] ?? ih =: sum xs + x+ ?? "commutativity"+ =: x + sum xs =: sum (x .: xs) =: qed
− SBVTestSuite/GoldFiles/array_misc_32.gold
@@ -1,34 +0,0 @@-** Calling: z3 -nw -in -smt2-[GOOD] ; Automatically generated by SBV. Do not edit.-[GOOD] (set-option :print-success true)-[GOOD] (set-option :global-declarations true)-[GOOD] (set-option :smtlib2_compliant true)-[GOOD] (set-option :diagnostic-output-channel "stdout")-[GOOD] (set-option :produce-models true)-[GOOD] (set-option :pp.max_depth 4294967295)-[GOOD] (set-option :pp.min_alias_size 4294967295)-[GOOD] (set-option :model.inline_def true )-[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.-[GOOD] ; --- uninterpreted sorts ----[GOOD] ; --- tuples ----[GOOD] ; --- sums ----[GOOD] ; --- literal constants ----[GOOD] (define-fun s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))))-[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))))-[GOOD] ; --- top level inputs ----[GOOD] ; --- constant tables ----[GOOD] ; --- non-constant tables ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user defined functions ----[GOOD] ; --- assignments ----[GOOD] (define-fun s2 () Bool (= s0 s1))-[GOOD] ; --- delayedEqualities ----[GOOD] ; --- formula ----[GOOD] (assert (not s2))-[SEND] (check-sat)-[RECV] unsat-*** Solver : Z3-*** Exit code: ExitSuccess--FINAL OUTPUT:-Q.E.D.
− SBVTestSuite/GoldFiles/array_misc_33.gold
@@ -1,34 +0,0 @@-** Calling: z3 -nw -in -smt2-[GOOD] ; Automatically generated by SBV. Do not edit.-[GOOD] (set-option :print-success true)-[GOOD] (set-option :global-declarations true)-[GOOD] (set-option :smtlib2_compliant true)-[GOOD] (set-option :diagnostic-output-channel "stdout")-[GOOD] (set-option :produce-models true)-[GOOD] (set-option :pp.max_depth 4294967295)-[GOOD] (set-option :pp.min_alias_size 4294967295)-[GOOD] (set-option :model.inline_def true )-[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.-[GOOD] ; --- uninterpreted sorts ----[GOOD] ; --- tuples ----[GOOD] ; --- sums ----[GOOD] ; --- literal constants ----[GOOD] (define-fun s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 1.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))))-[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))))-[GOOD] ; --- top level inputs ----[GOOD] ; --- constant tables ----[GOOD] ; --- non-constant tables ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user defined functions ----[GOOD] ; --- assignments ----[GOOD] (define-fun s2 () Bool (= s0 s1))-[GOOD] ; --- delayedEqualities ----[GOOD] ; --- formula ----[GOOD] (assert (not s2))-[SEND] (check-sat)-[RECV] sat-*** Solver : Z3-*** Exit code: ExitSuccess--FINAL OUTPUT:-Falsifiable
− SBVTestSuite/GoldFiles/array_misc_34.gold
@@ -1,34 +0,0 @@-** Calling: z3 -nw -in -smt2-[GOOD] ; Automatically generated by SBV. Do not edit.-[GOOD] (set-option :print-success true)-[GOOD] (set-option :global-declarations true)-[GOOD] (set-option :smtlib2_compliant true)-[GOOD] (set-option :diagnostic-output-channel "stdout")-[GOOD] (set-option :produce-models true)-[GOOD] (set-option :pp.max_depth 4294967295)-[GOOD] (set-option :pp.min_alias_size 4294967295)-[GOOD] (set-option :model.inline_def true )-[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.-[GOOD] ; --- uninterpreted sorts ----[GOOD] ; --- tuples ----[GOOD] ; --- sums ----[GOOD] ; --- literal constants ----[GOOD] (define-fun s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 1.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))))-[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))))-[GOOD] ; --- top level inputs ----[GOOD] ; --- constant tables ----[GOOD] ; --- non-constant tables ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user defined functions ----[GOOD] ; --- assignments ----[GOOD] (define-fun s2 () Bool (distinct s0 s1))-[GOOD] ; --- delayedEqualities ----[GOOD] ; --- formula ----[GOOD] (assert (not s2))-[SEND] (check-sat)-[RECV] unsat-*** Solver : Z3-*** Exit code: ExitSuccess--FINAL OUTPUT:-Q.E.D.
SBVTestSuite/GoldFiles/lambda08.gold view
@@ -13,34 +13,34 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 1.0 1.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 2.0 1.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 4.0 1.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 5.0 1.0)))))+[GOOD] (define-fun s2 () (Seq (_ BitVec 64)) (seq.++ (seq.unit #x0000000000000001) (seq.unit #x0000000000000002) (seq.unit #x0000000000000003) (seq.unit #x0000000000000004) (seq.unit #x0000000000000005))) [GOOD] ; --- top level inputs ----[GOOD] (declare-fun s0 () (Seq (_ FloatingPoint 8 24)))-[GOOD] (declare-fun s1 () (Seq (_ FloatingPoint 8 24)))+[GOOD] (declare-fun s0 () (Seq (_ BitVec 64)))+[GOOD] (declare-fun s1 () (Seq (_ BitVec 64))) [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user defined functions ----[GOOD] ; |sbv.map @(SBV Float -> SBV Float)_55d10191cd @(SBV [Float] -> SBV [Float])| :: [SFloat] -> [SFloat] [Recursive]-[GOOD] (define-fun-rec |sbv.map @(SBV Float -> SBV Float)_55d10191cd @(SBV [Float] -> SBV [Float])| ((l1_s0 (Seq (_ FloatingPoint 8 24)))) (Seq (_ FloatingPoint 8 24))+[GOOD] ; |sbv.map @(SBV Int64 -> SBV Int64)_bc2a222730 @(SBV [Int64] -> SBV [Int64])| :: [SInt64] -> [SInt64] [Recursive]+[GOOD] (define-fun-rec |sbv.map @(SBV Int64 -> SBV Int64)_bc2a222730 @(SBV [Int64] -> SBV [Int64])| ((l1_s0 (Seq (_ BitVec 64)))) (Seq (_ BitVec 64)) (let ((l1_s2 0))- (let ((l1_s4 (as seq.empty (Seq (_ FloatingPoint 8 24)))))- (let ((l1_s6 ((_ to_fp 8 24) roundNearestTiesToEven (/ 1.0 1.0))))+ (let ((l1_s4 (as seq.empty (Seq (_ BitVec 64)))))+ (let ((l1_s6 #x0000000000000001)) (let ((l1_s9 1)) (let ((l1_s1 (seq.len l1_s0))) (let ((l1_s3 (= l1_s1 l1_s2))) (let ((l1_s5 (seq.nth l1_s0 l1_s2)))- (let ((l1_s7 (fp.add roundNearestTiesToEven l1_s5 l1_s6)))+ (let ((l1_s7 (bvadd l1_s5 l1_s6))) (let ((l1_s8 (seq.unit l1_s7))) (let ((l1_s10 (- l1_s1 l1_s9))) (let ((l1_s11 (seq.extract l1_s0 l1_s9 l1_s10)))- (let ((l1_s12 (|sbv.map @(SBV Float -> SBV Float)_55d10191cd @(SBV [Float] -> SBV [Float])| l1_s11)))+ (let ((l1_s12 (|sbv.map @(SBV Int64 -> SBV Int64)_bc2a222730 @(SBV [Int64] -> SBV [Int64])| l1_s11))) (let ((l1_s13 (seq.++ l1_s8 l1_s12))) (let ((l1_s14 (ite l1_s3 l1_s4 l1_s13))) l1_s14))))))))))))))) [GOOD] ; --- assignments --- [GOOD] (define-fun s3 () Bool (= s0 s2))-[GOOD] (define-fun s4 () (Seq (_ FloatingPoint 8 24)) (|sbv.map @(SBV Float -> SBV Float)_55d10191cd @(SBV [Float] -> SBV [Float])| s0))+[GOOD] (define-fun s4 () (Seq (_ BitVec 64)) (|sbv.map @(SBV Int64 -> SBV Int64)_bc2a222730 @(SBV [Int64] -> SBV [Int64])| s0)) [GOOD] (define-fun s5 () Bool (= s1 s4)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula ---@@ -49,26 +49,26 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s1))-[RECV] ((s1 (seq.++ (seq.unit (fp #b0 #x80 #b00000000000000000000000))- (seq.unit (fp #b0 #x80 #b10000000000000000000000))- (seq.unit (fp #b0 #x81 #b00000000000000000000000))- (seq.unit (fp #b0 #x81 #b01000000000000000000000))- (seq.unit (fp #b0 #x81 #b10000000000000000000000)))))+[RECV] ((s1 (seq.++ (seq.unit #x0000000000000002)+ (seq.unit #x0000000000000003)+ (seq.unit #x0000000000000004)+ (seq.unit #x0000000000000005)+ (seq.unit #x0000000000000006)))) [SEND] (get-value (s0))-[RECV] ((s0 (seq.++ (seq.unit (fp #b0 #x7f #b00000000000000000000000))- (seq.unit (fp #b0 #x80 #b00000000000000000000000))- (seq.unit (fp #b0 #x80 #b10000000000000000000000))- (seq.unit (fp #b0 #x81 #b00000000000000000000000))- (seq.unit (fp #b0 #x81 #b01000000000000000000000)))))+[RECV] ((s0 (seq.++ (seq.unit #x0000000000000001)+ (seq.unit #x0000000000000002)+ (seq.unit #x0000000000000003)+ (seq.unit #x0000000000000004)+ (seq.unit #x0000000000000005)))) [SEND] (get-value (s1))-[RECV] ((s1 (seq.++ (seq.unit (fp #b0 #x80 #b00000000000000000000000))- (seq.unit (fp #b0 #x80 #b10000000000000000000000))- (seq.unit (fp #b0 #x81 #b00000000000000000000000))- (seq.unit (fp #b0 #x81 #b01000000000000000000000))- (seq.unit (fp #b0 #x81 #b10000000000000000000000)))))+[RECV] ((s1 (seq.++ (seq.unit #x0000000000000002)+ (seq.unit #x0000000000000003)+ (seq.unit #x0000000000000004)+ (seq.unit #x0000000000000005)+ (seq.unit #x0000000000000006)))) *** Solver : Z3 *** Exit code: ExitSuccess RESULT:- s0 = [1.0,2.0,3.0,4.0,5.0] :: [Float]- s1 = [2.0,3.0,4.0,5.0,6.0] :: [Float]+ s0 = [1,2,3,4,5] :: [Int64]+ s1 = [2,3,4,5,6] :: [Int64]
+ SBVTestSuite/GoldFiles/listFloat1.gold view
@@ -0,0 +1,18 @@++EXCEPTION:++*** Data.SBV: Unsupported complicated comparison:+***+*** Op : ==+*** Type: [SFloat]+***+*** Due to the presence of NaN, comparisons over this type require+*** special support in SMTLib. And in general this can lead to+*** performance issues since the comparison is no longer a natively+*** supported operation in the logic.+***+*** NB. If you want the semantics NaN == NaN, and +0 /= -0, then you can use .=== instead.+***+*** For this case, please use: Data.SBV.List.listEq+*** but beware of performance/decidability implications.+
+ SBVTestSuite/GoldFiles/listFloat2.gold view
@@ -0,0 +1,56 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-option :pp.max_depth 4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def true )+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] ; --- top level inputs ---+[GOOD] (declare-fun s0 () (_ FloatingPoint 8 24)) ; tracks user variable "x"+[GOOD] ; --- constant tables ---+[GOOD] ; --- non-constant tables ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user defined functions ---+[GOOD] ; |listEq @(SBV [Float] -> SBV [Float] -> SBV Bool)| :: [SFloat] -> [SFloat] -> SBool [Recursive]+[GOOD] (define-fun-rec |listEq @(SBV [Float] -> SBV [Float] -> SBV Bool)| ((l1_s0 (Seq (_ FloatingPoint 8 24))) (l1_s1 (Seq (_ FloatingPoint 8 24)))) Bool+ (let ((l1_s3 0))+ (let ((l1_s10 1))+ (let ((l1_s2 (seq.len l1_s0)))+ (let ((l1_s4 (= l1_s2 l1_s3)))+ (let ((l1_s5 (seq.len l1_s1)))+ (let ((l1_s6 (= l1_s3 l1_s5)))+ (let ((l1_s7 (seq.nth l1_s0 l1_s3)))+ (let ((l1_s8 (seq.nth l1_s1 l1_s3)))+ (let ((l1_s9 (fp.eq l1_s7 l1_s8)))+ (let ((l1_s11 (- l1_s2 l1_s10)))+ (let ((l1_s12 (seq.extract l1_s0 l1_s10 l1_s11)))+ (let ((l1_s13 (- l1_s5 l1_s10)))+ (let ((l1_s14 (seq.extract l1_s1 l1_s10 l1_s13)))+ (let ((l1_s15 (|listEq @(SBV [Float] -> SBV [Float] -> SBV Bool)| l1_s12 l1_s14)))+ (let ((l1_s16 (and l1_s9 l1_s15)))+ (let ((l1_s17 (ite l1_s4 l1_s6 l1_s16)))+ l1_s17)))))))))))))))))+[GOOD] ; --- assignments ---+[GOOD] (define-fun s1 () (Seq (_ FloatingPoint 8 24)) (seq.unit s0))+[GOOD] (define-fun s2 () Bool (|listEq @(SBV [Float] -> SBV [Float] -> SBV Bool)| s1 s1))+[GOOD] ; --- delayedEqualities ---+[GOOD] ; --- formula ---+[GOOD] (assert (not s2))+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (_ NaN 8 24)))+*** Solver : Z3+*** Exit code: ExitSuccess++FINAL OUTPUT:+Falsifiable. Counter-example:+ x = NaN :: Float
+ SBVTestSuite/GoldFiles/listFloat3.gold view
@@ -0,0 +1,34 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-option :pp.max_depth 4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def true )+[GOOD] (set-logic ALL) ; has lists, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] ; --- top level inputs ---+[GOOD] (declare-fun s0 () (_ FloatingPoint 8 24)) ; tracks user variable "x"+[GOOD] ; --- constant tables ---+[GOOD] ; --- non-constant tables ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user defined functions ---+[GOOD] ; --- assignments ---+[GOOD] (define-fun s1 () (Seq (_ FloatingPoint 8 24)) (seq.unit s0))+[GOOD] (define-fun s2 () Bool (= s1 s1))+[GOOD] ; --- delayedEqualities ---+[GOOD] ; --- formula ---+[GOOD] (assert (not s2))+[SEND] (check-sat)+[RECV] unsat+*** Solver : Z3+*** Exit code: ExitSuccess++FINAL OUTPUT:+Q.E.D.
SBVTestSuite/GoldFiles/tuple_enum.gold view
@@ -65,9 +65,9 @@ ((mkSBVTuple3 (proj_1_SBVTuple3 T1) (proj_2_SBVTuple3 T2) (proj_3_SBVTuple3 T3))))))-[GOOD] (declare-fun s24 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E String (_ FloatingPoint 8 24))))+[GOOD] (declare-fun s24 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E String Int))) [GOOD] (assert (= 1 (str.len (proj_2_SBVTuple3 (proj_2_SBVTuple2 s24)))))-[GOOD] (define-fun s25 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E String (_ FloatingPoint 8 24))) (mkSBVTuple2 #x05 (mkSBVTuple3 C (_ char #x41) ((_ to_fp 8 24) roundNearestTiesToEven (/ 8514437.0 1048576.0)))))+[GOOD] (define-fun s25 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E String Int)) (mkSBVTuple2 #x05 (mkSBVTuple3 C (_ char #x41) 812))) [GOOD] (define-fun s26 () Bool (= s24 s25)) [GOOD] (assert s26) [GOOD] (define-fun s27 () (Seq (SBVTuple2 E (Seq Bool))) (seq.++ (seq.unit (mkSBVTuple2 B (as seq.empty (Seq Bool)))) (seq.unit (mkSBVTuple2 A (seq.++ (seq.unit true) (seq.unit false)))) (seq.unit (mkSBVTuple2 C (seq.++ (seq.unit false) (seq.unit false) (seq.unit false) (seq.unit false) (seq.unit true) (seq.unit false))))))@@ -85,9 +85,9 @@ (seq.unit false) (seq.++ (seq.unit true) (seq.unit false)))))))) [SEND] (get-value (s24))-[RECV] ((s24 (mkSBVTuple2 #x05 (mkSBVTuple3 C "A" (fp #b0 #x82 #b00000011110101110000101)))))+[RECV] ((s24 (mkSBVTuple2 #x05 (mkSBVTuple3 C "A" 812)))) *** Solver : Z3 *** Exit code: ExitSuccess - FINAL: ([(B,[]),(A,[True,False]),(C,[False,False,False,False,True,False])],(5,(C,'A',8.12)))+ FINAL: ([(B,[]),(A,[True,False]),(C,[False,False,False,False,True,False])],(5,(C,'A',812))) DONE!
SBVTestSuite/TestSuite/Arrays/InitVals.hs view
@@ -125,9 +125,6 @@ , goldenCapturedIO "array_misc_30" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (-(1/0))) , goldenCapturedIO "array_misc_31" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Integer))- , goldenCapturedIO "array_misc_32" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double))- , goldenCapturedIO "array_misc_33" $ t proveWith (listArray [(1, 2), (3, 1)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double))- , goldenCapturedIO "array_misc_34" $ t proveWith (listArray [(1, 2), (3, 1)] 5 ./= listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double)) ] ] where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f
SBVTestSuite/TestSuite/Basics/Lambda.hs view
@@ -72,7 +72,7 @@ , P.sum . P.map P.sum ) - , goldenCapturedIO "lambda08" $ eval1 [1 .. 5 :: Float] (mapl (+1), P.map (+1))+ , goldenCapturedIO "lambda08" $ eval1 [1 .. 5 :: Int64] (mapl (+1), P.map (+1)) , goldenCapturedIO "lambda09" $ eval1 [1 .. 5 :: Int8] (mapl (+1), P.map (+1)) , goldenCapturedIO "lambda10" $ eval1 [1 .. 5 :: Integer] (mapl (+1), P.map (+1)) , goldenCapturedIO "lambda11" $ eval1 [1 .. 5 :: Word8] (mapl (+1), P.map (+1))
SBVTestSuite/TestSuite/Basics/List.hs view
@@ -9,6 +9,7 @@ -- Test the sequence/list functions. ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -20,6 +21,8 @@ import Data.SBV.Control import Utils.SBVTestFramework +import qualified Control.Exception as C+ import Prelude hiding ((++), (!!)) import qualified Prelude as P ((++)) @@ -46,6 +49,9 @@ , goldenCapturedIO "seqExamples6" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqExamples6 Unsat , goldenCapturedIO "seqExamples7" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqExamples7 Sat , goldenCapturedIO "seqExamples8" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqExamples8 Unsat+ , goldenCapturedIO "listFloat1" $ run listFloat1+ , goldenCapturedIO "listFloat2" $ run listFloat2+ , goldenCapturedIO "listFloat3" $ run listFloat3 , testCase "seqExamples9" $ assert seqExamples9 ] @@ -145,3 +151,20 @@ vals = sort $ concat (catMaybes (getModelValues "s" m) :: [[Word8]]) return $ vals == [0..255]++run :: Provable a => a -> FilePath -> IO ()+run t gf = do r <- proveWith defaultSMTCfg{verbose=True, redirectVerbose = Just gf} t+ appendFile gf ("\nFINAL OUTPUT:\n" <> show r <> "\n")+ `C.catch` (\(e :: C.SomeException) -> appendFile gf ("\nEXCEPTION:\n" <> show e <> "\n"))++listFloat1 :: Symbolic SBool+listFloat1 = do x :: SFloat <- free "x"+ pure $ L.singleton x .== L.singleton x++listFloat2 :: Symbolic SBool+listFloat2 = do x :: SFloat <- free "x"+ pure $ L.singleton x `L.listEq` L.singleton x++listFloat3 :: Symbolic SBool+listFloat3 = do x :: SFloat <- free "x"+ pure $ L.singleton x .=== L.singleton x
SBVTestSuite/TestSuite/Basics/Tuple.hs view
@@ -98,7 +98,7 @@ query $ do _ <- checkSat getValue lst -enum :: Symbolic ([(E, [Bool])], (Word8, (E, Char, Float)))+enum :: Symbolic ([(E, [Bool])], (Word8, (E, Char, Integer))) enum = do vTup1 :: SList (E, [Bool]) <- sList "v1" q <- sBool "q"@@ -112,8 +112,8 @@ constrain $ b !! 4 .== sTrue query $ do- vTup2 :: STuple Word8 (E, Char, Float) <- freshVar "v2"- constrain $ vTup2 .== literal (5, (C, 'A', 8.12))+ vTup2 :: STuple Word8 (E, Char, Integer) <- freshVar "v2"+ constrain $ vTup2 .== literal (5, (C, 'A', 812)) constrain $ vTup1 .== literal [(B, []), (A, [True, False]), (C, [False, False, False, False, True, False])]
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 12.0+Version : 12.1 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT