diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,27 @@ * Hackage: * GitHub: -* Latest Hackage released version: 7.10, 2018-07-20 +* Latest Hackage released version: 7.11, 2018-09-20 + +### Version 7.11, 2018-09-20 + + * Add support for symbolic lists. (That is, arbitrary but fixed length symbolic + lists of integers, floats, reals, etc. Nested lists are allowed as well.) + This is building on top of Joel Burget's initial work for supporting symbolic + strings and sequences, as supported by Z3. Note that the list theory solvers + are incomplete, so some queries might receive an unknown answer. See + "Documentation/SBV/Examples/Lists/Fibonacci.hs" for an example, and the + module "Data.SBV.List" for details. + + * A new module 'Data.SBV.List.Bounded' provides extra functions to manipulate + lists with given concrete bounds. Note that SMT solvers cannot deal with + recursive functions/inductive proofs in general, so the utilities in this + file can come in handy when expressing bounded-model-checking style + algorithms. See "Documentation/SBV/Examples/Lists/BoundedMutex.hs" for a + simple mutex algorithm proof. + + * Remove dependency on data-binary-ieee754 package; which is no longer + supported. ### Version 7.10, 2018-07-20 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -144,18 +144,21 @@ , SReal, AlgReal, sRealToSInteger -- ** Characters, Strings and Regular Expressions -- $strings - , SChar, SString, (.++), (.!!) + , SChar, SString + -- ** Symbolic lists + -- $lists + , SList -- * Arrays of symbolic values , SymArray(newArray_, newArray, readArray, writeArray), SArray, SFunArray -- * Creating symbolic values -- ** Single value -- $createSym - , sBool, sWord8, sWord16, sWord32, sWord64, sInt8, sInt16, sInt32, sInt64, sInteger, sReal, sFloat, sDouble, sChar, sString + , sBool, sWord8, sWord16, sWord32, sWord64, sInt8, sInt16, sInt32, sInt64, sInteger, sReal, sFloat, sDouble, sChar, sString, sList -- ** List of values -- $createSyms - , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sInt8s, sInt16s, sInt32s, sInt64s, sIntegers, sReals, sFloats, sDoubles, sChars, sStrings + , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sInt8s, sInt16s, sInt32s, sInt64s, sIntegers, sReals, sFloats, sDoubles, sChars, sStrings, sLists -- * Symbolic Equality and Comparisons , EqSymbolic(..), OrdSymbolic(..), Equality(..) @@ -293,7 +296,6 @@ import Data.SBV.Core.Model import Data.SBV.Core.Floating import Data.SBV.Core.Splittable -import Data.SBV.String ((.++), (.!!)) import Data.SBV.Provers.Prover @@ -714,7 +716,16 @@ that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental. -See "Data.SBV.Char", "Data.SBV.String", "Data.SBV.RegExp" for further related functions. +See "Data.SBV.Char", "Data.SBV.String", "Data.SBV.RegExp" for related functions. +-} + +{- $lists +Support for symbolic lists (intial version contributed by Joel Burget) +adds support for sequence support, described here: . Note +that this logic is still not part of official SMTLib (as of March 2018), so it should be considered +experimental. + +See "Data.SBV.List" for related functions. -} {- $shiftRotate diff --git a/Data/SBV/Char.hs b/Data/SBV/Char.hs --- a/Data/SBV/Char.hs +++ b/Data/SBV/Char.hs @@ -1,7 +1,3 @@ -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE OverloadedStrings #-} - ----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Char @@ -24,6 +20,10 @@ -- For details, see: ----------------------------------------------------------------------------- +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings #-} + module Data.SBV.Char ( -- * Occurrence in a string elem, notElem @@ -48,7 +48,7 @@ import qualified Data.Char as C -import Data.SBV.String (isInfixOf, charToStr) +import Data.SBV.String (isInfixOf, singleton) -- For doctest use only -- @@ -59,7 +59,7 @@ -- | Is the character in the string? -- -- >>> :set -XOverloadedStrings --- >>> prove $ \c -> c `elem` charToStr c +-- >>> prove $ \c -> c `elem` singleton c -- Q.E.D. -- >>> prove $ \c -> bnot (c `elem` "") -- Q.E.D. @@ -70,7 +70,7 @@ | Just cs <- unliteral s -- If only the second string is concrete, element-wise checking is still much better! = bAny (c .==) $ map literal cs | True - = charToStr c `isInfixOf` s + = singleton c `isInfixOf` s -- | Is the character not in the string? -- 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 @@ -190,6 +190,7 @@ KDouble -> specF CgDouble KString -> text "%s" KChar -> text "%c" + KList k -> die $ "list sort: " ++ show k KUserSort s _ -> die $ "uninterpreted sort: " ++ s where spec :: (Bool, Int) -> Doc spec (False, 1) = text "%d" @@ -485,6 +486,7 @@ len KBool = 5 -- SBool len (KBounded False n) = 5 + length (show n) -- SWordN len (KBounded True n) = 4 + length (show n) -- SIntN + len (KList s) = die $ "List sort: " ++ show s len (KUserSort s _) = die $ "Uninterpreted sort: " ++ s getMax 8 _ = 8 -- 8 is the max we can get with SInteger, so don't bother looking any further getMax m [] = m @@ -736,6 +738,7 @@ KUnbounded -> case cgInteger cfg of Nothing -> (True, True) -- won't matter, it'll be rejected later Just i -> (True, canOverflow True i) + KList s -> die $ "List sort " ++ show s KUserSort s _ -> die $ "Uninterpreted sort: " ++ s -- Div/Rem should be careful on 0, in the SBV world x `div` 0 is 0, x `rem` 0 is x -- NB: Quot is supposed to truncate toward 0; Not clear to me if C guarantees this behavior. diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -38,9 +38,11 @@ import Data.Maybe (isJust) import Data.List (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate) -import Data.Char (isPunctuation, isSpace, chr) +import Data.Char (isPunctuation, isSpace, chr, ord) import Data.Function (on) +import Data.Typeable (Typeable) + import Data.Int import Data.Word @@ -80,7 +82,7 @@ import Data.SBV.SMT.SMTLib (toIncSMTLib, toSMTLib) import Data.SBV.SMT.Utils (showTimeoutValue, addAnnotations, alignPlain, debug, mergeSExpr, SBVException(..)) -import Data.SBV.Utils.Lib (qfsToString) +import Data.SBV.Utils.Lib (qfsToString, isKString) import Data.SBV.Utils.SExpr import Data.SBV.Control.Types @@ -91,6 +93,8 @@ import GHC.Stack +import Unsafe.Coerce (unsafeCoerce) -- Only used safely! + -- | 'Query' as a 'SolverContext'. instance SolverContext Query where constrain = addQueryConstraint False [] @@ -365,16 +369,34 @@ sexprToVal (ENum (v, _)) = Just (fromIntegral v) sexprToVal _ = Nothing -instance SMTValue String where - sexprToVal (ECon s) - | length s >= 2 && head s == '"' && last s == '"' - = Just (tail (init s)) - sexprToVal _ = Nothing - instance SMTValue Char where sexprToVal (ENum (i, _)) = Just (chr (fromIntegral i)) sexprToVal _ = Nothing +instance (SMTValue a, Typeable a) => SMTValue [a] where + -- NB. The conflation of String/[Char] forces us to have this bastard case here + -- with unsafeCoerce to cast back to a regular string. This is unfortunate, + -- and the ice is thin here. But it works, and is much better than a plethora + -- of overlapping instances. Sigh. + sexprToVal (ECon s) + | isKString (undefined :: [a]) && length s >= 2 && head s == '"' && last s == '"' + = Just $ map unsafeCoerce s' + | True + = Just $ map (unsafeCoerce . c2w8) s' + where s' = qfsToString (tail (init s)) + c2w8 :: Char -> Word8 + c2w8 = fromIntegral . ord + + -- Otherwise we have a good old sequence, just parse it simply: + sexprToVal (EApp [ECon "seq.++", l, r]) = do l' <- sexprToVal l + r' <- sexprToVal r + return $ l' ++ r' + sexprToVal (EApp [ECon "seq.unit", a]) = do a' <- sexprToVal a + return [a'] + sexprToVal (EApp [ECon "as", ECon "seq.empty", _]) = return [] + + sexprToVal _ = Nothing + -- | Get the value of a term. getValue :: SMTValue a => SBV a -> Query a getValue s = do sw <- inNewContext (`sbvToSW` s) @@ -400,7 +422,7 @@ r <- ask cmd parse r bad $ \case EApp [EApp [ECon o, ECon v]] | o == show sw -> return v - _ -> bad r Nothing + _ -> bad r Nothing k -> error $ unlines ["" , "*** SBV.getUninterpretedValue: Called on an 'interpreted' kind" @@ -442,18 +464,44 @@ EDouble i | isDouble k -> Just $ CW KDouble (CWDouble i) ECon s | isString k -> Just $ CW KString (CWString (interpretString s)) ECon s | isUninterpreted k -> Just $ CW k (CWUserSort (getUIIndex k s, s)) + _ | isList k -> Just $ CW k (CWList (interpretList e)) _ -> Nothing where isIntegralLike = or [f k | f <- [isBoolean, isBounded, isInteger, isReal, isFloat, isDouble]] getUIIndex (KUserSort _ (Right xs)) i = i `elemIndex` xs getUIIndex _ _ = Nothing + stringLike xs = length xs >= 2 && head xs == '"' && last xs == '"' + -- Make sure strings are really strings interpretString xs - | length xs < 2 || head xs /= '"' || last xs /= '"' + | not (stringLike xs) = error $ "Expected a string constant with quotes, received: <" ++ xs ++ ">" | True = qfsToString $ tail (init xs) + + isStringSequence (KList (KBounded _ 8)) = True + isStringSequence _ = False + + -- Lists are tricky since z3 prints the 8-bit variants as strings. See: + interpretList (ECon s) + | isStringSequence k && stringLike s + = map (CWInteger . fromIntegral . ord) $ interpretString s + interpretList topExpr = walk topExpr + where walk (EApp [ECon "as", ECon "seq.empty", _]) = [] + walk (EApp [ECon "seq.unit", v]) = case recoverKindedValue ek v of + Just w -> [cwVal w] + Nothing -> error $ "Cannot parse a sequence item of kind " ++ show ek ++ " from: " ++ show v ++ extra v + walk (EApp [ECon "seq.++", pre, post]) = walk pre ++ walk post + walk cur = error $ "Expected a sequence constant, but received: " ++ show cur ++ extra cur + + extra cur | show cur == t = "" + | True = "\nWhile parsing: " ++ t + where t = show topExpr + + ek = case k of + KList ik -> ik + _ -> error $ "Impossible: Expected a sequence kind, bug got: " ++ show k -- | Get the value of a term. If the kind is Real and solver supports decimal approximations, -- we will "squash" the representations. diff --git a/Data/SBV/Core/Concrete.hs b/Data/SBV/Core/Concrete.hs --- a/Data/SBV/Core/Concrete.hs +++ b/Data/SBV/Core/Concrete.hs @@ -19,7 +19,7 @@ import System.Random (randomIO, randomRIO) import Data.Char (chr) -import Data.List (isPrefixOf) +import Data.List (isPrefixOf, intercalate) import Data.SBV.Core.Kind import Data.SBV.Core.AlgReals @@ -33,78 +33,45 @@ | CWDouble !Double -- ^ double | CWChar !Char -- ^ character | CWString !String -- ^ string + | CWList ![CWVal] -- ^ list | CWUserSort !(Maybe Int, String) -- ^ value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations +-- | Assing a rank to CW Values, this is structural and helps with ordering +cwRank :: CWVal -> Int +cwRank CWAlgReal {} = 0 +cwRank CWInteger {} = 1 +cwRank CWFloat {} = 2 +cwRank CWDouble {} = 3 +cwRank CWChar {} = 4 +cwRank CWString {} = 5 +cwRank CWList {} = 6 +cwRank CWUserSort {} = 7 + -- | Eq instance for CWVal. Note that we cannot simply derive Eq/Ord, since CWAlgReal doesn't have proper -- instances for these when values are infinitely precise reals. However, we do -- need a structural eq/ord for Map indexes; so define custom ones here: instance Eq CWVal where - CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b - CWInteger a == CWInteger b = a == b - CWUserSort a == CWUserSort b = a == b - CWFloat a == CWFloat b = a `fpIsEqualObjectH` b -- We don't want +0/-0 to be confused; and also we want NaN = NaN here! - CWDouble a == CWDouble b = a `fpIsEqualObjectH` b -- ditto - CWChar a == CWChar b = a == b - CWString a == CWString b = a == b - _ == _ = False + CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b + CWInteger a == CWInteger b = a == b + CWFloat a == CWFloat b = a `fpIsEqualObjectH` b -- We don't want +0/-0 to be confused; and also we want NaN = NaN here! + CWDouble a == CWDouble b = a `fpIsEqualObjectH` b -- ditto + CWChar a == CWChar b = a == b + CWString a == CWString b = a == b + CWList a == CWList b = a == b + CWUserSort a == CWUserSort b = a == b + _ == _ = False -- | Ord instance for CWVal. Same comments as the 'Eq' instance why this cannot be derived. instance Ord CWVal where - CWAlgReal a `compare` CWAlgReal b = a `algRealStructuralCompare` b - CWAlgReal _ `compare` CWInteger _ = LT - CWAlgReal _ `compare` CWFloat _ = LT - CWAlgReal _ `compare` CWDouble _ = LT - CWAlgReal _ `compare` CWChar _ = LT - CWAlgReal _ `compare` CWString _ = LT - CWAlgReal _ `compare` CWUserSort _ = LT - - CWInteger _ `compare` CWAlgReal _ = GT - CWInteger a `compare` CWInteger b = a `compare` b - CWInteger _ `compare` CWFloat _ = LT - CWInteger _ `compare` CWDouble _ = LT - CWInteger _ `compare` CWChar _ = LT - CWInteger _ `compare` CWString _ = LT - CWInteger _ `compare` CWUserSort _ = LT - - CWFloat _ `compare` CWAlgReal _ = GT - CWFloat _ `compare` CWInteger _ = GT - CWFloat a `compare` CWFloat b = a `fpCompareObjectH` b - CWFloat _ `compare` CWDouble _ = LT - CWFloat _ `compare` CWChar _ = LT - CWFloat _ `compare` CWString _ = LT - CWFloat _ `compare` CWUserSort _ = LT - - CWDouble _ `compare` CWAlgReal _ = GT - CWDouble _ `compare` CWInteger _ = GT - CWDouble _ `compare` CWFloat _ = GT - CWDouble a `compare` CWDouble b = a `fpCompareObjectH` b - CWDouble _ `compare` CWChar _ = LT - CWDouble _ `compare` CWString _ = LT - CWDouble _ `compare` CWUserSort _ = LT - - CWChar _ `compare` CWAlgReal _ = GT - CWChar _ `compare` CWInteger _ = GT - CWChar _ `compare` CWFloat _ = GT - CWChar _ `compare` CWDouble _ = GT - CWChar a `compare` CWChar b = a `compare` b - CWChar _ `compare` CWString _ = LT - CWChar _ `compare` CWUserSort _ = LT - - CWString _ `compare` CWAlgReal _ = GT - CWString _ `compare` CWInteger _ = GT - CWString _ `compare` CWFloat _ = GT - CWString _ `compare` CWDouble _ = GT - CWString _ `compare` CWChar _ = GT - CWString a `compare` CWString b = a `compare` b - CWString _ `compare` CWUserSort _ = LT - - CWUserSort _ `compare` CWAlgReal _ = GT - CWUserSort _ `compare` CWInteger _ = GT - CWUserSort _ `compare` CWFloat _ = GT - CWUserSort _ `compare` CWDouble _ = GT - CWUserSort _ `compare` CWChar _ = GT - CWUserSort _ `compare` CWString _ = GT - CWUserSort a `compare` CWUserSort b = a `compare` b + CWAlgReal a `compare` CWAlgReal b = a `algRealStructuralCompare` b + CWInteger a `compare` CWInteger b = a `compare` b + CWFloat a `compare` CWFloat b = a `fpCompareObjectH` b + CWDouble a `compare` CWDouble b = a `fpCompareObjectH` b + CWChar a `compare` CWChar b = a `compare` b + CWString a `compare` CWString b = a `compare` b + CWList a `compare` CWList b = a `compare` b + CWUserSort a `compare` CWUserSort b = a `compare` b + a `compare` b = cwRank a `compare` cwRank b -- | 'CW' represents a concrete word of a fixed size: -- For signed words, the most significant digit is considered to be the sign. @@ -215,26 +182,28 @@ trueCW = CW KBool (CWInteger 1) -- | Lift a unary function through a CW -liftCW :: (AlgReal -> b) -> (Integer -> b) -> (Float -> b) -> (Double -> b) -> (Char -> b) -> (String -> b) -> ((Maybe Int, String) -> b) -> CW -> b -liftCW f _ _ _ _ _ _ (CW _ (CWAlgReal v)) = f v -liftCW _ f _ _ _ _ _ (CW _ (CWInteger v)) = f v -liftCW _ _ f _ _ _ _ (CW _ (CWFloat v)) = f v -liftCW _ _ _ f _ _ _ (CW _ (CWDouble v)) = f v -liftCW _ _ _ _ f _ _ (CW _ (CWChar v)) = f v -liftCW _ _ _ _ _ f _ (CW _ (CWString v)) = f v -liftCW _ _ _ _ _ _ f (CW _ (CWUserSort v)) = f v +liftCW :: (AlgReal -> b) -> (Integer -> b) -> (Float -> b) -> (Double -> b) -> (Char -> b) -> (String -> b) -> ((Maybe Int, String) -> b) -> ([CWVal] -> b) -> CW -> b +liftCW f _ _ _ _ _ _ _ (CW _ (CWAlgReal v)) = f v +liftCW _ f _ _ _ _ _ _ (CW _ (CWInteger v)) = f v +liftCW _ _ f _ _ _ _ _ (CW _ (CWFloat v)) = f v +liftCW _ _ _ f _ _ _ _ (CW _ (CWDouble v)) = f v +liftCW _ _ _ _ f _ _ _ (CW _ (CWChar v)) = f v +liftCW _ _ _ _ _ f _ _ (CW _ (CWString v)) = f v +liftCW _ _ _ _ _ _ f _ (CW _ (CWUserSort v)) = f v +liftCW _ _ _ _ _ _ _ f (CW _ (CWList v)) = f v -- | Lift a binary function through a CW -liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> (Char -> Char -> b) -> (String -> String -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b -liftCW2 r i f d c s u x y = case (cwVal x, cwVal y) of - (CWAlgReal a, CWAlgReal b) -> r a b - (CWInteger a, CWInteger b) -> i a b - (CWFloat a, CWFloat b) -> f a b - (CWDouble a, CWDouble b) -> d a b - (CWChar a, CWChar b) -> c a b - (CWString a, CWString b) -> s a b - (CWUserSort a, CWUserSort b) -> u a b - _ -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y) +liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> (Char -> Char -> b) -> (String -> String -> b) -> ([CWVal] -> [CWVal] -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b +liftCW2 r i f d c s u v x y = case (cwVal x, cwVal y) of + (CWAlgReal a, CWAlgReal b) -> r a b + (CWInteger a, CWInteger b) -> i a b + (CWFloat a, CWFloat b) -> f a b + (CWDouble a, CWDouble b) -> d a b + (CWChar a, CWChar b) -> c a b + (CWString a, CWString b) -> s a b + (CWList a, CWList b) -> u a b + (CWUserSort a, CWUserSort b) -> v a b + _ -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y) -- | Map a unary function through a CW. mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (Char -> Char) -> (String -> String) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW @@ -246,6 +215,7 @@ CWChar a -> CWChar (c a) CWString a -> CWString (s a) CWUserSort a -> CWUserSort (u a) + CWList{} -> error "Data.SBV.mapCW: Unexpected call through mapCW with lists!" -- | Map a binary function through a CW. mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> (Char -> Char -> Char) -> (String -> String -> String) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW @@ -257,6 +227,7 @@ (True, CWChar a, CWChar b) -> normCW $ CW (kindOf x) (CWChar (c a b)) (True, CWString a, CWString b) -> normCW $ CW (kindOf x) (CWString (s a b)) (True, CWUserSort a, CWUserSort b) -> normCW $ CW (kindOf x) (CWUserSort (u a b)) + (True, CWList{}, CWList{}) -> error "Data.SBV.mapCW2: Unexpected call through mapCW2 with lists!" _ -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y) -- | Show instance for 'CW'. @@ -271,9 +242,13 @@ -- | Show a CW, with kind info if bool is True showCW :: Bool -> CW -> String showCW shk w | isBoolean w = show (cwToBool w) ++ (if shk then " :: Bool" else "") -showCW shk w = liftCW show show show show show show snd w ++ kInfo +showCW shk w = liftCW show show show show show show snd shL w ++ kInfo where kInfo | shk = " :: " ++ showBaseKind (kindOf w) | True = "" + shL xs = "[" ++ intercalate "," (map (showCW False . CW ke) xs) ++ "]" + where ke = case kindOf w of + KList k -> k + kw -> error $ "Data.SBV.showCW: Impossible happened, expected list, got: " ++ show kw -- | A version of show for kinds that says Bool instead of SBool showBaseKind :: Kind -> String @@ -284,14 +259,15 @@ -- | Create a constant word from an integral. mkConstCW :: Integral a => Kind -> a -> CW -mkConstCW KBool a = normCW $ CW KBool (CWInteger (toInteger a)) -mkConstCW k@KBounded{} a = normCW $ CW k (CWInteger (toInteger a)) -mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a)) -mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a))) -mkConstCW KFloat a = normCW $ CW KFloat (CWFloat (fromInteger (toInteger a))) -mkConstCW KDouble a = normCW $ CW KDouble (CWDouble (fromInteger (toInteger a))) -mkConstCW KChar a = error $ "Unexpected call to mkConstCW (Char) with value: " ++ show (toInteger a) -mkConstCW KString a = error $ "Unexpected call to mkConstCW (String) with value: " ++ show (toInteger a) +mkConstCW KBool a = normCW $ CW KBool (CWInteger (toInteger a)) +mkConstCW k@KBounded{} a = normCW $ CW k (CWInteger (toInteger a)) +mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a)) +mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a))) +mkConstCW KFloat a = normCW $ CW KFloat (CWFloat (fromInteger (toInteger a))) +mkConstCW KDouble a = normCW $ CW KDouble (CWDouble (fromInteger (toInteger a))) +mkConstCW KChar a = error $ "Unexpected call to mkConstCW (Char) with value: " ++ show (toInteger a) +mkConstCW KString a = error $ "Unexpected call to mkConstCW (String) with value: " ++ show (toInteger a) +mkConstCW k@KList{} a = error $ "Unexpected call to mkConstCW (" ++ show k ++ ") with value: " ++ show (toInteger a) mkConstCW (KUserSort s _) a = error $ "Unexpected call to mkConstCW with uninterpreted kind: " ++ s ++ " with value: " ++ show (toInteger a) -- | Generate a random constant value ('CWVal') of the correct kind. @@ -309,6 +285,8 @@ CWString <$> replicateM l (chr <$> randomRIO (0, 255)) KChar -> CWChar . chr <$> randomRIO (0, 255) KUserSort s _ -> error $ "Unexpected call to randomCWVal with uninterpreted kind: " ++ s + KList ek -> do l <- randomRIO (0, 100) + CWList <$> replicateM l (randomCWVal ek) where bounds :: Bool -> Int -> (Integer, Integer) bounds False w = (0, 2^w - 1) 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 @@ -11,9 +11,11 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PatternGuards #-} @@ -24,7 +26,7 @@ module Data.SBV.Core.Data ( SBool, SWord8, SWord16, SWord32, SWord64 - , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble, SChar, SString + , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble, SChar, SString, SList , nan, infinity, sNaN, sInfinity, RoundingMode(..), SRoundingMode , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero , sRNE, sRNA, sRTP, sRTN, sRTZ @@ -38,7 +40,7 @@ , sbvToSW, sbvToSymSW, forceSWArg , SBVExpr(..), newExpr , cache, Cached, uncache, uncacheAI, HasKind(..) - , Op(..), PBOp(..), FPOp(..), StrOp(..), RegExp(..), NamedSymVar, getTableIndex + , Op(..), PBOp(..), FPOp(..), StrOp(..), SeqOp(..), RegExp(..), NamedSymVar, getTableIndex , SBVPgm(..), Symbolic, runSymbolic, State, getPathCondition, extendPathCondition , inSMTMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) , SolverContext(..), internalVariable, internalConstraint, isCodeGenMode @@ -53,6 +55,7 @@ ) where import GHC.Generics (Generic) +import GHC.Exts (IsList(..)) import Control.DeepSeq (NFData(..)) import Control.Monad.Reader (ask) @@ -60,6 +63,8 @@ import Data.Int (Int8, Int16, Int32, Int64) import Data.Word (Word8, Word16, Word32, Word64) import Data.List (elemIndex) +import Data.Maybe (fromMaybe) +import Data.Typeable (Typeable) import qualified Data.Generics as G (Data(..)) @@ -142,10 +147,23 @@ -- | A symbolic string. Note that a symbolic string is /not/ a list of symbolic characters, -- that is, it is not the case that @SString = [SChar]@, unlike what one might expect following --- Haskell strings. An 'SString' is a symbolic value of its own, of possibly arbitrary length, +-- Haskell strings. An 'SString' is a symbolic value of its own, of possibly arbitrary but finite length, -- and internally processed as one unit as opposed to a fixed-length list of characters. type SString = SBV String +-- | A symbolic list of items. Note that a symbolic list is /not/ a list of symbolic items, +-- that is, it is not the case that @SList a = [a]@, unlike what one might expect following +-- haskell lists\/sequences. An 'SList' is a symbolic value of its own, of possibly arbitrary but finite +-- length, and internally processed as one unit as opposed to a fixed-length list of items. +-- Note that lists can be nested, i.e., we do allow lists of lists of ... items. +type SList a = SBV [a] + +-- | IsList instance allows list literals to be written compactly. +instance SymWord [a] => IsList (SList a) where + type Item (SList a) = a + fromList = literal + toList x = fromMaybe (error "IsList.toList used in a symbolic context!") (unliteral x) + -- | Not-A-Number for 'Double' and 'Float'. Surprisingly, Haskell -- Prelude doesn't have this value defined, so we provide it here. nan :: Floating a => a @@ -334,7 +352,7 @@ -- to be fed to a symbolic program. Note that these methods are typically not needed -- in casual uses with 'prove', 'sat', 'allSat' etc, as default instances automatically -- provide the necessary bits. -class (HasKind a, Ord a) => SymWord a where +class (HasKind a, Ord a, Typeable a) => SymWord a where -- | Create a user named input (universal) forall :: String -> Symbolic (SBV a) -- | Create an automatically named input diff --git a/Data/SBV/Core/Floating.hs b/Data/SBV/Core/Floating.hs --- a/Data/SBV/Core/Floating.hs +++ b/Data/SBV/Core/Floating.hs @@ -18,7 +18,7 @@ , blastSFloat, blastSDouble ) where -import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble, floatToWord, doubleToWord) +import qualified Data.ReinterpretCast as RC (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.Int (Int8, Int16, Int32, Int64) import Data.Word (Word8, Word16, Word32, Word64) @@ -379,7 +379,7 @@ sFloatAsSWord32 :: SFloat -> SWord32 sFloatAsSWord32 fVal | Just f <- unliteral fVal, not (isNaN f) - = literal (DB.floatToWord f) + = literal (RC.floatToWord f) | True = SBV (SVal w32 (Right (cache y))) where w32 = KBounded False 32 @@ -400,7 +400,7 @@ sDoubleAsSWord64 :: SDouble -> SWord64 sDoubleAsSWord64 fVal | Just f <- unliteral fVal, not (isNaN f) - = literal (DB.doubleToWord f) + = literal (RC.doubleToWord f) | True = SBV (SVal w64 (Right (cache y))) where w64 = KBounded False 64 @@ -428,7 +428,7 @@ -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number sWord32AsSFloat :: SWord32 -> SFloat sWord32AsSFloat fVal - | Just f <- unliteral fVal = literal $ DB.wordToFloat f + | Just f <- unliteral fVal = literal $ RC.wordToFloat f | True = SBV (SVal KFloat (Right (cache y))) where y st = do xsw <- sbvToSW st fVal newExpr st KFloat (SBVApp (IEEEFP (FP_Reinterpret (kindOf fVal) KFloat)) [xsw]) @@ -436,7 +436,7 @@ -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number sWord64AsSDouble :: SWord64 -> SDouble sWord64AsSDouble dVal - | Just d <- unliteral dVal = literal $ DB.wordToDouble d + | Just d <- unliteral dVal = literal $ RC.wordToDouble d | True = SBV (SVal KDouble (Right (cache y))) where y st = do xsw <- sbvToSW st dVal newExpr st KDouble (SBVApp (IEEEFP (FP_Reinterpret (kindOf dVal) KDouble)) [xsw]) 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 @@ -9,13 +9,14 @@ -- Internal data-structures for the sbv library ----------------------------------------------------------------------------- -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeSynonymInstances #-} + {-# OPTIONS_GHC -fno-warn-orphans #-} -module Data.SBV.Core.Kind (Kind(..), HasKind(..), constructUKind) where +module Data.SBV.Core.Kind (Kind(..), HasKind(..), constructUKind, smtType) where import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields) @@ -23,6 +24,12 @@ import Data.Word import Data.SBV.Core.AlgReals +import Data.List (isPrefixOf, intercalate) + +import Data.Typeable (Typeable) + +import Data.SBV.Utils.Lib (isKString) + -- | Kind of symbolic value data Kind = KBool | KBounded !Bool !Int @@ -33,28 +40,12 @@ | KDouble | KChar | KString - --- | Helper for Eq/Ord instances below -kindRank :: Kind -> Either Int (Either (Bool, Int) String) -kindRank KBool = Left 0 -kindRank (KBounded b i) = Right (Left (b, i)) -kindRank KUnbounded = Left 1 -kindRank KReal = Left 2 -kindRank (KUserSort s _) = Right (Right s) -kindRank KFloat = Left 3 -kindRank KDouble = Left 4 -kindRank KChar = Left 5 -kindRank KString = Left 6 -{-# INLINE kindRank #-} - --- | We want to equate user-sorts only by name -instance Eq Kind where - k1 == k2 = kindRank k1 == kindRank k2 - --- | We want to order user-sorts only by name -instance Ord Kind where - k1 `compare` k2 = kindRank k1 `compare` kindRank k2 + | KList Kind + deriving (Eq, Ord) +-- | The interesting about the show instance is that it can tell apart two kinds nicely; since it conveniently +-- ignores the enumeration constructors. Also, when we construct a 'KUserSort', we make sure we don't use any of +-- the reserved names; see 'constructUIKind' for details. instance Show Kind where show KBool = "SBool" show (KBounded False n) = "SWord" ++ show n @@ -66,7 +57,21 @@ show KDouble = "SDouble" show KString = "SString" show KChar = "SChar" + show (KList e) = "[" ++ show e ++ "]" +-- | How the type maps to SMT land +smtType :: Kind -> String +smtType KBool = "Bool" +smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" +smtType KUnbounded = "Int" +smtType KReal = "Real" +smtType KFloat = "(_ FloatingPoint 8 24)" +smtType KDouble = "(_ FloatingPoint 11 53)" +smtType KString = "String" +smtType KChar = "(_ BitVec 8)" +smtType (KList k) = "(Seq " ++ smtType k ++ ")" +smtType (KUserSort s _) = s + instance Eq G.DataType where a == b = G.tyconUQname (G.dataTypeName a) == G.tyconUQname (G.dataTypeName b) @@ -83,15 +88,23 @@ KReal -> True KFloat -> True KDouble -> True + KUserSort{} -> False KString -> False KChar -> False - KUserSort{} -> False + KList{} -> False -- | Construct an uninterpreted/enumerated kind from a piece of data; we distinguish simple enumerations as those -- are mapped to proper SMT-Lib2 data-types; while others go completely uninterpreted constructUKind :: forall a. (Read a, G.Data a) => a -> Kind -constructUKind a = KUserSort sortName mbEnumFields - where dataType = G.dataTypeOf a +constructUKind a + | any (`isPrefixOf` sortName) badPrefixes + = error $ "Data.SBV: Cannot construct user-sort with name: " ++ show sortName ++ ": Must not start with any of " ++ intercalate ", " badPrefixes + | True + = KUserSort sortName mbEnumFields + where -- make sure we don't step on ourselves: + badPrefixes = ["SBool", "SWord", "SInt", "SInteger", "SReal", "SFloat", "SDouble", "SString", "SChar", "["] + + dataType = G.dataTypeOf a sortName = G.tyconUQname . G.dataTypeName $ dataType constrs = G.dataTypeConstrs dataType isEnumeration = not (null constrs) && all (null . G.constrFields) constrs @@ -124,9 +137,11 @@ isUninterpreted :: a -> Bool isChar :: a -> Bool isString :: a -> Bool + isList :: a -> Bool showType :: a -> String -- defaults hasSign x = kindHasSign (kindOf x) + intSizeOf x = case kindOf x of KBool -> error "SBV.HasKind.intSizeOf((S)Bool)" KBounded _ s -> s @@ -134,27 +149,41 @@ KReal -> error "SBV.HasKind.intSizeOf((S)Real)" KFloat -> error "SBV.HasKind.intSizeOf((S)Float)" KDouble -> error "SBV.HasKind.intSizeOf((S)Double)" + KUserSort s _ -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s KString -> error "SBV.HasKind.intSizeOf((S)Double)" KChar -> error "SBV.HasKind.intSizeOf((S)Char)" - KUserSort s _ -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s + KList ek -> error $ "SBV.HasKind.intSizeOf((S)List)" ++ show ek + isBoolean x | KBool{} <- kindOf x = True | True = False + isBounded x | KBounded{} <- kindOf x = True | True = False + isReal x | KReal{} <- kindOf x = True | True = False + isFloat x | KFloat{} <- kindOf x = True | True = False + isDouble x | KDouble{} <- kindOf x = True | True = False + isInteger x | KUnbounded{} <- kindOf x = True | True = False + isUninterpreted x | KUserSort{} <- kindOf x = True | True = False + isString x | KString{} <- kindOf x = True | True = False + isChar x | KChar{} <- kindOf x = True | True = False + + isList x | KList{} <- kindOf x = True + | True = False + showType = show . kindOf -- default signature for uninterpreted/enumerated kinds @@ -175,7 +204,10 @@ instance HasKind Float where kindOf _ = KFloat instance HasKind Double where kindOf _ = KDouble instance HasKind Char where kindOf _ = KChar -instance HasKind String where kindOf _ = KString + +instance (Typeable a, HasKind a) => HasKind [a] where + kindOf _ | isKString (undefined :: [a]) = KString + | True = KList (kindOf (undefined :: a)) instance HasKind Kind where kindOf = id 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 @@ -9,18 +9,18 @@ -- Instance declarations for our symbolic world ----------------------------------------------------------------------------- -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} module Data.SBV.Core.Model ( Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), Metric(..), assertWithPenalty, SIntegral, SFiniteBits(..) @@ -29,7 +29,8 @@ , pbAtMost, pbAtLeast, pbExactly, pbLe, pbGe, pbEq, pbMutexed, pbStronglyMutexed , sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32 , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64 - , sInt64s, sInteger, sIntegers, sReal, sReals, sFloat, sFloats, sDouble, sDoubles, sChar, sChars, sString, sStrings, slet + , sInt64s, sInteger, sIntegers, sReal, sReals, sFloat, sFloats, sDouble, sDoubles, sChar, sChars, sString, sStrings, sList, sLists + , slet , sRealToSInteger, label, observe , sAssert , liftQRem, liftDMod, symbolicMergeWithKind @@ -57,6 +58,8 @@ import Data.String (IsString(..)) import Data.Word (Word8, Word16, Word32, Word64) +import Data.Dynamic (fromDynamic, toDyn) + import Test.QuickCheck (Testable(..), Arbitrary(..)) import qualified Test.QuickCheck.Test as QC (isSuccess) import qualified Test.QuickCheck as QC (quickCheckResult, counterexample) @@ -71,6 +74,7 @@ import Data.SBV.SMT.SMT (showModel) import Data.SBV.Utils.Boolean +import Data.SBV.Utils.Lib (isKString) -- Symbolic-Word class instances @@ -181,18 +185,32 @@ -- and in the presence of NaN's it would be incorrect to do any optimization isConcretely _ _ = False -instance SymWord String where - mkSymWord = genMkSymVar KString - literal = SBV . SVal KString . Left . CW KString . CWString - fromCW (CW _ (CWString a)) = a - fromCW c = error $ "SymWord.String: Unexpected non-string value: " ++ show c - instance SymWord Char where mkSymWord = genMkSymVar KChar literal c = SBV . SVal KChar . Left . CW KChar $ CWChar c fromCW (CW _ (CWChar a)) = a fromCW c = error $ "SymWord.String: Unexpected non-char value: " ++ show c +instance SymWord a => SymWord [a] where + mkSymWord + | isKString (undefined :: [a]) = genMkSymVar KString + | True = genMkSymVar (KList (kindOf (undefined :: a))) + + literal as + | isKString (undefined :: [a]) = case fromDynamic (toDyn as) of + Just s -> SBV . SVal KString . Left . CW KString . CWString $ s + Nothing -> error "SString: Cannot construct literal string!" + | True = let k = KList (kindOf (undefined :: a)) + toCWVal a = case literal a of + SBV (SVal _ (Left (CW _ cwval))) -> cwval + _ -> error "SymWord.Sequence: could not produce a concrete word for value" + in SBV $ SVal k $ Left $ CW k $ CWList $ map toCWVal as + + fromCW (CW _ (CWString a)) = fromMaybe (error "SString: Cannot extract a literal string!") + (fromDynamic (toDyn a)) + fromCW (CW _ (CWList a)) = fromCW . CW (kindOf (undefined :: a)) <$> a + fromCW c = error $ "SymWord.fromCW: Unexpected non-list value: " ++ show c + instance IsString SString where fromString = literal @@ -321,6 +339,14 @@ sStrings :: [String] -> Symbolic [SString] sStrings = symbolics +-- | Declare an 'SList' +sList :: forall a. SymWord a => String -> Symbolic (SList a) +sList = symbolic + +-- | Declare a list of 'SList's +sLists :: forall a. SymWord a => [String] -> Symbolic [SList a] +sLists = symbolics + -- | Convert an SReal to an SInteger. That is, it computes the -- largest integer @n@ that satisfies @sIntegerToSReal n <= r@ -- essentially giving us the @floor@. @@ -865,6 +891,7 @@ k@KBool -> error $ "Unexpected Fractional case for: " ++ show k k@KString -> error $ "Unexpected Fractional case for: " ++ show k k@KChar -> error $ "Unexpected Fractional case for: " ++ show k + k@KList{} -> error $ "Unexpected Fractional case for: " ++ show k k@KUserSort{} -> error $ "Unexpected Fractional case for: " ++ show k -- | Define Floating instance on SBV's; only for base types that are already floating; i.e., SFloat and SDouble 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 @@ -280,39 +280,39 @@ -- | Equality. svEqual :: SVal -> SVal -> SVal -svEqual = liftSym2B (mkSymOpSC (eqOptBool Equal trueSW) Equal) rationalCheck (==) (==) (==) (==) (==) (==) (==) +svEqual = liftSym2B (mkSymOpSC (eqOptBool Equal trueSW) Equal) rationalCheck (==) (==) (==) (==) (==) (==) (==) (==) -- | Inequality. svNotEqual :: SVal -> SVal -> SVal -svNotEqual = liftSym2B (mkSymOpSC (eqOptBool NotEqual falseSW) NotEqual) rationalCheck (/=) (/=) (/=) (/=) (/=) (/=) (/=) +svNotEqual = liftSym2B (mkSymOpSC (eqOptBool NotEqual falseSW) NotEqual) rationalCheck (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) -- | Less than. svLessThan :: SVal -> SVal -> SVal svLessThan x y | isConcreteMax x = svFalse | isConcreteMin y = svFalse - | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) rationalCheck (<) (<) (<) (<) (<) (<) (uiLift "<" (<)) x y + | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) rationalCheck (<) (<) (<) (<) (<) (<) (<) (uiLift "<" (<)) x y -- | Greater than. svGreaterThan :: SVal -> SVal -> SVal svGreaterThan x y | isConcreteMin x = svFalse | isConcreteMax y = svFalse - | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>) (>) (>) (>) (>) (>) (uiLift ">" (>)) x y + | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>) (>) (>) (>) (>) (>) (>) (uiLift ">" (>)) x y -- | Less than or equal to. svLessEq :: SVal -> SVal -> SVal svLessEq x y | isConcreteMin x = svTrue | isConcreteMax y = svTrue - | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) rationalCheck (<=) (<=) (<=) (<=) (<=) (<=) (uiLift "<=" (<=)) x y + | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) rationalCheck (<=) (<=) (<=) (<=) (<=) (<=) (<=) (uiLift "<=" (<=)) x y -- | Greater than or equal to. svGreaterEq :: SVal -> SVal -> SVal svGreaterEq x y | isConcreteMax x = svTrue | isConcreteMin y = svTrue - | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) (>=) (>=) (uiLift ">=" (>=)) x y + | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) (>=) (>=) (>=) (uiLift ">=" (>=)) x y -- | Bitwise and. svAnd :: SVal -> SVal -> SVal @@ -1198,9 +1198,9 @@ liftSym2 _ okCW opCR opCI opCF opCD (SVal k (Left a)) (SVal _ (Left b)) | okCW a b = SVal k . Left $! mapCW2 opCR opCI opCF opCD noCharLift2 noStringLift2 noUnint2 a b liftSym2 opS _ _ _ _ _ a@(SVal k _) b = SVal k $ Right $ liftSW2 opS k a b -liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> (Char -> Char -> Bool) -> (String -> String -> Bool) -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool) -> SVal -> SVal -> SVal -liftSym2B _ okCW opCR opCI opCF opCD opCC opCS opUI (SVal _ (Left a)) (SVal _ (Left b)) | okCW a b = svBool (liftCW2 opCR opCI opCF opCD opCC opCS opUI a b) -liftSym2B opS _ _ _ _ _ _ _ _ a b = SVal KBool $ Right $ liftSW2 opS KBool a b +liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> (Char -> Char -> Bool) -> (String -> String -> Bool) -> ([CWVal] -> [CWVal] -> Bool) -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool) -> SVal -> SVal -> SVal +liftSym2B _ okCW opCR opCI opCF opCD opCC opCS opCSeq opUI (SVal _ (Left a)) (SVal _ (Left b)) | okCW a b = svBool (liftCW2 opCR opCI opCF opCD opCC opCS opCSeq opUI a b) +liftSym2B opS _ _ _ _ _ _ _ _ _ a b = SVal KBool $ Right $ liftSW2 opS KBool a b -- | Create a symbolic two argument operation; with shortcut optimizations mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW @@ -1232,21 +1232,29 @@ uiLift w _ a b = error $ "Data.SBV.Core.Operations: Impossible happened while trying to lift " ++ w ++ " over " ++ show (a, b) -- | Predicate for optimizing word operations like (+) and (*). +-- NB. We specifically do *not* match for Double/Float; because +-- FP-arithmetic doesn't obey traditional rules. For instance, +-- 0 * x = 0 fails if x happens to be NaN or +/- Infinity. So, +-- we merely return False when given a floating-point value here. isConcreteZero :: SVal -> Bool isConcreteZero (SVal _ (Left (CW _ (CWInteger n)))) = n == 0 isConcreteZero (SVal KReal (Left (CW KReal (CWAlgReal v)))) = isExactRational v && v == 0 isConcreteZero _ = False -- | Predicate for optimizing word operations like (+) and (*). +-- NB. See comment on 'isConcreteZero' for why we don't match +-- for Float/Double values here. isConcreteOne :: SVal -> Bool isConcreteOne (SVal _ (Left (CW _ (CWInteger 1)))) = True isConcreteOne (SVal KReal (Left (CW KReal (CWAlgReal v)))) = isExactRational v && v == 1 isConcreteOne _ = False --- | Predicate for optimizing bitwise operations. +-- | Predicate for optimizing bitwise operations. The unbounded integer case of checking +-- against -1 might look dubious, but that's how Haskell treats 'Integer' as a member +-- of the Bits class, try @(-1 :: Integer) `testBit` i@ for any @i@ and you'll get 'True'. isConcreteOnes :: SVal -> Bool isConcreteOnes (SVal _ (Left (CW (KBounded b w) (CWInteger n)))) = n == if b then -1 else bit w - 1 -isConcreteOnes (SVal _ (Left (CW KUnbounded (CWInteger n)))) = n == -1 +isConcreteOnes (SVal _ (Left (CW KUnbounded (CWInteger n)))) = n == -1 -- see comment above isConcreteOnes (SVal _ (Left (CW KBool (CWInteger n)))) = n == 1 isConcreteOnes _ = False 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 @@ -27,7 +27,7 @@ module Data.SBV.Core.Symbolic ( NodeId(..) , SW(..), swKind, trueSW, falseSW - , Op(..), PBOp(..), OvOp(..), FPOp(..), StrOp(..), RegExp(..) + , Op(..), PBOp(..), OvOp(..), FPOp(..), StrOp(..), SeqOp(..), RegExp(..) , Quantifier(..), needsExistentials , RoundingMode(..) , SBVType(..), svUninterpreted, newUninterpreted, addAxiom @@ -155,6 +155,7 @@ | PseudoBoolean PBOp -- Pseudo-boolean ops, categorized separately | OverflowOp OvOp -- Overflow-ops, categorized separately | StrOp StrOp -- String ops, categorized separately + | SeqOp SeqOp -- Sequence ops, categorized separately deriving (Eq, Ord) -- | Floating point operations @@ -333,6 +334,30 @@ -- Note the breakage here with respect to argument order. We fix this explicitly later. show (StrInRe s) = "str.in.re " ++ show s +-- | Sequence operations. +data SeqOp = SeqConcat -- ^ See StrConcat + | SeqLen -- ^ See StrLen + | SeqUnit -- ^ See StrUnit + | SeqSubseq -- ^ See StrSubseq + | SeqIndexOf -- ^ See StrIndexOf + | SeqContains -- ^ See StrContains + | SeqPrefixOf -- ^ See StrPrefixOf + | SeqSuffixOf -- ^ See StrSuffixOf + | SeqReplace -- ^ See StrReplace + deriving (Eq, Ord) + +-- | Show instance for `SeqOp`. Again, mapping is important. +instance Show SeqOp where + show SeqConcat = "seq.++" + show SeqLen = "seq.len" + show SeqUnit = "seq.unit" + show SeqSubseq = "seq.extract" + show SeqIndexOf = "seq.indexof" + show SeqContains = "seq.contains" + show SeqPrefixOf = "seq.prefixof" + show SeqSuffixOf = "seq.suffixof" + show SeqReplace = "seq.replace" + -- Show instance for 'Op'. Note that this is largely for debugging purposes, not used -- for being read by any tool. instance Show Op where @@ -353,6 +378,7 @@ show (PseudoBoolean p) = show p show (OverflowOp o) = show o show (StrOp s) = show s + show (SeqOp s) = show s show op | Just s <- op `lookup` syms = s | True = error "impossible happened; can't find op!" @@ -1335,7 +1361,7 @@ rnf (Result kindInfo qcInfo obs cgs inps consts tbls arrs uis axs pgm cstr asserts outs) = rnf kindInfo `seq` rnf qcInfo `seq` rnf obs `seq` rnf cgs `seq` rnf inps `seq` rnf consts `seq` rnf tbls - `seq` rnf arrs `seq` rnf uis `seq` rnf axs + `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf cstr `seq` rnf asserts `seq` rnf outs instance NFData Kind where rnf a = seq a () @@ -1363,16 +1389,17 @@ -- | Translation tricks needed for specific capabilities afforded by each solver data SolverCapabilities = SolverCapabilities { - supportsQuantifiers :: Bool -- ^ Support for SMT-Lib2 style quantifiers? - , supportsUninterpretedSorts :: Bool -- ^ Support for SMT-Lib2 style uninterpreted-sorts - , supportsUnboundedInts :: Bool -- ^ Support for unbounded integers? - , supportsReals :: Bool -- ^ Support for reals? - , supportsApproxReals :: Bool -- ^ Supports printing of approximations of reals? - , supportsIEEE754 :: Bool -- ^ Support for floating point numbers? - , supportsOptimization :: Bool -- ^ Support for optimization routines? - , supportsPseudoBooleans :: Bool -- ^ Support for pseudo-boolean operations? - , supportsCustomQueries :: Bool -- ^ Support for interactive queries per SMT-Lib? - , supportsGlobalDecls :: Bool -- ^ Support for global decls, needed for push-pop. + supportsQuantifiers :: Bool -- ^ Support for SMT-Lib2 style quantifiers? + , supportsUninterpretedSorts :: Bool -- ^ Support for SMT-Lib2 style uninterpreted-sorts + , supportsUnboundedInts :: Bool -- ^ Support for unbounded integers? + , supportsReals :: Bool -- ^ Support for reals? + , supportsApproxReals :: Bool -- ^ Supports printing of approximations of reals? + , supportsIEEE754 :: Bool -- ^ Support for floating point numbers? + , supportsOptimization :: Bool -- ^ Support for optimization routines? + , supportsPseudoBooleans :: Bool -- ^ Support for pseudo-boolean operations? + , supportsCustomQueries :: Bool -- ^ Support for interactive queries per SMT-Lib? + , supportsGlobalDecls :: Bool -- ^ Support for global decls, needed for push-pop. + , supportsFlattenedSequences :: Maybe [String] -- ^ Supports flattened sequence output, with given config lines } -- | Rounding mode to be used for the IEEE floating-point operations. diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/List.hs @@ -0,0 +1,389 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.List +-- Copyright : (c) Joel Burget, Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- A collection of list utilities, useful when working with symbolic lists. +-- To the extent possible, the functions in this module follow those of "Data.List" +-- so importing qualified is the recommended workflow. Also, it is recommended +-- you use the @OverloadedLists@ extension to allow literal lists to +-- be used as symbolic-lists. +----------------------------------------------------------------------------- + +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.SBV.List ( + -- * Length, emptiness + length, null + -- * Deconstructing/Reconstructing + , head, tail, uncons, init, singleton, listToListAt, elemAt, (.!!), implode, concat, (.:), (.++) + -- * Containment + , isInfixOf, isSuffixOf, isPrefixOf + -- * Sublists + , take, drop, subList, replace, indexOf, offsetIndexOf + ) where + +import Prelude hiding (head, tail, init, length, take, drop, concat, null) +import qualified Prelude as P + +import Data.SBV.Core.Data hiding (StrOp(..)) +import Data.SBV.Core.Model + +import Data.List (genericLength, genericIndex, genericDrop, genericTake) +import qualified Data.List as L (tails, isSuffixOf, isPrefixOf, isInfixOf) + +-- For doctest use only +-- +-- $setup +-- >>> import Data.SBV.Provers.Prover (prove, sat) +-- >>> import Data.SBV.Utils.Boolean ((==>), (&&&), bnot, (<=>)) +-- >>> import Data.Int +-- >>> import Data.Word +-- >>> :set -XOverloadedLists +-- >>> :set -XScopedTypeVariables + +-- | Length of a list. +-- +-- >>> sat $ \(l :: SList Word16) -> length l .== 2 +-- Satisfiable. Model: +-- s0 = [0,0] :: [SWord16] +-- >>> sat $ \(l :: SList Word16) -> length l .< 0 +-- Unsatisfiable +-- >>> prove $ \(l1 :: SList Word16) (l2 :: SList Word16) -> length l1 + length l2 .== length (l1 .++ l2) +-- Q.E.D. +length :: SymWord a => SList a -> SInteger +length = lift1 SeqLen (Just (fromIntegral . P.length)) + +-- | @`null` s@ is True iff the list is empty +-- +-- >>> prove $ \(l :: SList Word16) -> null l <=> length l .== 0 +-- Q.E.D. +-- >>> prove $ \(l :: SList Word16) -> null l <=> l .== [] +-- Q.E.D. +null :: SymWord a => SList a -> SBool +null l + | Just cs <- unliteral l + = literal (P.null cs) + | True + = l .== literal [] + +-- | @`head`@ returns the first element of a list. Unspecified if the list is empty. +-- +-- >>> prove $ \c -> head (singleton c) .== (c :: SInteger) +-- Q.E.D. +head :: SymWord a => SList a -> SBV a +head = (`elemAt` 0) + +-- | @`tail`@ returns the tail of a list. Unspecified if the list is empty. +-- +-- >>> prove $ \(h :: SInteger) t -> tail (singleton h .++ t) .== t +-- Q.E.D. +-- >>> prove $ \(l :: SList Integer) -> length l .> 0 ==> length (tail l) .== length l - 1 +-- Q.E.D. +-- >>> prove $ \(l :: SList Integer) -> bnot (null l) ==> singleton (head l) .++ tail l .== l +-- Q.E.D. +tail :: SymWord a => SList a -> SList a +tail l + | Just (_:cs) <- unliteral l + = literal cs + | True + = subList l 1 (length l - 1) + +-- | @`uncons` returns the pair of the head and tail. Unspecified if the list is empty. +uncons :: SymWord a => SList a -> (SBV a, SList a) +uncons l = (head l, tail l) + +-- | @`init`@ returns all but the last element of the list. Unspecified if the list is empty. +-- +-- >>> prove $ \(h :: SInteger) t -> init (t .++ singleton h) .== t +-- Q.E.D. +init :: SymWord a => SList a -> SList a +init l + | Just cs@(_:_) <- unliteral l + = literal $ P.init cs + | True + = subList l 0 (length l - 1) + +-- | @`singleton` x@ is the list of length 1 that contains the only value `x`. +-- +-- >>> prove $ \(x :: SInteger) -> head (singleton x) .== x +-- Q.E.D. +-- >>> prove $ \(x :: SInteger) -> length (singleton x) .== 1 +-- Q.E.D. +singleton :: SymWord a => SBV a -> SList a +singleton = lift1 SeqUnit (Just (: [])) + +-- | @`listToListAt` l offset@. List of length 1 at @offset@ in @l@. Unspecified if +-- index is out of bounds. +-- +-- >>> prove $ \(l1 :: SList Integer) l2 -> listToListAt (l1 .++ l2) (length l1) .== listToListAt l2 0 +-- Q.E.D. +-- >>> sat $ \(l :: SList Word16) -> length l .>= 2 &&& listToListAt l 0 ./= listToListAt l (length l - 1) +-- Satisfiable. Model: +-- s0 = [0,0,4096] :: [SWord16] +listToListAt :: SymWord a => SList a -> SInteger -> SList a +listToListAt s offset = subList s offset 1 + +-- | @`elemAt` l i@ is the value stored at location @i@. Unspecified if +-- index is out of bounds. +-- +-- >>> prove $ \i -> i .>= 0 &&& i .<= 4 ==> [1,1,1,1,1] `elemAt` i .== (1::SInteger) +-- Q.E.D. +-- >>> prove $ \(l :: SList Integer) i e -> l `elemAt` i .== e ==> indexOf l (singleton e) .<= i +-- Q.E.D. +elemAt :: forall a. SymWord a => SList a -> SInteger -> SBV a +elemAt l i + | Just xs <- unliteral l, Just ci <- unliteral i, ci >= 0, ci < genericLength xs, let x = xs `genericIndex` ci + = literal x + | True + = SBV (SVal kElem (Right (cache (y (l `listToListAt` i))))) + where kElem = kindOf (undefined :: a) + kSeq = KList kElem + -- This is trickier than it needs to be, but necessary since there's + -- no SMTLib function to extract the element from a list. Instead, + -- we form a singleton list, and assert that it is equivalent to + -- the extracted value. See + y si st = do e <- internalVariable st kElem + es <- newExpr st kSeq (SBVApp (SeqOp SeqUnit) [e]) + let esSBV = SBV (SVal kSeq (Right (cache (\_ -> return es)))) + internalConstraint st False [] $ unSBV $ esSBV .== si + return e + +-- | Short cut for 'elemAt' +(.!!) :: SymWord a => SList a -> SInteger -> SBV a +(.!!) = elemAt + +-- | @`implode` es@ is the list of length @|es|@ containing precisely those +-- elements. Note that there is no corresponding function @explode@, since +-- we wouldn't know the length of a symbolic list. +-- +-- >>> prove $ \(e1 :: SInteger) e2 e3 -> length (implode [e1, e2, e3]) .== 3 +-- Q.E.D. +-- >>> prove $ \(e1 :: SInteger) e2 e3 -> map (elemAt (implode [e1, e2, e3])) (map literal [0 .. 2]) .== [e1, e2, e3] +-- Q.E.D. +implode :: SymWord a => [SBV a] -> SList a +implode = foldr ((.++) . singleton) (literal []) + +-- | Concatenate two lists. See also `.++`. +concat :: SymWord a => SList a -> SList a -> SList a +concat x y | isConcretelyEmpty x = y + | isConcretelyEmpty y = x + | True = lift2 SeqConcat (Just (++)) x y + +-- | Prepend an element, the traditional @cons@. +infixr 5 .: +(.:) :: SymWord a => SBV a -> SList a -> SList a +a .: as = singleton a .++ as + +-- | Short cut for `concat`. +-- +-- >>> sat $ \x y z -> length x .== 5 &&& length y .== 1 &&& x .++ y .++ z .== [1 .. 12] +-- Satisfiable. Model: +-- s0 = [1,2,3,4,5] :: [SInteger] +-- s1 = [6] :: [SInteger] +-- s2 = [7,8,9,10,11,12] :: [SInteger] +infixr 5 .++ +(.++) :: SymWord a => SList a -> SList a -> SList a +(.++) = concat + +-- | @`isInfixOf` sub l@. Does @l@ contain the subsequence @sub@? +-- +-- >>> prove $ \(l1 :: SList Integer) l2 l3 -> l2 `isInfixOf` (l1 .++ l2 .++ l3) +-- Q.E.D. +-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isInfixOf` l2 &&& l2 `isInfixOf` l1 <=> l1 .== l2 +-- Q.E.D. +isInfixOf :: SymWord a => SList a -> SList a -> SBool +sub `isInfixOf` l + | isConcretelyEmpty sub + = literal True + | True + = lift2 SeqContains (Just (flip L.isInfixOf)) l sub -- NB. flip, since `SeqContains` takes args in rev order! + +-- | @`isPrefixOf` pre l@. Is @pre@ a prefix of @l@? +-- +-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` (l1 .++ l2) +-- Q.E.D. +-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` l2 ==> subList l2 0 (length l1) .== l1 +-- Q.E.D. +isPrefixOf :: SymWord a => SList a -> SList a -> SBool +pre `isPrefixOf` l + | isConcretelyEmpty pre + = literal True + | True + = lift2 SeqPrefixOf (Just L.isPrefixOf) pre l + +-- | @`isSuffixOf` suf l@. Is @suf@ a suffix of @l@? +-- +-- >>> prove $ \(l1 :: SList Word16) l2 -> l2 `isSuffixOf` (l1 .++ l2) +-- Q.E.D. +-- >>> prove $ \(l1 :: SList Word16) l2 -> l1 `isSuffixOf` l2 ==> subList l2 (length l2 - length l1) (length l1) .== l1 +-- Q.E.D. +isSuffixOf :: SymWord a => SList a -> SList a -> SBool +suf `isSuffixOf` l + | isConcretelyEmpty suf + = literal True + | True + = lift2 SeqSuffixOf (Just L.isSuffixOf) suf l + +-- | @`take` len l@. Corresponds to Haskell's `take` on symbolic lists. +-- +-- >>> prove $ \(l :: SList Integer) i -> i .>= 0 ==> length (take i l) .<= i +-- Q.E.D. +take :: SymWord a => SInteger -> SList a -> SList a +take i l = ite (i .<= 0) (literal []) + $ ite (i .>= length l) l + $ subList l 0 i + +-- | @`drop` len s@. Corresponds to Haskell's `drop` on symbolic-lists. +-- +-- >>> prove $ \(l :: SList Word16) i -> length (drop i l) .<= length l +-- Q.E.D. +-- >>> prove $ \(l :: SList Word16) i -> take i l .++ drop i l .== l +-- Q.E.D. +drop :: SymWord a => SInteger -> SList a -> SList a +drop i s = ite (i .>= ls) (literal []) + $ ite (i .<= 0) s + $ subList s i (ls - i) + where ls = length s + +-- | @`subList` s offset len@ is the sublist of @s@ at offset `offset` with length `len`. +-- This function is under-specified when the offset is outside the range of positions in @s@ or @len@ +-- is negative or @offset+len@ exceeds the length of @s@. For a friendlier version of this function +-- that acts like Haskell's `take`\/`drop`, see `strTake`\/`strDrop`. +-- +-- >>> prove $ \(l :: SList Integer) i -> i .>= 0 &&& i .< length l ==> subList l 0 i .++ subList l i (length l - i) .== l +-- Q.E.D. +-- >>> sat $ \i j -> subList [1..5] i j .== ([2..4] :: SList Integer) +-- Satisfiable. Model: +-- s0 = 1 :: Integer +-- s1 = 3 :: Integer +-- >>> sat $ \i j -> subList [1..5] i j .== ([6..7] :: SList Integer) +-- Unsatisfiable +subList :: SymWord a => SList a -> SInteger -> SInteger -> SList a +subList l offset len + | Just c <- unliteral l -- a constant list + , Just o <- unliteral offset -- a constant offset + , Just sz <- unliteral len -- a constant length + , let lc = genericLength c -- length of the list + , let valid x = x >= 0 && x <= lc -- predicate that checks valid point + , valid o -- offset is valid + , sz >= 0 -- length is not-negative + , valid $ o + sz -- we don't overrun + = literal $ genericTake sz $ genericDrop o c + | True -- either symbolic, or something is out-of-bounds + = lift3 SeqSubseq Nothing l offset len + +-- | @`replace` l src dst@. Replace the first occurrence of @src@ by @dst@ in @s@ +-- +-- >>> prove $ \l -> replace [1..5] l [6..10] .== [6..10] ==> l .== ([1..5] :: SList Word8) +-- Q.E.D. +-- >>> prove $ \(l1 :: SList Integer) l2 l3 -> length l2 .> length l1 ==> replace l1 l2 l3 .== l1 +-- Q.E.D. +replace :: SymWord a => SList a -> SList a -> SList a -> SList a +replace l src dst + | Just b <- unliteral src, P.null b -- If src is null, simply prepend + = dst .++ l + | Just a <- unliteral l + , Just b <- unliteral src + , Just c <- unliteral dst + = literal $ walk a b c + | True + = lift3 SeqReplace Nothing l src dst + where walk haystack needle newNeedle = go haystack -- note that needle is guaranteed non-empty here. + where go [] = [] + go i@(c:cs) + | needle `L.isPrefixOf` i = newNeedle ++ genericDrop (genericLength needle :: Integer) i + | True = c : go cs + +-- | @`indexOf` l sub@. Retrieves first position of @sub@ in @l@, @-1@ if there are no occurrences. +-- Equivalent to @`offsetIndexOf` l sub 0@. +-- +-- >>> prove $ \(l :: SList Int8) i -> i .> 0 &&& i .< length l ==> indexOf l (subList l i 1) .<= i +-- Q.E.D. +-- >>> prove $ \(l :: SList Word16) i -> i .> 0 &&& i .< length l ==> indexOf l (subList l i 1) .== i +-- Falsifiable. Counter-example: +-- s0 = [0,0,0,0,0] :: [SWord16] +-- s1 = 4 :: Integer +-- >>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 ==> indexOf l1 l2 .== -1 +-- Q.E.D. +indexOf :: SymWord a => SList a -> SList a -> SInteger +indexOf s sub = offsetIndexOf s sub 0 + +-- | @`offsetIndexOf` l sub offset@. Retrieves first position of @sub@ at or +-- after @offset@ in @l@, @-1@ if there are no occurrences. +-- +-- >>> prove $ \(l :: SList Int8) sub -> offsetIndexOf l sub 0 .== indexOf l sub +-- Q.E.D. +-- >>> prove $ \(l :: SList Int8) sub i -> i .>= length l &&& length sub .> 0 ==> offsetIndexOf l sub i .== -1 +-- Q.E.D. +-- >>> prove $ \(l :: SList Int8) sub i -> i .> length l ==> offsetIndexOf l sub i .== -1 +-- Q.E.D. +offsetIndexOf :: SymWord a => SList a -> SList a -> SInteger -> SInteger +offsetIndexOf s sub offset + | Just c <- unliteral s -- a constant list + , Just n <- unliteral sub -- a constant search pattern + , Just o <- unliteral offset -- at a constant offset + , o >= 0, o <= genericLength c -- offset is good + = case [i | (i, t) <- zip [o ..] (L.tails (genericDrop o c)), n `L.isPrefixOf` t] of + (i:_) -> literal i + _ -> -1 + | True + = lift3 SeqIndexOf Nothing s sub offset + +-- | Lift a unary operator over lists. +lift1 :: forall a b. (SymWord a, SymWord b) => SeqOp -> Maybe (a -> b) -> SBV a -> SBV b +lift1 w mbOp a + | Just cv <- concEval1 mbOp a + = cv + | True + = SBV $ SVal k $ Right $ cache r + where k = kindOf (undefined :: b) + r st = do swa <- sbvToSW st a + newExpr st k (SBVApp (SeqOp w) [swa]) + +-- | Lift a binary operator over lists. +lift2 :: forall a b c. (SymWord a, SymWord b, SymWord c) => SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c +lift2 w mbOp a b + | Just cv <- concEval2 mbOp a b + = cv + | True + = SBV $ SVal k $ Right $ cache r + where k = kindOf (undefined :: c) + r st = do swa <- sbvToSW st a + swb <- sbvToSW st b + newExpr st k (SBVApp (SeqOp w) [swa, swb]) + +-- | Lift a ternary operator over lists. +lift3 :: forall a b c d. (SymWord a, SymWord b, SymWord c, SymWord d) => SeqOp -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d +lift3 w mbOp a b c + | Just cv <- concEval3 mbOp a b c + = cv + | True + = SBV $ SVal k $ Right $ cache r + where k = kindOf (undefined :: d) + r st = do swa <- sbvToSW st a + swb <- sbvToSW st b + swc <- sbvToSW st c + newExpr st k (SBVApp (SeqOp w) [swa, swb, swc]) + +-- | Concrete evaluation for unary ops +concEval1 :: (SymWord a, SymWord b) => Maybe (a -> b) -> SBV a -> Maybe (SBV b) +concEval1 mbOp a = literal <$> (mbOp <*> unliteral a) + +-- | Concrete evaluation for binary ops +concEval2 :: (SymWord a, SymWord b, SymWord c) => Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c) +concEval2 mbOp a b = literal <$> (mbOp <*> unliteral a <*> unliteral b) + +-- | Concrete evaluation for ternary ops +concEval3 :: (SymWord a, SymWord b, SymWord c, SymWord d) => Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> Maybe (SBV d) +concEval3 mbOp a b c = literal <$> (mbOp <*> unliteral a <*> unliteral b <*> unliteral c) + +-- | Is the list concretely known empty? +isConcretelyEmpty :: SymWord a => SList a -> Bool +isConcretelyEmpty sl | Just l <- unliteral sl = P.null l + | True = False diff --git a/Data/SBV/List/Bounded.hs b/Data/SBV/List/Bounded.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/List/Bounded.hs @@ -0,0 +1,95 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.List.Bounded +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- A collection of bounded list utilities, useful when working with symbolic lists. +-- These functions all take a concrete bound, and operate on the prefix of a symbolic +-- list that is at most that long. Due to limitations on writing recursive functions +-- over lists (the classic symbolic termination problem), we cannot write arbitrary +-- recursive programs on symbolic lists. But most of the time all we need is a +-- bounded prefix of this list, at which point these functions come in handy. +----------------------------------------------------------------------------- +-- +{-# LANGUAGE OverloadedLists #-} + +module Data.SBV.List.Bounded ( + -- * General folds + bfoldr, bfoldl + -- * Map, filter, zipWith + , bmap, bfilter, bzipWith + -- * Aggregates + , bsum, bprod, band, bor, bany, ball, bmaximum, bminimum + ) + where + +import Data.SBV +import Data.SBV.List ((.:)) +import qualified Data.SBV.List as L + +-- | Case analysis on a symbolic list. (Not exported.) +lcase :: (SymWord a, Mergeable b) => SList a -> b -> (SBV a -> SList a -> b) -> b +lcase s e c = ite (L.null s) e (c (L.head s) (L.tail s)) + +-- | Bounded fold from the right. +bfoldr :: (SymWord a, SymWord b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b +bfoldr cnt f b = go cnt + where go 0 _ = b + go i s = lcase s b (\h t -> h `f` go (i-1) t) + +-- | Bounded fold from the left. +bfoldl :: (SymWord a, SymWord b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b +bfoldl cnt f = go cnt + where go 0 b _ = b + go i b s = lcase s b (\h t -> go (i-1) (b `f` h) t) + +-- | Bounded sum. +bsum :: (SymWord a, Num a) => Int -> SList a -> SBV a +bsum i = bfoldl i (+) 0 + +-- | Bounded product. +bprod :: (SymWord a, Num a) => Int -> SList a -> SBV a +bprod i = bfoldl i (*) 1 + +-- | Bounded map. +bmap :: (SymWord a, SymWord b) => Int -> (SBV a -> SBV b) -> SList a -> SList b +bmap i f = bfoldr i (\x -> (f x .:)) [] + +-- | Bounded filter. +bfilter :: SymWord a => Int -> (SBV a -> SBool) -> SList a -> SList a +bfilter i f = bfoldr i (\x y -> ite (f x) (x .: y) y) [] + +-- | Bounded logical and +band :: Int -> SList Bool -> SBool +band i = bfoldr i (&&&) (true :: SBool) + +-- | Bounded logical and +bor :: Int -> SList Bool -> SBool +bor i = bfoldr i (|||) (false :: SBool) + +-- | Bounded any +bany :: SymWord a => Int -> (SBV a -> SBool) -> SList a -> SBool +bany i f = bor i . bmap i f + +-- | Bounded all +ball :: SymWord a => Int -> (SBV a -> SBool) -> SList a -> SBool +ball i f = band i . bmap i f + +-- | Bounded maximum. Undefined if list is empty. +bmaximum :: (SymWord a, Num a) => Int -> SList a -> SBV a +bmaximum i l = bfoldl (i-1) smax (L.head l) (L.tail l) + +-- | Bounded minimum. Undefined if list is empty. +bminimum :: (SymWord a, Num a) => Int -> SList a -> SBV a +bminimum i l = bfoldl (i-1) smin (L.head l) (L.tail l) + +-- | Bounded zipWith +bzipWith :: (SymWord a, SymWord b, SymWord c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c +bzipWith cnt f = go cnt + where go 0 _ _ = [] + go i xs ys = ite (L.null xs ||| L.null ys) + [] + (f (L.head xs) (L.head ys) .: go (i-1) (L.tail xs) (L.tail ys)) diff --git a/Data/SBV/Provers/ABC.hs b/Data/SBV/Provers/ABC.hs --- a/Data/SBV/Provers/ABC.hs +++ b/Data/SBV/Provers/ABC.hs @@ -36,5 +36,6 @@ , supportsPseudoBooleans = False , supportsCustomQueries = False , supportsGlobalDecls = False + , supportsFlattenedSequences = Nothing } } diff --git a/Data/SBV/Provers/Boolector.hs b/Data/SBV/Provers/Boolector.hs --- a/Data/SBV/Provers/Boolector.hs +++ b/Data/SBV/Provers/Boolector.hs @@ -34,5 +34,6 @@ , supportsPseudoBooleans = False , supportsCustomQueries = True , supportsGlobalDecls = False + , supportsFlattenedSequences = Nothing } } diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs --- a/Data/SBV/Provers/CVC4.hs +++ b/Data/SBV/Provers/CVC4.hs @@ -36,5 +36,6 @@ , supportsPseudoBooleans = False , supportsCustomQueries = True , supportsGlobalDecls = True + , supportsFlattenedSequences = Nothing } } diff --git a/Data/SBV/Provers/MathSAT.hs b/Data/SBV/Provers/MathSAT.hs --- a/Data/SBV/Provers/MathSAT.hs +++ b/Data/SBV/Provers/MathSAT.hs @@ -38,6 +38,7 @@ , supportsPseudoBooleans = False , supportsCustomQueries = True , supportsGlobalDecls = False + , supportsFlattenedSequences = Nothing } } diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -36,5 +36,6 @@ , supportsPseudoBooleans = False , supportsCustomQueries = True , supportsGlobalDecls = False + , supportsFlattenedSequences = Nothing } } diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -36,6 +36,9 @@ , supportsPseudoBooleans = True , supportsCustomQueries = True , supportsGlobalDecls = True + , supportsFlattenedSequences = Just [ "(set-option :pp.max_depth 4294967295)" + , "(set-option :pp.min_alias_size 4294967295)" + ] } } diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -1,9 +1,3 @@ -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE OverloadedStrings #-} - ----------------------------------------------------------------------------- -- | -- Module : Data.SBV.RegExp @@ -20,6 +14,12 @@ -- this module. ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings #-} + module Data.SBV.RegExp ( -- * Regular expressions RegExp(..) @@ -88,7 +88,7 @@ -- | Matching a character simply means the singleton string matches the regex. instance RegExpMatchable SChar where - match = match . charToStr + match = match . singleton -- | Matching symbolic strings. instance RegExpMatchable SString where diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -627,20 +627,7 @@ (False, True) -> return (ln:sofar) SolverException e -> do terminateProcess pid - C.throwIO $ SBVException { sbvExceptionDescription = e - , sbvExceptionSent = mbCommand - , sbvExceptionExpected = Nothing - , sbvExceptionReceived = Just $ unlines (reverse sofar) - , sbvExceptionStdOut = Nothing - , sbvExceptionStdErr = Nothing - , sbvExceptionExitCode = Nothing - , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } } - , sbvExceptionReason = Nothing - , sbvExceptionHint = Nothing - } - - SolverTimeout e -> do terminateProcess pid -- NB. Do not *wait* for the process, just quit. - C.throwIO $ SBVException { sbvExceptionDescription = "Timeout! " ++ e + C.throwIO SBVException { sbvExceptionDescription = e , sbvExceptionSent = mbCommand , sbvExceptionExpected = Nothing , sbvExceptionReceived = Just $ unlines (reverse sofar) @@ -649,11 +636,24 @@ , sbvExceptionExitCode = Nothing , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } } , sbvExceptionReason = Nothing - , sbvExceptionHint = if not (verbose cfg) - then Just ["Run with 'verbose=True' for further information"] - else Nothing + , sbvExceptionHint = Nothing } + SolverTimeout e -> do terminateProcess pid -- NB. Do not *wait* for the process, just quit. + C.throwIO SBVException { sbvExceptionDescription = "Timeout! " ++ e + , sbvExceptionSent = mbCommand + , sbvExceptionExpected = Nothing + , sbvExceptionReceived = Just $ unlines (reverse sofar) + , sbvExceptionStdOut = Nothing + , sbvExceptionStdErr = Nothing + , sbvExceptionExitCode = Nothing + , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } } + , sbvExceptionReason = Nothing + , sbvExceptionHint = if not (verbose cfg) + then Just ["Run with 'verbose=True' for further information"] + else Nothing + } + terminateSolver = do hClose inh outMVar <- newEmptyMVar out <- hGetContents outh `C.catch` (\(e :: C.SomeException) -> handleAsync e (return (show e))) @@ -680,19 +680,19 @@ ExitSuccess -> return () _ -> if ignoreExitCode cfg then msg ["Ignoring non-zero exit code of " ++ show ex ++ " per user request!"] - else C.throwIO $ SBVException { sbvExceptionDescription = "Failed to complete the call to " ++ nm - , sbvExceptionSent = Nothing - , sbvExceptionExpected = Nothing - , sbvExceptionReceived = Nothing - , sbvExceptionStdOut = Just out - , sbvExceptionStdErr = Just err - , sbvExceptionExitCode = Just ex - , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } } - , sbvExceptionReason = Nothing - , sbvExceptionHint = if not (verbose cfg) - then Just ["Run with 'verbose=True' for further information"] - else Nothing - } + else C.throwIO SBVException { sbvExceptionDescription = "Failed to complete the call to " ++ nm + , sbvExceptionSent = Nothing + , sbvExceptionExpected = Nothing + , sbvExceptionReceived = Nothing + , sbvExceptionStdOut = Just out + , sbvExceptionStdErr = Just err + , sbvExceptionExitCode = Just ex + , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } } + , sbvExceptionReason = Nothing + , sbvExceptionHint = if not (verbose cfg) + then Just ["Run with 'verbose=True' for further information"] + else Nothing + } return (send, ask, getResponseFromSolver, terminateSolver, cleanUp, pid) 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 @@ -8,6 +8,7 @@ -- -- Conversion of symbolic programs to SMTLib format, Using v2 of the standard ----------------------------------------------------------------------------- + {-# LANGUAGE PatternGuards #-} module Data.SBV.SMT.SMTLib2(cvt, cvtInc) where @@ -22,6 +23,7 @@ import qualified Data.Set as Set import Data.SBV.Core.Data +import Data.SBV.Core.Kind (smtType) import Data.SBV.SMT.Utils import Data.SBV.Control.Types @@ -43,6 +45,7 @@ usorts = [(s, dt) | KUserSort s dt <- Set.toList kindInfo] hasNonBVArrays = (not . null) [() | (_, (_, (k1, k2), _)) <- arrs, not (isBounded k1 && isBounded k2)] hasArrayInits = (not . null) [() | (_, (_, _, ArrayFree (Just _))) <- arrs] + hasList = any isList kindInfo rm = roundingMode cfg solverCaps = capabilities (solver cfg) @@ -64,11 +67,11 @@ -- NB. This isn't really fool proof! -- we never set QF_S (ALL seems to work better in all cases) - + | hasArrayInits = ["(set-logic ALL)"] - | hasString + | hasString || hasList = ["(set-logic ALL)"] | hasDouble || hasFloat @@ -94,7 +97,8 @@ | True = "UF" -- SBV always requires the production of models! - getModels = ["(set-option :produce-models true)"] + getModels = "(set-option :produce-models true)" + : concat [flattenConfig | hasList, Just flattenConfig <- [supportsFlattenedSequences solverCaps]] -- process all other settings we're given userSettings = concatMap opts $ solverSetOptions cfg @@ -432,17 +436,6 @@ swFunType :: [SW] -> SW -> String swFunType ss s = "(" ++ unwords (map swType ss) ++ ") " ++ swType s -smtType :: Kind -> String -smtType KBool = "Bool" -smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" -smtType KUnbounded = "Int" -smtType KReal = "Real" -smtType KFloat = "(_ FloatingPoint 8 24)" -smtType KDouble = "(_ FloatingPoint 11 53)" -smtType KString = "String" -smtType KChar = "(_ BitVec 8)" -smtType (KUserSort s _) = s - cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!" cvtType (SBVType xs) = "(" ++ unwords (map smtType body) ++ ") " ++ smtType ret @@ -478,8 +471,9 @@ doubleOp = any isDouble arguments floatOp = any isFloat arguments boolOp = all isBoolean arguments - charOp = all isChar arguments - stringOp = all isString arguments + charOp = any isChar arguments + stringOp = any isString arguments + listOp = any isList arguments bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr | True = error $ "SBV.SMTLib2: Unsupported operation on real values: " ++ show expr @@ -560,6 +554,14 @@ in "(" ++ o ++ " " ++ a1 ++ " " ++ a2 ++ ")" stringCmp _ o sbvs = error $ "SBV.SMT.SMTLib2.sh.stringCmp: Unexpected arguments: " ++ show (o, sbvs) + -- NB. Likewise for sequences + seqCmp swap o [a, b] + | KList{} <- kindOf (head arguments) + = let [a1, a2] | swap = [b, a] + | True = [a, b] + in "(" ++ o ++ " " ++ a1 ++ " " ++ a2 ++ ")" + seqCmp _ o sbvs = error $ "SBV.SMT.SMTLib2.sh.seqCmp: Unexpected arguments: " ++ show (o, sbvs) + lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")" lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) @@ -577,6 +579,7 @@ KDouble -> error "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index" KChar -> error "SBV.SMT.SMTLib2.cvtExp: unexpected char valued index" KString -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" + KList k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected list valued: " ++ show k KUserSort s _ -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s lkUp = "(" ++ getTable tableMap t ++ " " ++ ssw i ++ ")" cond @@ -591,6 +594,7 @@ KDouble -> ("fp.lt", "fp.geq") KChar -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" KString -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" + KList k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected sequence valued index: " ++ show k KUserSort s _ -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s mkCnst = cvtCW rm . mkConstCW (kindOf i) le0 = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")" @@ -652,6 +656,8 @@ sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in.re " ++ unwords (map ssw args) ++ " " ++ show r ++ ")" sh (SBVApp (StrOp op) args) = "(" ++ show op ++ " " ++ unwords (map ssw args) ++ ")" + sh (SBVApp (SeqOp op) args) = "(" ++ show op ++ " " ++ unwords (map ssw args) ++ ")" + sh inp@(SBVApp op args) | intOp, Just f <- lookup op smtOpIntTable = f True (map ssw args) @@ -667,6 +673,8 @@ = f False (map ssw args) | stringOp, Just f <- lookup op smtStringTable = f (map ssw args) + | listOp, Just f <- lookup op smtListTable + = f (map ssw args) | Just f <- lookup op uninterpretedTable = f (map ssw args) | True @@ -744,6 +752,15 @@ , (LessEq, stringCmp False "str.<=") , (GreaterEq, stringCmp True "str.<=") ] + -- For lists, equality is really the only operator + -- Likewise here, things might change for comparisons + smtListTable = [ (Equal, lift2S "=" "=" True) + , (NotEqual, liftNS "distinct" "distinct" True) + , (LessThan, seqCmp False "seq.<") + , (GreaterThan, seqCmp True "seq.<") + , (LessEq, seqCmp False "seq.<=") + , (GreaterEq, seqCmp True "seq.<=") + ] ----------------------------------------------------------------------------------------------- -- Casts supported by SMTLib. (From: ) diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs --- a/Data/SBV/String.hs +++ b/Data/SBV/String.hs @@ -22,7 +22,7 @@ -- * Length, emptiness length, null -- * Deconstructing/Reconstructing - , head, tail, charToStr, strToStrAt, strToCharAt, (.!!), implode, concat, (.++) + , head, tail, init, singleton, strToStrAt, strToCharAt, (.!!), implode, concat, (.:), (.++) -- * Containment , isInfixOf, isSuffixOf, isPrefixOf -- * Substrings @@ -31,10 +31,10 @@ , strToNat, natToStr ) where -import Prelude hiding (head, tail, length, take, drop, concat, null) +import Prelude hiding (head, tail, init, length, take, drop, concat, null) import qualified Prelude as P -import Data.SBV.Core.Data +import Data.SBV.Core.Data hiding (SeqOp(..)) import Data.SBV.Core.Model import qualified Data.Char as C @@ -75,18 +75,18 @@ -- | @`head`@ returns the head of a string. Unspecified if the string is empty. -- --- >>> prove $ \c -> head (charToStr c) .== c +-- >>> prove $ \c -> head (singleton c) .== c -- Q.E.D. head :: SString -> SChar head = (`strToCharAt` 0) -- | @`tail`@ returns the tail of a string. Unspecified if the string is empty. -- --- >>> prove $ \h s -> tail (charToStr h .++ s) .== s +-- >>> prove $ \h s -> tail (singleton h .++ s) .== s -- Q.E.D. -- >>> prove $ \s -> length s .> 0 ==> length (tail s) .== length s - 1 -- Q.E.D. --- >>> prove $ \s -> bnot (null s) ==> charToStr (head s) .++ tail s .== s +-- >>> prove $ \s -> bnot (null s) ==> singleton (head s) .++ tail s .== s -- Q.E.D. tail :: SString -> SString tail s @@ -95,19 +95,30 @@ | True = subStr s 1 (length s - 1) --- | @`charToStr` c@ is the string of length 1 that contains the only character +-- | @`init`@ returns all but the last element of the list. Unspecified if the string is empty. +-- +-- >>> prove $ \c t -> init (t .++ singleton c) .== t +-- Q.E.D. +init :: SString -> SString +init s + | Just cs@(_:_) <- unliteral s + = literal $ P.init cs + | True + = subStr s 0 (length s - 1) + +-- | @`singleton` c@ is the string of length 1 that contains the only character -- whose value is the 8-bit value @c@. -- --- >>> prove $ \c -> c .== literal 'A' ==> charToStr c .== "A" +-- >>> prove $ \c -> c .== literal 'A' ==> singleton c .== "A" -- Q.E.D. --- >>> prove $ \c -> length (charToStr c) .== 1 +-- >>> prove $ \c -> length (singleton c) .== 1 -- Q.E.D. -charToStr :: SChar -> SString -charToStr = lift1 StrUnit (Just wrap) +singleton :: SChar -> SString +singleton = lift1 StrUnit (Just wrap) where wrap c = [c] -- | @`strToStrAt` s offset@. Substring of length 1 at @offset@ in @s@. Unspecified if --- index is out of bounds. +-- offset is out of bounds. -- -- >>> prove $ \s1 s2 -> strToStrAt (s1 .++ s2) (length s1) .== strToStrAt s2 0 -- Q.E.D. @@ -122,7 +133,7 @@ -- -- >>> prove $ \i -> i .>= 0 &&& i .<= 4 ==> "AAAAA" `strToCharAt` i .== literal 'A' -- Q.E.D. --- >>> prove $ \s i c -> s `strToCharAt` i .== c ==> indexOf s (charToStr c) .<= i +-- >>> prove $ \s i c -> s `strToCharAt` i .== c ==> indexOf s (singleton c) .<= i -- Q.E.D. strToCharAt :: SString -> SInteger -> SChar strToCharAt s i @@ -154,7 +165,12 @@ -- >>> prove $ \c1 c2 c3 -> map (strToCharAt (implode [c1, c2, c3])) (map literal [0 .. 2]) .== [c1, c2, c3] -- Q.E.D. implode :: [SChar] -> SString -implode = foldr ((.++) . charToStr) "" +implode = foldr ((.++) . singleton) "" + +-- | Prepend an element, the traditional @cons@. +infixr 5 .: +(.:) :: SChar -> SString -> SString +c .: cs = singleton c .++ cs -- | Concatenate two strings. See also `.++`. concat :: SString -> SString -> SString diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs --- a/Data/SBV/Tools/GenTest.hs +++ b/Data/SBV/Tools/GenTest.hs @@ -112,6 +112,7 @@ valOf [] = "()" valOf [x] = s x valOf xs = "[" ++ intercalate ", " (map s xs) ++ "]" + t cw = case kindOf cw of KBool -> "Bool" KBounded False 8 -> "Word8" @@ -128,8 +129,10 @@ KChar -> error "SBV.renderTest: Unsupported char" KString -> error "SBV.renderTest: Unsupported string" KReal -> error $ "SBV.renderTest: Unsupported real valued test value: " ++ show cw + KList es -> error $ "SBV.renderTest: Unsupported list valued test: [" ++ show es ++ "]" KUserSort us _ -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw + s cw = case kindOf cw of KBool -> take 5 (show (cwToBool cw) ++ repeat ' ') KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w @@ -139,6 +142,7 @@ KChar -> error "SBV.renderTest: Unsupported char" KString -> error "SBV.renderTest: Unsupported string" KReal -> let CWAlgReal w = cwVal cw in algRealToHaskell w + KList es -> error $ "SBV.renderTest: Unsupported list valued sort: [" ++ show es ++ "]" KUserSort us _ -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us c :: String -> [([CW], [CW])] -> String @@ -231,6 +235,7 @@ KDouble -> let CWDouble w = cwVal cw in showCDouble w KChar -> error "SBV.renderTest: Unsupported char" KString -> error "SBV.renderTest: Unsupported string" + k@KList{} -> error $ "SBV.renderTest: Unsupported list sort!" ++ show k KUserSort us _ -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us KReal -> error "SBV.renderTest: Real values are not supported when generating C test-cases." outLine @@ -279,29 +284,32 @@ | True = "rev (map (\\s. s == \"1\") (explode (string_tl r)))" toF True = '1' toF False = '0' - blast cw = case kindOf cw of - KBool -> [toF (cwToBool cw)] - KBounded False 8 -> xlt 8 (cwVal cw) - KBounded False 16 -> xlt 16 (cwVal cw) - KBounded False 32 -> xlt 32 (cwVal cw) - KBounded False 64 -> xlt 64 (cwVal cw) - KBounded True 8 -> xlt 8 (cwVal cw) - KBounded True 16 -> xlt 16 (cwVal cw) - KBounded True 32 -> xlt 32 (cwVal cw) - KBounded True 64 -> xlt 64 (cwVal cw) - KFloat -> error "SBV.renderTest: Float values are not supported when generating Forte test-cases." - KDouble -> error "SBV.renderTest: Double values are not supported when generating Forte test-cases." - KChar -> error "SBV.renderTest: Char values are not supported when generating Forte test-cases." - KString -> error "SBV.renderTest: String values are not supported when generating Forte test-cases." - KReal -> error "SBV.renderTest: Real values are not supported when generating Forte test-cases." - KUnbounded -> error "SBV.renderTest: Unbounded integers are not supported when generating Forte test-cases." - _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw + blast cw = let noForte w = error "SBV.renderTest: " ++ w ++ " values are not supported when generating Forte test-cases." + in case kindOf cw of + KBool -> [toF (cwToBool cw)] + KBounded False 8 -> xlt 8 (cwVal cw) + KBounded False 16 -> xlt 16 (cwVal cw) + KBounded False 32 -> xlt 32 (cwVal cw) + KBounded False 64 -> xlt 64 (cwVal cw) + KBounded True 8 -> xlt 8 (cwVal cw) + KBounded True 16 -> xlt 16 (cwVal cw) + KBounded True 32 -> xlt 32 (cwVal cw) + KBounded True 64 -> xlt 64 (cwVal cw) + KFloat -> noForte "Float" + KDouble -> noForte "Double" + KChar -> noForte "Char" + KString -> noForte "String" + KReal -> noForte "Real" + KList ek -> noForte $ "List of " ++ show ek + KUnbounded -> noForte "Unbounded integers" + _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw xlt s (CWInteger v) = [toF (testBit v i) | i <- [s-1, s-2 .. 0]] xlt _ (CWFloat r) = error $ "SBV.renderTest.Forte: Unexpected float value: " ++ show r xlt _ (CWDouble r) = error $ "SBV.renderTest.Forte: Unexpected double value: " ++ show r xlt _ (CWChar r) = error $ "SBV.renderTest.Forte: Unexpected char value: " ++ show r xlt _ (CWString r) = error $ "SBV.renderTest.Forte: Unexpected string value: " ++ show r xlt _ (CWAlgReal r) = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r + xlt _ CWList{} = error "SBV.renderTest.Forte: Unexpected list value!" xlt _ (CWUserSort r) = error $ "SBV.renderTest.Forte: Unexpected uninterpreted value: " ++ show r mkLine (i, o) = "(" ++ mkTuple (form (fst ss) (concatMap blast i)) ++ ", " ++ mkTuple (form (snd ss) (concatMap blast o)) ++ ")" mkTuple [] = "()" diff --git a/Data/SBV/Utils/Lib.hs b/Data/SBV/Utils/Lib.hs --- a/Data/SBV/Utils/Lib.hs +++ b/Data/SBV/Utils/Lib.hs @@ -9,16 +9,26 @@ -- Misc helpers ----------------------------------------------------------------------------- +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + module Data.SBV.Utils.Lib ( mlift2, mlift3, mlift4, mlift5, mlift6, mlift7, mlift8 , joinArgs, splitArgs - , stringToQFS, qfsToString) + , stringToQFS, qfsToString + , isKString + ) where -import Data.Char (isSpace, chr, ord) -import Data.Maybe (fromJust, isNothing) +import Data.Char (isSpace, chr, ord) +import Data.Dynamic (fromDynamic, toDyn, Typeable) +import Data.Maybe (fromJust, isJust, isNothing) import Numeric (readHex, readOct, showHex) +-- We have a nasty issue with the usual String/List confusion in Haskell. However, we can +-- do a simple dynamic trick to determine where we are. The ice is thin here, but it seems to work. +isKString :: forall a. Typeable a => a -> Bool +isKString _ = isJust (fromDynamic (toDyn (undefined :: a)) :: Maybe String) -- | Monadic lift over 2-tuples mlift2 :: Monad m => (a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r diff --git a/Data/SBV/Utils/PrettyNum.hs b/Data/SBV/Utils/PrettyNum.hs --- a/Data/SBV/Utils/PrettyNum.hs +++ b/Data/SBV/Utils/PrettyNum.hs @@ -30,6 +30,7 @@ import Data.Numbers.CrackNum (floatToFP, doubleToFP) import Data.SBV.Core.Data +import Data.SBV.Core.Kind (smtType) import Data.SBV.Core.AlgReals (algRealToSMTLib2) import Data.SBV.Utils.Lib (stringToQFS) @@ -308,6 +309,7 @@ else negIf (w < 0) $ smtLibHex (intSizeOf x) (abs w) | isChar x , CWChar c <- cwVal x = smtLibHex 8 (fromIntegral (ord c)) | isString x , CWString s <- cwVal x = '\"' : stringToQFS s ++ "\"" + | isList x , CWList xs <- cwVal x = smtLibSeq (kindOf x) xs | True = error $ "SBV.cvtCW: Impossible happened: Kind/Value disagreement on: " ++ show (kindOf x, x) where roundModeConvert s = fromMaybe s (listToMaybe [smtRoundingMode m | m <- [minBound .. maxBound] :: [RoundingMode], show m == s]) -- Carefully code hex numbers, SMTLib is picky about lengths of hex constants. For the time @@ -322,6 +324,14 @@ negIf :: Bool -> String -> String negIf True a = "(bvneg " ++ a ++ ")" negIf False a = a + + smtLibSeq :: Kind -> [CWVal] -> String + smtLibSeq k [] = "(as seq.empty " ++ smtType k ++ ")" + smtLibSeq (KList ek) xs = let mkSeq [e] = e + mkSeq es = "(seq.++ " ++ unwords es ++ ")" + mkUnit inner = "(seq.unit " ++ inner ++ ")" + in mkSeq (mkUnit . cwToSMTLib rm . CW ek <$> xs) + smtLibSeq k _ = error "SBV.cwToSMTLib: Impossible case (smtLibSeq), received kind: " ++ show k -- anamoly at the 2's complement min value! Have to use binary notation here -- as there is no positive value we can provide to make the bvneg work.. (see above) diff --git a/Data/SBV/Utils/SExpr.hs b/Data/SBV/Utils/SExpr.hs --- a/Data/SBV/Utils/SExpr.hs +++ b/Data/SBV/Utils/SExpr.hs @@ -13,13 +13,13 @@ module Data.SBV.Utils.SExpr (SExpr(..), parenDeficit, parseSExpr) where -import Data.Bits (setBit, testBit) -import Data.Word (Word32, Word64) -import Data.Char (isDigit, ord, isSpace) -import Data.List (isPrefixOf) -import Data.Maybe (fromMaybe, listToMaybe) -import Numeric (readInt, readDec, readHex, fromRat) -import Data.Binary.IEEE754 (wordToFloat, wordToDouble) +import Data.Bits (setBit, testBit) +import Data.Word (Word32, Word64) +import Data.Char (isDigit, ord, isSpace) +import Data.List (isPrefixOf) +import Data.Maybe (fromMaybe, listToMaybe) +import Numeric (readInt, readDec, readHex, fromRat) +import Data.ReinterpretCast (wordToFloat, wordToDouble) import Data.SBV.Core.AlgReals import Data.SBV.Core.Data (nan, infinity, RoundingMode(..)) diff --git a/Documentation/SBV/Examples/Lists/BoundedMutex.hs b/Documentation/SBV/Examples/Lists/BoundedMutex.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/Lists/BoundedMutex.hs @@ -0,0 +1,126 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.Lists.BoundedMutex +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Demonstrates use of bounded list utilities, proving a simple +-- mutex algorithm correct up to given bounds. +----------------------------------------------------------------------------- + +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedLists #-} + +module Documentation.SBV.Examples.Lists.BoundedMutex where + +import Data.SBV +import Data.SBV.Control + +import qualified Data.SBV.List as L +import qualified Data.SBV.List.Bounded as L + +-- | Each agent can be in one of the three states +data State = Idle -- ^ Regular work + | Ready -- ^ Intention to enter critical state + | Critical -- ^ In the critical state + +-- | Make 'State' a symbolic enumeration +mkSymbolicEnumeration ''State + +-- | The type synonym 'SState' is mnemonic for symbolic state. +type SState = SBV State + +-- | Symbolic version of 'Idle' +idle :: SState +idle = literal Idle + +-- | Symbolic version of 'Ready' +ready :: SState +ready = literal Ready + +-- | Symbolic version of 'Critical' +critical :: SState +critical = literal Critical + +-- | A bounded mutex property holds for two sequences of state transitions, if they are not in +-- their critical section at the same time up to that given bound. +mutex :: Int -> SList State -> SList State -> SBool +mutex i p1s p2s = L.band i $ L.bzipWith i (\p1 p2 -> p1 ./= critical ||| p2 ./= critical) p1s p2s + +-- | A sequence is valid upto a bound if it starts at 'Idle', and follows the mutex rules. That is: +-- +-- * From 'Idle' it can switch to 'Ready' or stay 'Idle' +-- * From 'Ready' it can switch to 'Critical' if it's its turn +-- * From 'Critical' it can either stay in 'Critical' or go back to 'Idle' +-- +-- The variable @me@ identifies the agent id. +validSequence :: Int -> Integer -> SList Integer -> SList State -> SBool +validSequence b me pturns proc = bAnd [ L.length proc .== fromIntegral b + , idle .== L.head proc + , check b pturns proc idle + ] + where check 0 _ _ _ = true + check i ts ps prev = let (cur, rest) = L.uncons ps + (turn, turns) = L.uncons ts + ok = ite (prev .== idle) (cur `sElem` [idle, ready]) + $ ite (prev .== ready &&& turn .== literal me) (cur `sElem` [critical]) + $ ite (prev .== critical) (cur `sElem` [critical, idle]) + $ (cur `sElem` [prev]) + in ok &&& check (i-1) turns rest cur + +-- | The mutex algorithm, coded implicity as an assignment to turns. Turns start at @1@, and at each stage is either +-- @1@ or @2@; giving preference to that process. The only condition is that if either process is in its critical +-- section, then the turn value stays the same. Note that this is sufficient to satisfy safety (i.e., mutual +-- exclusion), though it does not guarantee liveness. +validTurns :: Int -> SList Integer -> SList State -> SList State -> SBool +validTurns b turns process1 process2 = bAnd [ L.length turns .== fromIntegral b + , 1 .== L.head turns + , check b turns process1 process2 1 + ] + where check 0 _ _ _ _ = true + check i ts proc1 proc2 prev = cur `sElem` [1, 2] + &&& (p1 .== critical ||| p2 .== critical ==> cur .== prev) + &&& check (i-1) rest p1s p2s cur + where (cur, rest) = L.uncons ts + (p1, p1s) = L.uncons proc1 + (p2, p2s) = L.uncons proc2 + +-- | Check that we have the mutex property so long as 'validSequence' and 'validTurns' holds; i.e., +-- so long as both the agents and the arbiter act according to the rules. The check is bounded up-to-the +-- given concrete bound; so this is an example of a bounded-model-checking style proof. We have: +-- +-- >>> checkMutex 20 +-- All is good! +checkMutex :: Int -> IO () +checkMutex b = runSMT $ do + p1 :: SList State <- sList "p1" + p2 :: SList State <- sList "p2" + turns :: SList Integer <- sList "turns" + + -- Ensure that both sequences and the turns are valid + constrain $ validSequence b 1 turns p1 + constrain $ validSequence b 2 turns p2 + constrain $ validTurns b turns p1 p2 + + -- Try to assert that mutex does not hold. If we get a + -- counter example, we would've found a violation! + constrain $ bnot $ mutex b p1 p2 + + query $ do cs <- checkSat + case cs of + Unk -> error "Solver said Unknown!" + Unsat -> io . putStrLn $ "All is good!" + Sat -> do io . putStrLn $ "Violation detected!" + do p1V <- getValue p1 + p2V <- getValue p2 + ts <- getValue turns + + io . putStrLn $ "P1: " ++ show p1V + io . putStrLn $ "P2: " ++ show p2V + io . putStrLn $ "Ts: " ++ show ts diff --git a/Documentation/SBV/Examples/Lists/Fibonacci.hs b/Documentation/SBV/Examples/Lists/Fibonacci.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/Lists/Fibonacci.hs @@ -0,0 +1,49 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.Lists.Fibonacci +-- Copyright : (c) Joel Burget +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Define the fibonacci sequence as an SBV symbolic list. +----------------------------------------------------------------------------- + +module Documentation.SBV.Examples.Lists.Fibonacci where + +import Data.SBV + +import Data.SBV.List ((.!!)) +import qualified Data.SBV.List as L + +import Data.SBV.Control + +-- | Compute a prefix of the fibonacci numbers. We have: +-- >>> mkFibs 10 +-- [1,1,2,3,5,8,13,21,34,55] +mkFibs :: Int -> IO [Integer] +mkFibs n = take n <$> runSMT genFibs + +-- | Generate fibonacci numbers as a sequence. Note that we constrain only +-- the first 200 entries. +genFibs :: Symbolic [Integer] +genFibs = do fibs <- sList "fibs" + + -- constrain the length + constrain $ L.length fibs .== 200 + + -- Constrain first two elements + constrain $ fibs .!! 0 .== 1 + constrain $ fibs .!! 1 .== 1 + + -- Constrain an arbitrary element at index `i` + let constr i = constrain $ fibs .!! i + fibs .!! (i+1) .== fibs .!! (i+2) + + -- Constrain the remaining elts + mapM_ (constr . fromIntegral) [(0::Int) .. 197] + + query $ do cs <- checkSat + case cs of + Unk -> error "Solver returned unknown!" + Unsat -> error "Solver couldn't generate the fibonacci sequence!" + Sat -> getValue fibs diff --git a/Documentation/SBV/Examples/Lists/Nested.hs b/Documentation/SBV/Examples/Lists/Nested.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/Lists/Nested.hs @@ -0,0 +1,40 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.Lists.Nested +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Demonstrates nested lists +----------------------------------------------------------------------------- + +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Documentation.SBV.Examples.Lists.Nested where + +import Data.SBV +import Data.SBV.Control + +import Data.SBV.List ((.!!)) +import qualified Data.SBV.List as L + +-- | Simple example demonstrating the use of nested lists. We have: +-- +-- >>> nestedExample +-- [[1,2,3],[4,5,6,7],[8,9,10],[11,12,13]] +nestedExample :: IO () +nestedExample = runSMT $ do a :: SList [Integer] <- free "a" + + constrain $ a .!! 0 .== [1, 2, 3] + constrain $ a .!! 1 .== [4, 5, 6, 7] + constrain $ L.tail (L.tail a) .== [[8, 9, 10], [11, 12, 13]] + constrain $ L.length a .== 4 + + query $ do cs <- checkSat + case cs of + Unk -> error "Solver said unknown!" + Unsat -> io $ putStrLn "Unsat" + Sat -> do v <- getValue a + io $ print v diff --git a/Documentation/SBV/Examples/Strings/RegexCrossword.hs b/Documentation/SBV/Examples/Strings/RegexCrossword.hs --- a/Documentation/SBV/Examples/Strings/RegexCrossword.hs +++ b/Documentation/SBV/Examples/Strings/RegexCrossword.hs @@ -8,6 +8,7 @@ -- -- This example solves regex crosswords from ----------------------------------------------------------------------------- + {-# LANGUAGE OverloadedStrings #-} module Documentation.SBV.Examples.Strings.RegexCrossword where @@ -17,6 +18,7 @@ import Data.SBV import Data.SBV.Control +import Data.SBV.String ((.!!)) import qualified Data.SBV.String as S import qualified Data.SBV.RegExp as R diff --git a/Documentation/SBV/Examples/Strings/SQLInjection.hs b/Documentation/SBV/Examples/Strings/SQLInjection.hs --- a/Documentation/SBV/Examples/Strings/SQLInjection.hs +++ b/Documentation/SBV/Examples/Strings/SQLInjection.hs @@ -11,6 +11,7 @@ -- but this example finds program inputs which result in a query containing a -- SQL injection. ----------------------------------------------------------------------------- + {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -23,6 +24,7 @@ import Data.SBV import Data.SBV.Control +import Data.SBV.String ((.++)) import qualified Data.SBV.RegExp as R -- | Simple expression language @@ -104,10 +106,13 @@ -- query ("SELECT msg FROM msgs where topicid='" ++ my_topicid ++ "'") -- @ -- --- We have: +-- We have: (NB. Turning this doctest off, since Z3 no longer can handle +-- it, see: .) -- --- >>> findInjection exampleProgram --- "h'; DROP TABLE 'users" +-- @ +-- findInjection exampleProgram +-- "h'; DROP TABLE 'users" +-- @ -- -- Indeed, if we substitute the suggested string, we get the program: -- diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -7,18 +7,16 @@ ### Build Status - Linux: - - GHC 8.2.1 [![Build1][3]][1] - - GHC 8.2.2 [![Build1][4]][1] - - GHC 8.4.1 [![Build1][5]][1] + - GHC 8.2.2 [![Build1][3]][1] + - GHC 8.4.3 [![Build1][4]][1] - Mac OSX: - - GHC 8.2.1 [![Build1][6]][1] + - GHC 8.4.3 [![Build1][5]][1] - Windows: - - GHC 8.4.2 [![Build5][7]][2] + - GHC 8.4.3 [![Build5][6]][2] [1]: https://travis-ci.org/LeventErkok/sbv [2]: https://ci.appveyor.com/project/LeventErkok/sbv [3]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/1 [4]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/2 [5]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/3 -[6]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/4 -[7]: https://ci.appveyor.com/api/projects/status/github/LeventErkok/sbv?svg=true +[6]: https://ci.appveyor.com/api/projects/status/github/LeventErkok/sbv?svg=true diff --git a/SBVTestSuite/GoldFiles/freshVars.gold b/SBVTestSuite/GoldFiles/freshVars.gold --- a/SBVTestSuite/GoldFiles/freshVars.gold +++ b/SBVTestSuite/GoldFiles/freshVars.gold @@ -4,6 +4,8 @@ [GOOD] (set-option :global-declarations true) [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :produce-models true) [GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- @@ -102,6 +104,31 @@ [GOOD] (define-fun s57 () (_ BitVec 8) #x58) [GOOD] (define-fun s58 () Bool (= s53 s57)) [GOOD] (assert s58) +[GOOD] (define-fun s59 () Int 1) +[GOOD] (define-fun s60 () Bool (= s43 s59)) +[GOOD] (assert s60) +[GOOD] (define-fun s61 () Bool (not s44)) +[GOOD] (assert s61) +[GOOD] (declare-fun s62 () String) +[GOOD] (declare-fun s63 () (Seq Int)) +[GOOD] (declare-fun s64 () (Seq (Seq Int))) +[GOOD] (declare-fun s65 () (Seq (_ BitVec 8))) +[GOOD] (declare-fun s66 () (Seq (Seq (_ BitVec 16)))) +[GOOD] (define-fun s67 () String "hello") +[GOOD] (define-fun s68 () Bool (= s62 s67)) +[GOOD] (assert s68) +[GOOD] (define-fun s69 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4))) +[GOOD] (define-fun s70 () Bool (= s63 s69)) +[GOOD] (assert s70) +[GOOD] (define-fun s71 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7))))) +[GOOD] (define-fun s72 () Bool (= s64 s71)) +[GOOD] (assert s72) +[GOOD] (define-fun s73 () (Seq (_ BitVec 8)) (seq.++ (seq.unit #x01) (seq.unit #x02))) +[GOOD] (define-fun s74 () Bool (= s65 s73)) +[GOOD] (assert s74) +[GOOD] (define-fun s75 () (Seq (Seq (_ BitVec 16))) (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006))))) +[GOOD] (define-fun s76 () Bool (= s66 s75)) +[GOOD] (assert s76) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -142,27 +169,49 @@ [RECV] ((s52 42)) [SEND] (get-value (s53)) [RECV] ((s53 #x58)) +[SEND] (get-value (s62)) +[RECV] ((s62 "hello")) +[SEND] (get-value (s63)) +[RECV] ((s63 (seq.++ (seq.unit 1) (seq.++ (seq.unit 2) (seq.++ (seq.unit 3) (seq.unit 4)))))) +[SEND] (get-value (s64)) +[RECV] ((s64 (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.++ (seq.unit 2) (seq.unit 3)))) + (seq.unit (seq.++ (seq.unit 4) + (seq.++ (seq.unit 5) + (seq.++ (seq.unit 6) (seq.unit 7)))))))) +[SEND] (get-value (s65)) +[RECV] ((s65 "\x01\x02")) +[SEND] (get-value (s66)) +[RECV] ((s66 (seq.++ (seq.unit (seq.++ (seq.unit #x0001) + (seq.++ (seq.unit #x0002) (seq.unit #x0003)))) + (seq.++ (seq.unit (as seq.empty (Seq (_ BitVec 16)))) + (seq.unit (seq.++ (seq.unit #x0004) + (seq.++ (seq.unit #x0005) (seq.unit #x0006)))))))) *** Solver : Z3 *** Exit code: ExitSuccess FINAL:Satisfiable. Model: - a = 0 :: Integer - vBool = True :: Bool - vWord8 = 1 :: Word8 - s5 = 2 :: Word16 - s6 = 3 :: Word32 - vWord64 = 4 :: Word64 - vInt8 = 5 :: Int8 - s9 = 6 :: Int16 - s10 = 7 :: Int32 - vInt64 = 8 :: Int64 - vFloat = 9.0 :: Float - s13 = 10.0 :: Double - s14 = 11.0 :: Real - vInteger = 12 :: Integer - vBinOp = Plus :: BinOp - i1 = 1 :: Integer - i2 = False :: Bool - mustBe42 = 42 :: Integer - mustBeX = 'X' :: Char + a = 0 :: Integer + vBool = True :: Bool + vWord8 = 1 :: Word8 + s5 = 2 :: Word16 + s6 = 3 :: Word32 + vWord64 = 4 :: Word64 + vInt8 = 5 :: Int8 + s9 = 6 :: Int16 + s10 = 7 :: Int32 + vInt64 = 8 :: Int64 + vFloat = 9.0 :: Float + s13 = 10.0 :: Double + s14 = 11.0 :: Real + vInteger = 12 :: Integer + vBinOp = Plus :: BinOp + i1 = 1 :: Integer + i2 = False :: Bool + mustBe42 = 42 :: Integer + mustBeX = 'X' :: Char + vString = "hello" :: String + vList1 = [1,2,3,4] :: [SInteger] + vList2 = [[1,2,3],[4,5,6,7]] :: [[SInteger]] + vList3 = [1,2] :: [SWord8] + vList4 = [[1,2,3],[],[4,5,6]] :: [[SWord16]] DONE! diff --git a/SBVTestSuite/GoldFiles/query_Lists1.gold b/SBVTestSuite/GoldFiles/query_Lists1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_Lists1.gold @@ -0,0 +1,36 @@ +** 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-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s1 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4) (seq.unit 5))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s2 () Bool (= s0 s1)) +[GOOD] (assert s2) +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 (seq.++ (seq.unit 1) + (seq.++ (seq.unit 2) + (seq.++ (seq.unit 3) (seq.++ (seq.unit 4) (seq.unit 5))))))) +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +[1,2,3,4,5] diff --git a/SBVTestSuite/GoldFiles/query_badOption.gold b/SBVTestSuite/GoldFiles/query_badOption.gold --- a/SBVTestSuite/GoldFiles/query_badOption.gold +++ b/SBVTestSuite/GoldFiles/query_badOption.gold @@ -26,6 +26,7 @@ *** proof (bool) (default: false) *** rlimit (unsigned int) (default: 0) *** smtlib2_compliant (bool) (default: false) +*** stats (bool) (default: false) *** timeout (unsigned int) (default: 4294967295) *** trace (bool) (default: false) *** trace_file_name (string) (default: z3.log) diff --git a/SBVTestSuite/GoldFiles/seqConcat.gold b/SBVTestSuite/GoldFiles/seqConcat.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqConcat.gold @@ -0,0 +1,24 @@ +** 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-logic QF_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_1) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqConcatBad.gold b/SBVTestSuite/GoldFiles/seqConcatBad.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqConcatBad.gold @@ -0,0 +1,24 @@ +** 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-logic QF_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_2) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqExamples1.gold b/SBVTestSuite/GoldFiles/seqExamples1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqExamples1.gold @@ -0,0 +1,24 @@ +** 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-logic QF_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_1) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqExamples2.gold b/SBVTestSuite/GoldFiles/seqExamples2.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqExamples2.gold @@ -0,0 +1,32 @@ +** 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-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s1 () (Seq Int) (seq.unit 2)) +[GOOD] (define-fun s3 () (Seq Int) (seq.unit 1)) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s2 () (Seq Int) (seq.++ s0 s1)) +[GOOD] (define-fun s4 () (Seq Int) (seq.++ s3 s0)) +[GOOD] (define-fun s5 () Bool (= s2 s4)) +[GOOD] (assert s5) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqExamples3.gold b/SBVTestSuite/GoldFiles/seqExamples3.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqExamples3.gold @@ -0,0 +1,40 @@ +** 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-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s4 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4))) +[GOOD] (define-fun s7 () (Seq Int) (seq.++ (seq.unit 3) (seq.unit 4) (seq.unit 5) (seq.unit 6))) +[GOOD] (define-fun s9 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" +[GOOD] (declare-fun s1 () (Seq Int)) ; tracks user variable "b" +[GOOD] (declare-fun s2 () (Seq Int)) ; tracks user variable "c" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () (Seq Int) (seq.++ s0 s1)) +[GOOD] (define-fun s5 () Bool (= s3 s4)) +[GOOD] (define-fun s6 () (Seq Int) (seq.++ s1 s2)) +[GOOD] (define-fun s8 () Bool (= s6 s7)) +[GOOD] (define-fun s10 () Bool (= s1 s9)) +[GOOD] (define-fun s11 () Bool (not s10)) +[GOOD] (assert s5) +[GOOD] (assert s8) +[GOOD] (assert s11) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqExamples4.gold b/SBVTestSuite/GoldFiles/seqExamples4.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqExamples4.gold @@ -0,0 +1,37 @@ +** 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-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s8 () Int 2) +[GOOD] (define-fun s2 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) +[GOOD] (define-fun s4 () (Seq Int) (seq.++ (seq.unit 3) (seq.unit 4) (seq.unit 5))) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" +[GOOD] (declare-fun s1 () (Seq Int)) ; tracks user variable "b" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () (Seq Int) (seq.++ s2 s0)) +[GOOD] (define-fun s5 () (Seq Int) (seq.++ s1 s4)) +[GOOD] (define-fun s6 () Bool (= s3 s5)) +[GOOD] (define-fun s7 () Int (seq.len s0)) +[GOOD] (define-fun s9 () Bool (<= s7 s8)) +[GOOD] (assert s6) +[GOOD] (assert s9) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqExamples5.gold b/SBVTestSuite/GoldFiles/seqExamples5.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqExamples5.gold @@ -0,0 +1,45 @@ +** 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-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s3 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2))) +[GOOD] (define-fun s6 () (Seq Int) (seq.++ (seq.unit 2) (seq.unit 1))) +[GOOD] (define-fun s12 () (Seq Int) (seq.unit 1)) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" +[GOOD] (declare-fun s1 () (Seq Int)) ; tracks user variable "b" +[GOOD] (declare-fun s2 () (Seq Int)) ; tracks user variable "c" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s4 () (Seq Int) (seq.++ s3 s1)) +[GOOD] (define-fun s5 () (Seq Int) (seq.++ s0 s4)) +[GOOD] (define-fun s7 () (Seq Int) (seq.++ s6 s2)) +[GOOD] (define-fun s8 () (Seq Int) (seq.++ s1 s7)) +[GOOD] (define-fun s9 () Bool (= s5 s8)) +[GOOD] (define-fun s10 () (Seq Int) (seq.++ s0 s1)) +[GOOD] (define-fun s11 () Bool (= s2 s10)) +[GOOD] (define-fun s13 () (Seq Int) (seq.++ s0 s12)) +[GOOD] (define-fun s14 () (Seq Int) (seq.++ s12 s0)) +[GOOD] (define-fun s15 () Bool (= s13 s14)) +[GOOD] (define-fun s16 () Bool (not s15)) +[GOOD] (assert s9) +[GOOD] (assert s11) +[GOOD] (assert s16) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqExamples6.gold b/SBVTestSuite/GoldFiles/seqExamples6.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqExamples6.gold @@ -0,0 +1,35 @@ +** 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-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" +[GOOD] (declare-fun s1 () (Seq Int)) ; tracks user variable "b" +[GOOD] (declare-fun s2 () (Seq Int)) ; tracks user variable "c" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () Bool (seq.contains s0 s1)) +[GOOD] (define-fun s4 () Bool (seq.contains s1 s2)) +[GOOD] (define-fun s5 () Bool (seq.contains s0 s2)) +[GOOD] (define-fun s6 () Bool (not s5)) +[GOOD] (assert s3) +[GOOD] (assert s4) +[GOOD] (assert s6) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqExamples7.gold b/SBVTestSuite/GoldFiles/seqExamples7.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqExamples7.gold @@ -0,0 +1,38 @@ +** 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-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" +[GOOD] (declare-fun s1 () (Seq Int)) ; tracks user variable "b" +[GOOD] (declare-fun s2 () (Seq Int)) ; tracks user variable "c" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () Bool (seq.contains s0 s1)) +[GOOD] (define-fun s4 () Bool (seq.contains s0 s2)) +[GOOD] (define-fun s5 () Bool (seq.contains s1 s2)) +[GOOD] (define-fun s6 () Bool (not s5)) +[GOOD] (define-fun s7 () Bool (seq.contains s2 s1)) +[GOOD] (define-fun s8 () Bool (not s7)) +[GOOD] (assert s3) +[GOOD] (assert s4) +[GOOD] (assert s6) +[GOOD] (assert s8) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqExamples8.gold b/SBVTestSuite/GoldFiles/seqExamples8.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqExamples8.gold @@ -0,0 +1,42 @@ +** 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-logic ALL) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" +[GOOD] (declare-fun s1 () (Seq Int)) ; tracks user variable "b" +[GOOD] (declare-fun s2 () (Seq Int)) ; tracks user variable "c" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s3 () Bool (seq.prefixof s1 s0)) +[GOOD] (define-fun s4 () Bool (seq.suffixof s2 s0)) +[GOOD] (define-fun s5 () Int (seq.len s0)) +[GOOD] (define-fun s6 () Int (seq.len s1)) +[GOOD] (define-fun s7 () Int (seq.len s2)) +[GOOD] (define-fun s8 () Int (+ s6 s7)) +[GOOD] (define-fun s9 () Bool (= s5 s8)) +[GOOD] (define-fun s10 () (Seq Int) (seq.++ s1 s2)) +[GOOD] (define-fun s11 () Bool (= s0 s10)) +[GOOD] (define-fun s12 () Bool (not s11)) +[GOOD] (assert s3) +[GOOD] (assert s4) +[GOOD] (assert s9) +[GOOD] (assert s12) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqIndexOf.gold b/SBVTestSuite/GoldFiles/seqIndexOf.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqIndexOf.gold @@ -0,0 +1,24 @@ +** 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-logic QF_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_1) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/seqIndexOfBad.gold b/SBVTestSuite/GoldFiles/seqIndexOfBad.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/seqIndexOfBad.gold @@ -0,0 +1,24 @@ +** 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-logic QF_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] ; --- skolem constants --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (assert s_2) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -1,4 +1,16 @@ +----------------------------------------------------------------------------- +-- | +-- Module : SBVTestSuite.SBVTest.Main +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Main entry point to the test suite +----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} + module Main(main) where import Test.Tasty @@ -20,6 +32,7 @@ import qualified TestSuite.Basics.Higher import qualified TestSuite.Basics.Index import qualified TestSuite.Basics.IteTest +import qualified TestSuite.Basics.List import qualified TestSuite.Basics.ProofTests import qualified TestSuite.Basics.PseudoBoolean import qualified TestSuite.Basics.QRem @@ -81,6 +94,7 @@ import qualified TestSuite.Queries.Int_Yices import qualified TestSuite.Queries.Int_Z3 import qualified TestSuite.Queries.Interpolants +import qualified TestSuite.Queries.Lists import qualified TestSuite.Queries.Strings import qualified TestSuite.Queries.Uninterpreted import qualified TestSuite.QuickCheck.QC @@ -151,6 +165,7 @@ , TestSuite.Basics.Higher.tests , TestSuite.Basics.Index.tests , TestSuite.Basics.IteTest.tests + , TestSuite.Basics.List.tests , TestSuite.Basics.ProofTests.tests , TestSuite.Basics.PseudoBoolean.tests , TestSuite.Basics.QRem.tests @@ -204,6 +219,7 @@ , TestSuite.Queries.Enums.tests , TestSuite.Queries.FreshVars.tests , TestSuite.Queries.Int_Z3.tests + , TestSuite.Queries.Lists.tests , TestSuite.Queries.Strings.tests , TestSuite.Queries.Uninterpreted.tests , TestSuite.Uninterpreted.AUF.tests diff --git a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs @@ -16,18 +16,19 @@ module TestSuite.Basics.ArithNoSolver(tests) where -import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble, floatToWord, doubleToWord) +import qualified Data.ReinterpretCast as RC (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.SBV.Internals import Utils.SBVTestFramework -import Data.Maybe (fromJust, isJust) +import Data.Maybe (fromJust, isJust, fromMaybe) import Data.List (genericIndex, isInfixOf, isPrefixOf, isSuffixOf, genericTake, genericDrop, genericLength) import qualified Data.Char as C import qualified Data.SBV.Char as SC import qualified Data.SBV.String as SS +import qualified Data.SBV.List as SL -- Test suite tests :: TestTree @@ -70,6 +71,7 @@ ++ genIntCasts ++ genChars ++ genStrings + ++ genLists genBinTest :: String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree] genBinTest nm op = map mkTest $ @@ -87,19 +89,21 @@ genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [TestTree] genBoolTest nm op opS = map mkTest $ - zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `opS` y | x <- sw8s, y <- sw8s ] - ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `opS` y | x <- sw16s, y <- sw16s] - ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `opS` y | x <- sw32s, y <- sw32s] - ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `opS` y | x <- sw64s, y <- sw64s] - ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `opS` y | x <- si8s, y <- si8s ] - ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `opS` y | x <- si16s, y <- si16s] - ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `opS` y | x <- si32s, y <- si32s] - ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `opS` y | x <- si64s, y <- si64s] - ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `opS` y | x <- siUBs, y <- siUBs] - ++ zipWith pair [(show x, show y, x `op` y) | x <- iCs, y <- iCs ] [x `opS` y | x <- siCs, y <- siCs ] - ++ zipWith pair [(show x, show y, x `op` y) | x <- ss, y <- ss ] [x `opS` y | x <- sss, y <- sss ] + zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `opS` y | x <- sw8s, y <- sw8s ] + ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `opS` y | x <- sw16s, y <- sw16s] + ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `opS` y | x <- sw32s, y <- sw32s] + ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `opS` y | x <- sw64s, y <- sw64s] + ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `opS` y | x <- si8s, y <- si8s ] + ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `opS` y | x <- si16s, y <- si16s] + ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `opS` y | x <- si32s, y <- si32s] + ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `opS` y | x <- si64s, y <- si64s] + ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `opS` y | x <- siUBs, y <- siUBs] + ++ zipWith pair [(show x, show y, x `op` y) | x <- iCs, y <- iCs ] [x `opS` y | x <- siCs, y <- siCs ] + ++ zipWith pair [(show x, show y, x `op` y) | x <- ss, y <- ss ] [x `opS` y | x <- sss, y <- sss ] + ++ zipWith pair [(show x, show y, toL x `op` toL y) | x <- ssl, y <- ssl ] [x `opS` y | x <- ssl, y <- ssl ] where pair (x, y, a) b = (x, y, Just a == unliteral b) mkTest (x, y, s) = testCase ("arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y) (s `showsAs` "True") + toL x = fromMaybe (error "genBoolTest: Cannot extract a literal!") (unliteral x) genUnTest :: String -> (forall a. (Num a, Bits a) => a -> a) -> [TestTree] genUnTest nm op = map mkTest $ @@ -415,11 +419,11 @@ ++ map cvtTestI [("fromFP_Double_ToInteger", show x, (fromSDouble sRNE :: SDouble -> SInteger) (literal x), ((fromIntegral :: Integer -> SInteger) . fpRound0) x) | x <- ds] ++ map cvtTestI [("fromFP_Double_ToReal", show x, (fromSDouble sRNE :: SDouble -> SReal) (literal x), (fromRational . fpRatio0) x) | x <- ds] - ++ map cvtTest [("reinterp_Word32_Float", show x, sWord32AsSFloat (literal x), literal (DB.wordToFloat x)) | x <- w32s] - ++ map cvtTest [("reinterp_Word64_Double", show x, sWord64AsSDouble (literal x), literal (DB.wordToDouble x)) | x <- w64s] + ++ map cvtTest [("reinterp_Word32_Float", show x, sWord32AsSFloat (literal x), literal (RC.wordToFloat x)) | x <- w32s] + ++ map cvtTest [("reinterp_Word64_Double", show x, sWord64AsSDouble (literal x), literal (RC.wordToDouble x)) | x <- w64s] - ++ map cvtTestI [("reinterp_Float_Word32", show x, sFloatAsSWord32 (literal x), literal (DB.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN - ++ map cvtTestI [("reinterp_Double_Word64", show x, sDoubleAsSWord64 (literal x), literal (DB.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN + ++ map cvtTestI [("reinterp_Float_Word32", show x, sFloatAsSWord32 (literal x), literal (RC.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN + ++ map cvtTestI [("reinterp_Double_Word64", show x, sDoubleAsSWord64 (literal x), literal (RC.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN floatRun1 nm f g cmb = map (nm,) [cmb (x, f x, extract (g (literal x))) | x <- fs] doubleRun1 nm f g cmb = map (nm,) [cmb (x, f x, extract (g (literal x))) | x <- ds] @@ -515,7 +519,7 @@ ++ [("null", show s, check1 SS.null null s ) | s <- ss ] ++ [("head", show s, check1 SS.head head s ) | s <- ss, not (null s) ] ++ [("tail", show s, check1 SS.tail tail s ) | s <- ss, not (null s) ] - ++ [("charToStr", show c, check1 SS.charToStr (: []) c ) | c <- cs ] + ++ [("singleton", show c, check1 SS.singleton (: []) c ) | c <- cs ] ++ [("implode", show s, checkI SS.implode s ) | s <- ss ] ++ [("strToNat", show s, check1 SS.strToNat strToNat s ) | s <- ss ] ++ [("natToStr", show i, check1 SS.natToStr natToStr i ) | i <- iUBs ]) @@ -594,6 +598,80 @@ Nothing -> False Just x -> x == cop arg1 arg2 arg3 +genLists :: [TestTree] +genLists = map mkTest1 ( [("length", show l, check1 SL.length llen l ) | l <- sl ] + ++ [("null", show l, check1 SL.null null l ) | l <- sl ] + ++ [("head", show l, check1 SL.head head l ) | l <- sl, not (null l) ] + ++ [("tail", show l, check1 SL.tail tail l ) | l <- sl, not (null l) ] + ++ [("singleton", show i, check1 SL.singleton (: []) i ) | i <- iUBs ] + ++ [("implode", show l, checkI SL.implode id l ) | l <- sl ]) + ++ map mkTest2 ( [("listToListAt", show l, show i, check2 SL.listToListAt listToListAt l i ) | l <- sl, i <- range l ] + ++ [("elemAt", show l, show i, check2 SL.elemAt elemAt l i ) | l <- sl, i <- range l ] + ++ [("concat", show l, show l1, check2 SL.concat (++) l l1 ) | l <- sl, l1 <- sl ] + ++ [("isInfixOf", show l, show l1, check2 SL.isInfixOf isInfixOf l l1 ) | l <- sl, l1 <- sl ] + ++ [("isSuffixOf", show l, show l1, check2 SL.isSuffixOf isSuffixOf l l1 ) | l <- sl, l1 <- sl ] + ++ [("isPrefixOf", show l, show l1, check2 SL.isPrefixOf isPrefixOf l l1 ) | l <- sl, l1 <- sl ] + ++ [("take", show l, show i, check2 SL.take genericTake i l ) | l <- sl, i <- iUBs ] + ++ [("drop", show l, show i, check2 SL.drop genericDrop i l ) | l <- sl, i <- iUBs ] + ++ [("indexOf", show l, show l1, check2 SL.indexOf indexOf l l1 ) | l <- sl, l1 <- sl ]) + ++ map mkTest3 ( [("subList", show l, show i, show j, check3 SL.subList subList l i j ) | l <- sl, i <- range l, j <- range l, i + j <= genericLength l] + ++ [("replace", show l, show l1, show l2, check3 SL.replace replace l l1 l2) | l <- sl, l1 <- sl, l2 <- sl ] + ++ [("offsetIndexOf", show l, show l1, show i, check3 SL.offsetIndexOf offsetIndexOf l l1 i ) | l <- sl, l1 <- sl, i <- range l ]) + where llen :: [Integer] -> Integer + llen = fromIntegral . length + + range :: [Integer] -> [Integer] + range l = map fromIntegral [0 .. length l - 1] + + indexOf :: [Integer] -> [Integer] -> Integer + indexOf s1 s2 = go 0 s1 + where go i x + | s2 `isPrefixOf` x = i + | True = case x of + [] -> -1 + (_:r) -> go (i+1) r + + listToListAt :: [Integer] -> Integer -> [Integer] + s `listToListAt` i = [s `elemAt` i] + + elemAt :: [Integer] -> Integer -> Integer + l `elemAt` i = l `genericIndex` i + + subList :: [Integer] -> Integer -> Integer -> [Integer] + subList s i j = genericTake j (genericDrop i s) + + replace :: [Integer] -> [Integer] -> [Integer] -> [Integer] + replace s [] y = y ++ s + replace s x y = go s + where go [] = [] + go h@(c:rest) | x `isPrefixOf` h = y ++ drop (length x) h + | True = c : go rest + + offsetIndexOf :: [Integer] -> [Integer] -> Integer -> Integer + offsetIndexOf x y i = case indexOf (genericDrop i x) y of + -1 -> -1 + r -> r+i + + mkTest1 (nm, x, t) = testCase ("genLists-" ++ nm ++ "." ++ x) (assert t) + mkTest2 (nm, x, y, t) = testCase ("genLists-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t) + mkTest3 (nm, x, y, z, t) = testCase ("genLists-" ++ nm ++ "." ++ x ++ "_" ++ y ++ "_" ++ z) (assert t) + + checkI sop cop arg = case unliteral (sop (map literal arg)) of + Nothing -> False + Just x -> x == cop arg + + check1 sop cop arg = case unliteral (sop (literal arg)) of + Nothing -> False + Just x -> x == cop arg + + check2 sop cop arg1 arg2 = case unliteral (sop (literal arg1) (literal arg2)) of + Nothing -> False + Just x -> x == cop arg1 arg2 + + check3 sop cop arg1 arg2 arg3 = case unliteral (sop (literal arg1) (literal arg2) (literal arg3)) of + Nothing -> False + Just x -> x == cop arg1 arg2 arg3 + -- Concrete test data xsUnsigned :: (Num a, Bounded a) => [a] xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound) @@ -694,3 +772,13 @@ sss :: [SString] sss = map literal ss + +-- Lists are the worst in coverage! +sl :: [[Integer]] +sl = [[], [0], [-1, 1], [-10, 0, 10], [3, 4, 5, 4, 5, 3]] + +-- Lists are the worst in coverage! +ssl :: [SList Integer] +ssl = map literal sl + +{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} diff --git a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs @@ -11,21 +11,23 @@ -- constant folding. ----------------------------------------------------------------------------- -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Basics.ArithSolver(tests) where -import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble, floatToWord, doubleToWord) +import qualified Data.ReinterpretCast as RC (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.SBV.Internals import Utils.SBVTestFramework import Data.List (genericIndex, isInfixOf, isPrefixOf, isSuffixOf, genericTake, genericDrop, genericLength) -import qualified Data.Char as C -import qualified Data.SBV.Char as SC +import qualified Data.Char as C +import qualified Data.SBV.Char as SC import qualified Data.SBV.String as SS +import qualified Data.SBV.List as SL -- Test suite tests :: TestTree @@ -71,6 +73,7 @@ ++ genIntCasts ++ genChars ++ genStrings + ++ genLists ) genBinTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree] @@ -90,25 +93,31 @@ return $ literal r .== a `op` b genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [TestTree] -genBoolTest nm op opS = map mkTest $ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- w8s ] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- i8s ] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- iUBs] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- reducedCS, y <- reducedCS] - ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- ss, y <- ss, nm `elem` allowedStringComps] - where -- Currently Z3 doesn't allow for string comparisons, so only test equals and distinct +genBoolTest nm op opS = map mkTest $ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- w8s ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- i8s ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- iUBs ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- reducedCS, y <- reducedCS ] + ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- ss, y <- ss, nm `elem` allowedStringComps] + ++ [(show x, show y, mkThm2L x y (x `op` y)) | x <- sl, y <- sl, nm `elem` allowedListComps ] + where -- Currently Z3 doesn't allow for string/list comparisons, so only test equals and distinct -- See: http://github.com/LeventErkok/sbv/issues/368 for tracking issue. allowedStringComps = ["==", "/="] + allowedListComps = ["==", "/="] mkTest (x, y, t) = testCase ("genBoolTest.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t) mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y return $ literal r .== a `opS` b + mkThm2L x y r = isTheorem $ do [a, b :: SList Integer] <- mapM free ["x", "y"] + constrain $ a .== literal x + constrain $ b .== literal y + return $ literal r .== a `opS` b genUnTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a) -> [TestTree] genUnTest unboundedOK nm op = map mkTest $ [(show x, mkThm x (op x)) | x <- w8s ] @@ -446,11 +455,11 @@ -- ++ [("fromFP_Double_ToInteger", show x, mkThmC' (m fromSDouble :: SDouble -> SInteger) x (((fromIntegral :: Integer -> Integer) . fpRound0) x)) | x <- ds] -- ++ [("fromFP_Double_ToReal", show x, mkThmC' (m fromSDouble :: SDouble -> SReal) x ( (fromRational . fpRatio0) x)) | x <- ds] - ++ [("reinterp_Word32_Float", show x, mkThmC sWord32AsSFloat x (DB.wordToFloat x)) | x <- w32s] - ++ [("reinterp_Word64_Double", show x, mkThmC sWord64AsSDouble x (DB.wordToDouble x)) | x <- w64s] + ++ [("reinterp_Word32_Float", show x, mkThmC sWord32AsSFloat x (RC.wordToFloat x)) | x <- w32s] + ++ [("reinterp_Word64_Double", show x, mkThmC sWord64AsSDouble x (RC.wordToDouble x)) | x <- w64s] - ++ [("reinterp_Float_Word32", show x, mkThmP sFloatAsSWord32 x (DB.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN - ++ [("reinterp_Double_Word64", show x, mkThmP sDoubleAsSWord64 x (DB.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN + ++ [("reinterp_Float_Word32", show x, mkThmP sFloatAsSWord32 x (RC.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN + ++ [("reinterp_Double_Word64", show x, mkThmP sDoubleAsSWord64 x (RC.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN m f = f sRNE @@ -560,7 +569,7 @@ ++ [("null", show s, mkThm1 SS.null null s ) | s <- ss ] ++ [("head", show s, mkThm1 SS.head head s ) | s <- ss, not (null s) ] ++ [("tail", show s, mkThm1 SS.tail tail s ) | s <- ss, not (null s) ] - ++ [("charToStr", show c, mkThm1 SS.charToStr (: []) c ) | c <- cs ] + ++ [("singleton", show c, mkThm1 SS.singleton (: []) c ) | c <- cs ] ++ [("implode", show s, mkThmI SS.implode s ) | s <- ss ] ++ [("strToNat", show s, mkThm1 SS.strToNat strToNat s ) | s <- ss ] ++ [("natToStr", show i, mkThm1 SS.natToStr natToStr i ) | i <- iUBs ]) @@ -647,6 +656,88 @@ constrain $ c .== literal arg3 return $ literal (cop arg1 arg2 arg3) .== sop a b c +genLists :: [TestTree] +genLists = map mkTest1 ( [("length", show l, mkThm1 SL.length llen l ) | l <- sl ] + ++ [("null", show l, mkThm1 SL.null null l ) | l <- sl ] + ++ [("head", show l, mkThm1 SL.head head l ) | l <- sl, not (null l) ] + ++ [("tail", show l, mkThm1 SL.tail tail l ) | l <- sl, not (null l) ] + ++ [("singleton", show i, mkThm1 SL.singleton (: []) i ) | i <- iUBs ] + ++ [("implode", show l, mkThmI SL.implode id l ) | l <- sl ]) + ++ map mkTest2 ( [("listToListAt", show l, show i, mkThm2 SL.listToListAt listToListAt l i ) | l <- sl, i <- range l ] + ++ [("elemAt", show l, show i, mkThm2 SL.elemAt elemAt l i ) | l <- sl, i <- range l ] + ++ [("concat", show l, show l1, mkThm2 SL.concat (++) l l1 ) | l <- sl, l1 <- sl ] + ++ [("isInfixOf", show l, show l1, mkThm2 SL.isInfixOf isInfixOf l l1 ) | l <- sl, l1 <- sl ] + ++ [("isSuffixOf", show l, show l1, mkThm2 SL.isSuffixOf isSuffixOf l l1 ) | l <- sl, l1 <- sl ] + ++ [("isPrefixOf", show l, show l1, mkThm2 SL.isPrefixOf isPrefixOf l l1 ) | l <- sl, l1 <- sl ] + ++ [("take", show l, show i, mkThm2 SL.take genericTake i l ) | l <- sl, i <- iUBs ] + ++ [("drop", show l, show i, mkThm2 SL.drop genericDrop i l ) | l <- sl, i <- iUBs ] + ++ [("indexOf", show l, show l1, mkThm2 SL.indexOf indexOf l l1 ) | l <- sl, l1 <- sl ]) + ++ map mkTest3 ( [("subList", show l, show i, show j, mkThm3 SL.subList subList l i j ) | l <- sl, i <- range l, j <- range l, i + j <= genericLength l] + ++ [("replace", show l, show l1, show l2, mkThm3 SL.replace replace l l1 l2) | l <- sl, l1 <- sl, l2 <- sl ] + ++ [("offsetIndexOf", show l, show l1, show i, mkThm3 SL.offsetIndexOf offsetIndexOf l l1 i ) | l <- sl, l1 <- sl, i <- range l ]) + where llen :: [Integer] -> Integer + llen = fromIntegral . length + + range :: [Integer] -> [Integer] + range l = map fromIntegral [0 .. length l - 1] + + indexOf :: [Integer] -> [Integer] -> Integer + indexOf s1 s2 = go 0 s1 + where go i x + | s2 `isPrefixOf` x = i + | True = case x of + [] -> -1 + (_:r) -> go (i+1) r + + listToListAt :: [Integer] -> Integer -> [Integer] + s `listToListAt` i = [s `elemAt` i] + + elemAt :: [Integer] -> Integer -> Integer + l `elemAt` i = l `genericIndex` i + + subList :: [Integer] -> Integer -> Integer -> [Integer] + subList s i j = genericTake j (genericDrop i s) + + replace :: [Integer] -> [Integer] -> [Integer] -> [Integer] + replace s [] y = y ++ s + replace s x y = go s + where go [] = [] + go h@(c:rest) | x `isPrefixOf` h = y ++ drop (length x) h + | True = c : go rest + + offsetIndexOf :: [Integer] -> [Integer] -> Integer -> Integer + offsetIndexOf x y i = case indexOf (genericDrop i x) y of + -1 -> -1 + r -> r+i + + mkTest1 (nm, x, t) = testCase ("genLists-" ++ nm ++ "." ++ x) (assert t) + mkTest2 (nm, x, y, t) = testCase ("genLists-" ++ nm ++ "." ++ x ++ "_" ++ y) (assert t) + mkTest3 (nm, x, y, z, t) = testCase ("genLists-" ++ nm ++ "." ++ x ++ "_" ++ y ++ "_" ++ z) (assert t) + + mkThmI sop cop arg = isTheorem $ do let v c = do sc <- free_ + constrain $ sc .== literal c + return sc + vs <- mapM v arg + return $ literal (cop arg) .== sop vs + + mkThm1 sop cop arg = isTheorem $ do a <- free "a" + constrain $ a .== literal arg + return $ literal (cop arg) .== sop a + + mkThm2 sop cop arg1 arg2 = isTheorem $ do a <- free "a" + b <- free "b" + constrain $ a .== literal arg1 + constrain $ b .== literal arg2 + return $ literal (cop arg1 arg2) .== sop a b + + mkThm3 sop cop arg1 arg2 arg3 = isTheorem $ do a <- free "a" + b <- free "b" + c <- free "c" + constrain $ a .== literal arg1 + constrain $ b .== literal arg2 + constrain $ c .== literal arg3 + return $ literal (cop arg1 arg2 arg3) .== sop a b c + -- Concrete test data xsSigned, xsUnsigned :: (Num a, Bounded a) => [a] xsUnsigned = [0, 1, maxBound - 1, maxBound] @@ -705,5 +796,9 @@ -- Ditto for strings, just a few things ss :: [String] ss = ["", "palTRY", "teSTing", "SBV", "sTRIngs", "123", "surely", "thIS", "hI", "ly", "0"] + +-- Lists are the worst in coverage! +sl :: [[Integer]] +sl = [[], [0], [-1, 1], [-10, 0, 10], [3, 4, 5, 4, 5, 3]] {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} diff --git a/SBVTestSuite/TestSuite/Basics/List.hs b/SBVTestSuite/TestSuite/Basics/List.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Basics/List.hs @@ -0,0 +1,141 @@ +----------------------------------------------------------------------------- +-- | +-- Module : TestSuite.Basics.List +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Test the sequence/list functions. +-- Most of these tests are adopted from +----------------------------------------------------------------------------- + +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module TestSuite.Basics.List(tests) where + +import Data.SBV.Control +import Utils.SBVTestFramework + +import Data.SBV.List ((.!!), (.++)) +import qualified Data.SBV.List as L + +import Control.Monad (unless) +import Data.Maybe (catMaybes) +import Data.List (sort) + +-- Test suite +tests :: TestTree +tests = + testGroup "Basics.List" [ + goldenCapturedIO "seqConcat" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqConcatSat Sat + , goldenCapturedIO "seqConcatBad" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqConcatUnsat Unsat + , goldenCapturedIO "seqIndexOf" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqIndexOfSat Sat + , goldenCapturedIO "seqIndexOfBad" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqIndexOfUnsat Unsat + , goldenCapturedIO "seqExamples1" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqExamples1 Sat + , goldenCapturedIO "seqExamples2" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqExamples2 Unsat + , goldenCapturedIO "seqExamples3" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqExamples3 Sat + , goldenCapturedIO "seqExamples4" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqExamples4 Sat + , goldenCapturedIO "seqExamples5" $ \rf -> checkWith z3{redirectVerbose=Just rf} seqExamples5 Sat + , 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 + , testCase "seqExamples9" $ assert seqExamples9 + ] + +checkWith :: SMTConfig -> Symbolic () -> CheckSatResult -> IO () +checkWith cfg props csExpected = runSMTWith cfg{verbose=True} $ do + _ <- props + query $ do cs <- checkSat + unless (cs == csExpected) $ + case cs of + Unsat -> error "Failed! Expected Sat, got UNSAT" + Sat -> getModel >>= \r -> error $ "Failed! Expected Unsat, got SAT:\n" ++ show (SatResult (Satisfiable cfg r)) + Unk -> getUnknownReason >>= \r -> error $ "Failed! Expected Unsat, got UNK:\n" ++ show r + +seqConcatSat :: Symbolic () +seqConcatSat = constrain $ [1..3] .++ [4..6] .== ([1..6] :: SList Integer) + +seqConcatUnsat :: Symbolic () +seqConcatUnsat = constrain $ [1..3] .++ [4..6] .== ([1..7] :: SList Integer) + +seqIndexOfSat :: Symbolic () +seqIndexOfSat = constrain $ L.indexOf ([1,2,3,1,2,3] :: SList Integer) [1] .== 0 + +seqIndexOfUnsat :: Symbolic () +seqIndexOfUnsat = constrain $ L.indexOf ([1,2,3,1,2,3] :: SList Integer) [1] ./= 0 + +-- Basic sequence operations +seqExamples1 :: Symbolic () +seqExamples1 = constrain $ bAnd + [ L.singleton (([1,2,3] :: SList Integer) .!! 1) .++ L.singleton (([1,2,3] :: SList Integer) .!! 0) .== [2,1] + , ([1,2,3,1,2,3] :: SList Integer) `L.indexOf` [1] .== 0 + , L.offsetIndexOf ([1,2,3,1,2,3] :: SList Integer) [1] 1 .== 3 + , L.subList ([4,4,1,2,3,5,5] :: SList Integer) 2 3 .== [1,2,3] + ] + +-- A list cannot overlap with two different elements +seqExamples2 :: Symbolic () +seqExamples2 = do + a :: SList Integer <- sList "a" + constrain $ a .++ [2] .== [1] .++ a + +-- Strings a, b, c can have a non-trivial overlap. +seqExamples3 :: Symbolic () +seqExamples3 = do + [a, b, c :: SList Integer] <- sLists ["a", "b", "c"] + constrain $ a .++ b .== [1..4] + constrain $ b .++ c .== [3..6] + constrain $ bnot $ b .== [] + +-- There is a solution to a of length at most 2. +seqExamples4 :: Symbolic () +seqExamples4 = do + [a, b :: SList Integer] <- sLists ["a", "b"] + constrain $ [1..3] .++ a .== b .++ [3..5] + constrain $ L.length a .<= 2 + +-- There is a solution to a that is not a sequence of 1's. +seqExamples5 :: Symbolic () +seqExamples5 = do + [a, b, c :: SList Integer] <- sLists ["a", "b", "c"] + constrain $ a .++ [1,2] .++ b .== b .++ [2,1] .++ c + constrain $ c .== a .++ b + constrain $ bnot $ a.++ [1] .== [1] .++ a + +-- Contains is transitive. +seqExamples6 :: Symbolic () +seqExamples6 = do + [a, b, c :: SList Integer] <- sLists ["a", "b", "c"] + constrain $ b `L.isInfixOf` a + constrain $ c `L.isInfixOf` b + constrain $ bnot $ c `L.isInfixOf` a + +-- But containment is not a linear order. +seqExamples7 :: Symbolic () +seqExamples7 = do + [a, b, c :: SList Integer] <- sLists ["a", "b", "c"] + constrain $ b `L.isInfixOf` a + constrain $ c `L.isInfixOf` a + constrain $ bnot $ c `L.isInfixOf` b + constrain $ bnot $ b `L.isInfixOf` c + +-- Any string is equal to the prefix and suffix that add up to a its length. +seqExamples8 :: Symbolic () +seqExamples8 = do + [a, b, c :: SList Integer] <- sLists ["a", "b", "c"] + constrain $ b `L.isPrefixOf` a + constrain $ c `L.isSuffixOf` a + constrain $ L.length a .== L.length b + L.length c + constrain $ bnot $ a .== b .++ c + +-- Generate all length one sequences, to enumerate all and making sure we can parse correctly +seqExamples9 :: IO Bool +seqExamples9 = do m <- allSat $ do (s :: SList Word8) <- sList "s" + return $ L.length s .== 1 + + let vals :: [Word8] + vals = sort $ concat (catMaybes (getModelValues "s" m) :: [[Word8]]) + + return $ vals == [0..255] diff --git a/SBVTestSuite/TestSuite/Basics/String.hs b/SBVTestSuite/TestSuite/Basics/String.hs --- a/SBVTestSuite/TestSuite/Basics/String.hs +++ b/SBVTestSuite/TestSuite/Basics/String.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE OverloadedStrings #-} ----------------------------------------------------------------------------- -- | -- Module : TestSuite.Basics.String @@ -11,11 +10,14 @@ -- Most of these tests are adopted from ----------------------------------------------------------------------------- +{-# LANGUAGE OverloadedStrings #-} + module TestSuite.Basics.String(tests) where import Data.SBV.Control import Utils.SBVTestFramework +import Data.SBV.String ((.!!), (.++)) import qualified Data.SBV.String as S import qualified Data.SBV.RegExp as R @@ -75,7 +77,7 @@ -- Basic string operations strExamples1 :: Symbolic () strExamples1 = constrain $ bAnd - [ S.charToStr ("abc" .!! 1) .++ S.charToStr ("abc" .!! 0) .== "ba" + [ S.singleton ("abc" .!! 1) .++ S.singleton ("abc" .!! 0) .== "ba" , "abcabc" `S.indexOf` "a" .== 0 , S.offsetIndexOf "abcabc" "a" 1 .== 3 , S.subStr "xxabcyy" 2 3 .== "abc" diff --git a/SBVTestSuite/TestSuite/Queries/BadOption.hs b/SBVTestSuite/TestSuite/Queries/BadOption.hs --- a/SBVTestSuite/TestSuite/Queries/BadOption.hs +++ b/SBVTestSuite/TestSuite/Queries/BadOption.hs @@ -8,6 +8,7 @@ -- -- Testing that a bad option setting is caught properly. ----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Queries.BadOption (tests) where diff --git a/SBVTestSuite/TestSuite/Queries/FreshVars.hs b/SBVTestSuite/TestSuite/Queries/FreshVars.hs --- a/SBVTestSuite/TestSuite/Queries/FreshVars.hs +++ b/SBVTestSuite/TestSuite/Queries/FreshVars.hs @@ -14,6 +14,8 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE OverloadedLists #-} module TestSuite.Queries.FreshVars (tests) where @@ -42,21 +44,24 @@ constrain $ a .== 0 - query $ do vBool :: SBool <- freshVar "vBool" - vWord8 :: SWord8 <- freshVar "vWord8" - vWord16 :: SWord16 <- freshVar_ - vWord32 :: SWord32 <- freshVar_ - vWord64 :: SWord64 <- freshVar "vWord64" - vInt8 :: SInt8 <- freshVar "vInt8" - vInt16 :: SInt16 <- freshVar_ - vInt32 :: SInt32 <- freshVar_ - vInt64 :: SInt64 <- freshVar "vInt64" - vFloat :: SFloat <- freshVar "vFloat" - vDouble :: SDouble <- freshVar_ - vReal :: SReal <- freshVar_ - vInteger :: SInteger <- freshVar "vInteger" - vBinOp :: SBinOp <- freshVar "vBinOp" + setOption $ OptionKeyword ":pp.max_depth" ["4294967295"] + setOption $ OptionKeyword ":pp.min_alias_size" ["4294967295"] + query $ do vBool :: SBool <- freshVar "vBool" + vWord8 :: SWord8 <- freshVar "vWord8" + vWord16 :: SWord16 <- freshVar_ + vWord32 :: SWord32 <- freshVar_ + vWord64 :: SWord64 <- freshVar "vWord64" + vInt8 :: SInt8 <- freshVar "vInt8" + vInt16 :: SInt16 <- freshVar_ + vInt32 :: SInt32 <- freshVar_ + vInt64 :: SInt64 <- freshVar "vInt64" + vFloat :: SFloat <- freshVar "vFloat" + vDouble :: SDouble <- freshVar_ + vReal :: SReal <- freshVar_ + vInteger :: SInteger <- freshVar "vInteger" + vBinOp :: SBinOp <- freshVar "vBinOp" + constrain vBool constrain $ vWord8 .== 1 constrain $ vWord16 .== 2 @@ -86,7 +91,21 @@ constrain $ readArray viSArray 96 .== mustBe42 constrain $ readArray viFArray false .== mustBeX + constrain $ vi1 .== 1 + constrain $ bnot vi2 + vString :: SString <- freshVar "vString" + vList1 :: SList Integer <- freshVar "vList1" + vList2 :: SList [Integer] <- freshVar "vList2" + vList3 :: SList Word8 <- freshVar "vList3" + vList4 :: SList [Word16] <- freshVar "vList4" + + constrain $ vString .== "hello" + constrain $ vList1 .== [1,2,3,4] + constrain $ vList2 .== [[1,2,3], [4,5,6,7]] + constrain $ vList3 .== [1,2] + constrain $ vList4 .== [[1,2,3],[],[4,5,6]] + cs <- checkSat case cs of Sat -> do aVal <- getValue a @@ -108,6 +127,11 @@ vi2Val <- getValue vi2 mustBe42Val <- getValue mustBe42 mustBeXVal <- getValue mustBeX + vStringVal <- getValue vString + vList1Val <- getValue vList1 + vList2Val <- getValue vList2 + vList3Val <- getValue vList3 + vList4Val <- getValue vList4 mkSMTResult [ a |-> aVal , vBool |-> vBoolVal @@ -128,5 +152,10 @@ , vi2 |-> vi2Val , mustBe42 |-> mustBe42Val , mustBeX |-> mustBeXVal + , vString |-> vStringVal + , vList1 |-> vList1Val + , vList2 |-> vList2Val + , vList3 |-> vList3Val + , vList4 |-> vList4Val ] _ -> error "didn't expect non-Sat here!" diff --git a/SBVTestSuite/TestSuite/Queries/Int_ABC.hs b/SBVTestSuite/TestSuite/Queries/Int_ABC.hs --- a/SBVTestSuite/TestSuite/Queries/Int_ABC.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_ABC.hs @@ -8,6 +8,7 @@ -- -- Testing ABC specific interactive features. ----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Queries.Int_ABC (tests) where diff --git a/SBVTestSuite/TestSuite/Queries/Int_Boolector.hs b/SBVTestSuite/TestSuite/Queries/Int_Boolector.hs --- a/SBVTestSuite/TestSuite/Queries/Int_Boolector.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_Boolector.hs @@ -8,6 +8,7 @@ -- -- Testing Boolector specific interactive features. ----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Queries.Int_Boolector (tests) where diff --git a/SBVTestSuite/TestSuite/Queries/Int_CVC4.hs b/SBVTestSuite/TestSuite/Queries/Int_CVC4.hs --- a/SBVTestSuite/TestSuite/Queries/Int_CVC4.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_CVC4.hs @@ -8,6 +8,7 @@ -- -- Testing CVC4 specific interactive features ----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Queries.Int_CVC4 (tests) where diff --git a/SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs b/SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs --- a/SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs @@ -8,6 +8,7 @@ -- -- Testing MathSAT specific interactive features. ----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Queries.Int_Mathsat (tests) where diff --git a/SBVTestSuite/TestSuite/Queries/Int_Yices.hs b/SBVTestSuite/TestSuite/Queries/Int_Yices.hs --- a/SBVTestSuite/TestSuite/Queries/Int_Yices.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_Yices.hs @@ -8,6 +8,7 @@ -- -- Testing Yices specific interactive features. ----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Queries.Int_Yices (tests) where diff --git a/SBVTestSuite/TestSuite/Queries/Int_Z3.hs b/SBVTestSuite/TestSuite/Queries/Int_Z3.hs --- a/SBVTestSuite/TestSuite/Queries/Int_Z3.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_Z3.hs @@ -8,6 +8,7 @@ -- -- Testing Z3 specific interactive features. ----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Queries.Int_Z3 (tests) where diff --git a/SBVTestSuite/TestSuite/Queries/Interpolants.hs b/SBVTestSuite/TestSuite/Queries/Interpolants.hs --- a/SBVTestSuite/TestSuite/Queries/Interpolants.hs +++ b/SBVTestSuite/TestSuite/Queries/Interpolants.hs @@ -9,6 +9,7 @@ -- Testing a few interpolant computations. -- ----------------------------------------------------------------------------- + {-# LANGUAGE ScopedTypeVariables #-} module TestSuite.Queries.Interpolants (tests) where diff --git a/SBVTestSuite/TestSuite/Queries/Lists.hs b/SBVTestSuite/TestSuite/Queries/Lists.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Queries/Lists.hs @@ -0,0 +1,44 @@ +----------------------------------------------------------------------------- +-- | +-- Module : TestSuite.Queries.Lists +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Testing a few lists +----------------------------------------------------------------------------- + +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module TestSuite.Queries.Lists (tests) where + +import Data.SBV +import Data.SBV.Control + +import Utils.SBVTestFramework + +-- Test suite +tests :: TestTree +tests = + testGroup "Basics.QueryLists" + [ goldenCapturedIO "query_Lists1" $ testQuery queryLists1 + ] + +testQuery :: Show a => Symbolic a -> FilePath -> IO () +testQuery t rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t + appendFile rf ("\nFINAL OUTPUT:\n" ++ show r ++ "\n") + +queryLists1 :: Symbolic [Integer] +queryLists1 = do a :: SList Integer <- sList "a" + + constrain $ a .== [1..5] + + query $ do _ <- checkSat + + av <- getValue a + + if av == [1..5] + then return av + else error $ "Didn't expect this: " ++ show av diff --git a/SBVTestSuite/TestSuite/Queries/Strings.hs b/SBVTestSuite/TestSuite/Queries/Strings.hs --- a/SBVTestSuite/TestSuite/Queries/Strings.hs +++ b/SBVTestSuite/TestSuite/Queries/Strings.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE OverloadedStrings #-} ----------------------------------------------------------------------------- -- | -- Module : TestSuite.Queries.Strings @@ -9,6 +8,8 @@ -- -- Testing a few strings ----------------------------------------------------------------------------- + +{-# LANGUAGE OverloadedStrings #-} module TestSuite.Queries.Strings (tests) where diff --git a/SBVTestSuite/TestSuite/Uninterpreted/Sort.hs b/SBVTestSuite/TestSuite/Uninterpreted/Sort.hs --- a/SBVTestSuite/TestSuite/Uninterpreted/Sort.hs +++ b/SBVTestSuite/TestSuite/Uninterpreted/Sort.hs @@ -30,9 +30,9 @@ instance SatModel L where parseCWs = undefined -- make GHC shut up about the missing method, we won't actually call it -type SList = SBV L +type UList = SBV L -len :: SList -> SInteger +len :: UList -> SInteger len = uninterpret "len" p0 :: Symbolic SBool diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 7.10 +Version: 7.11 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 @@ -48,14 +48,17 @@ TypeOperators TypeSynonymInstances Build-Depends : base >= 4.9 && < 5 - , ghc, QuickCheck, crackNum, template-haskell + , crackNum >= 2.2 + , ghc, QuickCheck, template-haskell , array, async, containers, deepseq, directory, filepath, time - , pretty, process, mtl, random, syb, data-binary-ieee754 + , pretty, process, mtl, random, syb, reinterpret-cast , generic-deriving Exposed-modules : Data.SBV , Data.SBV.Control , Data.SBV.Dynamic , Data.SBV.Internals + , Data.SBV.List + , Data.SBV.List.Bounded , Data.SBV.String , Data.SBV.Char , Data.SBV.RegExp @@ -80,6 +83,9 @@ , Documentation.SBV.Examples.Crypto.RC4 , Documentation.SBV.Examples.Existentials.CRCPolynomial , Documentation.SBV.Examples.Existentials.Diophantine + , Documentation.SBV.Examples.Lists.Fibonacci + , Documentation.SBV.Examples.Lists.Nested + , Documentation.SBV.Examples.Lists.BoundedMutex , Documentation.SBV.Examples.Misc.Enumerate , Documentation.SBV.Examples.Misc.Floating , Documentation.SBV.Examples.Misc.ModelExtract @@ -160,7 +166,7 @@ , DeriveDataTypeable , Rank2Types , ScopedTypeVariables - Build-depends : base >= 4.9, data-binary-ieee754, filepath, syb + Build-depends : base >= 4.9, reinterpret-cast, filepath, syb , sbv, directory, random, mtl, containers , template-haskell, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, QuickCheck Hs-Source-Dirs : SBVTestSuite @@ -187,6 +193,7 @@ , TestSuite.Basics.SmallShifts , TestSuite.Basics.SquashReals , TestSuite.Basics.String + , TestSuite.Basics.List , TestSuite.Basics.TOut , TestSuite.BitPrecise.BitTricks , TestSuite.BitPrecise.Legato @@ -240,6 +247,7 @@ , TestSuite.Queries.Int_Yices , TestSuite.Queries.Int_Z3 , TestSuite.Queries.Interpolants + , TestSuite.Queries.Lists , TestSuite.Queries.Strings , TestSuite.Queries.Uninterpreted , TestSuite.QuickCheck.QC