diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,17 @@ * Hackage: * GitHub: +### 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 diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -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, "^") ] diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs --- a/Data/SBV/Core/Data.hs +++ b/Data/SBV/Core/Data.hs @@ -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 diff --git a/Data/SBV/Core/Kind.hs b/Data/SBV/Core/Kind.hs --- a/Data/SBV/Core/Kind.hs +++ b/Data/SBV/Core/Kind.hs @@ -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 diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -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) diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs --- a/Data/SBV/Core/Operations.hs +++ b/Data/SBV/Core/Operations.hs @@ -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 diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -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 ] diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -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@? -- diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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.<") diff --git a/Data/SBV/TP/List.hs b/Data/SBV/TP/List.hs --- a/Data/SBV/TP/List.hs +++ b/Data/SBV/TP/List.hs @@ -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@ -- diff --git a/Data/SBV/TP/TP.hs b/Data/SBV/TP/TP.hs --- a/Data/SBV/TP/TP.hs +++ b/Data/SBV/TP/TP.hs @@ -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 diff --git a/Documentation/SBV/Examples/Queries/CaseSplit.hs b/Documentation/SBV/Examples/Queries/CaseSplit.hs --- a/Documentation/SBV/Examples/Queries/CaseSplit.hs +++ b/Documentation/SBV/Examples/Queries/CaseSplit.hs @@ -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) diff --git a/Documentation/SBV/Examples/TP/SumReverse.hs b/Documentation/SBV/Examples/TP/SumReverse.hs --- a/Documentation/SBV/Examples/TP/SumReverse.hs +++ b/Documentation/SBV/Examples/TP/SumReverse.hs @@ -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 diff --git a/SBVTestSuite/GoldFiles/array_misc_32.gold b/SBVTestSuite/GoldFiles/array_misc_32.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/array_misc_32.gold +++ /dev/null @@ -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. diff --git a/SBVTestSuite/GoldFiles/array_misc_33.gold b/SBVTestSuite/GoldFiles/array_misc_33.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/array_misc_33.gold +++ /dev/null @@ -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 diff --git a/SBVTestSuite/GoldFiles/array_misc_34.gold b/SBVTestSuite/GoldFiles/array_misc_34.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/array_misc_34.gold +++ /dev/null @@ -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. diff --git a/SBVTestSuite/GoldFiles/lambda08.gold b/SBVTestSuite/GoldFiles/lambda08.gold --- a/SBVTestSuite/GoldFiles/lambda08.gold +++ b/SBVTestSuite/GoldFiles/lambda08.gold @@ -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] diff --git a/SBVTestSuite/GoldFiles/listFloat1.gold b/SBVTestSuite/GoldFiles/listFloat1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/listFloat1.gold @@ -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. + diff --git a/SBVTestSuite/GoldFiles/listFloat2.gold b/SBVTestSuite/GoldFiles/listFloat2.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/listFloat2.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/listFloat3.gold b/SBVTestSuite/GoldFiles/listFloat3.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/listFloat3.gold @@ -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. diff --git a/SBVTestSuite/GoldFiles/tuple_enum.gold b/SBVTestSuite/GoldFiles/tuple_enum.gold --- a/SBVTestSuite/GoldFiles/tuple_enum.gold +++ b/SBVTestSuite/GoldFiles/tuple_enum.gold @@ -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! diff --git a/SBVTestSuite/TestSuite/Arrays/InitVals.hs b/SBVTestSuite/TestSuite/Arrays/InitVals.hs --- a/SBVTestSuite/TestSuite/Arrays/InitVals.hs +++ b/SBVTestSuite/TestSuite/Arrays/InitVals.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Basics/Lambda.hs b/SBVTestSuite/TestSuite/Basics/Lambda.hs --- a/SBVTestSuite/TestSuite/Basics/Lambda.hs +++ b/SBVTestSuite/TestSuite/Basics/Lambda.hs @@ -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)) diff --git a/SBVTestSuite/TestSuite/Basics/List.hs b/SBVTestSuite/TestSuite/Basics/List.hs --- a/SBVTestSuite/TestSuite/Basics/List.hs +++ b/SBVTestSuite/TestSuite/Basics/List.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Basics/Tuple.hs b/SBVTestSuite/TestSuite/Basics/Tuple.hs --- a/SBVTestSuite/TestSuite/Basics/Tuple.hs +++ b/SBVTestSuite/TestSuite/Basics/Tuple.hs @@ -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])] diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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