packages feed

sbv 7.10 → 7.11

raw patch · 67 files changed

+2233/−381 lines, 67 filesdep +reinterpret-castdep −data-binary-ieee754dep ~crackNum

Dependencies added: reinterpret-cast

Dependencies removed: data-binary-ieee754

Dependency ranges changed: crackNum

Files

CHANGES.md view
@@ -1,7 +1,27 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* 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
Data/SBV.hs view
@@ -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: <http://rise4fun.com/z3/tutorialcontent/sequences>. 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
Data/SBV/Char.hs view
@@ -1,7 +1,3 @@-{-# LANGUAGE Rank2Types          #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE OverloadedStrings   #-}- ----------------------------------------------------------------------------- -- | -- Module      :  Data.SBV.Char@@ -24,6 +20,10 @@ -- For details, see: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml> ----------------------------------------------------------------------------- +{-# 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? --
Data/SBV/Compilers/C.hs view
@@ -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.
Data/SBV/Control/Utils.hs view
@@ -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: <http://github.com/Z3Prover/z3/issues/1808>+        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.
Data/SBV/Core/Concrete.hs view
@@ -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)
Data/SBV/Core/Data.hs view
@@ -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
Data/SBV/Core/Floating.hs view
@@ -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])
Data/SBV/Core/Kind.hs view
@@ -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
Data/SBV/Core/Model.hs view
@@ -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
Data/SBV/Core/Operations.hs view
@@ -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
Data/SBV/Core/Symbolic.hs view
@@ -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.
+ Data/SBV/List.hs view
@@ -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 <http://github.com/Z3Prover/z3/issues/1302>+        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
+ Data/SBV/List/Bounded.hs view
@@ -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))
Data/SBV/Provers/ABC.hs view
@@ -36,5 +36,6 @@                               , supportsPseudoBooleans     = False                               , supportsCustomQueries      = False                               , supportsGlobalDecls        = False+                              , supportsFlattenedSequences = Nothing                               }          }
Data/SBV/Provers/Boolector.hs view
@@ -34,5 +34,6 @@                               , supportsPseudoBooleans     = False                               , supportsCustomQueries      = True                               , supportsGlobalDecls        = False+                              , supportsFlattenedSequences = Nothing                               }          }
Data/SBV/Provers/CVC4.hs view
@@ -36,5 +36,6 @@                               , supportsPseudoBooleans     = False                               , supportsCustomQueries      = True                               , supportsGlobalDecls        = True+                              , supportsFlattenedSequences = Nothing                               }          }
Data/SBV/Provers/MathSAT.hs view
@@ -38,6 +38,7 @@                               , supportsPseudoBooleans     = False                               , supportsCustomQueries      = True                               , supportsGlobalDecls        = False+                              , supportsFlattenedSequences = Nothing                               }          }
Data/SBV/Provers/Yices.hs view
@@ -36,5 +36,6 @@                               , supportsPseudoBooleans     = False                               , supportsCustomQueries      = True                               , supportsGlobalDecls        = False+                              , supportsFlattenedSequences = Nothing                               }          }
Data/SBV/Provers/Z3.hs view
@@ -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)"+                                                                  ]                               }          }
Data/SBV/RegExp.hs view
@@ -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
Data/SBV/SMT/SMT.hs view
@@ -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)
Data/SBV/SMT/SMTLib2.hs view
@@ -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: <http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml>)
Data/SBV/String.hs view
@@ -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
Data/SBV/Tools/GenTest.hs view
@@ -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 []  = "()"
Data/SBV/Utils/Lib.hs view
@@ -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
Data/SBV/Utils/PrettyNum.hs view
@@ -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)
Data/SBV/Utils/SExpr.hs view
@@ -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(..))
+ Documentation/SBV/Examples/Lists/BoundedMutex.hs view
@@ -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
+ Documentation/SBV/Examples/Lists/Fibonacci.hs view
@@ -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
+ Documentation/SBV/Examples/Lists/Nested.hs view
@@ -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
Documentation/SBV/Examples/Strings/RegexCrossword.hs view
@@ -8,6 +8,7 @@ -- -- This example solves regex crosswords from <http://regexcrossword.com> -----------------------------------------------------------------------------+ {-# 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
Documentation/SBV/Examples/Strings/SQLInjection.hs view
@@ -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: <http://github.com/LeventErkok/sbv/issues/418>.) ----- >>> findInjection exampleProgram--- "h'; DROP TABLE 'users"+-- @+--   findInjection exampleProgram+--   "h'; DROP TABLE 'users"+-- @ -- -- Indeed, if we substitute the suggested string, we get the program: --
README.md view
@@ -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
SBVTestSuite/GoldFiles/freshVars.gold view
@@ -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!
+ SBVTestSuite/GoldFiles/query_Lists1.gold view
@@ -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]
SBVTestSuite/GoldFiles/query_badOption.gold view
@@ -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)
+ SBVTestSuite/GoldFiles/seqConcat.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqConcatBad.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqExamples1.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqExamples2.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqExamples3.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqExamples4.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqExamples5.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqExamples6.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqExamples7.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqExamples8.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqIndexOf.gold view
@@ -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
+ SBVTestSuite/GoldFiles/seqIndexOfBad.gold view
@@ -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
SBVTestSuite/SBVTest.hs view
@@ -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
SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs view
@@ -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) #-}
SBVTestSuite/TestSuite/Basics/ArithSolver.hs view
@@ -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) #-}
+ SBVTestSuite/TestSuite/Basics/List.hs view
@@ -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 <http://rise4fun.com/z3/tutorialcontent/sequences>+-----------------------------------------------------------------------------++{-# 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]
SBVTestSuite/TestSuite/Basics/String.hs view
@@ -1,4 +1,3 @@-{-# LANGUAGE OverloadedStrings #-} ----------------------------------------------------------------------------- -- | -- Module      :  TestSuite.Basics.String@@ -11,11 +10,14 @@ -- Most of these tests are adopted from <http://rise4fun.com/z3/tutorialcontent/sequences> ----------------------------------------------------------------------------- +{-# 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"
SBVTestSuite/TestSuite/Queries/BadOption.hs view
@@ -8,6 +8,7 @@ -- -- Testing that a bad option setting is caught properly. -----------------------------------------------------------------------------+ {-# LANGUAGE ScopedTypeVariables #-}  module TestSuite.Queries.BadOption (tests)  where
SBVTestSuite/TestSuite/Queries/FreshVars.hs view
@@ -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!"
SBVTestSuite/TestSuite/Queries/Int_ABC.hs view
@@ -8,6 +8,7 @@ -- -- Testing ABC specific interactive features. -----------------------------------------------------------------------------+ {-# LANGUAGE ScopedTypeVariables #-}  module TestSuite.Queries.Int_ABC (tests)  where
SBVTestSuite/TestSuite/Queries/Int_Boolector.hs view
@@ -8,6 +8,7 @@ -- -- Testing Boolector specific interactive features. -----------------------------------------------------------------------------+ {-# LANGUAGE ScopedTypeVariables #-}  module TestSuite.Queries.Int_Boolector (tests)  where
SBVTestSuite/TestSuite/Queries/Int_CVC4.hs view
@@ -8,6 +8,7 @@ -- -- Testing CVC4 specific interactive features -----------------------------------------------------------------------------+ {-# LANGUAGE ScopedTypeVariables #-}  module TestSuite.Queries.Int_CVC4 (tests)  where
SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs view
@@ -8,6 +8,7 @@ -- -- Testing MathSAT specific interactive features. -----------------------------------------------------------------------------+ {-# LANGUAGE ScopedTypeVariables #-}  module TestSuite.Queries.Int_Mathsat (tests)  where
SBVTestSuite/TestSuite/Queries/Int_Yices.hs view
@@ -8,6 +8,7 @@ -- -- Testing Yices specific interactive features. -----------------------------------------------------------------------------+ {-# LANGUAGE ScopedTypeVariables #-}  module TestSuite.Queries.Int_Yices (tests)  where
SBVTestSuite/TestSuite/Queries/Int_Z3.hs view
@@ -8,6 +8,7 @@ -- -- Testing Z3 specific interactive features. -----------------------------------------------------------------------------+ {-# LANGUAGE ScopedTypeVariables #-}  module TestSuite.Queries.Int_Z3 (tests)  where
SBVTestSuite/TestSuite/Queries/Interpolants.hs view
@@ -9,6 +9,7 @@ -- Testing a few interpolant computations. -- -----------------------------------------------------------------------------+ {-# LANGUAGE ScopedTypeVariables #-}  module TestSuite.Queries.Interpolants (tests)  where
+ SBVTestSuite/TestSuite/Queries/Lists.hs view
@@ -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
SBVTestSuite/TestSuite/Queries/Strings.hs view
@@ -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
SBVTestSuite/TestSuite/Uninterpreted/Sort.hs view
@@ -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
sbv.cabal view
@@ -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