packages feed

sbv 8.9 → 8.10

raw patch · 100 files changed

+1982/−862 lines, 100 filesdep +text

Dependencies added: text

Files

CHANGES.md view
@@ -1,7 +1,28 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 8.9, 2020-10-28+* Latest Hackage released version: 8.9, 2021-02-13++### Version 8.10, 2021-02-13++  * Add "Documentation/SBV/Examples/Misc/NestedArray.hs" to demonstrate how+    to model multi-dimensional arrays in SBV.++  * Add "Documentation/SBV/Examples/Puzzles/Murder.hs" as another puzzle example.++  * Performance updates: Thanks to Jeff Young, SBV now uses better underlying+    data structures, performing better for heavy use-case scenarios.++  * SBV now tracks constants more closely in query mode, providing more support+    for constant arrays in a seamless way. (See #574 for details.)++  * Pop-calls are now support for Yices and Boolector. (#577)++  * Changes required to make SBV work with latest version of z3 regarding+    String and Characters, which now allow for unicode characters. This required+    renaming of certain recognizers in 'Data.SBV.Char' to restrict them to the+    Latin1 subset. Otherwise, the changes should be transparent to the end user.+    Please report any issues you might run into when you use SChar and SString types.  ### Version 8.9, 2020-10-28 
@@ -1,4 +1,4 @@-Copyright (c) 2010-2020, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2021, Levent Erkok (erkokl@gmail.com) All rights reserved.  The sbv library is distributed with the BSD3 license. See the LICENSE file
Data/SBV/Char.hs view
@@ -32,13 +32,14 @@         -- * Conversion to\/from 'SInteger'         , ord, chr         -- * Conversion to upper\/lower case-        , toLower, toUpper+        , toLowerL1, toUpperL1         -- * Converting digits to ints and back         , digitToInt, intToDigit         -- * Character classification-        , isControl, isSpace, isLower, isUpper, isAlpha, isAlphaNum, isPrint, isDigit, isOctDigit, isHexDigit, isLetter, isMark, isNumber, isPunctuation, isSymbol, isSeparator+        , isControlL1, isSpaceL1, isLowerL1, isUpperL1, isAlphaL1, isAlphaNumL1, isPrintL1, isDigit, isOctDigit, isHexDigit+        , isLetterL1, isMarkL1, isNumberL1, isPunctuationL1, isSymbolL1, isSeparatorL1         -- * Subranges-        , isAscii, isLatin1, isAsciiLetter, isAsciiUpper, isAsciiLower+        , isAscii, isLatin1, isAsciiUpper, isAsciiLower         ) where  import Prelude hiding (elem, notElem)@@ -86,11 +87,9 @@  | Just cc <- unliteral c  = literal (fromIntegral (C.ord cc))  | True- = SBV $ SVal kTo $ Right $ cache r- where kFrom = KBounded False 8-       kTo   = KUnbounded-       r st = do csv <- sbvToSV st c-                 newExpr st kTo (SBVApp (KindCast kFrom kTo) [csv])+ = SBV $ SVal KUnbounded $ Right $ cache r+ where r st = do csv <- sbvToSV st c+                 newExpr st KUnbounded (SBVApp (StrOp StrToCode) [csv])  -- | Conversion from an integer to a character. --@@ -104,38 +103,40 @@  = literal (C.chr (fromIntegral cw))  | True  = SBV $ SVal KChar $ Right $ cache r- where w8 :: SWord8-       w8 = sFromIntegral w-       r st = do SV _ n <- sbvToSV st w8-                 return $ SV KChar n+ where r st = do wsv <- sbvToSV st w+                 newExpr st KChar (SBVApp (StrOp StrFromCode) [wsv]) --- | Convert to lower-case.+-- | Lift a char function to a symbolic version. If the given char is+-- not in the class recognized by predicate, the output is the same as the input.+-- Only works for the Latin1 set, i.e., the first 256 characters.+liftFunL1 :: (Char -> Char) -> SChar -> SChar+liftFunL1 f c = walk kernel+  where kernel = [g | g <- map C.chr [0 .. 255], g /= f g]+        walk []     = c+        walk (d:ds) = ite (literal d .== c) (literal (f d)) (walk ds)++-- | Lift a char predicate to a symbolic version. Only works for the Latin1 set, i.e., the+-- first 256 characters.+liftPredL1 :: (Char -> Bool) -> SChar -> SBool+liftPredL1 predicate c = c `sElem` [literal g | g <- map C.chr [0 .. 255], predicate g]++-- | Convert to lower-case. Only works for the Latin1 subset, otherwise returns its argument unchanged. ----- >>> prove $ \c -> toLower (toLower c) .== toLower c+-- >>> prove $ \c -> toLowerL1 (toLowerL1 c) .== toLowerL1 c -- Q.E.D.--- >>> prove $ \c -> isLower c .=> toLower (toUpper c) .== c+-- >>> prove $ \c -> isLowerL1 c .&& c `notElem` "\181\255" .=> toLowerL1 (toUpperL1 c) .== c -- Q.E.D.-toLower :: SChar -> SChar-toLower c = ite (isUpper c) (chr (ord c + 32)) c+toLowerL1 :: SChar -> SChar+toLowerL1 = liftFunL1 C.toLower --- | Convert to upper-case. N.B. There are three special cases!------   * The character \223 is special. It corresponds to the German Eszett, it is considered lower-case,---     and furthermore it's upper-case maps back to itself within our character-set. So, we leave it---     untouched.------   * The character \181 maps to upper-case \924, which is beyond our character set. We leave it---     untouched. (This is the A with an acute accent.)------   * The character \255 maps to upper-case \376, which is beyond our character set. We leave it---     untouched. (This is the non-breaking space character.)+-- | Convert to upper-case. Only works for the Latin1 subset, otherwise returns its argument unchanged. ----- >>> prove $ \c -> toUpper (toUpper c) .== toUpper c+-- >>> prove $ \c -> toUpperL1 (toUpperL1 c) .== toUpperL1 c -- Q.E.D.--- >>> prove $ \c -> isUpper c .=> toUpper (toLower c) .== c+-- >>> prove $ \c -> isUpperL1 c .=> toUpperL1 (toLowerL1 c) .== c -- Q.E.D.-toUpper :: SChar -> SChar-toUpper c = ite (isLower c .&& c `notElem` "\181\223\255") (chr (ord c - 32)) c+toUpperL1 :: SChar -> SChar+toUpperL1 = liftFunL1 C.toUpper  -- | Convert a digit to an integer. Works for hexadecimal digits too. If the input isn't a digit, -- then return -1.@@ -148,7 +149,7 @@ digitToInt c = ite (uc `elem` "0123456789") (sFromIntegral (o - ord (literal '0')))              $ ite (uc `elem` "ABCDEF")     (sFromIntegral (o - ord (literal 'A') + 10))              $ -1-  where uc = toUpper c+  where uc = toUpperL1 c         o  = ord uc  -- | Convert an integer to a digit, inverse of 'digitToInt'. If the integer is out of@@ -166,141 +167,119 @@              $ ite (i .>= 10 .&& i .<= 15) (chr (sFromIntegral i + ord (literal 'a') - 10))              $ literal ' ' --- | Is this a control character? Control characters are essentially the non-printing characters.-isControl :: SChar -> SBool-isControl = (`elem` controls)-  where controls = "\NUL\SOH\STX\ETX\EOT\ENQ\ACK\a\b\t\n\v\f\r\SO\SI\DLE\DC1\DC2\DC3\DC4\NAK\SYN\ETB\CAN\EM\SUB\ESC\FS\GS\RS\US\DEL\128\129\130\131\132\133\134\135\136\137\138\139\140\141\142\143\144\145\146\147\148\149\150\151\152\153\154\155\156\157\158\159"+-- | Is this a control character? Control characters are essentially the non-printing characters. Only works for the Latin1 subset, otherwise returns 'sFalse'.+isControlL1 :: SChar -> SBool+isControlL1 = liftPredL1 C.isControl --- | Is this white-space? That is, one of "\t\n\v\f\r \160".-isSpace :: SChar -> SBool-isSpace = (`elem` spaces)-  where spaces = "\t\n\v\f\r \160"+-- | Is this white-space? Only works for the Latin1 subset, otherwise returns 'sFalse'.+isSpaceL1 :: SChar -> SBool+isSpaceL1 = liftPredL1 C.isSpace --- | Is this a lower-case character?+-- | Is this a lower-case character? Only works for the Latin1 subset, otherwise returns 'sFalse'. ----- >>> prove $ \c -> isUpper c .=> isLower (toLower c)+-- >>> prove $ \c -> isUpperL1 c .=> isLowerL1 (toLowerL1 c) -- Q.E.D.-isLower :: SChar -> SBool-isLower = (`elem` lower)-  where lower = "abcdefghijklmnopqrstuvwxyz\181\223\224\225\226\227\228\229\230\231\232\233\234\235\236\237\238\239\240\241\242\243\244\245\246\248\249\250\251\252\253\254\255"+isLowerL1 :: SChar -> SBool+isLowerL1 = liftPredL1 C.isLower --- | Is this an upper-case character?+-- | Is this an upper-case character? Only works for the Latin1 subset, otherwise returns 'sFalse'. ----- >>> prove $ \c -> sNot (isLower c .&& isUpper c)+-- >>> prove $ \c -> sNot (isLowerL1 c .&& isUpperL1 c) -- Q.E.D.-isUpper :: SChar -> SBool-isUpper = (`elem` upper)-  where upper = "ABCDEFGHIJKLMNOPQRSTUVWXYZ\192\193\194\195\196\197\198\199\200\201\202\203\204\205\206\207\208\209\210\211\212\213\214\216\217\218\219\220\221\222"+isUpperL1 :: SChar -> SBool+isUpperL1 = liftPredL1 C.isUpper  -- | Is this an alphabet character? That is lower-case, upper-case and title-case letters, plus letters of caseless scripts and modifiers letters.-isAlpha :: SChar -> SBool-isAlpha = (`elem` alpha)-  where alpha = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz\170\181\186\192\193\194\195\196\197\198\199\200\201\202\203\204\205\206\207\208\209\210\211\212\213\214\216\217\218\219\220\221\222\223\224\225\226\227\228\229\230\231\232\233\234\235\236\237\238\239\240\241\242\243\244\245\246\248\249\250\251\252\253\254\255"+-- Only works for the Latin1 subset, otherwise returns 'sFalse'.+isAlphaL1 :: SChar -> SBool+isAlphaL1 = liftPredL1 C.isAlpha --- | Is this an 'isAlpha' or 'isNumber'.+-- | Is this an alphabetical character or a digit? Only works for the Latin1 subset, otherwise returns 'sFalse'. ----- >>> prove $ \c -> isAlphaNum c .<=> isAlpha c .|| isNumber c+-- >>> prove $ \c -> isAlphaNumL1 c .<=> isAlphaL1 c .|| isNumberL1 c -- Q.E.D.-isAlphaNum :: SChar -> SBool-isAlphaNum c = isAlpha c .|| isNumber c+isAlphaNumL1 :: SChar -> SBool+isAlphaNumL1 = liftPredL1 C.isAlphaNum --- | Is this a printable character? Essentially the complement of 'isControl', with one--- exception. The Latin-1 character \173 is neither control nor printable. Go figure.------ >>> prove $ \c -> c .== literal '\173' .|| isControl c .<=> sNot (isPrint c)--- Q.E.D.-isPrint :: SChar -> SBool-isPrint c = c ./= literal '\173' .&& sNot (isControl c)+-- | Is this a printable character? Only works for the Latin1 subset, otherwise returns 'sFalse'.+isPrintL1 :: SChar -> SBool+isPrintL1 = liftPredL1 C.isPrint --- | Is this an ASCII digit, i.e., one of @0@..@9@. Note that this is a subset of 'isNumber'+-- | Is this an ASCII digit, i.e., one of @0@..@9@. Note that this is a subset of 'isNumberL1'  ----- >>> prove $ \c -> isDigit c .=> isNumber c+-- >>> prove $ \c -> isDigit c .=> isNumberL1 c -- Q.E.D. isDigit :: SChar -> SBool-isDigit = (`elem` "0123456789")+isDigit = liftPredL1 C.isDigit  -- | Is this an Octal digit, i.e., one of @0@..@7@.------ >>> prove $ \c -> isOctDigit c .=> isDigit c--- Q.E.D. isOctDigit :: SChar -> SBool-isOctDigit = (`elem` "01234567")+isOctDigit = liftPredL1 C.isOctDigit  -- | Is this a Hex digit, i.e, one of @0@..@9@, @a@..@f@, @A@..@F@. ----- >>> prove $ \c -> isHexDigit c .=> isAlphaNum c+-- >>> prove $ \c -> isHexDigit c .=> isAlphaNumL1 c -- Q.E.D. isHexDigit :: SChar -> SBool-isHexDigit = (`elem` "0123456789abcdefABCDEF")+isHexDigit = liftPredL1 C.isHexDigit --- | Is this an alphabet character. Note that this function is equivalent to 'isAlpha'.+-- | Is this an alphabet character. Only works for the Latin1 subset, otherwise returns 'sFalse'. ----- >>> prove $ \c -> isLetter c .<=> isAlpha c+-- >>> prove $ \c -> isLetterL1 c .<=> isAlphaL1 c -- Q.E.D.-isLetter :: SChar -> SBool-isLetter = isAlpha+isLetterL1 :: SChar -> SBool+isLetterL1 = liftPredL1 C.isLetter --- | Is this a mark? Note that the Latin-1 subset doesn't have any marks; so this function--- is simply constant false for the time being.+-- | Is this a mark? Only works for the Latin1 subset, otherwise returns 'sFalse'. ----- >>> prove $ sNot . isMark+-- Note that there are no marks in the Latin1 set, so this function always returns false!+--+-- >>> prove $ sNot . isMarkL1 -- Q.E.D.-isMark :: SChar -> SBool-isMark = const sFalse+isMarkL1 :: SChar -> SBool+isMarkL1 = liftPredL1 C.isMark --- | Is this a number character? Note that this set contains not only the digits, but also--- the codes for a few numeric looking characters like 1/2 etc. Use 'isDigit' for the digits @0@ through @9@.-isNumber :: SChar -> SBool-isNumber = (`elem` "0123456789\178\179\185\188\189\190")+-- | Is this a number character? Only works for the Latin1 subset, otherwise returns 'sFalse'.+isNumberL1 :: SChar -> SBool+isNumberL1 = liftPredL1 C.isNumber --- | Is this a punctuation mark?-isPunctuation :: SChar -> SBool-isPunctuation = (`elem` "!\"#%&'()*,-./:;?@[\\]_{}\161\167\171\182\183\187\191")+-- | Is this a punctuation mark? Only works for the Latin1 subset, otherwise returns 'sFalse'.+isPunctuationL1 :: SChar -> SBool+isPunctuationL1 = liftPredL1 C.isPunctuation --- | Is this a symbol?-isSymbol :: SChar -> SBool-isSymbol = (`elem` "$+<=>^`|~\162\163\164\165\166\168\169\172\174\175\176\177\180\184\215\247")+-- | Is this a symbol? Only works for the Latin1 subset, otherwise returns 'sFalse'.+isSymbolL1 :: SChar -> SBool+isSymbolL1 = liftPredL1 C.isSymbol --- | Is this a separator?+-- | Is this a separator? Only works for the Latin1 subset, otherwise returns 'sFalse'. ----- >>> prove $ \c -> isSeparator c .=> isSpace c+-- >>> prove $ \c -> isSeparatorL1 c .=> isSpaceL1 c -- Q.E.D.-isSeparator :: SChar -> SBool-isSeparator = (`elem` " \160")+isSeparatorL1 :: SChar -> SBool+isSeparatorL1 = liftPredL1 C.isSeparator  -- | Is this an ASCII character, i.e., the first 128 characters. isAscii :: SChar -> SBool isAscii c = ord c .< 128 --- | Is this a Latin1 character? Note that this function is always true since 'SChar' corresponds--- precisely to Latin1 for the time being.------ >>> prove isLatin1--- Q.E.D.+-- | Is this a Latin1 character? isLatin1 :: SChar -> SBool-isLatin1 = const sTrue---- | Is this an ASCII letter?------ >>> prove $ \c -> isAsciiLetter c .<=> isAsciiUpper c .|| isAsciiLower c--- Q.E.D.-isAsciiLetter :: SChar -> SBool-isAsciiLetter c = isAsciiUpper c .|| isAsciiLower c+isLatin1 c = ord c .< 256  -- | Is this an ASCII Upper-case letter? i.e., @A@ thru @Z@ -- -- >>> prove $ \c -> isAsciiUpper c .<=> ord c .>= ord (literal 'A') .&& ord c .<= ord (literal 'Z') -- Q.E.D.--- >>> prove $ \c -> isAsciiUpper c .<=> isAscii c .&& isUpper c+-- >>> prove $ \c -> isAsciiUpper c .<=> isAscii c .&& isUpperL1 c -- Q.E.D. isAsciiUpper :: SChar -> SBool-isAsciiUpper = (`elem` literal ['A' .. 'Z'])+isAsciiUpper = liftPredL1 C.isAsciiUpper  -- | Is this an ASCII Lower-case letter? i.e., @a@ thru @z@ -- -- >>> prove $ \c -> isAsciiLower c .<=> ord c .>= ord (literal 'a') .&& ord c .<= ord (literal 'z') -- Q.E.D.--- >>> prove $ \c -> isAsciiLower c .<=> isAscii c .&& isLower c+-- >>> prove $ \c -> isAsciiLower c .<=> isAscii c .&& isLowerL1 c -- Q.E.D. isAsciiLower :: SChar -> SBool-isAsciiLower = (`elem` literal ['a' .. 'z'])+isAsciiLower = liftPredL1 C.isAsciiLower
Data/SBV/Client.hs view
@@ -28,7 +28,7 @@ import Control.Monad (filterM) import Data.Generics -import qualified Control.Exception   as C+import qualified Control.Exception as C  import qualified "template-haskell" Language.Haskell.TH as TH @@ -47,13 +47,13 @@  -- | The default configs corresponding to supported SMT solvers defaultSolverConfig :: Solver -> SMTConfig-defaultSolverConfig Z3        = z3-defaultSolverConfig Yices     = yices-defaultSolverConfig DReal     = dReal+defaultSolverConfig ABC       = abc defaultSolverConfig Boolector = boolector defaultSolverConfig CVC4      = cvc4+defaultSolverConfig DReal     = dReal defaultSolverConfig MathSAT   = mathSAT-defaultSolverConfig ABC       = abc+defaultSolverConfig Yices     = yices+defaultSolverConfig Z3        = z3  -- | Return the known available solver configs, installed on your machine. getAvailableSolvers :: IO [SMTConfig]
Data/SBV/Compilers/C.hs view
@@ -442,7 +442,7 @@  -- | Generate the C program genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SV -> Doc -> ([Doc], [String])-genCProg cfg fn proto (Result kindInfo _tvals _ovals cgs ins preConsts tbls arrs _uis _axioms (SBVPgm asgns) cstrs origAsserts _) inVars outVars mbRet extDecls+genCProg cfg fn proto (Result kindInfo _tvals _ovals cgs ins (_, preConsts) tbls arrs _uis _axioms (SBVPgm asgns) cstrs origAsserts _) inVars outVars mbRet extDecls   | isNothing (cgInteger cfg) && KUnbounded `Set.member` kindInfo   = error $ "SBV->C: Unbounded integers are not supported by the C compiler."           ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."@@ -510,7 +510,7 @@                          $$ vcat (map text ls)                          $$ text "" -       typeWidth = getMax 0 $ [len (kindOf s) | (s, _) <- assignments] ++ [len (kindOf s) | (_, (s, _)) <- fst ins]+       typeWidth = getMax 0 $ [len (kindOf s) | (s, _) <- assignments] ++ [len (kindOf s) | (_, NamedSymVar s _) <- fst ins]                 where len KReal{}            = 5                       len KFloat{}           = 6 -- SFloat                       len KDouble{}          = 7 -- SDouble
Data/SBV/Control/BaseIO.hs view
@@ -19,7 +19,7 @@ import Data.SBV.Control.Types (CheckSatResult, SMTInfoFlag, SMTInfoResponse, SMTOption, SMTReasonUnknown) import Data.SBV.Core.Concrete (CV) import Data.SBV.Core.Data     (HasKind, Symbolic, SymArray, SymVal, SBool, SBV, SBVType)-import Data.SBV.Core.Symbolic (Query, QueryContext, QueryState, State, SMTModel, SMTResult, SV)+import Data.SBV.Core.Symbolic (Query, QueryContext, QueryState, State, SMTModel, SMTResult, SV, Name)  import qualified Data.SBV.Control.Query as Trans import qualified Data.SBV.Control.Utils as Trans@@ -51,7 +51,7 @@ -- | Get the observables recorded during a query run. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.Control.getObservables'-getObservables :: Query [(String, CV)]+getObservables :: Query [(Name, CV)] getObservables = Trans.getObservables  -- | Get the uninterpreted constants/functions recorded during a run.
Data/SBV/Control/Query.hs view
@@ -9,11 +9,13 @@ -- Querying a solver interactively. ----------------------------------------------------------------------------- +{-# LANGUAGE BangPatterns        #-} {-# LANGUAGE LambdaCase          #-} {-# LANGUAGE NamedFieldPuns      #-} {-# LANGUAGE Rank2Types          #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections       #-}+{-# LANGUAGE ViewPatterns        #-}  {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} @@ -38,17 +40,23 @@  import qualified Data.Map.Strict    as M import qualified Data.IntMap.Strict as IM+import qualified Data.Sequence      as S+import qualified Data.Text          as T  -import Data.Char     (toLower)-import Data.List     (intercalate, nubBy, sortBy, sortOn)-import Data.Maybe    (listToMaybe, catMaybes)-import Data.Function (on)+import Data.Char      (toLower)+import Data.List      (intercalate, nubBy, sortOn)+import Data.Maybe     (listToMaybe, catMaybes)+import Data.Function  (on)+import Data.Bifunctor (first)+import Data.Foldable  (toList)  import Data.SBV.Core.Data  import Data.SBV.Core.Symbolic   ( MonadQuery(..), State(..)                                 , incrementInternalCounter, validationRequested+                                , prefixExistentials, prefixUniversals+                                , namedSymVar, getSV, lookupInput, userInputsToList                                 )  import Data.SBV.Utils.SExpr@@ -314,31 +322,31 @@           uis   <- getUIs             -- for "sat", display the prefix existentials. for "proof", display the prefix universals-          let allModelInputs = if isSAT then takeWhile ((/= ALL) . fst) qinps-                                        else takeWhile ((== ALL) . fst) qinps+          let allModelInputs = if isSAT then prefixExistentials qinps+                                        else prefixUniversals   qinps                -- Add on observables only if we're not in a quantified context-              grabObservables = length allModelInputs == length qinps -- i.e., we didn't drop anything+              grabObservables = S.length allModelInputs == S.length qinps -- i.e., we didn't drop anything            obsvs <- if grabObservables                       then getObservables                       else do queryDebug ["*** In a quantified context, obvservables will not be printed."]-                              return []--          let sortByNodeId :: [(SV, (String, CV))] -> [(String, CV)]-              sortByNodeId = map snd . sortBy (compare `on` (\(SV _ nid, _) -> nid))+                              return mempty -              grab (sv, nm) = wrap <$> getValueCV mbi sv-                 where wrap c = (sv, (nm, c))+          let grab (NamedSymVar sv nm) = wrap <$> getValueCV mbi sv+                where+                  wrap !c = (sv, (nm, c)) -          inputAssocs <- mapM (grab . snd) allModelInputs+          inputAssocs <- mapM (grab . namedSymVar) allModelInputs -          let assocs =  sortOn fst obsvs-                     ++ sortByNodeId [p | p@(_, (nm, _)) <- inputAssocs, not (isNonModelVar cfg nm)]+          let name     = fst . snd+              removeSV = snd+              prepare  = S.unstableSort . S.filter (not . isNonModelVar cfg . name)+              assocs   = S.fromList (sortOn fst obsvs) <> fmap removeSV (prepare inputAssocs)            -- collect UIs, and UI functions if requested-          let uiFuns = [ui | ui@(nm, SBVType as) <- uis, length as >  1, satTrackUFs cfg, not (isNonModelVar cfg nm)] -- functions have at least two things in their type!-              uiRegs = [ui | ui@(nm, SBVType as) <- uis, length as == 1,                  not (isNonModelVar cfg nm)]+          let uiFuns = [ui | ui@(T.pack -> nm, SBVType as) <- uis, length as >  1, satTrackUFs cfg, not (isNonModelVar cfg nm)] -- functions have at least two things in their type!+              uiRegs = [ui | ui@(T.pack -> nm, SBVType as) <- uis, length as == 1,                  not (isNonModelVar cfg nm)]            -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out           -- as cex's tend to get larger@@ -349,10 +357,10 @@                   Just cmds -> mapM_ (send True) cmds            bindings <- let get i@(ALL, _)      = return (i, Nothing)-                          get i@(EX, (sv, _)) = case sv `lookup` inputAssocs of-                                                  Just (_, cv) -> return (i, Just cv)-                                                  Nothing      -> do cv <- getValueCV mbi sv-                                                                     return (i, Just cv)+                          get i@(EX, getSV -> sv) = case lookupInput fst sv inputAssocs of+                                                      Just (_, (_, cv)) -> return (i, Just cv)+                                                      Nothing           -> do cv <- getValueCV mbi sv+                                                                              return (i, Just cv)                            flipQ i@(q, sv) = case (isSAT, q) of                                              (True,  _ )  -> i@@ -368,8 +376,8 @@           uiVals    <- mapM (\ui@(nm, _) -> (nm,) <$> getUICVal mbi ui) uiRegs            return SMTModel { modelObjectives = []-                          , modelBindings   = bindings-                          , modelAssocs     = uiVals ++ assocs+                          , modelBindings   = toList <$> bindings+                          , modelAssocs     = uiVals ++ toList (first T.unpack <$> assocs)                           , modelUIFuns     = uiFunVals                           } @@ -382,7 +390,7 @@                          r <- ask cmd -                        inputs <- map snd <$> getQuantifiedInputs+                        inputs <- toList . fmap namedSymVar <$> getQuantifiedInputs                          parse r bad $ \case EApp (ECon "objectives" : es) -> catMaybes <$> mapM (getObjValue (bad r) inputs) es                                             _                             -> bad r Nothing@@ -395,9 +403,9 @@                   EApp [ECon nm, v] -> locate nm v               -- Regular case                   _                 -> dontUnderstand (show expr) -          where locate nm v = case listToMaybe [p | p@(sv, _) <- inputs, show sv == nm] of-                                Nothing               -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names-                                Just (sv, actualName) -> grab sv v >>= \val -> return $ Just (actualName, val)+          where locate nm v = case listToMaybe [p | p@(NamedSymVar sv _) <- inputs, show sv == nm] of+                                Nothing                          -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names+                                Just (NamedSymVar sv actualName) -> grab sv v >>= \val -> return $ Just (T.unpack actualName, val)                  dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."                                                   , "While trying to process: " ++ s@@ -763,7 +771,7 @@ mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult mkSMTResult asgns = do              QueryState{queryConfig} <- getQueryState-             inps <- getQuantifiedInputs+             inps <- userInputsToList <$> getQuantifiedInputs               let grabValues st = do let extract (Assign s n) = sbvToSV st (SBV s) >>= \sv -> return (sv, n) @@ -776,8 +784,8 @@                                     let userSS = map fst modelAssignment                                          missing, extra, dup :: [String]-                                        missing = [n | (EX, (s, n)) <- inps, s `notElem` userSS]-                                        extra   = [show s | s <- userSS, s `notElem` map (fst . snd) inps]+                                        missing = [T.unpack n | (EX, NamedSymVar s n) <- inps, s `notElem` userSS]+                                        extra   = [show s | s <- userSS, s `notElem` map (getSV . namedSymVar) inps]                                         dup     = let walk []     = []                                                       walk (n:ns)                                                         | n `elem` ns = show n : walk (filter (/= n) ns)@@ -808,7 +816,7 @@                                                             , "*** Data.SBV: Check your query result construction!"                                                             ] -                                    let findName s = case [nm | (_, (i, nm)) <- inps, s == i] of+                                    let findName s = case [T.unpack nm | (_, NamedSymVar i nm) <- inps, s == i] of                                                         [nm] -> nm                                                         []   -> error "*** Data.SBV: Impossible happened: Cannot find " ++ show s ++ " in the input list"                                                         nms  -> error $ unlines [ ""
Data/SBV/Control/Utils.hs view
@@ -15,9 +15,11 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE LambdaCase             #-} {-# LANGUAGE NamedFieldPuns         #-}+{-# LANGUAGE OverloadedStrings      #-} {-# LANGUAGE ScopedTypeVariables    #-} {-# LANGUAGE TupleSections          #-} {-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE ViewPatterns           #-}  {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} @@ -40,16 +42,19 @@      , executeQuery      ) where -import Data.List  (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort, isPrefixOf)+import Data.List  (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort) -import Data.Char     (isPunctuation, isSpace, chr, ord, isDigit)-import Data.Function (on)+import Data.Char      (isPunctuation, isSpace, isDigit)+import Data.Function  (on)+import Data.Bifunctor (first)  import Data.Proxy +import qualified Data.Foldable      as F (toList) import qualified Data.Map.Strict    as Map import qualified Data.IntMap.Strict as IMap import qualified Data.Sequence      as S+import qualified Data.Text          as T  import Control.Monad            (join, unless, zipWithM, when, replicateM) import Control.Monad.IO.Class   (MonadIO, liftIO)@@ -58,7 +63,7 @@  import Data.Maybe (isNothing, isJust) -import Data.IORef (readIORef, writeIORef)+import Data.IORef (readIORef, writeIORef, IORef)  import Data.Time (getZonedTime) @@ -78,6 +83,9 @@                               , registerLabel, svMkSymVar, validationRequested                               , isSafetyCheckingIStage, isSetupIStage, isRunIStage, IStage(..), QueryT(..)                               , extractSymbolicSimulationState, MonadSymbolic(..), newUninterpreted+                              , UserInputs, getInputs, prefixExistentials, getSV, quantifier, getUserName+                              , namedSymVar, NamedSymVar(..), lookupInput, userInputs, userInputsToList+                              , getUserName', Name, CnstMap                               )  import Data.SBV.Core.AlgReals   (mergeAlgReals, AlgReal(..), RealPoint(..))@@ -156,22 +164,31 @@ io = liftIO  -- | Sync-up the external solver with new context we have generated-syncUpSolver :: (MonadIO m, MonadQuery m) => IncState -> m ()-syncUpSolver is = do+syncUpSolver :: (MonadIO m, MonadQuery m) => IORef CnstMap -> IncState -> m ()+syncUpSolver rGlobalConsts is = do         cfg <- getConfig++        -- update global consts to have the new ones+        (newConsts, allConsts) <- liftIO $ do nc <- readIORef (rNewConsts is)+                                              oc <- readIORef rGlobalConsts+                                              let allConsts = Map.union nc oc+                                              writeIORef rGlobalConsts allConsts+                                              pure (nc, allConsts)+         ls  <- io $ do let swap  (a, b)        = (b, a)                            cmp   (a, _) (b, _) = a `compare` b                            arrange (i, (at, rt, es)) = ((i, at, rt), es)                        inps        <- reverse <$> readIORef (rNewInps is)                        ks          <- readIORef (rNewKinds is)-                       cnsts       <- sortBy cmp . map swap . Map.toList <$> readIORef (rNewConsts is)                        arrs        <- IMap.toAscList <$> readIORef (rNewArrs is)                        tbls        <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef (rNewTbls is)                        uis         <- Map.toAscList <$> readIORef (rNewUIs is)                        as          <- readIORef (rNewAsgns is)                        constraints <- readIORef (rNewConstraints is) -                       return $ toIncSMTLib cfg inps ks cnsts arrs tbls uis as constraints cfg+                       let cnsts = sortBy cmp . map swap . Map.toList $ newConsts++                       return $ toIncSMTLib cfg inps ks (allConsts, cnsts) arrs tbls uis as constraints cfg         mapM_ (send True) $ mergeSExpr ls  -- | Retrieve the query context@@ -199,9 +216,9 @@  -- | Generalization of 'Data.SBV.Control.inNewContext' inNewContext :: (MonadIO m, MonadQuery m) => (State -> IO a) -> m a-inNewContext act = do st <- queryState+inNewContext act = do st@State{rconstMap} <- queryState                       (is, r) <- io $ withNewIncState st act-                      syncUpSolver is+                      syncUpSolver rconstMap is                       return r  -- | Generic 'Queriable' instance for 'SymVal' values@@ -755,7 +772,7 @@                                        | EDouble i   <- e -> Just $ CV KDouble (CDouble i)                                        | True             -> Nothing -                           KChar       | ENum (i, _) <- e -> Just $ CV KChar $ CChar $ chr $ fromIntegral i+                           KChar       | ECon s      <- e -> Just $ CV KChar $ CChar $ interpretChar s                                        | True             -> Nothing                             KString     | ECon s      <- e -> Just $ CV KString $ CString $ interpretString s@@ -783,13 +800,10 @@           | True           = qfsToString $ tail (init xs) -        isStringSequence (KList (KBounded _ 8)) = True-        isStringSequence _                      = False+        interpretChar xs = case interpretString xs of+                             [c] -> c+                             _   -> error $ "Expected a singleton char constant, received: <" ++ xs ++ ">" -        -- 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 (CInteger . fromIntegral . ord) $ interpretString s         interpretList ek topExpr = walk topExpr           where walk (EApp [ECon "as", ECon "seq.empty", _]) = []                 walk (EApp [ECon "seq.unit", v])             = case recoverKindedValue ek v of@@ -833,15 +847,22 @@                   mbAssocs = parseSExprFunction setExpr -                 decode (args, r) | isTrue r = ComplementSet $ Set.fromList [x | (x, False) <- map contents args]  -- deletions from universal-                                  | True     = RegularSet    $ Set.fromList [x | (x, True)  <- map contents args]  -- additions to empty+                 decode (args, r) | isTrue r = ComplementSet $ Set.fromList [x | (x, False) <- concatMap (contents True)  args]  -- deletions from universal+                                  | True     = RegularSet    $ Set.fromList [x | (x, True)  <- concatMap (contents False) args]  -- additions to empty -                 contents ([v], r) = (element v, isTrue r)-                 contents bad      = tbd $ "Multi-valued set member seen: " ++ show bad+                 contents cvt ([v], r) = let t = isTrue r in map (, t) (element cvt v)+                 contents _   bad      = tbd $ "Multi-valued set member seen: " ++ show bad -                 element x = case recoverKindedValue ke x of-                               Just v  -> cvVal v-                               Nothing -> tbd $ "Unexpected value for kind: " ++ show (x, ke)+                 element cvt x = case (cvt, ke) of+                                   (True, KChar) -> case recoverKindedValue KString x of+                                                      Just v  -> case cvVal v of+                                                                  CString [c] -> [CChar c]+                                                                  CString _   -> []+                                                                  _           -> tbd $ "Unexpected value for kind: " ++ show (x, ke)+                                                      Nothing -> tbd $ "Unexpected value for kind: " ++ show (x, ke)+                                   _             -> case recoverKindedValue ke x of+                                                      Just v  -> [cvVal v]+                                                      Nothing -> tbd $ "Unexpected value for kind: " ++ show (x, ke)          interpretTuple te = walk (1 :: Int) (zipWith recoverKindedValue ks args) []                 where (ks, n) = case k of@@ -854,7 +875,7 @@                       -- present tuples, so we accommodate both:                       args = try te                         where -- Z3 way-                              try (EApp (ECon f : as)) = case splitAt (length "mkSBVTuple") f of+                              try (EApp (ECon f : as)) = case splitAt (T.length "mkSBVTuple") f of                                                              ("mkSBVTuple", c) | all isDigit c && read c == n && length as == n -> as                                                              _  -> bad                               -- CVC4 way@@ -1035,32 +1056,30 @@                                            _                -> bad r Nothing  -- | What are the top level inputs? Trackers are returned as top level existentials-getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m [(Quantifier, NamedSymVar)]+getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m UserInputs getQuantifiedInputs = do State{rinps} <- queryState-                         ((rQinps, rTrackers), _) <- liftIO $ readIORef rinps--                         let qinps    = reverse rQinps-                             trackers = map (EX,) $ reverse rTrackers+                         (rQinps, rTrackers) <- liftIO $ getInputs <$> readIORef rinps +                         let trackers = (EX,) <$> rTrackers                              -- separate the existential prefix, which will go first-                             (preQs, postQs) = span (\(q, _) -> q == EX) qinps+                             (preQs, postQs) = S.spanl (\(q, _) -> q == EX) rQinps -                         return $ preQs ++ trackers ++ postQs+                         return $ preQs <> trackers <> postQs  -- | Get observables, i.e., those explicitly labeled by the user with a call to 'Data.SBV.observe'.-getObservables :: (MonadIO m, MonadQuery m) => m [(String, CV)]+getObservables :: (MonadIO m, MonadQuery m) => m [(Name, CV)] getObservables = do State{rObservables} <- queryState                      rObs <- liftIO $ readIORef rObservables                      -- This intentionally reverses the result; since 'rObs' stores in reversed order-                    let walk []             sofar = return sofar-                        walk ((n, f, s):os) sofar = do cv <- getValueCV Nothing s-                                                       if f cv+                    let walk []             !sofar = return sofar+                        walk ((n, f, s):os) !sofar = do cv <- getValueCV Nothing s+                                                        if f cv                                                           then walk os ((n, cv) : sofar)                                                           else walk os            sofar -                    walk rObs []+                    walk (F.toList rObs) []  -- | Get UIs, both constants and functions. This call returns both the before and after query ones. -- | Generalization of 'Data.SBV.Control.getUIs'.@@ -1087,11 +1106,11 @@                       -- Functions have at least two kinds in their type and all components must be "interpreted"                      let allUiFuns = [u | satTrackUFs cfg                                         -- config says consider UIFs                                         , u@(nm, SBVType as) <- allUninterpreteds, length as > 1  -- get the function ones-                                        , not (isNonModelVar cfg nm)                              -- make sure they aren't explicitly ignored+                                        , not (isNonModelVar cfg (T.pack nm))                     -- make sure they aren't explicitly ignored                                      ]                           allUiRegs = [u | u@(nm, SBVType as) <- allUninterpreteds, length as == 1  -- non-function ones-                                        , not (isNonModelVar cfg nm)                               -- make sure not ignored+                                        , not (isNonModelVar cfg (T.pack nm))                      -- make sure not ignored                                      ]                           -- We can only "allSat" if all component types themselves are interpreted. (Otherwise@@ -1124,23 +1143,22 @@                                                        , "***             SBV will use equivalence classes to generate all-satisfying instances."                                                        ] -                     let allModelInputs  = takeWhile ((/= ALL) . fst) qinps+                     let allModelInputs  = prefixExistentials qinps                          -- Add on observables only if we're not in a quantified context:-                         grabObservables = length allModelInputs == length qinps -- i.e., we didn't drop anything--                         vars :: [(SVal, NamedSymVar)]-                         vars = let sortByNodeId :: [NamedSymVar] -> [NamedSymVar]-                                    sortByNodeId = sortBy (compare `on` (\(SV _ n, _) -> n))+                         grabObservables = S.length allModelInputs == S.length qinps -- i.e., we didn't drop anything -                                    mkSVal :: NamedSymVar -> (SVal, NamedSymVar)-                                    mkSVal nm@(sv, _) = (SVal (kindOf sv) (Right (cache (const (return sv)))), nm)+                         vars :: S.Seq (SVal, NamedSymVar)+                         vars = let mkSVal :: NamedSymVar -> (SVal, NamedSymVar)+                                    mkSVal nm@(getSV -> sv) = (SVal (kindOf sv) (Right (cache (const (return sv)))), nm) -                                    ignored n = isNonModelVar cfg n || "__internal_sbv" `isPrefixOf` n+                                    ignored n = isNonModelVar cfg n || "__internal_sbv" `T.isPrefixOf` n -                                in map mkSVal $ sortByNodeId [nv | (_, nv@(_, n)) <- allModelInputs, not (ignored n)]+                                in fmap (mkSVal . namedSymVar)+                                   . S.filter (not . ignored . getUserName . namedSymVar)+                                   $ allModelInputs                           -- If we have any universals, then the solutions are unique upto prefix existentials.-                         w = ALL `elem` map fst qinps+                         w = ALL `elem` F.toList (quantifier <$> qinps)                       res <- loop grabObservables topState (allUiFuns, uiFuns) allUiRegs qinps vars cfg AllSatResult { allSatMaxModelCountReached  = False                                                                                                                     , allSatHasPrefixExistentials = w@@ -1156,13 +1174,13 @@           loop grabObservables topState (allUiFuns, uiFunsToReject) allUiRegs qinps vars cfg = go (1::Int)            where go :: Int -> AllSatResult -> m AllSatResult-                 go !cnt sofar+                 go !cnt !sofar                    | Just maxModels <- allSatMaxModelCount cfg, cnt > maxModels                    = do queryDebug ["*** Maximum model count request of " ++ show maxModels ++ " reached, stopping the search."]                          when (allSatPrintAlong cfg) $ io $ putStrLn "Search stopped since model count request was reached." -                        return $ sofar { allSatMaxModelCountReached = True }+                        return $! sofar { allSatMaxModelCountReached = True }                    | True                    = do queryDebug ["Looking for solution " ++ show cnt] @@ -1191,8 +1209,8 @@                                        endMsg $ Just $ "[" ++ m ++ "]"                                        return sofar{ allSatSolverReturnedDSat = True } -                          Sat    -> do assocs <- mapM (\(sval, (sv, n)) -> do cv <- getValueCV Nothing sv-                                                                              return (sv, (n, (sval, cv)))) vars+                          Sat    -> do assocs <- mapM (\(sval, NamedSymVar sv n) -> do !cv <- getValueCV Nothing sv+                                                                                       return (sv, (n, (sval, cv)))) vars                                         let getUIFun ui@(nm, t) = do cvs <- getUIFunCVAssoc Nothing ui                                                                     return (nm, (t, cvs))@@ -1204,25 +1222,27 @@                                        obsvs <- if grabObservables                                                    then getObservables                                                    else do queryDebug ["*** In a quantified context, observables will not be printed."]-                                                           return []+                                                           return mempty -                                       bindings <- let grab i@(ALL, _)      = return (i, Nothing)-                                                       grab i@(EX, (sv, _)) = case sv `lookup` assocs of-                                                                                Just (_, (_, cv)) -> return (i, Just cv)-                                                                                Nothing           -> do cv <- getValueCV Nothing sv-                                                                                                        return (i, Just cv)+                                       bindings <- let grab i@(ALL, _)          = return (i, Nothing)+                                                       grab i@(EX, getSV -> sv) = case lookupInput fst sv assocs of+                                                                                Just (_, (_, (_, cv))) -> return (i, Just cv)+                                                                                Nothing                -> do !cv <- getValueCV Nothing sv+                                                                                                             return (i, Just cv)                                                    in if validationRequested cfg                                                          then Just <$> mapM grab qinps                                                          else return Nothing                                         let model = SMTModel { modelObjectives = []-                                                            , modelBindings   = bindings-                                                            , modelAssocs     = uiRegVals ++ sortOn fst obsvs ++ [(n, cv) | (_, (n, (_, cv))) <- assocs]+                                                            , modelBindings   = F.toList <$> bindings+                                                            , modelAssocs     =    uiRegVals+                                                                                <> (first T.unpack <$> sortOn fst obsvs)+                                                                                <> [(T.unpack n, cv) | (_, (n, (_, cv))) <- F.toList assocs]                                                             , modelUIFuns     = uiFunVals                                                             }                                            m = Satisfiable cfg model -                                           (interpreteds, uninterpreteds) = partition (not . isFree . kindOf . fst) (map (snd . snd) assocs)+                                           (interpreteds, uninterpreteds) = S.partition (not . isFree . kindOf . fst) (fmap (snd . snd) assocs)                                             interpretedRegUis = filter (not . isFree . kindOf . snd) uiRegVals @@ -1235,7 +1255,7 @@                                            -- NB. When the kind is floating, we *have* to be careful, since +/- zero, and NaN's                                            -- and equality don't get along!                                            interpretedEqs :: [SVal]-                                           interpretedEqs = [mkNotEq (kindOf sv) sv (SVal (kindOf sv) (Left cv)) | (sv, cv) <- interpretedRegUiSVs ++ interpreteds]+                                           interpretedEqs = [mkNotEq (kindOf sv) sv (SVal (kindOf sv) (Left cv)) | (sv, cv) <- interpretedRegUiSVs <> F.toList interpreteds]                                               where mkNotEq k a b                                                      | isDouble k || isFloat k = svNot (a `fpNotEq` b)                                                      | True                    = a `svNotEqual` b@@ -1252,7 +1272,7 @@                                                             . map (map fst)                -- throw away values, we only need svals                                                             . groupBy ((==) `on` snd)      -- make sure they belong to the same sort and have the same value                                                             . sortOn snd                   -- sort them according to their CV (i.e., sort/value)-                                                            $ uninterpreteds+                                                            $ F.toList uninterpreteds                                              where pwDistinct :: [SVal] -> [SVal]                                                    pwDistinct ss = [x `svNotEqual` y | (x:ys) <- tails ss, y <- ys] @@ -1440,9 +1460,9 @@           skolemize :: [(Quantifier, NamedSymVar)] -> [Either SV (SV, [SV])]          skolemize quants = go quants ([], [])-           where go []                   (_,  sofar) = reverse sofar-                 go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar)-                 go ((EX,  (v, _)):rest) (us, sofar) = go rest (us,   Right (v, reverse us) : sofar)+           where go []                        (_,  sofar) = reverse sofar+                 go ((ALL, getSV -> v) :rest) (us, sofar) = go rest (v:us, Left v : sofar)+                 go ((EX,  getSV -> v) :rest) (us, sofar) = go rest (us,   Right (v, reverse us) : sofar)           qinps      = if isSat then fst is else map flipQ (fst is)          skolemMap  = skolemize qinps@@ -1511,8 +1531,8 @@                     case queryContext of                       QueryInternal -> return ()         -- we're good, internal usages don't mess with scopes                       QueryExternal -> do-                        ((userInps, _), _) <- readIORef (rinps st)-                        let badInps = reverse [n | (ALL, (_, n)) <- userInps]+                        userInps  <- userInputsToList . userInputs <$> readIORef (rinps st)+                        let badInps = reverse [n | (ALL, getUserName' -> n) <- userInps]                         case badInps of                           [] -> return ()                           _  -> let plu | length badInps > 1 = "s require"
Data/SBV/Core/Data.hs view
@@ -44,7 +44,7 @@  , sbvToSV, sbvToSymSV, forceSVArg  , SBVExpr(..), newExpr  , cache, Cached, uncache, uncacheAI, HasKind(..)- , Op(..), PBOp(..), FPOp(..), StrOp(..), SeqOp(..), 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@@ -142,14 +142,9 @@ -- | IEEE-754 double-precision floating point numbers type SDouble = SBV Double --- | A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character--- is currently an 8-bit unsigned value, corresponding to the ISO-8859-1 (Latin-1) character--- set: <http://en.wikipedia.org/wiki/ISO/IEC_8859-1>. A Haskell 'Char', on the other hand, is based--- on unicode. Therefore, there isn't a 1-1 correspondence between a Haskell character and an SBV--- character for the time being. This limitation is due to the SMT-solvers only supporting this--- particular subset. However, there is a pending proposal to add support for unicode, and SBV--- will track these changes to have full unicode support as solvers become available. For--- details, see: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>+-- | A symbolic character. Note that this is the full unicode character set.+-- see: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>+-- for details. type SChar = SBV Char  -- | A symbolic string. Note that a symbolic string is /not/ a list of symbolic characters,
Data/SBV/Core/Kind.hs view
@@ -119,7 +119,7 @@ smtType KFloat          = "(_ FloatingPoint  8 24)" smtType KDouble         = "(_ FloatingPoint 11 53)" smtType KString         = "String"-smtType KChar           = "(_ BitVec 8)"+smtType KChar           = "String" smtType (KList k)       = "(Seq "   ++ smtType k ++ ")" smtType (KSet  k)       = "(Array " ++ smtType k ++ " Bool)" smtType (KUserSort s _) = s
Data/SBV/Core/Model.hs view
@@ -2476,7 +2476,7 @@                                      QC.pre cond                                      unless (r || null modelVals) $ QC.monitor (QC.counterexample (complain modelVals))                                      QC.assert r-     where test = do (r, Result{resTraces=tvals, resObservables=ovals, resConsts=cs, resConstraints=cstrs, resUIConsts=unints}) <- runSymbolic (Concrete Nothing) prop+     where test = do (r, Result{resTraces=tvals, resObservables=ovals, resConsts=(_, cs), resConstraints=cstrs, resUIConsts=unints}) <- runSymbolic (Concrete Nothing) prop                       let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)                          cond = and [cvToBool (cval v) | (False, _, v) <- F.toList cstrs] -- Only pick-up "hard" constraints, as indicated by False in the fist component
Data/SBV/Core/Symbolic.hs view
@@ -9,28 +9,33 @@ -- Symbolic values ----------------------------------------------------------------------------- +{-# LANGUAGE BangPatterns               #-} {-# LANGUAGE CPP                        #-} {-# LANGUAGE DefaultSignatures          #-} {-# LANGUAGE DeriveDataTypeable         #-} {-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveGeneric              #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE FunctionalDependencies     #-} {-# LANGUAGE GADTs                      #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE NamedFieldPuns             #-}+{-# LANGUAGE OverloadedStrings          #-} {-# LANGUAGE PatternGuards              #-} {-# LANGUAGE Rank2Types                 #-} {-# LANGUAGE ScopedTypeVariables        #-} {-# LANGUAGE TupleSections              #-} {-# LANGUAGE TypeOperators              #-} {-# LANGUAGE UndecidableInstances       #-} -- for undetermined s in MonadState+{-# LANGUAGE ViewPatterns               #-}  {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}  module Data.SBV.Core.Symbolic   ( NodeId(..)   , SV(..), swKind, trueSV, falseSV-  , Op(..), PBOp(..), OvOp(..), FPOp(..), NROp(..), StrOp(..), SeqOp(..), SetOp(..), RegExp(..)+  , Op(..), PBOp(..), OvOp(..), FPOp(..), NROp(..), StrOp(..), SeqOp(..), SetOp(..)+  , RegExp(..), regExpToSMTString   , Quantifier(..), needsExistentials, VarContext(..)   , RoundingMode(..)   , SBVType(..), svUninterpreted, newUninterpreted@@ -41,8 +46,11 @@   , SBVExpr(..), newExpr, isCodeGenMode, isSafetyCheckingIStage, isRunIStage, isSetupIStage   , Cached, cache, uncache, modifyState, modifyIncState   , ArrayIndex(..), FArrayIndex(..), uncacheAI, uncacheFAI-  , NamedSymVar-  , getSValPathCondition, extendSValPathCondition+  , NamedSymVar(..), Name, UserInputs, Inputs(..), getSV, swNodeId, namedNodeId, getUniversals+  , prefixExistentials, prefixUniversals, onUserInputs, onInternInputs, onAllInputs+  , addInternInput, addUserInput, getInputs, inputsFromListWith, userInputsToList+  , getUserName', internInputsToList, inputsToList, quantifier, namedSymVar, getUserName+  , lookupInput , getSValPathCondition, extendSValPathCondition   , getTableIndex   , SBVPgm(..), MonadSymbolic(..), SymbolicT, Symbolic, runSymbolic, State(..), withNewIncState, IncState(..), incrementInternalCounter   , inSMTMode, SBVRunMode(..), IStage(..), Result(..)@@ -50,14 +58,14 @@   , addAssertion, addNewSMTOption, imposeConstraint, internalConstraint, internalVariable   , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension   , SolverCapabilities(..)-  , extractSymbolicSimulationState+  , extractSymbolicSimulationState, CnstMap   , OptimizeStyle(..), Objective(..), Penalty(..), objectiveName, addSValOptGoal   , MonadQuery(..), QueryT(..), Query, Queriable(..), Fresh(..), QueryState(..), QueryContext(..)   , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine   , validationRequested, outputSVal   ) where -import Control.Arrow               (first, second, (***))+import Control.Arrow               ((***)) import Control.DeepSeq             (NFData(..)) import Control.Monad               (when) import Control.Monad.Except        (MonadError, ExceptT)@@ -76,6 +84,7 @@ import Data.Time (getCurrentTime, UTCTime)  import GHC.Stack+import GHC.Generics (Generic)  import qualified Control.Monad.State.Lazy    as LS import qualified Control.Monad.State.Strict  as SS@@ -87,7 +96,8 @@ import qualified Data.Map.Strict             as Map  (Map, empty, toList, lookup, insert, size) import qualified Data.Set                    as Set  (Set, empty, toList, insert, member) import qualified Data.Foldable               as F    (toList)-import qualified Data.Sequence               as S    (Seq, empty, (|>))+import qualified Data.Sequence               as S    (Seq, empty, (|>), (<|), filter, takeWhileL, fromList, lookup, elemIndexL)+import qualified Data.Text                   as T  import System.Mem.StableName @@ -104,7 +114,8 @@ #endif  -- | A symbolic node id-newtype NodeId = NodeId Int deriving (Eq, Ord, G.Data)+newtype NodeId = NodeId { getId :: Int }+  deriving (Eq, Ord, G.Data)  -- | A symbolic word, tracking it's signedness and size. data SV = SV !Kind !NodeId@@ -131,6 +142,10 @@ swKind :: SV -> Kind swKind (SV k _) = k +-- | retrieve the node id of a symbolic word+swNodeId :: SV -> NodeId+swNodeId (SV _ nid) = nid+ -- | Forcing an argument; this is a necessary evil to make sure all the arguments -- to an uninterpreted function are evaluated before called; the semantics of uinterpreted -- functions is necessarily strict; deviating from Haskell's@@ -314,6 +329,8 @@            | StrReplace      -- ^ Replace the first occurrence of @src@ by @dst@ in @s@            | StrStrToNat     -- ^ Retrieve integer encoded by string @s@ (ground rewriting only)            | StrNatToStr     -- ^ Retrieve string encoded by integer @i@ (ground rewriting only)+           | StrToCode       -- ^ Equivalent to Haskell's ord+           | StrFromCode     -- ^ Equivalent to Haskell's chr            | StrInRe RegExp  -- ^ Check if string is in the regular expression            deriving (Eq, Ord, G.Data) @@ -364,34 +381,41 @@    negate      = error "Num.RegExp: no negate method" --- | Show instance for `RegExp`. The mapping is done so the outcome matches the--- SMTLib string reg-exp operations+-- | Convert a reg-exp to a Haskell-like string instance Show RegExp where-  show (Literal s)       = "(str.to.re \"" ++ stringToQFS s ++ "\")"-  show All               = "re.allchar"-  show None              = "re.nostr"-  show (Range ch1 ch2)   = "(re.range \"" ++ stringToQFS [ch1] ++ "\" \"" ++ stringToQFS [ch2] ++ "\")"-  show (Conc [])         = show (1 :: Integer)-  show (Conc [x])        = show x-  show (Conc xs)         = "(re.++ " ++ unwords (map show xs) ++ ")"-  show (KStar r)         = "(re.* " ++ show r ++ ")"-  show (KPlus r)         = "(re.+ " ++ show r ++ ")"-  show (Opt   r)         = "(re.opt " ++ show r ++ ")"-  show (Loop  lo hi r)-     | lo >= 0, hi >= lo = "((_ re.loop " ++ show lo ++ " " ++ show hi ++ ") " ++ show r ++ ")"-     | True              = error $ "Invalid regular-expression Loop with arguments: " ++ show (lo, hi)-  show (Inter r1 r2)     = "(re.inter " ++ show r1 ++ " " ++ show r2 ++ ")"-  show (Union [])        = "re.nostr"-  show (Union [x])       = show x-  show (Union xs)        = "(re.union " ++ unwords (map show xs) ++ ")"+  show = regExpToString show +-- | Convert a reg-exp to a SMT-lib acceptable representation+regExpToSMTString :: RegExp -> String+regExpToSMTString = regExpToString (\s -> '"' : stringToQFS s ++ "\"")++-- | Convert a RegExp to a string, parameterized by how strings are converted+regExpToString :: (String -> String) -> RegExp -> String+regExpToString fs (Literal s)       = "(str.to.re " ++ fs s ++ ")"+regExpToString _  All               = "re.allchar"+regExpToString _  None              = "re.nostr"+regExpToString fs (Range ch1 ch2)   = "(re.range " ++ fs [ch1] ++ " " ++ fs [ch2] ++ ")"+regExpToString _  (Conc [])         = show (1 :: Integer)+regExpToString fs (Conc [x])        = regExpToString fs x+regExpToString fs (Conc xs)         = "(re.++ " ++ unwords (map (regExpToString fs) xs) ++ ")"+regExpToString fs (KStar r)         = "(re.* " ++ regExpToString fs r ++ ")"+regExpToString fs (KPlus r)         = "(re.+ " ++ regExpToString fs r ++ ")"+regExpToString fs (Opt   r)         = "(re.opt " ++ regExpToString fs r ++ ")"+regExpToString fs (Loop  lo hi r)+   | lo >= 0, hi >= lo = "((_ re.loop " ++ show lo ++ " " ++ show hi ++ ") " ++ regExpToString fs r ++ ")"+   | True              = error $ "Invalid regular-expression Loop with arguments: " ++ show (lo, hi)+regExpToString fs (Inter r1 r2)     = "(re.inter " ++ regExpToString fs r1 ++ " " ++ regExpToString fs r2 ++ ")"+regExpToString _  (Union [])        = "re.nostr"+regExpToString fs (Union [x])       = regExpToString fs x+regExpToString fs (Union xs)        = "(re.union " ++ unwords (map (regExpToString fs) xs) ++ ")"+ -- | Show instance for @StrOp@. Note that the mapping here is -- important to match the SMTLib equivalents, see here: <http://rise4fun.com/z3/tutorialcontent/sequences> instance Show StrOp where   show StrConcat   = "str.++"   show StrLen      = "str.len"-  show StrUnit     = "seq.unit"      -- NB. The "seq" prefix is intentional; works uniformly.-  show StrNth      = "seq.nth"       -- NB. The "seq" prefix is intentional; works uniformly.+  show StrUnit     = "str.unit"      -- NB. This is actually a no-op, since in SMTLib characters are the same as strings.+  show StrNth      = "str.at"   show StrSubstr   = "str.substr"   show StrIndexOf  = "str.indexof"   show StrContains = "str.contains"@@ -400,8 +424,10 @@   show StrReplace  = "str.replace"   show StrStrToNat = "str.to.int"    -- NB. SMTLib uses "int" here though only nats are supported   show StrNatToStr = "int.to.str"    -- NB. SMTLib uses "int" here though only nats are supported+  show StrToCode   = "str.to_code"+  show StrFromCode = "str.from_code"   -- Note the breakage here with respect to argument order. We fix this explicitly later.-  show (StrInRe s) = "str.in.re " ++ show s+  show (StrInRe s) = "str.in.re " ++ regExpToSMTString s  -- | Sequence operations. data SeqOp = SeqConcat    -- ^ See StrConcat@@ -578,9 +604,44 @@ -- | A program is a sequence of assignments newtype SBVPgm = SBVPgm {pgmAssignments :: S.Seq (SV, SBVExpr)} +-- | Helper synonym for text, in case we switch to something else later.+type Name = T.Text+ -- | 'NamedSymVar' pairs symbolic values and user given/automatically generated names-type NamedSymVar = (SV, String)+data NamedSymVar = NamedSymVar !SV !Name+                 deriving (Show,Generic) +-- | For comparison purposes, we simply use the SV and ignore the name+instance Eq NamedSymVar where+  (==) (NamedSymVar l _) (NamedSymVar r _) = l == r++instance Ord NamedSymVar where+  compare (NamedSymVar l _) (NamedSymVar r _) = compare l r++-- | Convert to a named symvar, from string+toNamedSV' :: SV -> String -> NamedSymVar+toNamedSV' s = NamedSymVar s . T.pack++-- | Convert to a named symvar, from text+toNamedSV :: SV -> Name -> NamedSymVar+toNamedSV = NamedSymVar++-- | Get the node id from a named sym var+namedNodeId :: NamedSymVar -> NodeId+namedNodeId = swNodeId . getSV++-- | Get the SV from a named sym var+getSV :: NamedSymVar -> SV+getSV (NamedSymVar s _) = s++-- | Get the user-name typed value from named sym var+getUserName :: NamedSymVar -> Name+getUserName (NamedSymVar _ nm) = nm++-- | Get the string typed value from named sym var+getUserName' :: NamedSymVar -> String+getUserName' = T.unpack . getUserName+ -- | Style of optimization. Note that in the pareto case the user is allowed -- to specify a max number of fronts to query the solver for, since there might -- potentially be an infinite number of them and there is no way to know exactly@@ -696,7 +757,7 @@                      , resObservables :: [(String, CV -> Bool, SV)]                   -- ^ observable expressions (part of the model)                      , resUISegs      :: [(String, [String])]                         -- ^ uninterpeted code segments                      , resInputs      :: ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- ^ inputs (possibly existential) + tracker vars-                     , resConsts      :: [(SV, CV)]                                   -- ^ constants+                     , resConsts      :: (CnstMap, [(SV, CV)])                        -- ^ constants                      , resTables      :: [((Int, Kind, Kind), [SV])]                  -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts                      , resArrays      :: [(Int, ArrayInfo)]                           -- ^ arrays (user specified)                      , resUIConsts    :: [(String, SBVType)]                          -- ^ uninterpreted constants@@ -712,10 +773,10 @@   -- If there's nothing interesting going on, just print the constant. Note that the   -- definiton of interesting here is rather subjective; but essentially if we reduced   -- the result to a single constant already, without any reference to anything.-  show Result{resConsts=cs, resOutputs=[r]}+  show Result{resConsts=(_, cs), resOutputs=[r]}     | Just c <- r `lookup` cs     = show c-  show (Result kinds _ _ cgs is cs ts as uis axs xs cstrs asserts os) = intercalate "\n" $+  show (Result kinds _ _ cgs is (_, cs) ts as uis axs xs cstrs asserts os) = intercalate "\n" $                    (if null usorts then [] else "SORTS" : map ("  " ++) usorts)                 ++ ["INPUTS"]                 ++ map shn (fst is)@@ -759,13 +820,14 @@            shcg (s, ss) = ("Variable: " ++ s) : map ("  " ++) ss -          shn (q, (sv, nm)) = "  " ++ ni ++ " :: " ++ show (swKind sv) ++ ex ++ alias+          shn (q, NamedSymVar sv nm) = "  " <> ni <> " :: " ++ show (swKind sv) ++ ex ++ alias             where ni = show sv-                  ex | q == ALL = ""-                     | True     = ", existential"-                  alias | ni == nm = ""-                        | True     = ", aliasing " ++ show nm+                  ex    | q == ALL          = ""+                        | True              = ", existential" +                  alias | ni == T.unpack nm = ""+                        | True              = ", aliasing " ++ show nm+           sha (i, (nm, (ai, bi), ctx)) = "  " ++ ni ++ " :: " ++ show ai ++ " -> " ++ show bi ++ alias                                        ++ "\n     Context: "     ++ show ctx             where ni = "array_" ++ show i@@ -925,19 +987,130 @@         finalIncState <- readIORef (rIncState st)         return (finalIncState, r) ++-- | User defined, with proper quantifiers+type UserInputs = S.Seq (Quantifier, NamedSymVar)++-- | Internally declared, always existential+type InternInps = S.Seq NamedSymVar++-- | Entire set of names, for faster lookup+type AllInps = Set.Set Name++-- | Inputs as a record of maps and sets. See above type-synonyms for their roles.+data Inputs = Inputs { userInputs   :: !UserInputs+                     , internInputs :: !InternInps+                     , allInputs    :: !AllInps+                     } deriving (Eq,Show)++-- | Semigroup instance; combining according to indexes.+instance Semigroup Inputs where+  (Inputs lui lii lai) <> (Inputs rui rii rai) = Inputs (lui <> rui) (lii <> rii) (lai <> rai)++-- | Monoid instance, we start with no maps.+instance Monoid Inputs where+  mempty = Inputs { userInputs   = mempty+                  , internInputs = mempty+                  , allInputs    = mempty+                  }++-- | Get the quantifier+quantifier :: (Quantifier, NamedSymVar) -> Quantifier+quantifier = fst++-- | Get the named symbolic variable+namedSymVar :: (Quantifier, NamedSymVar) -> NamedSymVar+namedSymVar = snd++-- | Modify the user-inputs field+onUserInputs :: (UserInputs -> UserInputs) -> Inputs -> Inputs+onUserInputs f inp@Inputs{userInputs} = inp{userInputs = f userInputs}++-- | Modify the internal-inputs field+onInternInputs :: (InternInps -> InternInps) -> Inputs -> Inputs+onInternInputs f inp@Inputs{internInputs} = inp{internInputs = f internInputs}++-- | Modify the all-inputs field+onAllInputs :: (AllInps -> AllInps) -> Inputs -> Inputs+onAllInputs f inp@Inputs{allInputs} = inp{allInputs = f allInputs}++-- | Add a new internal input+addInternInput :: SV -> Name -> Inputs -> Inputs+addInternInput sv nm = goAll . goIntern+  where !new = toNamedSV sv nm+        goIntern = onInternInputs (S.|> new)+        goAll    = onAllInputs    (Set.insert nm)++-- | Add a new user input+addUserInput :: Quantifier -> SV -> Name -> Inputs -> Inputs+addUserInput q sv nm = goAll . goUser+  where new = toNamedSV sv nm+        goUser = onUserInputs (S.|> (q, new)) -- add to the end of the sequence+        goAll  = onAllInputs  (Set.insert nm)++-- | Return user and internal inputs+getInputs :: Inputs -> (UserInputs, InternInps)+getInputs Inputs{userInputs, internInputs} = (userInputs, internInputs)++-- | Find a user-input from its SV+lookupInput :: Eq a => (a -> SV) -> SV -> S.Seq a -> Maybe a+lookupInput f sv ns = res+  where+    i   = getId (swNodeId sv)+    svs = fmap f ns+    res = case S.lookup i ns of -- Nothing on negative Int or Int > length seq+            Nothing    -> secondLookup+            x@(Just e) -> if sv == f e then x else secondLookup+              -- we try the fast lookup first, if the node ids don't match then+              -- we use the more expensive O (n) to find the index and the elem+    secondLookup = S.elemIndexL sv svs >>= flip S.lookup ns++-- | Extract universals+getUniversals :: UserInputs -> S.Seq NamedSymVar+getUniversals = fmap namedSymVar . S.filter ((== ALL) . quantifier)++-- | Get a prefix of the user inputs by a predicate. Note that we could not rely+-- on fusion here but this is cheap and easy until there is an observable slow down from not fusing.+userInpsPrefixBy :: ((Quantifier, NamedSymVar) -> Bool) -> UserInputs -> UserInputs+userInpsPrefixBy = S.takeWhileL++-- | Find prefix existentials, i.e., those that are at skolem positions and have valid model values.+prefixExistentials :: UserInputs -> UserInputs+prefixExistentials = userInpsPrefixBy ((/= ALL) . quantifier)++-- | Find prefix universals. Corresponds to the above in a proof context.+prefixUniversals :: UserInputs -> UserInputs+prefixUniversals = userInpsPrefixBy ((== ALL) . quantifier)++-- | Conversion from named-symvars to user-inputs+inputsFromListWith :: (NamedSymVar -> Quantifier) -> [NamedSymVar] -> UserInputs+inputsFromListWith f = S.fromList . fmap go+  where go n = (f n, n)++-- | Helper functions around inputs.+-- TODO: remove these functions once lists have been pushed to edges of code base.+userInputsToList :: UserInputs -> [(Quantifier, NamedSymVar)]+userInputsToList = F.toList++-- | Conversion from internal-inputs to list of named sym vars+internInputsToList :: InternInps -> [NamedSymVar]+internInputsToList = F.toList++-- | Convert to regular lists+inputsToList :: Inputs -> ([(Quantifier, NamedSymVar)], [NamedSymVar])+inputsToList =  (userInputsToList *** internInputsToList) . getInputs+ -- | The state of the symbolic interpreter data State  = State { pathCond     :: SVal                             -- ^ kind KBool                     , startTime    :: UTCTime                     , runMode      :: IORef SBVRunMode                     , rIncState    :: IORef IncState                     , rCInfo       :: IORef [(String, CV)]-                    , rObservables :: IORef [(String, CV -> Bool, SV)]+                    , rObservables :: IORef (S.Seq (Name, CV -> Bool, SV))                     , rctr         :: IORef Int                     , rUsedKinds   :: IORef KindSet                     , rUsedLbls    :: IORef (Set.Set String)-                    , rinps        :: IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set.Set String) -- First : User defined, with proper quantifiers-                                                                                                           -- Second: Internally declared, always existential-                                                                                                           -- Third : Entire set of names, for faster lookup+                    , rinps        :: IORef Inputs                     , rConstraints :: IORef (S.Seq (Bool, [(String, String)], SV))                     , routs        :: IORef [SV]                     , rtblMap      :: IORef TableMap@@ -1050,8 +1223,9 @@         R.modifyIORef' (field incState) update  -- | Add an observable+-- notice that we cons like a list, we should build at the end of the seq, but cons to preserve semantics for now recordObservable :: State -> String -> (CV -> Bool) -> SV -> IO ()-recordObservable st nm chk sv = modifyState st rObservables ((nm, chk, sv):) (return ())+recordObservable st (T.pack -> nm) chk sv = modifyState st rObservables ((nm, chk, sv) S.<|) (return ())  -- | Increment the variable counter incrementInternalCounter :: State -> IO Int@@ -1096,8 +1270,8 @@                             ++ "      Previously used at: " ++ show t'           | True    = cont -        validChar x = isAlphaNum x || x `elem` "_"-        enclosed    = head nm == '|' && last nm == '|' && length nm > 2 && not (any (`elem` "|\\") (tail (init nm)))+        validChar x = isAlphaNum x || x `elem` ("_" :: String)+        enclosed    = head nm == '|' && last nm == '|' && length nm > 2 && not (any (`elem` ("|\\" :: String)) (tail (init nm)))  -- | Add a new sAssert based constraint addAssertion :: State -> Maybe CallStack -> String -> SV -> IO ()@@ -1111,32 +1285,32 @@ -- Such variables are existentially quantified in a SAT context, and universally quantified -- in a proof context. internalVariable :: State -> Kind -> IO SV-internalVariable st k = do (sv, nm) <- newSV st k+internalVariable st k = do (NamedSymVar sv nm) <- newSV st k                            rm <- readIORef (runMode st)                            let q = case rm of                                      SMTMode  _ _ True  _ -> EX                                      SMTMode  _ _ False _ -> ALL                                      CodeGen              -> ALL                                      Concrete{}           -> ALL-                               n = "__internal_sbv_" ++ nm-                               v = (sv, n)-                           modifyState st rinps (first ((q, v) :) *** Set.insert n)+                               n = "__internal_sbv_" <> nm+                               v = NamedSymVar sv n+                           modifyState st rinps (addUserInput q sv n)                                      $ modifyIncState st rNewInps (\newInps -> case q of                                                                                  EX -> v : newInps                                                                                  -- I don't think the following can actually happen                                                                                  -- but just be safe:                                                                                  ALL  -> noInteractive [ "Internal universally quantified variable creation:"-                                                                                                       , "  Named: " ++ nm+                                                                                                       , "  Named: " <> T.unpack nm                                                                                                        ])                            return sv {-# INLINE internalVariable #-}  -- | Create a new SV-newSV :: State -> Kind -> IO (SV, String)+newSV :: State -> Kind -> IO NamedSymVar newSV st k = do ctr <- incrementInternalCounter st                 let sv = SV k (NodeId ctr)                 registerKind st k-                return (sv, 's' : show ctr)+                return $ NamedSymVar sv $ 's' `T.cons` T.pack (show ctr) {-# INLINE newSV #-}  -- | Register a new kind with the system, used for uninterpreted sorts.@@ -1218,7 +1392,7 @@     -- has the kind we asked for, because the constMap stores the full CV     -- which already has a kind field in it.     Just sv -> return sv-    Nothing -> do (sv, _) <- newSV st (kindOf c)+    Nothing -> do (NamedSymVar sv _) <- newSV st (kindOf c)                   let ins = Map.insert c sv                   modifyState st rconstMap ins $ modifyIncState st rNewConsts ins                   return sv@@ -1248,7 +1422,7 @@      -- get the same expression but at a different type. See      -- <http://github.com/GaloisInc/cryptol/issues/566> as an example.      Just sv | kindOf sv == k -> return sv-     _                        -> do (sv, _) <- newSV st k+     _                        -> do (NamedSymVar sv _) <- newSV st k                                     let append (SBVPgm xs) = SBVPgm (xs S.|> (sv, e))                                     modifyState st spgm append $ modifyIncState st rNewAsgns append                                     modifyState st rexprMap (Map.insert e sv) (return ())@@ -1365,8 +1539,8 @@                                   NonQueryVar mq -> (False, mq)                                   QueryVar       -> (True,  Just EX) -            mkS q = do (sv, internalName) <- newSV st k-                       let nm = fromMaybe internalName mbNm+            mkS q = do (NamedSymVar sv internalName) <- newSV st k+                       let nm = fromMaybe (T.unpack internalName) mbNm                        introduceUserName st (isQueryVar, isTracker) nm k q sv              mkC cv = do registerKind st k@@ -1398,10 +1572,10 @@                          in if isUserSort k                            then bad ("Cannot validate models in the presence of user defined kinds, saw: " ++ show k) cant-                           else do (sv, internalName) <- newSV st k+                           else do (NamedSymVar sv internalName) <- newSV st k -                                   let nm = fromMaybe internalName mbNm-                                       nsv = (sv, nm)+                                   let nm = fromMaybe (T.unpack internalName) mbNm+                                       nsv = toNamedSV' sv nm                                         cv = case [(q, v) | ((q, nsv'), v) <- env, nsv == nsv'] of                                               []              -> if isTracker@@ -1416,7 +1590,7 @@                                                                  -- we'd have to validate for each possible value. But that's more or less useless. Instead,                                                                  -- just issue a warning and use 0 for this value.                                                                  mkConstCV k (0::Integer)-                                              [(EX, Nothing)] -> bad ("Cannot locate model value of variable: " ++ show (snd nsv)) report+                                              [(EX, Nothing)] -> bad ("Cannot locate model value of variable: " ++ show (getUserName' nsv)) report                                               [(EX, Just c)]  -> c                                               r               -> bad (   "Found multiple matching values for variable: " ++ show nsv                                                                       ++ "\n*** " ++ show r) report@@ -1426,9 +1600,9 @@ -- | Introduce a new user name. We simply append a suffix if we have seen this variable before. introduceUserName :: State -> (Bool, Bool) -> String -> Kind -> Quantifier -> SV -> IO SVal introduceUserName st@State{runMode} (isQueryVar, isTracker) nmOrig k q sv = do-        (_, old) <- readIORef (rinps st)+        old <- allInputs <$> readIORef (rinps st) -        let nm  = mkUnique nmOrig old+        let nm  = mkUnique (T.pack nmOrig) old          -- If this is not a query variable and we're in a query, reject it.         -- See https://github.com/LeventErkok/sbv/issues/554 for the rationale.@@ -1447,7 +1621,7 @@         if isTracker && q == ALL            then error $ "SBV: Impossible happened! A universally quantified tracker variable is being introduced: " ++ show nm            else do let newInp olds = case q of-                                      EX  -> (sv, nm) : olds+                                      EX  -> toNamedSV sv nm : olds                                       ALL -> noInteractive [ "Adding a new universally quantified variable: "                                                            , "  Name      : " ++ show nm                                                            , "  Kind      : " ++ show k@@ -1456,16 +1630,17 @@                                                            , "Only existential variables are supported in query mode."                                                            ]                    if isTracker-                      then modifyState st rinps (second ((sv, nm) :) *** Set.insert nm)+                      then modifyState st rinps (addInternInput sv nm)                                      $ noInteractive ["Adding a new tracker variable in interactive mode: " ++ show nm]-                      else modifyState st rinps (first ((q, (sv, nm)) :) *** Set.insert nm)+                      else modifyState st rinps (addUserInput q sv nm)                                      $ modifyIncState st rNewInps newInp                    return $ SVal k $ Right $ cache (const (return sv))     where -- The following can be rather slow if we keep reusing the same prefix, but I doubt it'll be a problem in practice          -- Also, the following will fail if we span the range of integers without finding a match, but your computer would          -- die way ahead of that happening if that's the case!-         mkUnique prefix names = head $ dropWhile (`Set.member` names) (prefix : [prefix ++ "_" ++ show i | i <- [(0::Int)..]])+         mkUnique :: T.Text -> Set.Set Name -> T.Text+         mkUnique prefix names = head $ dropWhile (`Set.member` names) (prefix : [prefix <> "_" <> T.pack (show i) | i <- [(0::Int)..]])  -- | Generalization of 'Data.SBV.runSymbolic' runSymbolic :: MonadIO m => SBVRunMode -> SymbolicT m a -> m (a, Result)@@ -1475,11 +1650,11 @@      rm        <- newIORef currentRunMode      ctr       <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements      cInfo     <- newIORef []-     observes  <- newIORef []+     observes  <- newIORef mempty      pgm       <- newIORef (SBVPgm S.empty)      emap      <- newIORef Map.empty      cmap      <- newIORef Map.empty-     inps      <- newIORef (([], []), Set.empty)+     inps      <- newIORef mempty      outs      <- newIORef []      tables    <- newIORef Map.empty      arrays    <- newIORef IMap.empty@@ -1547,14 +1722,16 @@                                        , rObservables=observes                                        } = do    SBVPgm rpgm  <- readIORef pgm-   inpsO <- (reverse *** reverse) . fst <$> readIORef inps+   inpsO <- inputsToList <$> readIORef inps    outsO <- reverse <$> readIORef outs     let swap  (a, b)              = (b, a)        cmp   (a, _) (b, _)       = a `compare` b        arrange (i, (at, rt, es)) = ((i, at, rt), es) -   cnsts <- sortBy cmp . map swap . Map.toList <$> readIORef (rconstMap st)+   constMap <- readIORef (rconstMap st)+   let cnsts = sortBy cmp . map swap . Map.toList $ constMap+    tbls  <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef tables    arrs  <- IMap.toAscList <$> readIORef arrays    unint <- Map.toList <$> readIORef uis@@ -1563,11 +1740,12 @@    cgMap <- Map.toList <$> readIORef cgs     traceVals   <- reverse <$> readIORef cInfo-   observables <- reverse <$> readIORef observes+   observables <- reverse . fmap (\(n,f,sv) -> (T.unpack n, f, sv)) . F.toList+                  <$> readIORef observes    extraCstrs  <- readIORef cstrs    assertions  <- reverse <$> readIORef asserts -   return $ Result knds traceVals observables cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO+   return $ Result knds traceVals observables cgMap inpsO (constMap, cnsts) tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO  -- | Generalization of 'Data.SBV.addNewSMTOption' addNewSMTOption :: MonadSymbolic m => SMTOption -> m ()@@ -1621,7 +1799,7 @@                             walk (Maximize          nm v)     = Maximize nm                     <$> mkGoal nm v                             walk (AssertWithPenalty nm v mbP) = flip (AssertWithPenalty nm) mbP <$> mkGoal nm v -                        obj' <- walk obj+                        !obj' <- walk obj                         liftIO $ modifyState st rOptGoals (obj' :)                                            $ noInteractive [ "Adding an optimization objective:"                                                            , "  Objective: " ++ show obj@@ -1733,6 +1911,9 @@   rnf _ = () #endif +instance NFData NamedSymVar where+  rnf (NamedSymVar s n) = rnf s `seq` rnf n+ instance NFData Result where   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@@ -1831,7 +2012,7 @@        , allSatMaxModelCount         :: Maybe Int      -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all.        , allSatPrintAlong            :: Bool           -- ^ In a 'Data.SBV.allSat' call, print models as they are found.        , satTrackUFs                 :: Bool           -- ^ In a 'Data.SBV.sat' call, should we try to extract values of uninterpreted functions?-       , isNonModelVar               :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)+       , isNonModelVar               :: T.Text -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)        , validateModel               :: Bool           -- ^ If set, SBV will attempt to validate the model it gets back from the solver.        , optimizeValidateConstraints :: Bool           -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.        , transcript                  :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)@@ -1896,13 +2077,13 @@                -> IO res  -- | Solvers that SBV is aware of-data Solver = Z3-            | Yices-            | DReal+data Solver = ABC             | Boolector             | CVC4+            | DReal             | MathSAT-            | ABC+            | Yices+            | Z3             deriving (Show, Enum, Bounded)  -- | An SMT solver
Data/SBV/Either.hs view
@@ -182,7 +182,7 @@ second = bimap id  -- | Return the value from the left component. The behavior is undefined if--- passed a right value.+-- passed a right value, i.e., it can return any value. -- -- >>> fromLeft (sLeft (literal 'a') :: SEither Char Integer) -- 'a' :: SChar@@ -190,7 +190,7 @@ -- Q.E.D. -- >>> sat $ \x -> x .== (fromLeft (sRight 4 :: SEither Char Integer)) -- Satisfiable. Model:---   s0 = '\NUL' :: Char+--   s0 = 'A' :: Char -- -- Note how we get a satisfying assignment in the last case: The behavior -- is unspecified, thus the SMT solver picks whatever satisfies the@@ -227,7 +227,7 @@                     return e  -- | Return the value from the right component. The behavior is undefined if--- passed a left value.+-- passed a left value, i.e., it can return any value. -- -- >>> fromRight (sRight (literal 'a') :: SEither Integer Char) -- 'a' :: SChar
Data/SBV/List.hs view
@@ -130,7 +130,7 @@ -- Q.E.D. -- >>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1) -- Satisfiable. Model:---   s0 = [0,0,8] :: [Word16]+--   s0 = [0,0,16384] :: [Word16] listToListAt :: SymVal a => SList a -> SInteger -> SList a listToListAt s offset = subList s offset 1
Data/SBV/Maybe.hs view
@@ -99,7 +99,7 @@ fromMaybe def = maybe def id  -- | Return the value of an optional value. The behavior is undefined if--- passed Nothing. Compare to 'fromMaybe'.+-- passed Nothing, i.e., it can return any value. Compare to 'fromMaybe'. -- -- >>> fromJust (sJust (literal 'a')) -- 'a' :: SChar@@ -107,7 +107,7 @@ -- Q.E.D. -- >>> sat $ \x -> x .== (fromJust sNothing :: SChar) -- Satisfiable. Model:---   s0 = '\NUL' :: Char+--   s0 = 'A' :: Char -- -- Note how we get a satisfying assignment in the last case: The behavior -- is unspecified, thus the SMT solver picks whatever satisfies the
Data/SBV/Provers/Boolector.hs view
@@ -18,7 +18,7 @@  -- | The description of the Boolector SMT solver -- The default executable is @\"boolector\"@, which must be in your path. You can use the @SBV_BOOLECTOR@ environment variable to point to the executable on your system.--- The default options are @\"-m --smt2\"@. You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options.+-- You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options. boolector :: SMTSolver boolector = SMTSolver {            name         = Boolector@@ -42,7 +42,7 @@                               , supportsOptimization       = False                               , supportsPseudoBooleans     = False                               , supportsCustomQueries      = True-                              , supportsGlobalDecls        = False+                              , supportsGlobalDecls        = True                               , supportsDataTypes          = False                               , supportsDirectAccessors    = False                               , supportsFlattenedModels    = Nothing
Data/SBV/Provers/CVC4.hs view
@@ -22,7 +22,7 @@  -- | The description of the CVC4 SMT solver -- The default executable is @\"cvc4\"@, which must be in your path. You can use the @SBV_CVC4@ environment variable to point to the executable on your system.--- The default options are @\"--lang smt\"@. You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options.+-- You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options. cvc4 :: SMTSolver cvc4 = SMTSolver {            name         = CVC4
Data/SBV/Provers/MathSAT.hs view
@@ -22,7 +22,7 @@  -- | The description of the MathSAT SMT solver -- The default executable is @\"mathsat\"@, which must be in your path. You can use the @SBV_MATHSAT@ environment variable to point to the executable on your system.--- The default options are @\"-input=smt2\"@. You can use the @SBV_MATHSAT_OPTIONS@ environment variable to override the options.+-- You can use the @SBV_MATHSAT_OPTIONS@ environment variable to override the options. mathSAT :: SMTSolver mathSAT = SMTSolver {            name         = MathSAT
Data/SBV/Provers/Prover.hs view
@@ -31,7 +31,7 @@        , runSMT, runSMTWith        , SatModel(..), Modelable(..), displayModels, extractModels        , getModelDictionaries, getModelValues, getModelUninterpretedValues-       , boolector, cvc4, yices, dReal, z3, mathSAT, abc, defaultSMTCfg, defaultDeltaSMTCfg+       , abc, boolector, cvc4, dReal, mathSAT, yices, z3, defaultSMTCfg, defaultDeltaSMTCfg        ) where  @@ -54,6 +54,7 @@  import qualified Data.Map.Strict as M import qualified Data.Foldable   as S (toList)+import qualified Data.Text       as T  import Data.SBV.Core.Data import Data.SBV.Core.Symbolic@@ -68,13 +69,13 @@  import GHC.Stack -import qualified Data.SBV.Provers.Boolector  as Boolector-import qualified Data.SBV.Provers.CVC4       as CVC4-import qualified Data.SBV.Provers.Yices      as Yices-import qualified Data.SBV.Provers.DReal      as DReal-import qualified Data.SBV.Provers.Z3         as Z3-import qualified Data.SBV.Provers.MathSAT    as MathSAT-import qualified Data.SBV.Provers.ABC        as ABC+import qualified Data.SBV.Provers.ABC       as ABC+import qualified Data.SBV.Provers.Boolector as Boolector+import qualified Data.SBV.Provers.CVC4      as CVC4+import qualified Data.SBV.Provers.DReal     as DReal+import qualified Data.SBV.Provers.MathSAT   as MathSAT+import qualified Data.SBV.Provers.Yices     as Yices+import qualified Data.SBV.Provers.Z3        as Z3  mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig mkConfig s smtVersion startOpts = SMTConfig { verbose                     = False@@ -105,6 +106,10 @@ allOnStdOut :: Control.SMTOption allOnStdOut = Control.DiagnosticOutputChannel "stdout" +-- | Default configuration for the ABC synthesis and verification tool.+abc :: SMTConfig+abc = mkConfig ABC.abc SMTLib2 [allOnStdOut]+ -- | Default configuration for the Boolector SMT solver boolector :: SMTConfig boolector = mkConfig Boolector.boolector SMTLib2 []@@ -114,28 +119,24 @@ cvc4 = mkConfig CVC4.cvc4 SMTLib2 [allOnStdOut]  -- | Default configuration for the Yices SMT Solver.-yices :: SMTConfig-yices = mkConfig Yices.yices SMTLib2 []---- | Default configuration for the Yices SMT Solver. dReal :: SMTConfig dReal = mkConfig DReal.dReal SMTLib2 [ Control.OptionKeyword ":smtlib2_compliant" ["true"]                                      ] +-- | Default configuration for the MathSAT SMT solver+mathSAT :: SMTConfig+mathSAT = mkConfig MathSAT.mathSAT SMTLib2 [allOnStdOut]++-- | Default configuration for the Yices SMT Solver.+yices :: SMTConfig+yices = mkConfig Yices.yices SMTLib2 []+ -- | Default configuration for the Z3 SMT solver z3 :: SMTConfig z3 = mkConfig Z3.z3 SMTLib2 [ Control.OptionKeyword ":smtlib2_compliant" ["true"]                             , allOnStdOut                             ] --- | Default configuration for the MathSAT SMT solver-mathSAT :: SMTConfig-mathSAT = mkConfig MathSAT.mathSAT SMTLib2 [allOnStdOut]---- | Default configuration for the ABC synthesis and verification tool.-abc :: SMTConfig-abc = mkConfig ABC.abc SMTLib2 [allOnStdOut]- -- | The default solver used by SBV. This is currently set to z3. defaultSMTCfg :: SMTConfig defaultSMTCfg = z3@@ -276,21 +277,19 @@                                           ]  -                   let universals = [s | (ALL, s) <- qinps]+                   let universals = S.toList $ getUniversals qinps                         firstUniversal                          | null universals = error "Data.SBV: Impossible happened! Universal optimization with no universals!"-                         | True            = minimum (map (nodeId . fst) universals)--                       nodeId (SV _ n) = n+                         | True            = minimum $ fmap (swNodeId . getSV) universals                         mappings :: M.Map SV SBVExpr                        mappings = M.fromList (S.toList (pgmAssignments spgm)) -                       chaseUniversal entry = map snd $ go entry []+                       chaseUniversal entry = go entry []                          where go x sofar                                 | nx >= firstUniversal-                                = nub $ [unm | unm@(u, _) <- universals, nx >= nodeId u] ++ sofar+                                = nub $ [unm | unm <- universals, nx >= swNodeId (getSV unm)] ++ sofar                                 | True                                 = let oVars (LkUp _ a b)             = [a, b]                                       oVars (IEEEFP (FP_Cast _ _ o)) = [o]@@ -299,7 +298,7 @@                                                Nothing            -> []                                                Just (SBVApp o ss) -> nub (oVars o ++ ss)                                   in foldr go sofar vars-                                where nx = nodeId x+                                where nx = swNodeId x                     let needsUniversalOpt = let tag _  [] = Nothing                                                tag nm xs = Just (nm, xs)@@ -315,7 +314,7 @@                                                , "*** Data.SBV: Problem needs optimization of metric in the scope of universally quantified variable(s):"                                                , "***"                                                ]-                                           ++  [ "***          " ++  pad s ++ " [Depends on: " ++ intercalate ", " xs ++ "]"  | (s, xs) <- needsUniversalOpt ]+                                           ++  [ "***          " ++  pad s ++ " [Depends on: " ++ intercalate ", " (getUserName' <$> xs) ++ "]"  | (s, xs) <- needsUniversalOpt ]                                            ++  [ "***"                                                , "*** Optimization is only meaningful with existentially quantified metrics."                                                ]@@ -417,9 +416,9 @@                                                      , "Unable to validate the produced model."                                                      ]) (Just res) -          check env = do let univs    = [n | ((ALL, (_, n)), _) <- env]+          check env = do let univs    = [T.unpack n | ((ALL, NamedSymVar _ n), _) <- env]                              envShown = showModelDictionary True True cfg modelBinds-                                where modelBinds = [(n, fake q s v) | ((q, (s, n)), v) <- env]+                                where modelBinds = [(T.unpack n, fake q s v) | ((q, NamedSymVar s n), v) <- env]                                       fake q s Nothing                                         | q == ALL                                         = RegularCV $ CV (kindOf s) $ CUserSort (Nothing, "<universally quantified>")
Data/SBV/Provers/Yices.hs view
@@ -20,7 +20,7 @@  -- | The description of the Yices SMT solver -- The default executable is @\"yices-smt2\"@, which must be in your path. You can use the @SBV_YICES@ environment variable to point to the executable on your system.--- SBV does not pass any arguments to yices. You can use the @SBV_YICES_OPTIONS@ environment variable to override the options.+-- You can use the @SBV_YICES_OPTIONS@ environment variable to override the options. yices :: SMTSolver yices = SMTSolver {            name         = Yices@@ -44,7 +44,7 @@                               , supportsOptimization       = False                               , supportsPseudoBooleans     = False                               , supportsCustomQueries      = True-                              , supportsGlobalDecls        = False+                              , supportsGlobalDecls        = True                               , supportsDataTypes          = False                               , supportsDirectAccessors    = False                               , supportsFlattenedModels    = Nothing
Data/SBV/Provers/Z3.hs view
@@ -20,7 +20,7 @@  -- | The description of the Z3 SMT solver. -- The default executable is @\"z3\"@, which must be in your path. You can use the @SBV_Z3@ environment variable to point to the executable on your system.--- The default options are @\"-nw -in -smt2\"@. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options.+-- You can use the @SBV_Z3_OPTIONS@ environment variable to override the options. z3 :: SMTSolver z3 = SMTSolver {            name         = Z3
Data/SBV/RegExp.hs view
@@ -73,9 +73,6 @@ -- >>> :set -XScopedTypeVariables  -- | Matchable class. Things we can match against a 'RegExp'.--- (TODO: Currently SBV does *not* optimize this call if the input is a concrete string or--- a character, but rather directly calls down to the solver. We might want to perform the--- operation on the Haskell side for performance reasons, should this become important.) -- -- For instance, you can generate valid-looking phone numbers like this: --@@ -87,7 +84,7 @@ -- >>> let phone = pre * "-" * post -- >>> sat $ \s -> (s :: SString) `match` phone -- Satisfiable. Model:---   s0 = "100-8000" :: String+--   s0 = "388-3826" :: String class RegExpMatchable a where    -- | @`match` s r@ checks whether @s@ is in the language generated by @r@.    match :: a -> RegExp -> SBool@@ -141,7 +138,7 @@ -- -- >>> newline -- (re.union (str.to.re "\n") (str.to.re "\r") (str.to.re "\f"))--- >>> prove $ \c -> c `match` newline .=> isSpace c+-- >>> prove $ \c -> c `match` newline .=> isSpaceL1 c -- Q.E.D. newline :: RegExp newline = oneOf "\n\r\f"@@ -149,44 +146,38 @@ -- | Recognize a tab. -- -- >>> tab--- (str.to.re "\x09")+-- (str.to.re "\t") -- >>> prove $ \c -> c `match` tab .=> c .== literal '\t' -- Q.E.D. tab :: RegExp tab = oneOf "\t" +-- | Lift a char function to a regular expression that recognizes it.+liftPredL1 :: (Char -> Bool) -> RegExp+liftPredL1 predicate = oneOf $ filter predicate (map C.chr [0 .. 255])+ -- | Recognize white-space, but without a new line. ----- >>> whiteSpaceNoNewLine--- (re.union (str.to.re "\x09") (re.union (str.to.re "\v") (str.to.re "\xa0") (str.to.re " "))) -- >>> prove $ \c -> c `match` whiteSpaceNoNewLine .=> c `match` whiteSpace .&& c ./= literal '\n' -- Q.E.D. whiteSpaceNoNewLine :: RegExp-whiteSpaceNoNewLine = tab + oneOf "\v\160 "+whiteSpaceNoNewLine = liftPredL1 (\c -> C.isSpace c && c `P.notElem` ("\n" :: String))  -- | Recognize white space. ----- >>> prove $ \c -> c `match` whiteSpace .=> isSpace c+-- >>> prove $ \c -> c `match` whiteSpace .=> isSpaceL1 c -- Q.E.D. whiteSpace :: RegExp-whiteSpace = newline + whiteSpaceNoNewLine+whiteSpace = liftPredL1 C.isSpace --- | Recognize a punctuation character. Anything that satisfies the predicate 'isPunctuation' will--- be accepted.  (TODO: Will need modification when we move to unicode.)+-- | Recognize a punctuation character. ----- >>> prove $ \c -> c `match` punctuation .=> isPunctuation c+-- >>> prove $ \c -> c `match` punctuation .=> isPunctuationL1 c -- Q.E.D. punctuation :: RegExp-punctuation = oneOf $ filter C.isPunctuation $ map C.chr [0..255]+punctuation = liftPredL1 C.isPunctuation  -- | Recognize an alphabet letter, i.e., @A@..@Z@, @a@..@z@.------ >>> asciiLetter--- (re.union (re.range "a" "z") (re.range "A" "Z"))--- >>> prove $ \c -> c `match` asciiLetter .<=> toUpper c `match` asciiLetter--- Q.E.D.--- >>> prove $ \c -> c `match` asciiLetter .<=> toLower c `match` asciiLetter--- Q.E.D. asciiLetter :: RegExp asciiLetter = asciiLower + asciiUpper @@ -196,9 +187,9 @@ -- (re.range "a" "z") -- >>> prove $ \c -> (c :: SChar) `match` asciiLower  .=> c `match` asciiLetter -- Q.E.D.--- >>> prove $ \c -> c `match` asciiLower  .=> toUpper c `match` asciiUpper+-- >>> prove $ \c -> c `match` asciiLower  .=> toUpperL1 c `match` asciiUpper -- Q.E.D.--- >>> prove $ \c -> c `match` asciiLetter .=> toLower c `match` asciiLower+-- >>> prove $ \c -> c `match` asciiLetter .=> toLowerL1 c `match` asciiLower -- Q.E.D. asciiLower :: RegExp asciiLower = Range 'a' 'z'@@ -209,9 +200,9 @@ -- (re.range "A" "Z") -- >>> prove $ \c -> (c :: SChar) `match` asciiUpper  .=> c `match` asciiLetter -- Q.E.D.--- >>> prove $ \c -> c `match` asciiUpper  .=> toLower c `match` asciiLower+-- >>> prove $ \c -> c `match` asciiUpper  .=> toLowerL1 c `match` asciiLower -- Q.E.D.--- >>> prove $ \c -> c `match` asciiLetter .=> toUpper c `match` asciiUpper+-- >>> prove $ \c -> c `match` asciiLetter .=> toUpperL1 c `match` asciiUpper -- Q.E.D. asciiUpper :: RegExp asciiUpper = Range 'A' 'Z'@@ -313,7 +304,7 @@  -- | Quiet GHC about testing only imports __unused :: a-__unused = undefined isSpace length take elem notElem head+__unused = undefined isSpaceL1 length take elem notElem head  {- $matching A symbolic string or a character ('SString' or 'SChar') can be matched against a regular-expression. Note
Data/SBV/SMT/SMT.hs view
@@ -12,8 +12,10 @@ {-# LANGUAGE DefaultSignatures          #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE NamedFieldPuns             #-}+{-# LANGUAGE OverloadedStrings          #-} {-# LANGUAGE Rank2Types                 #-} {-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE ViewPatterns               #-}  {-# OPTIONS_GHC -Wall -Werror #-} @@ -59,6 +61,7 @@ import System.Process     (runInteractiveProcess, waitForProcess, terminateProcess)  import qualified Data.Map.Strict as M+import qualified Data.Text       as T  import Data.SBV.Core.AlgReals import Data.SBV.Core.Data@@ -531,9 +534,9 @@   where warn s = if warnEmpty then s else ""          relevantVars  = filter (not . ignore) allVars-        ignore (s, _)+        ignore (T.pack -> s, _)           | includeEverything = False-          | True              = "__internal_sbv_" `isPrefixOf` s || isNonModelVar cfg s+          | True              = "__internal_sbv_" `T.isPrefixOf` s || isNonModelVar cfg s          shM (s, RegularCV v) = let vs = shCV cfg v in ((length s, s), (vlength vs, vs))         shM (s, other)       = let vs = show other in ((length s, s), (vlength vs, vs))@@ -964,7 +967,7 @@                                   , ";;;"                                   , ";;;           Solver    : " ++ show name                                   , ";;;           Executable: " ++ fromMaybe "Unable to locate the executable" mbPath-                                  , ";;;           Options   : " ++ unwords (options cfg)+                                  , ";;;           Options   : " ++ unwords (options cfg ++ extraArgs cfg)                                   , ";;;"                                   , ";;; This file is an auto-generated loadable SMT-Lib file."                                   , ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
Data/SBV/SMT/SMTLib2.hs view
@@ -11,6 +11,7 @@  {-# LANGUAGE PatternGuards       #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns        #-}  {-# OPTIONS_GHC -Wall -Werror #-} @@ -27,7 +28,7 @@ import qualified Data.Set             as Set  import Data.SBV.Core.Data-import Data.SBV.Core.Symbolic (QueryContext(..), SetOp(..), OvOp(..))+import Data.SBV.Core.Symbolic (QueryContext(..), SetOp(..), OvOp(..), CnstMap, getUserName', getSV, regExpToSMTString) import Data.SBV.Core.Kind (smtType, needsFlattening) import Data.SBV.SMT.Utils import Data.SBV.Control.Types@@ -41,7 +42,7 @@  -- | Translate a problem into an SMTLib2 script cvt :: SMTLibConverter [String]-cvt ctx kindInfo isSat comments (inputs, trackerVars) skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out cfg = pgm+cvt ctx kindInfo isSat comments (inputs, trackerVars) skolemInps (allConsts, consts) tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out cfg = pgm   where hasInteger     = KUnbounded `Set.member` kindInfo         hasReal        = KReal      `Set.member` kindInfo         hasFloat       = KFloat     `Set.member` kindInfo@@ -49,7 +50,7 @@         hasChar        = KChar      `Set.member` kindInfo         hasDouble      = KDouble    `Set.member` kindInfo         hasRounding    = not $ null [s | (s, _) <- usorts, s == "RoundingMode"]-        hasBVs         = hasChar || not (null [() | KBounded{} <- Set.toList kindInfo])   -- Remember, characters map to Word8+        hasBVs         = not (null [() | KBounded{} <- Set.toList kindInfo])         usorts         = [(s, dt) | KUserSort s dt <- Set.toList kindInfo]         trueUSorts     = [s | (s, _) <- usorts, s /= "RoundingMode"]         tupleArities   = findTupleArities kindInfo@@ -118,6 +119,7 @@            | hasMaybe              = setAll "has maybe type"            | hasSets               = setAll "has sets"            | hasList               = setAll "has lists"+           | hasChar               = setAll "has chars"            | hasString             = setAll "has strings"            | hasArrayInits         = setAll "has array initializers"            | hasOverflows          = setAll "has overflow checks"@@ -180,9 +182,9 @@              ++ [ "; --- literal constants ---" ]              ++ concatMap (declConst cfg) consts              ++ [ "; --- skolem constants ---" ]-             ++ [ "(declare-fun " ++ show s ++ " " ++ svFunType ss s ++ ")" ++ userName s | Right (s, ss) <- skolemInps]+             ++ concat [declareFun s (SBVType (map kindOf (ss ++ [s]))) (userName s) | Right (s, ss) <- skolemInps]              ++ [ "; --- optimization tracker variables ---" | not (null trackerVars) ]-             ++ [ "(declare-fun " ++ show s ++ " " ++ svFunType [] s ++ ") ; tracks " ++ nm | (s, nm) <- trackerVars]+             ++ concat [declareFun s (SBVType [kindOf s]) (Just ("tracks " <> nm)) | var <- trackerVars, let s = getSV var, let nm = getUserName' var]              ++ [ "; --- constant tables ---" ]              ++ concatMap (uncurry (:) . constTable) constTables              ++ [ "; --- skolemized tables ---" ]@@ -230,7 +232,7 @@          (constTables, skolemTables) = ([(t, d) | (t, Left d) <- allTables], [(t, d) | (t, Right d) <- allTables])         allTables = [(t, genTableData rm skolemMap (not (null foralls), forallArgs) (map fst consts) t) | t <- tbls]-        (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray cfg (not (null foralls)) consts skolemMap) arrs+        (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray cfg (not (null foralls)) allConsts skolemMap) arrs         delayedEqualities = concatMap snd skolemTables          delayedAsserts []              = []@@ -322,10 +324,10 @@         mkLet (s, SBVApp (Label m) [e]) = "(let ((" ++ show s ++ " " ++ cvtSV                skolemMap          e ++ ")) ; " ++ m         mkLet (s, e)                    = "(let ((" ++ show s ++ " " ++ cvtExp solverCaps rm skolemMap tableMap e ++ "))" -        userNameMap = M.fromList (map snd inputs)+        userNameMap = M.fromList $ map ((\nSymVar -> (getSV nSymVar, getUserName' nSymVar)) . snd) inputs         userName s = case M.lookup s userNameMap of-                        Just u  | show s /= u -> " ; tracks user variable " ++ show u-                        _ -> ""+                        Just u  | show s /= u -> Just $ "tracks user variable " ++ show u+                        _ -> Nothing  -- | Declare new sorts declSort :: (String, Maybe [String]) -> [String]@@ -403,7 +405,7 @@ -- for a list of what we include, in case something doesn't show up -- and you need it! cvtInc :: SMTLibIncConverter [String]-cvtInc inps newKs consts arrs tbls uis (SBVPgm asgnsSeq) cstrs cfg =+cvtInc inps newKs (allConsts, consts) arrs tbls uis (SBVPgm asgnsSeq) cstrs cfg =             -- any new settings?                settings             -- sorts@@ -416,7 +418,7 @@             -- constants             ++ concatMap (declConst cfg) consts             -- inputs-            ++ map declInp inps+            ++ concatMap declInp inps             -- arrays             ++ concat arrayConstants             -- uninterpreteds@@ -441,9 +443,9 @@          newKinds = Set.toList newKs -        declInp (s, _) = "(declare-fun " ++ show s ++ " () " ++ svType s ++ ")"+        declInp (getSV -> s) = declareFun s (SBVType [kindOf s]) Nothing -        (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray cfg False consts skolemMap) arrs+        (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray cfg False allConsts skolemMap) arrs          allTables = [(t, either id id (genTableData rm skolemMap (False, []) (map fst consts) t)) | t <- tbls]         (tableDecls, tableAssigns) = unzip $ map constTable allTables@@ -488,7 +490,7 @@   = defineFun cfg (s, cvtCV (roundingMode cfg) c) Nothing  declUI :: (String, SBVType) -> [String]-declUI (i, t) = ["(declare-fun " ++ i ++ " " ++ cvtType t ++ ")"]+declUI (i, t) = declareName i t Nothing  -- NB. We perform no check to as to whether the axiom is meaningful in any way. declAx :: (String, [String]) -> String@@ -545,9 +547,11 @@ -- we might have to skolemize those. Implement this properly. -- The difficulty is with the Mutate/Merge: We have to postpone an init if -- the components are themselves postponed, so this cannot be implemented as a simple map.-declArray :: SMTConfig -> Bool -> [(SV, CV)] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String])+declArray :: SMTConfig -> Bool -> CnstMap -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String]) declArray cfg quantified consts skolemMap (i, (_, (aKnd, bKnd), ctx)) = (adecl : zipWith wrap [(0::Int)..] (map snd pre), zipWith wrap [lpre..] (map snd post), setup)-  where constNames = map fst consts+  where constMapping = M.fromList [(s, c) | (c, s) <- M.assocs consts]+        constNames   = M.keys constMapping+         topLevel = not quantified || case ctx of                                        ArrayFree mbi      -> maybe True (`elem` constNames) mbi                                        ArrayMutate _ a b  -> all (`elem` constNames) [a, b]@@ -565,11 +569,14 @@          adecl = case ctx of                   ArrayFree (Just v) -> "(define-fun "  ++ nm ++ " () " ++ atyp ++ " ((as const " ++ atyp ++ ") " ++ constInit v ++ "))"+                  ArrayFree Nothing+                    | bKnd == KChar  ->  -- Can't support yet, because we need to make sure all the elements are length-1 strings. So, punt for now.+                                         tbd "Free array declarations containing SChars"                   _                  -> "(declare-fun " ++ nm ++ " () " ++ atyp ++                                                  ")"          -- CVC4 chokes if the initializer is not a constant. (Z3 is ok with it.) So, print it as         -- a constant if we have it in the constants; otherwise, we merely print it and hope for the best.-        constInit v = case v `lookup` consts of+        constInit v = case v `M.lookup` constMapping of                         Nothing -> ssv v                      -- Z3 will work, CVC4 will choke. Others don't even support this.                         Just c  -> cvtCV (roundingMode cfg) c -- Z3 and CVC4 will work. Other's don't support this. @@ -716,9 +723,11 @@           = let idx v = "(" ++ s ++ "_constrIndex " ++ v ++ ")" in "(" ++ o ++ " " ++ idx a ++ " " ++ idx b ++ ")"         unintComp o sbvs = error $ "SBV.SMT.SMTLib2.sh.unintComp: Unexpected arguments: "   ++ show (o, sbvs, map kindOf arguments) -        -- NB. String comparisons are currently not supported by Z3; but will be with the new logic.+        stringOrChar KString = True+        stringOrChar KChar   = True+        stringOrChar _       = False         stringCmp swap o [a, b]-          | KString <- kindOf (head arguments)+          | stringOrChar (kindOf (head arguments))           = let [a1, a2] | swap = [b, a]                          | True = [a, b]             in "(" ++ o ++ " " ++ a1 ++ " " ++ a2 ++ ")"@@ -857,7 +866,9 @@         sh (SBVApp (OverflowOp op) args) = "(not (" ++ show op ++ " " ++ unwords (map ssv args) ++ "))"          -- Note the unfortunate reversal in StrInRe..-        sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in.re " ++ unwords (map ssv args) ++ " " ++ show r ++ ")"+        sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in.re " ++ unwords (map ssv args) ++ " " ++ regExpToSMTString r ++ ")"+        -- StrUnit is no-op, since a character in SMTLib is the same as a string+        sh (SBVApp (StrOp StrUnit)     [a])  = ssv a         sh (SBVApp (StrOp op)          args) = "(" ++ show op ++ " " ++ unwords (map ssv args) ++ ")"          sh (SBVApp (SeqOp op) args) = "(" ++ show op ++ " " ++ unwords (map ssv args) ++ ")"@@ -901,9 +912,7 @@           = f (any hasSign args) (map ssv args)           | floatOp || doubleOp, Just f <- lookup op smtOpFloatDoubleTable           = f (any hasSign args) (map ssv args)-          | charOp, Just f <- lookup op smtCharTable-          = f False (map ssv args)-          | stringOp, Just f <- lookup op smtStringTable+          | charOp || stringOp, Just f <- lookup op smtStringTable           = f (map ssv args)           | listOp, Just f <- lookup op smtListTable           = f (map ssv args)@@ -982,16 +991,6 @@                                      , (GreaterEq,   unintComp ">=")                                      ] -                -- For chars, the underlying type is currently SWord8, so we go with the regular bit-vector operations-                -- TODO: This will change when we move to unicode!-                smtCharTable = [ (Equal,         eqBV)-                               , (NotEqual,      neqBV)-                               , (LessThan,      lift2S  "bvult" (error "smtChar.<: did-not expect signed char here!"))-                               , (GreaterThan,   lift2S  "bvugt" (error "smtChar.>: did-not expect signed char here!"))-                               , (LessEq,        lift2S  "bvule" (error "smtChar.<=: did-not expect signed char here!"))-                               , (GreaterEq,     lift2S  "bvuge" (error "smtChar.>=: did-not expect signed char here!"))-                               ]-                 -- For strings, equality and comparisons are the only operators                 -- TODO: The string comparison operators will most likely change with the new theory!                 smtStringTable = [ (Equal,       lift2S "="        "="        True)@@ -1011,6 +1010,86 @@                                , (LessEq,      seqCmp False "seq.<=")                                , (GreaterEq,   seqCmp True  "seq.<=")                                ]++declareFun :: SV -> SBVType -> Maybe String -> [String]+declareFun = declareName . show++declareName :: String -> SBVType -> Maybe String -> [String]+declareName s t@(SBVType inputKS) mbCmnt = decl : restrict+  where decl        = "(declare-fun " ++ s ++ " " ++ cvtType t ++ ")" ++ maybe "" (" ; " ++) mbCmnt++        (args, result) = case inputKS of+                          [] -> error $ "SBV.declareName: Unexpected empty type for: " ++ show s+                          _  -> (init inputKS, last inputKS)++        -- Does the kind KChar *not* occur in the kind anywhere?+        charFree k = null [() | KChar <- G.universe k]+        noChars    = charFree result+        needsQuant = not $ null args++        resultVar | needsQuant = "result"+                  | True       = s++        argList   = ["a" ++ show i | (i, _) <- zip [1::Int ..] args]+        argTList  = ["(" ++ a ++ " " ++ smtType k ++ ")" | (a, k) <- zip argList args]+        resultExp = "(" ++ s ++ " " ++ unwords argList ++ ")"++        restrict | noChars    = []+                 | needsQuant =    [               "(assert (forall (" ++ unwords argTList ++ ")"+                                   ,               "                (let ((" ++ resultVar ++ " " ++ resultExp ++ "))"+                                   ]+                                ++ (case constraints of+                                      []     ->  [ "                     true"]+                                      [x]    ->  [ "                     " ++ x]+                                      (x:xs) ->  ( "                     (and " ++ x)+                                              :  [ "                          " ++ c | c <- xs]+                                              ++ [ "                     )"])+                                ++ [        "                )))"]+                 | True       = case constraints of+                                 []     -> []+                                 [x]    -> ["(assert " ++ x ++ ")"]+                                 (x:xs) -> ( "(assert (and " ++ x)+                                        :  [ "             " ++ c | c <- xs]+                                        ++ [ "        ))"]++        constraints = walk 0 resultVar (\nm -> "(= 1 (str.len " ++ nm ++ "))") result++        mkAnd []  = "true"+        mkAnd [c] = c+        mkAnd cs  = "(and " ++ unwords cs ++ ")"++        walk :: Int -> String -> (String -> String) -> Kind -> [String]+        walk _d _nm _f KBool     {}       = []+        walk _d _nm _f KBounded  {}       = []+        walk _d _nm _f KUnbounded{}       = []+        walk _d _nm _f KReal     {}       = []+        walk _d _nm _f KUserSort {}       = []+        walk _d _nm _f KFloat    {}       = []+        walk _d _nm _f KDouble   {}       = []+        walk _d  nm  f KChar     {}       = [f nm]+        walk _d _nm _f KString   {}       = []+        walk  d  nm _f  (KList k)+          | charFree k                    = []+          | True                          = let fnm   = "seq" ++ show d+                                                cstrs = walk (d+1) ("(seq.nth " ++ nm ++ " " ++ fnm ++ ")")+                                                             (\snm -> "(= 1 (str.len " ++ snm ++ "))") k+                                            in ["(forall ((" ++ fnm ++ " " ++ smtType KUnbounded ++ ")) " ++ "(=> (and (>= " ++ fnm ++ " 0) (< " ++ fnm ++ " (seq.len " ++ nm ++ "))) " ++ mkAnd cstrs ++ "))"]+        walk  d  nm  _f (KSet k)+          | charFree k                    = []+          | True                          = let fnm    = "set" ++ show d+                                                cstrs  = walk (d+1) nm (\snm -> "(=> (select " ++ snm ++ " " ++ fnm ++ ") (= 1 (str.len " ++ fnm ++ ")))") k+                                            in ["(forall ((" ++ fnm ++ " " ++ smtType k ++ ")) " ++ mkAnd cstrs ++ ")"]+        walk  d  nm  f (KTuple ks)        = let tt        = "SBVTuple" ++ show (length ks)+                                                project i = "(proj_" ++ show i ++ "_" ++ tt ++ " " ++ nm ++ ")"+                                                nmks      = [(project i, k) | (i, k) <- zip [1::Int ..] ks]+                                            in concatMap (\(n, k) -> walk (d+1) n f k) nmks+        walk  d  nm  f km@(KMaybe k)      = let n = "(get_just_SBVMaybe " ++ nm ++ ")"+                                            in  ["(=> " ++ "((_ is (just_SBVMaybe (" ++ smtType k ++ ") " ++ smtType km ++ ")) " ++ nm ++ ") " ++ c ++ ")" | c <- walk (d+1) n f k]+        walk  d  nm  f ke@(KEither k1 k2) = let n1 = "(get_left_SBVEither "  ++ nm ++ ")"+                                                n2 = "(get_right_SBVEither " ++ nm ++ ")"+                                                c1 = ["(=> " ++ "((_ is (left_SBVEither ("  ++ smtType k1 ++ ") " ++ smtType ke ++ ")) " ++ nm ++ ") " ++ c ++ ")" | c <- walk (d+1) n1 f k1]+                                                c2 = ["(=> " ++ "((_ is (right_SBVEither (" ++ smtType k2 ++ ") " ++ smtType ke ++ ")) " ++ nm ++ ") " ++ c ++ ")" | c <- walk (d+1) n2 f k2]+                                            in c1 ++ c2  ----------------------------------------------------------------------------------------------- -- Casts supported by SMTLib. (From: <http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml>)
Data/SBV/SMT/Utils.hs view
@@ -31,7 +31,7 @@ import Control.Monad.Trans (MonadIO, liftIO)  import Data.SBV.Core.Data-import Data.SBV.Core.Symbolic (QueryContext)+import Data.SBV.Core.Symbolic (QueryContext, CnstMap) import Data.SBV.Utils.Lib (joinArgs)  import Data.List (intercalate)@@ -47,7 +47,7 @@                        -> [String]                                      -- ^ extra comments to place on top                        -> ([(Quantifier, NamedSymVar)], [NamedSymVar])  -- ^ inputs and aliasing names and trackers                        -> [Either SV (SV, [SV])]                        -- ^ skolemized inputs-                       -> [(SV, CV)]                                    -- ^ constants+                       -> (CnstMap, [(SV, CV)])                         -- ^ constants. The map, and as rendered in order                        -> [((Int, Kind, Kind), [SV])]                   -- ^ auto-generated tables                        -> [(Int, ArrayInfo)]                            -- ^ user specified arrays                        -> [(String, SBVType)]                           -- ^ uninterpreted functions/constants@@ -61,7 +61,7 @@ -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.) type SMTLibIncConverter a =  [NamedSymVar]                         -- ^ inputs                           -> Set.Set Kind                          -- ^ new kinds-                          -> [(SV, CV)]                            -- ^ constants+                          -> (CnstMap, [(SV, CV)])                  -- ^ all constants sofar, and new constants                           -> [(Int, ArrayInfo)]                    -- ^ newly created arrays                           -> [((Int, Kind, Kind), [SV])]           -- ^ newly created tables                           -> [(String, SBVType)]                   -- ^ newly created uninterpreted functions/constants
Data/SBV/Set.hs view
@@ -138,8 +138,8 @@ -- -- >>> prove $ \x (s :: SSet Integer) -> x `delete` (x `insert` s) .== s -- Falsifiable. Counter-example:---   s0 =   0 :: Integer---   s1 = {0} :: {Integer}+--   s0 =   2 :: Integer+--   s1 = {2} :: {Integer} -- -- But the above is true if the element isn't in the set to start with: --@@ -181,7 +181,7 @@ -- -- >>> prove $ \x (s :: SSet Integer) -> x `insert` (x `delete` s) .== s -- Falsifiable. Counter-example:---   s0 =  0 :: Integer+--   s0 =  2 :: Integer --   s1 = {} :: {Integer} -- -- But the above is true if the element is in the set to start with:@@ -283,8 +283,8 @@ -- -- >>> prove $ \x -> isFull (observe "set" (x `delete` (full :: SSet Integer))) -- Falsifiable. Counter-example:---   set = U - {0} :: {Integer}---   s0  =       0 :: Integer+--   set = U - {2} :: {Integer}+--   s0  =       2 :: Integer -- -- >>> isFull (full :: SSet Integer) -- True@@ -371,7 +371,7 @@ -- -- >>> prove $ \x (s :: SSet Integer) -> s `isProperSubsetOf` (x `insert` s) -- Falsifiable. Counter-example:---   s0 = 0 :: Integer+--   s0 = 2 :: Integer --   s1 = U :: {Integer} -- -- >>> prove $ \x (s :: SSet Integer) -> x `notMember` s .=> s `isProperSubsetOf` (x `insert` s)@@ -379,8 +379,8 @@ -- -- >>> prove $ \x (s :: SSet Integer) -> (x `delete` s) `isProperSubsetOf` s -- Falsifiable. Counter-example:---   s0 =         0 :: Integer---   s1 = U - {0,1} :: {Integer}+--   s0 =         2 :: Integer+--   s1 = U - {2,3} :: {Integer} -- -- >>> prove $ \x (s :: SSet Integer) -> x `member` s .=> (x `delete` s) `isProperSubsetOf` s -- Q.E.D.@@ -534,7 +534,7 @@ False >>> sat $ \(x::SSet (Maybe Integer)) y z -> distinct [x, y, z] Satisfiable. Model:-  s0 = U - {Just 0} :: {Maybe Integer}+  s0 = U - {Just 2} :: {Maybe Integer}   s1 =           {} :: {Maybe Integer}   s2 =            U :: {Maybe Integer}
Data/SBV/String.hs view
@@ -57,7 +57,7 @@ -- -- >>> sat $ \s -> length s .== 2 -- Satisfiable. Model:---   s0 = "\NUL\NUL" :: String+--   s0 = "AB" :: String -- >>> sat $ \s -> length s .< 0 -- Unsatisfiable -- >>> prove $ \s1 s2 -> length s1 + length s2 .== length (s1 .++ s2)@@ -133,7 +133,7 @@ -- Q.E.D. -- >>> sat $ \s -> length s .>= 2 .&& strToStrAt s 0 ./= strToStrAt s (length s - 1) -- Satisfiable. Model:---   s0 = "\NUL\NUL\EOT" :: String+--   s0 = "ABC" :: String strToStrAt :: SString -> SInteger -> SString strToStrAt s offset = subStr s offset 1
Data/SBV/Tools/GenTest.hs view
@@ -48,7 +48,7 @@          | i == n = return $ TV $ reverse sofar          | True   = do t <- tc                        gen (i+1) (t:sofar)-        tc = do (_, Result {resTraces=tvals, resConsts=cs, resConstraints=cstrs, resOutputs=os}) <- runSymbolic (Concrete Nothing) (m >>= output)+        tc = do (_, Result {resTraces=tvals, resConsts=(_, cs), resConstraints=cstrs, resOutputs=os}) <- runSymbolic (Concrete Nothing) (m >>= output)                 let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpeted constants!") . (`lookup` cs)                     cond = and [cvToBool (cval v) | (False, _, v) <- F.toList cstrs] -- Only pick-up "hard" constraints, as indicated by False in the fist component                 if cond
Data/SBV/Utils/Lib.hs view
@@ -25,7 +25,7 @@ import Data.Dynamic (fromDynamic, toDyn, Typeable) import Data.Maybe   (fromJust, isJust, isNothing) -import Numeric (readHex, readOct, showHex)+import Numeric (readHex, 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.@@ -107,42 +107,27 @@           f m (x:xs)                = Just x : f m xs           f _ []                    = [] --- | Given a QF_S string (i.e., one that works in the string theory), convert it to a Haskell equivalent+-- | Given an SMTLib string (i.e., one that works in the string theory), convert it to a Haskell equivalent qfsToString :: String -> String qfsToString = go-  where go ""                                                          = ""-        go ('\\':'n'       : rest)                                     = chr 10 : go rest-        go ('\\':'\\'       : rest)                                    = '\\'   : go rest-        go ('\\':'v'       : rest)                                     = chr 11 : go rest-        go ('\\':'f'       : rest)                                     = chr 12 : go rest-        go ('\\':'r'       : rest)                                     = chr 13 : go rest-        go ('\\':'x':c1:c2 : rest) | [(v, "")] <- readHex [c1, c2]     = chr  v : go rest-        go ('\\':c1:c2:c3  : rest) | [(v, "")] <- readOct [c1, c2, c3] = chr  v : go rest-        go (c              : rest)                                     = c      : go rest+  where go "" = "" --- | Given a Haskell, convert it to one that's understood by the QF_S logic--- TODO: This function will require mods with the new String logic; as escapes+        go ('\\':'u':'{':d4:d3:d2:d1:d0:'}' : rest) | [(v, "")] <- readHex [d4, d3, d2, d1, d0] = chr v : go rest+        go ('\\':'u':       d3:d2:d1:d0     : rest) | [(v, "")] <- readHex [    d3, d2, d1, d0] = chr v : go rest+        go ('\\':'u':'{':   d3:d2:d1:d0:'}' : rest) | [(v, "")] <- readHex [    d3, d2, d1, d0] = chr v : go rest+        go ('\\':'u':'{':      d2:d1:d0:'}' : rest) | [(v, "")] <- readHex [        d2, d1, d0] = chr v : go rest+        go ('\\':'u':'{':         d1:d0:'}' : rest) | [(v, "")] <- readHex [            d1, d0] = chr v : go rest+        go ('\\':'u':'{':            d0:'}' : rest) | [(v, "")] <- readHex [                d0] = chr v : go rest++        -- Otherwise, just proceed; hopefully we covered everything above+        go (c : rest) = c : go rest++-- | Given a Haskell string, convert it to SMTLib. if ord is 0x00020 to 0x0007E, then we print it -- will completely be different! stringToQFS :: String -> String stringToQFS = concatMap cvt-  where -- strings are almost just show, but escapes are different. Sigh-        cvt c-         | 0 <= o && o < 32-         = escapeTable !! o-         | c == '\\'-         = "\\\\"-         | c == '"'-         = "\"\""-         | o >= 128 && o < 256-         = "\\x" ++ showHex (ord c) ""-         | o > 256-         = error $ "Data.SBV: stringToQFS: Haskell character: " ++ show c ++ " is not representable in QF_S"-         | True-         = [c]-         where o = ord c--        -- | First 32 values are coded in a custom way by Z3:-        escapeTable :: [String]-        escapeTable = [ "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n",   "\\v",   "\\f",   "\\r",   "\\x0E", "\\x0F"-                      , "\\x10", "\\x11", "\\x12", "\\x13", "\\x14", "\\x15", "\\x16", "\\x17", "\\x18", "\\x19", "\\x1A", "\\x1B", "\\x1C", "\\x1D", "\\x1E", "\\x1F"-                      ]+  where cvt c+         | c == '"'                 = "\"\""+         | oc >= 0x20 && oc <= 0x7E = [c]+         | True                     = "\\u{" ++ showHex oc "" ++ "}"+         where oc = ord c
Data/SBV/Utils/PrettyNum.hs view
@@ -419,7 +419,7 @@   | hasSign x        , CInteger  w      <- cvVal x = if w == negate (2 ^ intSizeOf x)                                                      then mkMinBound (intSizeOf x)                                                      else negIf (w < 0) $ smtLibHex (intSizeOf x) (abs w)-  | isChar x         , CChar c          <- cvVal x = smtLibHex 8 (fromIntegral (ord c))+  | isChar x         , CChar c          <- cvVal x = "(_ char " ++ smtLibHex 8 (fromIntegral (ord c)) ++ ")"   | isString x       , CString s        <- cvVal x = '\"' : stringToQFS s ++ "\""   | isList x         , CList xs         <- cvVal x = smtLibSeq (kindOf x) xs   | isSet x          , CSet s           <- cvVal x = smtLibSet (kindOf x) s
Documentation/SBV/Examples/Existentials/Diophantine.hs view
@@ -74,15 +74,15 @@ -- We have: -- -- >>> test--- NonHomogeneous [[0,2,0],[1,0,0]] [[0,1,1],[1,0,2]]+-- NonHomogeneous [[1,0,0],[0,2,0]] [[0,1,1],[1,0,2]] -- -- which means that the solutions are of the form: -----    @(0, 2, 0) + k (0, 1, 1) + k' (1, 0, 2) = (k', 2+k, k+2k')@+--    @(1, 0, 0) + k (0, 1, 1) + k' (1, 0, 2) = (1+k', k, k+2k')@ -- -- OR -----    @(1, 0, 0) + k (0, 1, 1) + k' (1, 0, 2) = (1+k', k, k+2k')@+--    @(0, 2, 0) + k (0, 1, 1) + k' (1, 0, 2) = (k', 2+k, k+2k')@ -- -- for arbitrary @k@, @k'@. It's easy to see that these are really solutions -- to the equation given. It's harder to see that they cover all possibilities,
Documentation/SBV/Examples/Misc/Auxiliary.hs view
@@ -15,6 +15,8 @@ -- considering them explicitly in model construction. ----------------------------------------------------------------------------- +{-# LANGUAGE OverloadedStrings   #-}+ {-# OPTIONS_GHC -Wall -Werror #-}  module Documentation.SBV.Examples.Misc.Auxiliary where
+ Documentation/SBV/Examples/Misc/NestedArray.hs view
@@ -0,0 +1,42 @@+-----------------------------------------------------------------------------+-- |+-- Module    : Documentation.SBV.Examples.Misc.NestedArray+-- Copyright : (c) Levent Erkok+-- License   : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Demonstrates how to model nested-arrays, i.e., arrays of arrays in SBV.+-- Instead of SMTLib's nested model, in SBV we use a tuple as an index,+-- which is isomorphic to nested arrays.+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.Misc.NestedArray where++import Data.SBV+import Data.SBV.Tuple+import Data.SBV.Control++-- | Model a nested array that is indexed by integers, and we store+-- another integer to integer array in each index. We have:+--+-- >>> nestedArray+-- (0,10)+nestedArray :: IO (Integer, Integer)+nestedArray = runSMT $ do+  idx <- sInteger "idx"+  arr <- newArray_ Nothing :: Symbolic (SArray (Integer, Integer) Integer)++  -- we'll assert that arr[idx][idx] = 10+  let val = readArray arr (tuple (idx, idx))+  constrain $ val .== literal 10++  query $ do+    cs <- checkSat+    case cs of+      Sat -> do idxVal <- getValue idx+                elt    <- getValue (readArray arr (tuple (idx, idx)))+                pure (idxVal, elt)+      _   -> error $ "Solver said: " ++ show cs
Documentation/SBV/Examples/Misc/SetAlgebra.hs view
@@ -362,9 +362,9 @@  >>> prove $ \(a :: SI) b c -> a `isSubsetOf` (b `union` c) .=> a `isSubsetOf` b .&& a `isSubsetOf` c Falsifiable. Counter-example:-  s0 =     {0} :: {Integer}+  s0 =     {2} :: {Integer}   s1 =       U :: {Integer}-  s2 = U - {0} :: {Integer}+  s2 = U - {2} :: {Integer}  Similarly, subset relation does /not/ distribute over intersection on the right: @@ -372,7 +372,7 @@  >>> prove $ \(a :: SI) b c -> (b `intersection` c) `isSubsetOf` a .=> b `isSubsetOf` a .&& c `isSubsetOf` a Falsifiable. Counter-example:-  s0 = U - {0} :: {Integer}+  s0 = U - {2} :: {Integer}   s1 =      {} :: {Integer}-  s2 =     {0} :: {Integer}+  s2 =     {2} :: {Integer} -}
Documentation/SBV/Examples/ProofTools/BMC.hs view
@@ -83,7 +83,7 @@ -- BMC: Iteration: 2 -- BMC: Iteration: 3 -- BMC: Solution found at iteration 3--- Right (3,[(0,10),(0,6),(2,6),(2,2)])+-- Right (3,[(0,10),(2,10),(2,6),(2,2)]) -- -- As expected, there's a solution in this case. Furthermore, since the BMC engine -- found a solution at depth @3@, we also know that there is no solution at
Documentation/SBV/Examples/Puzzles/Garden.hs view
@@ -30,6 +30,7 @@  {-# LANGUAGE DeriveAnyClass      #-} {-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE OverloadedStrings   #-} {-# LANGUAGE StandaloneDeriving  #-} {-# LANGUAGE TemplateHaskell     #-} @@ -38,7 +39,7 @@ module Documentation.SBV.Examples.Puzzles.Garden where  import Data.SBV-import Data.List(isSuffixOf)+import Data.Text(isSuffixOf)  -- | Colors of the flowers data Color = Red | Yellow | Blue
+ Documentation/SBV/Examples/Puzzles/Murder.hs view
@@ -0,0 +1,178 @@+-----------------------------------------------------------------------------+-- |+-- Module    : Documentation.SBV.Examples.Puzzles.Murder+-- Copyright : (c) Levent Erkok+-- License   : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Solution to "Malice and Alice," from George J. Summers' Logical Deduction Puzzles:+--+-- @+-- A man and a woman were together in a bar at the time of the murder.+-- The victim and the killer were together on a beach at the time of the murder.+-- One of Alice’s two children was alone at the time of the murder.+-- Alice and her husband were not together at the time of the murder.+-- The victim's twin was not the killer.+-- The killer was younger than the victim.+--+-- Who killed who?+-- @+-----------------------------------------------------------------------------++{-# LANGUAGE DeriveAnyClass     #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances  #-}+{-# LANGUAGE NamedFieldPuns     #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell    #-}+{-# OPTIONS_GHC -Wall -Werror   #-}++module Documentation.SBV.Examples.Puzzles.Murder where++import Data.Char+import Data.List++import Data.SBV+import Data.SBV.Control++-- | Locations+data Location = Bar | Beach | Alone++-- | Sexes+data Sex  = Male | Female++-- | Roles+data Role = Victim | Killer | Bystander++mkSymbolicEnumeration ''Location+mkSymbolicEnumeration ''Sex+mkSymbolicEnumeration ''Role++-- | A person has a name, age, together with location and sex.+-- We parameterize over a function so we can use this struct+-- both in a concrete context and a symbolic context. Note+-- that the name is always concrete.+data Person f = Person { nm       :: String+                       , age      :: f Integer+                       , location :: f Location+                       , sex      :: f Sex+                       , role     :: f Role+                       }++-- | Helper functor+newtype Const a = Const { getConst :: a }++-- | Show a person+instance Show (Person Const) where+  show (Person n a l s r) = unwords [n, show (getConst a), show (getConst l), show (getConst s), show (getConst r)]++-- | Create a new symbolic person+newPerson :: String -> Symbolic (Person SBV)+newPerson n = do+        p <- Person n <$> free_ <*> free_ <*> free_ <*> free_+        constrain $ age p .>= 20+        constrain $ age p .<= 50+        pure p++-- | Get the concrete value of the person in the model+getPerson :: Person SBV -> Query (Person Const)+getPerson Person{nm, age, location, sex, role} = Person nm <$> (Const <$> getValue age)+                                                           <*> (Const <$> getValue location)+                                                           <*> (Const <$> getValue sex)+                                                           <*> (Const <$> getValue role)++-- | Solve the puzzle. We have:+--+-- >>> killer+-- Alice     47  Bar    Female  Bystander+-- Husband   46  Beach  Male    Killer+-- Brother   47  Beach  Male    Victim+-- Daughter  20  Alone  Female  Bystander+-- Son       20  Bar    Male    Bystander+--+-- That is, Alice's brother was the victim and Alice's husband was the killer.+killer :: IO ()+killer = do+   persons <- puzzle+   let wps      = map (words . show) persons+       cwidths  = map ((+2) . maximum . map length) (transpose wps)+       align xs = concat $ zipWith (\i f -> take i (f ++ repeat ' ')) cwidths xs+       trim     = reverse . dropWhile isSpace . reverse+   mapM_ putStrLn $ map (trim . align) wps++-- | Constraints of the puzzle, coded following the English description.+puzzle :: IO [Person Const]+puzzle = runSMT $ do+  alice    <- newPerson "Alice"+  husband  <- newPerson "Husband"+  brother  <- newPerson "Brother"+  daughter <- newPerson "Daughter"+  son      <- newPerson "Son"++  -- Sex of each character+  constrain $ sex alice    .== sFemale+  constrain $ sex husband  .== sMale+  constrain $ sex brother  .== sMale+  constrain $ sex daughter .== sFemale+  constrain $ sex son      .== sMale++  let chars = [alice, husband, brother, daughter, son]++  -- Age relationships. To come up with "reasonable" numbers,+  -- we make the kids at least 25 years younger than the parents+  constrain $ age son      .<  age alice    - 25+  constrain $ age son      .<  age husband  - 25+  constrain $ age daughter .<  age alice    - 25+  constrain $ age daughter .<  age husband  - 25++  -- Ensure that there's a twin. Looking at the characters, the+  -- only possibilities are either Alice's kids, or Alice and her brother+  constrain $ age son .== age daughter .|| age alice .== age brother++  -- One victim, one killer+  constrain $ sum (map (\c -> oneIf (role c .== sVictim)) chars) .== (1 :: SInteger)+  constrain $ sum (map (\c -> oneIf (role c .== sKiller)) chars) .== (1 :: SInteger)++  let ifVictim p = role p .== sVictim+      ifKiller p = role p .== sKiller++      every f = sAnd (map f chars)+      some  f = sOr  (map f chars)++  -- A man and a woman were together in a bar at the time of the murder.+  constrain $ some $ \c -> sex c .== sFemale .&& location c .== sBar+  constrain $ some $ \c -> sex c .== sMale   .&& location c .== sBar++  -- The victim and the killer were together on a beach at the time of the murder.+  constrain $ every $ \c -> ifVictim c .=> location c .== sBeach+  constrain $ every $ \c -> ifKiller c .=> location c .== sBeach++  -- One of Alice’s two children was alone at the time of the murder.+  constrain $ location daughter .== sAlone .|| location son .== sAlone++  -- Alice and her husband were not together at the time of the murder.+  constrain $ location alice ./= location husband++  -- The victim has a twin+  constrain $ every $ \c -> ifVictim c .=> some (\d -> literal (nm c /= nm d) .&& age c .== age d)++  -- The victim's twin was not the killer.+  constrain $ every $ \c -> ifVictim c .=> every (\d -> age c .== age d .=> role d ./= sKiller)++  -- The killer was younger than the victim.+  constrain $ every $ \c -> ifKiller c .=> every (\d -> ifVictim d .=> age c .< age d)++  -- Ensure certain pairs can't be twins+  constrain $ age husband ./= age brother+  constrain $ age husband ./= age alice++  query $ do cs <- checkSat+             case cs of+               Sat -> do a <- getPerson alice+                         h <- getPerson husband+                         b <- getPerson brother+                         d <- getPerson daughter+                         s <- getPerson son+                         pure [a, h, b, d, s]+               _   -> error $ "Solver said: " ++ show cs
LICENSE view
@@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2020, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2021, Levent Erkok (erkokl@gmail.com) All rights reserved.  Redistribution and use in source and binary forms, with or without
SBVBenchSuite/BenchSuite/Puzzles/Garden.hs view
@@ -10,11 +10,12 @@ -- Bench suite for Documentation.SBV.Examples.Puzzles.Garden ----------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall -Werror #-}+{-# OPTIONS_GHC -Wall -Werror  #-}+{-# LANGUAGE OverloadedStrings #-}  module BenchSuite.Puzzles.Garden(benchmarks) where -import Data.List (isSuffixOf)+import Data.Text (isSuffixOf)  import Documentation.SBV.Examples.Puzzles.Garden
SBVBenchSuite/SBVBenchmark.hs view
@@ -130,7 +130,7 @@ -- because we can easily generate benchmarks that take a lot of wall time to -- solve, especially with 'Data.SBV.allSatWith' calls benchConfig :: Config-benchConfig = defaultConfig { timeLimit = Just 1.00 }+benchConfig = defaultConfig { timeLimit = Just 120.00 }  {- To benchmark sbv we require two use cases: For continuous integration we want a@@ -214,7 +214,7 @@ -- native on the same program. To construct a benchmark for only sbv one would -- call `runBenchmark` puzzles :: Benchmark-puzzles = bgroup "Puzzles" $ runBenchmark <$> puzzleBenchmarks+puzzles = bgroup "Puzzles" $ runOverheadBenchmark <$> puzzleBenchmarks   --------------------------- BitPrecise ------------------------------------------@@ -230,7 +230,7 @@                        ]  bitPrecise :: Benchmark-bitPrecise = bgroup "BitPrecise" $ runBenchmark <$> bitPreciseBenchmarks+bitPrecise = bgroup "BitPrecise" $ runOverheadBenchmark <$> bitPreciseBenchmarks   --------------------------- Query -----------------------------------------------@@ -247,7 +247,7 @@                   ]  queries :: Benchmark-queries = bgroup "Queries" $ runBenchmark <$> queryBenchmarks+queries = bgroup "Queries" $ runOverheadBenchmark <$> queryBenchmarks   --------------------------- WeakestPreconditions --------------------------------@@ -278,7 +278,7 @@                          ]  optimizations :: Benchmark-optimizations = bgroup "Optimizations" $ runBenchmark <$> optimizationBenchmarks+optimizations = bgroup "Optimizations" $ runOverheadBenchmark <$> optimizationBenchmarks   --------------------------- Uninterpreted ---------------------------------------@@ -293,7 +293,7 @@                           ]  uninterpreted :: Benchmark-uninterpreted = bgroup "Uninterpreted" $ runBenchmark <$> uninterpretedBenchmarks+uninterpreted = bgroup "Uninterpreted" $ runOverheadBenchmark <$> uninterpretedBenchmarks   --------------------------- ProofTools -----------------------------------------@@ -305,7 +305,7 @@                       ]  proofTools :: Benchmark-proofTools = bgroup "ProofTools" $ runBenchmark <$> proofToolBenchmarks+proofTools = bgroup "ProofTools" $ runOverheadBenchmark <$> proofToolBenchmarks   --------------------------- Code Generation -------------------------------------@@ -320,7 +320,7 @@  codeGeneration :: Benchmark codeGeneration = bgroup "CodeGeneration" $-                 runBenchmark <$> codeGenerationBenchmarks+                 runOverheadBenchmark <$> codeGenerationBenchmarks   --------------------------- Crypto ----------------------------------------------@@ -331,7 +331,7 @@                    ]  crypto :: Benchmark-crypto = bgroup "Crypto" $ runBenchmark <$> cryptoBenchmarks+crypto = bgroup "Crypto" $ runOverheadBenchmark <$> cryptoBenchmarks   --------------------------- Miscellaneous ---------------------------------------@@ -351,7 +351,7 @@                  ]  misc :: Benchmark-misc = bgroup "Miscellaneous" $ runBenchmark <$> miscBenchmarks+misc = bgroup "Miscellaneous" $ runOverheadBenchmark <$> miscBenchmarks   --------------------------- Lists -----------------------------------------------@@ -362,7 +362,7 @@                  ]  lists :: Benchmark-lists = bgroup "Lists" $ runBenchmark <$> listBenchmarks+lists = bgroup "Lists" $ runOverheadBenchmark <$> listBenchmarks   --------------------------- Strings ---------------------------------------------@@ -372,7 +372,7 @@                    ]  strings :: Benchmark-strings = bgroup "Strings" $ runBenchmark <$> stringBenchmarks+strings = bgroup "Strings" $ runOverheadBenchmark <$> stringBenchmarks   --------------------------- Existentials ----------------------------------------@@ -382,7 +382,7 @@                         ]  existentials :: Benchmark-existentials = bgroup "Existentials" $ runBenchmark <$> existentialBenchmarks+existentials = bgroup "Existentials" $ runOverheadBenchmark <$> existentialBenchmarks   --------------------------- Transformers ----------------------------------------@@ -391,4 +391,4 @@                         ]  transformers :: Benchmark-transformers = bgroup "Transformers" $ runBenchmark <$> transformerBenchmarks+transformers = bgroup "Transformers" $ runOverheadBenchmark <$> transformerBenchmarks
SBVBenchSuite/Utils/SBVBenchFramework.hs view
@@ -10,7 +10,6 @@ -- Various goodies for benchmarking SBV ----------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} @@ -102,7 +101,7 @@ compareBenchmarksWith :: BS.Config -> FilePath -> FilePath -> IO () compareBenchmarksWith conf old new = do   -- make the file name-  let fname = benchResultsFile $ (takeBaseName old) ++ "_vs_" ++ (takeBaseName new)+  let fname = benchResultsFile $ takeBaseName old ++ "_vs_" ++ takeBaseName new   -- this is lazy IO !!!   readFile old >>= appendFile fname   readFile new >>= appendFile fname
+ SBVTestSuite/GoldFiles/charConstr00.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-logic ALL) ; has chars, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () String (_ char #x41))+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () String) ; tracks user variable "x"+[GOOD] (assert (= 1 (str.len s0)))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () Bool (distinct s0 s1))+[GOOD] (assert s2)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 "B"))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",'B' :: Char)], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr01.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-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s0 () Int 4)+[GOOD] (define-fun s2 () String (_ char #x41))+[GOOD] ; --- skolem constants ---+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] (declare-fun cf (Int) String)+[GOOD] (assert (forall ((a1 Int))+                       (let ((result (cf a1)))+                            (= 1 (str.len result))+                       )))+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s1 () String (cf s0))+[GOOD] (define-fun s3 () Bool (distinct s1 s2))+[GOOD] (assert s3)+[SEND] (check-sat)+[RECV] sat+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[SEND] (get-value (cf))+[RECV] ((cf ((as const Array) "B")))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [], modelUIFuns = [("cf",(SInteger -> SChar,([],'B' :: Char)))]}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr02.gold view
@@ -0,0 +1,50 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] (declare-datatypes ((SBVTuple3 3)) ((par (T1 T2 T3)+                                           ((mkSBVTuple3 (proj_1_SBVTuple3 T1)+                                                         (proj_2_SBVTuple3 T2)+                                                         (proj_3_SBVTuple3 T3))))))+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s0 () Int 4)+[GOOD] (define-fun s2 () (SBVTuple3 String String String) (mkSBVTuple3 (_ char #x41) (_ char #x42) (_ char #x43)))+[GOOD] ; --- skolem constants ---+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] (declare-fun cf3 (Int) (SBVTuple3 String String String))+[GOOD] (assert (forall ((a1 Int))+                       (let ((result (cf3 a1)))+                            (and (= 1 (str.len (proj_1_SBVTuple3 result)))+                                 (= 1 (str.len (proj_2_SBVTuple3 result)))+                                 (= 1 (str.len (proj_3_SBVTuple3 result)))+                            )+                       )))+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s1 () (SBVTuple3 String String String) (cf3 s0))+[GOOD] (define-fun s3 () Bool (distinct s1 s2))+[GOOD] (assert s3)+[SEND] (check-sat)+[RECV] sat+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[SEND] (get-value (cf3))+[RECV] ((cf3 ((as const Array) (mkSBVTuple3 "A" "A" "A"))))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [], modelUIFuns = [("cf3",(SInteger -> (SChar, SChar, SChar),([],('A','A','A') :: (Char, Char, Char))))]}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr03.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-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has either type, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] (declare-datatypes ((SBVEither 2)) ((par (T1 T2)+                                           ((left_SBVEither  (get_left_SBVEither  T1))+                                            (right_SBVEither (get_right_SBVEither T2))))))+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () (SBVEither String String) ((as left_SBVEither (SBVEither String String)) (_ char #x41)))+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (SBVEither String String)) ; tracks user variable "x"+[GOOD] (assert (and (=> ((_ is (left_SBVEither (String) (SBVEither String String))) s0) (= 1 (str.len (get_left_SBVEither s0))))+                    (=> ((_ is (right_SBVEither (String) (SBVEither String String))) s0) (= 1 (str.len (get_right_SBVEither s0))))+               ))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () Bool (distinct s0 s1))+[GOOD] (assert s2)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (left_SBVEither "B")))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Left 'B' :: Either Char Char)], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr04.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-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] (declare-datatypes ((SBVEither 2)) ((par (T1 T2)+                                           ((left_SBVEither  (get_left_SBVEither  T1))+                                            (right_SBVEither (get_right_SBVEither T2))))))+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () (SBVEither Int String) ((as right_SBVEither (SBVEither Int String)) (_ char #x41)))+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (SBVEither Int String)) ; tracks user variable "x"+[GOOD] (assert (=> ((_ is (right_SBVEither (String) (SBVEither Int String))) s0) (= 1 (str.len (get_right_SBVEither s0)))))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () Bool (distinct s0 s1))+[GOOD] (assert s2)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (left_SBVEither 2)))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Left 2 :: Either Integer Char)], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr05.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-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] (declare-datatypes ((SBVEither 2)) ((par (T1 T2)+                                           ((left_SBVEither  (get_left_SBVEither  T1))+                                            (right_SBVEither (get_right_SBVEither T2))))))+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () (SBVEither String Int) ((as left_SBVEither (SBVEither String Int)) (_ char #x41)))+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (SBVEither String Int)) ; tracks user variable "x"+[GOOD] (assert (=> ((_ is (left_SBVEither (String) (SBVEither String Int))) s0) (= 1 (str.len (get_left_SBVEither s0)))))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () Bool (distinct s0 s1))+[GOOD] (assert s2)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (right_SBVEither 2)))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Right 2 :: Either Char Integer)], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr06.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-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] (declare-datatypes ((SBVEither 2)) ((par (T1 T2)+                                           ((left_SBVEither  (get_left_SBVEither  T1))+                                            (right_SBVEither (get_right_SBVEither T2))))))+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () (SBVEither String (SBVEither String Int)) ((as left_SBVEither (SBVEither String (SBVEither String Int))) (_ char #x41)))+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (SBVEither String (SBVEither String Int))) ; tracks user variable "x"+[GOOD] (assert (and (=> ((_ is (left_SBVEither (String) (SBVEither String (SBVEither String Int)))) s0) (= 1 (str.len (get_left_SBVEither s0))))+                    (=> ((_ is (right_SBVEither ((SBVEither String Int)) (SBVEither String (SBVEither String Int)))) s0) (=> ((_ is (left_SBVEither (String) (SBVEither String Int))) (get_right_SBVEither s0)) (= 1 (str.len (get_left_SBVEither (get_right_SBVEither s0))))))+               ))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () Bool (distinct s0 s1))+[GOOD] (assert s2)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 ((as left_SBVEither (SBVEither String (SBVEither String Int))) "B")))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Left 'B' :: Either Char (Either Char Integer))], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr07.gold view
@@ -0,0 +1,41 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has maybe type, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] (declare-datatypes ((SBVMaybe 1)) ((par (T)+                                           ((nothing_SBVMaybe)+                                            (just_SBVMaybe (get_just_SBVMaybe T))))))+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s3 () (SBVMaybe String) ((as just_SBVMaybe (SBVMaybe String)) (_ char #x41)))+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (SBVMaybe String)) ; tracks user variable "x"+[GOOD] (assert (=> ((_ is (just_SBVMaybe (String) (SBVMaybe String))) s0) (= 1 (str.len (get_just_SBVMaybe s0)))))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s1 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe String))) s0))+[GOOD] (define-fun s2 () Bool (ite s1 false true))+[GOOD] (define-fun s4 () Bool (distinct s0 s3))+[GOOD] (define-fun s5 () Bool (and s2 s4))+[GOOD] (assert s5)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (just_SBVMaybe "B")))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Just 'B' :: Maybe Char)], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr08.gold view
@@ -0,0 +1,51 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has sets, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () String (_ char #x41))+[GOOD] (define-fun s3 () String (_ char #x42))+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "x"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0)))))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () Bool (select s0 s1))+[GOOD] (define-fun s4 () Bool (select s0 s3))+[GOOD] (define-fun s5 () Bool (not s4))+[GOOD] (define-fun s6 () Bool (and s2 s5))+[GOOD] (assert s6)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (store (store (store (store (store (store ((as const (Array String Bool)) true)+                                                 "EF"+                                                 false)+                                          "CD"+                                          false)+                                   "GH"+                                   false)+                            "B"+                            false)+                     ""+                     false)+              "A"+              true)))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",U - {'B'} :: {Char})], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr09.gold view
@@ -0,0 +1,39 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)+                                           ((mkSBVTuple2 (proj_1_SBVTuple2 T1)+                                                         (proj_2_SBVTuple2 T2))))))+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s2 () Int 1)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (Seq (SBVTuple2 (SBVTuple2 String String) (Seq Int)))) ; tracks user variable "x"+[GOOD] (assert (forall ((seq0 Int)) (=> (and (>= seq0 0) (< seq0 (seq.len s0))) (and (= 1 (str.len (proj_1_SBVTuple2 (proj_1_SBVTuple2 (seq.nth s0 seq0))))) (= 1 (str.len (proj_2_SBVTuple2 (proj_1_SBVTuple2 (seq.nth s0 seq0)))))))))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s1 () Int (seq.len s0))+[GOOD] (define-fun s3 () Bool (= s1 s2))+[GOOD] (assert s3)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (seq.unit (mkSBVTuple2 (mkSBVTuple2 "A" "A") (seq.unit 0)))))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",[(('A','A'),[0])] :: [((Char, Char), [Integer])])], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr10.gold view
@@ -0,0 +1,46 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)+                                           ((mkSBVTuple2 (proj_1_SBVTuple2 T1)+                                                         (proj_2_SBVTuple2 T2))))))+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s2 () Int 1)+[GOOD] (define-fun s4 () Int 0)+[GOOD] (define-fun s8 () String (_ char #x42))+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (Seq (SBVTuple2 (SBVTuple2 String String) (Seq Int)))) ; tracks user variable "x"+[GOOD] (assert (forall ((seq0 Int)) (=> (and (>= seq0 0) (< seq0 (seq.len s0))) (and (= 1 (str.len (proj_1_SBVTuple2 (proj_1_SBVTuple2 (seq.nth s0 seq0))))) (= 1 (str.len (proj_2_SBVTuple2 (proj_1_SBVTuple2 (seq.nth s0 seq0)))))))))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s1 () Int (seq.len s0))+[GOOD] (define-fun s3 () Bool (= s1 s2))+[GOOD] (define-fun s5 () (SBVTuple2 (SBVTuple2 String String) (Seq Int)) (seq.nth s0 s4))+[GOOD] (define-fun s6 () (SBVTuple2 String String) (proj_1_SBVTuple2 s5))+[GOOD] (define-fun s7 () String (proj_1_SBVTuple2 s6))+[GOOD] (define-fun s9 () Bool (= s7 s8))+[GOOD] (assert s3)+[GOOD] (assert s9)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (seq.unit (mkSBVTuple2 (mkSBVTuple2 "B" "B") (seq.unit 0)))))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",[(('B','B'),[0])] :: [((Char, Char), [Integer])])], modelUIFuns = []}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/charConstr11.gold view
@@ -0,0 +1,53 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- tuples ---+[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)+                                           ((mkSBVTuple2 (proj_1_SBVTuple2 T1)+                                                         (proj_2_SBVTuple2 T2))))))+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s4 () Int 1)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () Int) ; tracks user variable "x"+[GOOD] (declare-fun s1 () String) ; tracks user variable "c"+[GOOD] (assert (= 1 (str.len s1)))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] (declare-fun cf4 (Int String) (Seq (SBVTuple2 (SBVTuple2 String String) (Seq Int))))+[GOOD] (assert (forall ((a1 Int) (a2 String))+                       (let ((result (cf4 a1 a2)))+                            (forall ((seq0 Int)) (=> (and (>= seq0 0) (< seq0 (seq.len result))) (and (= 1 (str.len (proj_1_SBVTuple2 (proj_1_SBVTuple2 (seq.nth result seq0))))) (= 1 (str.len (proj_2_SBVTuple2 (proj_1_SBVTuple2 (seq.nth result seq0))))))))+                       )))+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () (Seq (SBVTuple2 (SBVTuple2 String String) (Seq Int))) (cf4 s0 s1))+[GOOD] (define-fun s3 () Int (seq.len s2))+[GOOD] (define-fun s5 () Bool (= s3 s4))+[GOOD] (assert s5)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 2))+[SEND] (get-value (s1))+[RECV] ((s1 "A"))+[GOOD] (set-option :pp.max_depth      4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def  true      )+[SEND] (get-value (cf4))+[RECV] ((cf4 ((as const Array) (seq.unit (mkSBVTuple2 (mkSBVTuple2 "A" "A") (seq.unit 0))))))++MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",2 :: Integer),("c",'A' :: Char)], modelUIFuns = [("cf4",(SInteger -> SChar -> [((SChar, SChar), [SInteger])],([],[(('A','A'),[0])] :: [((Char, Char), [Integer])])))]}+DONE.*** Solver   : Z3+*** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/exceptionLocal1.gold view
@@ -1,8 +1,7 @@ ** Calling: yices-smt2 --incremental [GOOD] ; Automatically generated by SBV. Do not edit. [GOOD] (set-option :print-success true)-** Backend solver Yices does not support global decls.-** Some incremental calls, such as pop, will be limited.+[GOOD] (set-option :global-declarations true) [GOOD] (set-option :produce-models true) [GOOD] (set-logic ALL) ; external query, using all logics. [GOOD] ; --- uninterpreted sorts ---@@ -58,7 +57,7 @@ *** ***    Sent      : (define-fun s35 () (_ BitVec 32) (bvmul s34 s34)) ***    Expected  : success-***    Received  : (error "at line 40, column 35: in bvmul: maximal polynomial degree exceeded")+***    Received  : (error "at line 41, column 35: in bvmul: maximal polynomial degree exceeded") *** ***    Exit code : ExitSuccess ***    Executable: /usr/local/bin/yices-smt2
SBVTestSuite/GoldFiles/freshVars.gold view
@@ -89,21 +89,26 @@ [GOOD] (define-fun s45 () Int (select array_0 s43)) [GOOD] (define-fun s47 () Bool (= s45 s46)) [GOOD] (assert s47)-[GOOD] (define-fun s49 () (_ BitVec 8) #x61)-[GOOD] (declare-fun vFArray_uninitializedRead (Bool) (_ BitVec 8))-[GOOD] (define-fun s48 () (_ BitVec 8) (vFArray_uninitializedRead s44))+[GOOD] (define-fun s49 () String (_ char #x61))+[GOOD] (declare-fun vFArray_uninitializedRead (Bool) String)+[GOOD] (assert (forall ((a1 Bool))+                       (let ((result (vFArray_uninitializedRead a1)))+                            (= 1 (str.len result))+                       )))+[GOOD] (define-fun s48 () String (vFArray_uninitializedRead s44)) [GOOD] (define-fun s50 () Bool (= s48 s49)) [GOOD] (assert s50) [GOOD] (define-fun s51 () Int 42) [GOOD] (define-fun array_1 () (Array Int Int) ((as const (Array Int Int)) 42)) [GOOD] (define-fun array_1_initializer () Bool true) ; no initializiation needed [GOOD] (declare-fun s52 () Int)-[GOOD] (declare-fun s53 () (_ BitVec 8))+[GOOD] (declare-fun s53 () String)+[GOOD] (assert (= 1 (str.len s53))) [GOOD] (define-fun s54 () Int 96) [GOOD] (define-fun s55 () Int (select array_1 s54)) [GOOD] (define-fun s56 () Bool (= s52 s55)) [GOOD] (assert s56)-[GOOD] (define-fun s57 () (_ BitVec 8) #x58)+[GOOD] (define-fun s57 () String (_ char #x58)) [GOOD] (define-fun s58 () Bool (= s53 s57)) [GOOD] (assert s58) [GOOD] (define-fun s59 () Int 1)@@ -187,7 +192,7 @@ [SEND] (get-value (s52)) [RECV] ((s52 42)) [SEND] (get-value (s53))-[RECV] ((s53 #x58))+[RECV] ((s53 "X")) [SEND] (get-value (s62)) [RECV] ((s62 "hello")) [SEND] (get-value (s63))@@ -196,7 +201,7 @@ [RECV] ((s64 (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)))))) [SEND] (get-value (s65))-[RECV] ((s65 "\x01\x02"))+[RECV] ((s65 (seq.++ (seq.unit #x01) (seq.unit #x02)))) [SEND] (get-value (s66)) [RECV] ((s66 (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003)))                (seq.unit (as seq.empty (Seq (_ BitVec 16))))
SBVTestSuite/GoldFiles/query1.gold view
@@ -73,7 +73,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version)-[RECV] (:version "4.8.10")+[RECV] (:version "4.8.11") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4)@@ -104,7 +104,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version)-[RECV] (:version "4.8.10")+[RECV] (:version "4.8.11") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time)
SBVTestSuite/GoldFiles/query_Chars1.gold view
@@ -13,14 +13,15 @@ [GOOD] (define-fun s2 () Int 65) [GOOD] (define-fun s4 () Int 66) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a"+[GOOD] (declare-fun s0 () String) ; tracks user variable "a"+[GOOD] (assert (= 1 (str.len s0))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula ----[GOOD] (define-fun s1 () Int (bv2nat s0))+[GOOD] (define-fun s1 () Int (str.to_code s0)) [GOOD] (define-fun s3 () Bool (>= s1 s2)) [GOOD] (define-fun s5 () Bool (< s1 s4)) [GOOD] (assert s3)@@ -28,7 +29,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 #x41))+[RECV] ((s0 "A")) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/query_ListOfMaybe.gold view
@@ -20,7 +20,8 @@ [GOOD] (define-fun s4 () Int 0) [GOOD] (define-fun s8 () Int 1) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Seq (SBVMaybe (_ BitVec 8)))) ; tracks user variable "lst"+[GOOD] (declare-fun s0 () (Seq (SBVMaybe String))) ; tracks user variable "lst"+[GOOD] (assert (forall ((seq0 Int)) (=> (and (>= seq0 0) (< seq0 (seq.len s0))) (=> ((_ is (just_SBVMaybe (String) (SBVMaybe String))) (seq.nth s0 seq0)) (= 1 (str.len (get_just_SBVMaybe (seq.nth s0 seq0)))))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -29,13 +30,13 @@ [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (seq.len s0)) [GOOD] (define-fun s3 () Bool (= s1 s2))-[GOOD] (define-fun s5 () (SBVMaybe (_ BitVec 8)) (seq.nth s0 s4))-[GOOD] (define-fun s6 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 8)))) s5))+[GOOD] (define-fun s5 () (SBVMaybe String) (seq.nth s0 s4))+[GOOD] (define-fun s6 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe String))) s5)) [GOOD] (define-fun s7 () Bool (ite s6 false true)) [GOOD] (define-fun s9 () Int (- s1 s8))-[GOOD] (define-fun s10 () (Seq (SBVMaybe (_ BitVec 8))) (seq.extract s0 s8 s9))-[GOOD] (define-fun s11 () (SBVMaybe (_ BitVec 8)) (seq.nth s10 s4))-[GOOD] (define-fun s12 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 8)))) s11))+[GOOD] (define-fun s10 () (Seq (SBVMaybe String)) (seq.extract s0 s8 s9))+[GOOD] (define-fun s11 () (SBVMaybe String) (seq.nth s10 s4))+[GOOD] (define-fun s12 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe String))) s11)) [GOOD] (define-fun s13 () Bool (ite s12 true false)) [GOOD] (assert s3) [GOOD] (assert s7)@@ -43,9 +44,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (seq.++ (seq.unit (just_SBVMaybe #x00)) (seq.unit nothing_SBVMaybe))))+[RECV] ((s0 (seq.++ (seq.unit (just_SBVMaybe "A")) (seq.unit nothing_SBVMaybe)))) *** Solver   : Z3 *** Exit code: ExitSuccess  FINAL OUTPUT:-[Just '\NUL',Nothing]+[Just 'A',Nothing]
SBVTestSuite/GoldFiles/query_ListOfSum.gold view
@@ -20,7 +20,8 @@ [GOOD] (define-fun s4 () Int 0) [GOOD] (define-fun s8 () Int 1) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Seq (SBVEither Int (_ BitVec 8)))) ; tracks user variable "lst"+[GOOD] (declare-fun s0 () (Seq (SBVEither Int String))) ; tracks user variable "lst"+[GOOD] (assert (forall ((seq0 Int)) (=> (and (>= seq0 0) (< seq0 (seq.len s0))) (=> ((_ is (right_SBVEither (String) (SBVEither Int String))) (seq.nth s0 seq0)) (= 1 (str.len (get_right_SBVEither (seq.nth s0 seq0)))))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -29,13 +30,13 @@ [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (seq.len s0)) [GOOD] (define-fun s3 () Bool (= s1 s2))-[GOOD] (define-fun s5 () (SBVEither Int (_ BitVec 8)) (seq.nth s0 s4))-[GOOD] (define-fun s6 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s5))+[GOOD] (define-fun s5 () (SBVEither Int String) (seq.nth s0 s4))+[GOOD] (define-fun s6 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int String))) s5)) [GOOD] (define-fun s7 () Bool (ite s6 true false)) [GOOD] (define-fun s9 () Int (- s1 s8))-[GOOD] (define-fun s10 () (Seq (SBVEither Int (_ BitVec 8))) (seq.extract s0 s8 s9))-[GOOD] (define-fun s11 () (SBVEither Int (_ BitVec 8)) (seq.nth s10 s4))-[GOOD] (define-fun s12 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s11))+[GOOD] (define-fun s10 () (Seq (SBVEither Int String)) (seq.extract s0 s8 s9))+[GOOD] (define-fun s11 () (SBVEither Int String) (seq.nth s10 s4))+[GOOD] (define-fun s12 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int String))) s11)) [GOOD] (define-fun s13 () Bool (ite s12 false true)) [GOOD] (assert s3) [GOOD] (assert s7)@@ -43,9 +44,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (seq.++ (seq.unit (left_SBVEither 3)) (seq.unit (right_SBVEither #x00)))))+[RECV] ((s0 (seq.++ (seq.unit (left_SBVEither 3)) (seq.unit (right_SBVEither "A"))))) *** Solver   : Z3 *** Exit code: ExitSuccess  FINAL OUTPUT:-[Left 3,Right '\NUL']+[Left 3,Right 'A']
SBVTestSuite/GoldFiles/query_SumMaybeBoth.gold view
@@ -40,11 +40,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (left_SBVEither 0)))+[RECV] ((s0 (left_SBVEither 2))) [SEND] (get-value (s1))-[RECV] ((s1 (just_SBVMaybe 1)))+[RECV] ((s1 (just_SBVMaybe 3))) *** Solver   : Z3 *** Exit code: ExitSuccess  FINAL OUTPUT:-(Left 0,Just 1)+(Left 2,Just 3)
SBVTestSuite/GoldFiles/query_Sums.gold view
@@ -18,7 +18,8 @@ [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 1) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (SBVEither Int (_ BitVec 8))) ; tracks user variable "a"+[GOOD] (declare-fun s0 () (SBVEither Int String)) ; tracks user variable "a"+[GOOD] (assert (=> ((_ is (right_SBVEither (String) (SBVEither Int String))) s0) (= 1 (str.len (get_right_SBVEither s0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -27,7 +28,7 @@ [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (get_left_SBVEither s0)) [GOOD] (define-fun s3 () Bool (= s1 s2))-[GOOD] (define-fun s4 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s0))+[GOOD] (define-fun s4 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int String))) s0)) [GOOD] (define-fun s5 () Bool (ite s4 s3 false)) [GOOD] (assert s5) [SEND] (check-sat)
SBVTestSuite/GoldFiles/query_Tuples1.gold view
@@ -18,7 +18,8 @@ [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 1) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (SBVTuple2 Int (_ BitVec 8))) ; tracks user variable "a"+[GOOD] (declare-fun s0 () (SBVTuple2 Int String)) ; tracks user variable "a"+[GOOD] (assert (= 1 (str.len (proj_2_SBVTuple2 s0)))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -31,9 +32,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (mkSBVTuple2 1 #x00)))+[RECV] ((s0 (mkSBVTuple2 1 "A"))) *** Solver   : Z3 *** Exit code: ExitSuccess  FINAL OUTPUT:-(1,'\NUL')+(1,'A')
SBVTestSuite/GoldFiles/query_Tuples2.gold view
@@ -17,23 +17,24 @@                                                          (proj_2_SBVTuple2 T2)))))) [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s3 () (_ BitVec 8) #x63)+[GOOD] (define-fun s3 () String (_ char #x63)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (SBVTuple2 Int (SBVTuple2 (_ BitVec 8) SBVTuple0))) ; tracks user variable "a"+[GOOD] (declare-fun s0 () (SBVTuple2 Int (SBVTuple2 String SBVTuple0))) ; tracks user variable "a"+[GOOD] (assert (= 1 (str.len (proj_1_SBVTuple2 (proj_2_SBVTuple2 s0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula ----[GOOD] (define-fun s1 () (SBVTuple2 (_ BitVec 8) SBVTuple0) (proj_2_SBVTuple2 s0))-[GOOD] (define-fun s2 () (_ BitVec 8) (proj_1_SBVTuple2 s1))+[GOOD] (define-fun s1 () (SBVTuple2 String SBVTuple0) (proj_2_SBVTuple2 s0))+[GOOD] (define-fun s2 () String (proj_1_SBVTuple2 s1)) [GOOD] (define-fun s4 () Bool (= s2 s3)) [GOOD] (assert s4) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (mkSBVTuple2 0 (mkSBVTuple2 #x63 mkSBVTuple0))))+[RECV] ((s0 (mkSBVTuple2 0 (mkSBVTuple2 "c" mkSBVTuple0)))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/query_badOption.gold view
@@ -30,6 +30,7 @@ ***                  trace (bool) (default: false) ***                  trace_file_name (string) (default: z3.log) ***                  type_check (bool) (default: true)+***                  unicode (bool) ***                  unsat_core (bool) (default: false) ***                  verbose (unsigned int) (default: 0) ***                  warning (bool) (default: true)
SBVTestSuite/GoldFiles/query_boolector.gold view
@@ -1,8 +1,7 @@ ** Calling: boolector --smt2 --smt2-model --no-exit-codes --incremental [GOOD] ; Automatically generated by SBV. Do not edit. [GOOD] (set-option :print-success true)-** Backend solver Boolector does not support global decls.-** Some incremental calls, such as pop, will be limited.+[GOOD] (set-option :global-declarations true) [GOOD] (set-option :produce-models true) [GOOD] (set-logic ALL) ; external query, using all logics. [GOOD] ; --- uninterpreted sorts ---
SBVTestSuite/GoldFiles/query_sumMergeEither1.gold view
@@ -33,13 +33,13 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (left_SBVEither 0)))+[RECV] ((s0 (left_SBVEither 2))) [SEND] (get-value (s1))-[RECV] ((s1 (left_SBVEither 0)))+[RECV] ((s1 (left_SBVEither 2))) [SEND] (get-value (s2)) [RECV] ((s2 false)) *** Solver   : Z3 *** Exit code: ExitSuccess  FINAL OUTPUT:-(Left 0,Left 0,False)+(Left 2,Left 2,False)
SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold view
@@ -33,13 +33,13 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (just_SBVMaybe 0)))+[RECV] ((s0 (just_SBVMaybe 2))) [SEND] (get-value (s1))-[RECV] ((s1 (just_SBVMaybe 0)))+[RECV] ((s1 (just_SBVMaybe 2))) [SEND] (get-value (s2)) [RECV] ((s2 false)) *** Solver   : Z3 *** Exit code: ExitSuccess  FINAL OUTPUT:-(Just 0,Just 0,False)+(Just 2,Just 2,False)
SBVTestSuite/GoldFiles/query_uisatex1.gold view
@@ -29,12 +29,12 @@ [GOOD] (define-fun s32 () Int 121) [GOOD] (define-fun s37 () Int 8) [GOOD] (define-fun s39 () (_ FloatingPoint  8 24) (_ +oo 8 24))-[GOOD] (define-fun s41 () (_ BitVec 8) #x63)+[GOOD] (define-fun s41 () String (_ char #x63)) [GOOD] (define-fun s42 () String "hey") [GOOD] (define-fun s44 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0))) [GOOD] (define-fun s46 () String "tey") [GOOD] (define-fun s48 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0)))-[GOOD] (define-fun s50 () (_ BitVec 8) #x72)+[GOOD] (define-fun s50 () String (_ char #x72)) [GOOD] (define-fun s51 () String "foo") [GOOD] (define-fun s53 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0))) [GOOD] (define-fun s55 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))@@ -54,7 +54,7 @@ [GOOD] (declare-fun q1 (Int) Int) [GOOD] (declare-fun q2 (Bool Int) Int) [GOOD] (declare-fun q3 ((_ FloatingPoint  8 24) Bool Int) (_ FloatingPoint  8 24))-[GOOD] (declare-fun q4 ((_ BitVec 8) String) (_ FloatingPoint  8 24))+[GOOD] (declare-fun q4 (String String) (_ FloatingPoint  8 24)) [GOOD] (declare-fun q5 ((Seq Int) (Seq (_ FloatingPoint  8 24))) Int) [GOOD] ; --- user given axioms --- [GOOD] ; --- formula ---@@ -133,10 +133,10 @@               (_ +oo 8 24)))) [SEND] (get-value (q4)) [RECV] ((q4 (store (store ((as const Array) (fp #b0 #x85 #b00111000000000000000000))-                     #x63+                     "c"                      "tey"                      (fp #b0 #x85 #b01110000000000000000000))-              #x72+              "r"               "foo"               (fp #b0 #x80 #b11000000000000000000000)))) [SEND] (get-value (q5))
SBVTestSuite/GoldFiles/query_uisatex2.gold view
@@ -29,12 +29,12 @@ [GOOD] (define-fun s32 () Int 121) [GOOD] (define-fun s37 () Int 8) [GOOD] (define-fun s39 () (_ FloatingPoint  8 24) (_ +oo 8 24))-[GOOD] (define-fun s41 () (_ BitVec 8) #x63)+[GOOD] (define-fun s41 () String (_ char #x63)) [GOOD] (define-fun s42 () String "hey") [GOOD] (define-fun s44 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0))) [GOOD] (define-fun s46 () String "tey") [GOOD] (define-fun s48 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0)))-[GOOD] (define-fun s50 () (_ BitVec 8) #x72)+[GOOD] (define-fun s50 () String (_ char #x72)) [GOOD] (define-fun s51 () String "foo") [GOOD] (define-fun s53 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0))) [GOOD] (define-fun s55 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))@@ -54,7 +54,7 @@ [GOOD] (declare-fun q1 (Int) Int) [GOOD] (declare-fun q2 (Bool Int) Int) [GOOD] (declare-fun q3 ((_ FloatingPoint  8 24) Bool Int) (_ FloatingPoint  8 24))-[GOOD] (declare-fun q4 ((_ BitVec 8) String) (_ FloatingPoint  8 24))+[GOOD] (declare-fun q4 (String String) (_ FloatingPoint  8 24)) [GOOD] (declare-fun q5 ((Seq Int) (Seq (_ FloatingPoint  8 24))) Int) [GOOD] (declare-fun q6 (Int) Bool) [GOOD] ; --- user given axioms ---@@ -133,10 +133,10 @@               (_ +oo 8 24)))) [SEND] (get-value (q4)) [RECV] ((q4 (store (store ((as const Array) (fp #b0 #x85 #b00111000000000000000000))-                     #x63+                     "c"                      "tey"                      (fp #b0 #x85 #b01110000000000000000000))-              #x72+              "r"               "foo"               (fp #b0 #x80 #b11000000000000000000000)))) [SEND] (get-value (q5))
SBVTestSuite/GoldFiles/query_yices.gold view
@@ -1,8 +1,7 @@ ** Calling: yices-smt2 --incremental [GOOD] ; Automatically generated by SBV. Do not edit. [GOOD] (set-option :print-success true)-** Backend solver Yices does not support global decls.-** Some incremental calls, such as pop, will be limited.+[GOOD] (set-option :global-declarations true) [GOOD] (set-option :produce-models true) [GOOD] (set-logic ALL) ; external query, using all logics. [GOOD] ; --- uninterpreted sorts ---
SBVTestSuite/GoldFiles/set_compl1.gold view
@@ -13,9 +13,10 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s1 () (Array (_ BitVec 8) Bool) (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false) #x6f true) #x6c true) #x68 true) #x65 true))+[GOOD] (define-fun s1 () (Array String Bool) (store (store (store (store ((as const (Array String Bool)) false) (_ char #x6f) true) (_ char #x6c) true) (_ char #x68) true) (_ char #x65) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -27,43 +28,37 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                   #x65-                                   true)-                            #x68+[RECV] ((s0 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6c+                     "h"                      true)-              #x6f+              "e"               true)))-[GOOD] (define-fun s3 () (Array (_ BitVec 8) Bool) (complement s0))+[GOOD] (define-fun s3 () (Array String Bool) (complement s0)) [SEND] (get-value (s3))-[RECV] ((s3 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) true)-                                   #x65-                                   false)-                            #x68+[RECV] ((s3 (store (store (store (store ((as const (Array String Bool)) true) "o" false)+                            "l"                             false)-                     #x6c+                     "h"                      false)-              #x6f+              "e"               false)))-[GOOD] (define-fun s4 () (Array (_ BitVec 8) Bool) (complement s3))+[GOOD] (define-fun s4 () (Array String Bool) (complement s3)) [SEND] (get-value (s4))-[RECV] ((s4 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                   #x65-                                   true)-                            #x68+[RECV] ((s4 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6c+                     "h"                      true)-              #x6f+              "e"               true)))-[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (intersection s3 s0))+[GOOD] (define-fun s5 () (Array String Bool) (intersection s3 s0)) [SEND] (get-value (s5))-[RECV] ((s5 ((as const (Array (_ BitVec 8) Bool)) false)))-[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (union s3 s0))+[RECV] ((s5 ((as const (Array String Bool)) false)))+[GOOD] (define-fun s6 () (Array String Bool) (union s3 s0)) [SEND] (get-value (s6))-[RECV] ((s6 ((as const (Array (_ BitVec 8) Bool)) true)))+[RECV] ((s6 ((as const (Array String Bool)) true))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/set_delete1.gold view
@@ -13,11 +13,13 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (_ BitVec 8) #x65)-[GOOD] (define-fun s4 () (Array (_ BitVec 8) Bool) (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false) #x6f true) #x6c true) #x68 true) #x65 true))+[GOOD] (define-fun s2 () String (_ char #x65))+[GOOD] (define-fun s4 () (Array String Bool) (store (store (store (store ((as const (Array String Bool)) false) (_ char #x6f) true) (_ char #x6c) true) (_ char #x68) true) (_ char #x65) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () String) ; tracks user variable "a"+[GOOD] (assert (= 1 (str.len s0)))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -31,43 +33,33 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 #x65))+[RECV] ((s0 "e")) [SEND] (get-value (s1))-[RECV] ((s1 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                   #x65-                                   true)-                            #x68+[RECV] ((s1 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6c+                     "h"                      true)-              #x6f+              "e"               true)))-[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (store s1 s0 false))+[GOOD] (define-fun s6 () (Array String Bool) (store s1 s0 false)) [SEND] (get-value (s6))-[RECV] ((s6 (store (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                          #x65-                                          true)-                                   #x68-                                   true)-                            #x6c+[RECV] ((s6 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6f+                     "h"                      true)-              #x65+              "e"               false)))-[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (complement s1))-[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (store s7 s0 false))+[GOOD] (define-fun s7 () (Array String Bool) (complement s1))+[GOOD] (define-fun s8 () (Array String Bool) (store s7 s0 false)) [SEND] (get-value (s8))-[RECV] ((s8 (store (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) true)-                                          #x65-                                          false)-                                   #x68-                                   false)-                            #x6c+[RECV] ((s8 (store (store (store (store ((as const (Array String Bool)) true) "o" false)+                            "l"                             false)-                     #x6f+                     "h"                      false)-              #x65+              "e"               false))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/set_diff1.gold view
@@ -13,10 +13,12 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (Array (_ BitVec 8) Bool) (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))+[GOOD] (define-fun s2 () (Array String Bool) (store ((as const (Array String Bool)) false) (_ char #x61) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0)))))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -30,23 +32,23 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))+[RECV] ((s0 (store ((as const (Array String Bool)) false) "a" true))) [SEND] (get-value (s1))-[RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))-[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (setminus s0 s1))+[RECV] ((s1 (store ((as const (Array String Bool)) false) "a" true)))+[GOOD] (define-fun s5 () (Array String Bool) (setminus s0 s1)) [SEND] (get-value (s5))-[RECV] ((s5 ((as const (Array (_ BitVec 8) Bool)) false)))-[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (complement s1))-[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (setminus s0 s6))+[RECV] ((s5 ((as const (Array String Bool)) false)))+[GOOD] (define-fun s6 () (Array String Bool) (complement s1))+[GOOD] (define-fun s7 () (Array String Bool) (setminus s0 s6)) [SEND] (get-value (s7))-[RECV] ((s7 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))-[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s0))-[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (setminus s8 s1))+[RECV] ((s7 (store ((as const (Array String Bool)) false) "a" true)))+[GOOD] (define-fun s8 () (Array String Bool) (complement s0))+[GOOD] (define-fun s9 () (Array String Bool) (setminus s8 s1)) [SEND] (get-value (s9))-[RECV] ((s9 (store ((as const (Array (_ BitVec 8) Bool)) true) #x61 false)))-[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) (setminus s8 s6))+[RECV] ((s9 (store ((as const (Array String Bool)) true) "a" false)))+[GOOD] (define-fun s10 () (Array String Bool) (setminus s8 s6)) [SEND] (get-value (s10))-[RECV] ((s10 ((as const (Array (_ BitVec 8) Bool)) false)))+[RECV] ((s10 ((as const (Array String Bool)) false))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/set_disj1.gold view
@@ -13,10 +13,12 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (Array (_ BitVec 8) Bool) (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))+[GOOD] (define-fun s2 () (Array String Bool) (store ((as const (Array String Bool)) false) (_ char #x61) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0)))))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -30,25 +32,25 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))+[RECV] ((s0 (store ((as const (Array String Bool)) false) "a" true))) [SEND] (get-value (s1))-[RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))-[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) ((as const (Array (_ BitVec 8) Bool)) false))-[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (intersection s0 s1))+[RECV] ((s1 (store ((as const (Array String Bool)) false) "a" true)))+[GOOD] (define-fun s6 () (Array String Bool) ((as const (Array String Bool)) false))+[GOOD] (define-fun s5 () (Array String Bool) (intersection s0 s1)) [GOOD] (define-fun s7 () Bool (= s5 s6)) [SEND] (get-value (s7)) [RECV] ((s7 false))-[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s1))-[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (intersection s0 s8))+[GOOD] (define-fun s8 () (Array String Bool) (complement s1))+[GOOD] (define-fun s9 () (Array String Bool) (intersection s0 s8)) [GOOD] (define-fun s10 () Bool (= s9 s6)) [SEND] (get-value (s10)) [RECV] ((s10 true))-[GOOD] (define-fun s11 () (Array (_ BitVec 8) Bool) (complement s0))-[GOOD] (define-fun s12 () (Array (_ BitVec 8) Bool) (intersection s11 s1))+[GOOD] (define-fun s11 () (Array String Bool) (complement s0))+[GOOD] (define-fun s12 () (Array String Bool) (intersection s11 s1)) [GOOD] (define-fun s13 () Bool (= s12 s6)) [SEND] (get-value (s13)) [RECV] ((s13 true))-[GOOD] (define-fun s14 () (Array (_ BitVec 8) Bool) (intersection s11 s8))+[GOOD] (define-fun s14 () (Array String Bool) (intersection s11 s8)) [GOOD] (define-fun s15 () Bool (= s14 s6)) [SEND] (get-value (s15)) [RECV] ((s15 false))
SBVTestSuite/GoldFiles/set_empty1.gold view
@@ -13,9 +13,10 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s1 () (Array (_ BitVec 8) Bool) (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false) #x6f true) #x6c true) #x68 true) #x65 true))+[GOOD] (define-fun s1 () (Array String Bool) (store (store (store (store ((as const (Array String Bool)) false) (_ char #x6f) true) (_ char #x6c) true) (_ char #x68) true) (_ char #x65) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -27,20 +28,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                   #x65-                                   true)-                            #x68+[RECV] ((s0 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6c+                     "h"                      true)-              #x6f+              "e"               true)))-[GOOD] (define-fun s3 () (Array (_ BitVec 8) Bool) ((as const (Array (_ BitVec 8) Bool)) false))+[GOOD] (define-fun s3 () (Array String Bool) ((as const (Array String Bool)) false)) [GOOD] (define-fun s4 () Bool (= s0 s3)) [SEND] (get-value (s4)) [RECV] ((s4 false))-[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (complement s0))+[GOOD] (define-fun s5 () (Array String Bool) (complement s0)) [GOOD] (define-fun s6 () Bool (= s5 s3)) [SEND] (get-value (s6)) [RECV] ((s6 false))
SBVTestSuite/GoldFiles/set_full1.gold view
@@ -13,9 +13,10 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s1 () (Array (_ BitVec 8) Bool) (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false) #x6f true) #x6c true) #x68 true) #x65 true))+[GOOD] (define-fun s1 () (Array String Bool) (store (store (store (store ((as const (Array String Bool)) false) (_ char #x6f) true) (_ char #x6c) true) (_ char #x68) true) (_ char #x65) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -27,20 +28,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                   #x65-                                   true)-                            #x68+[RECV] ((s0 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6c+                     "h"                      true)-              #x6f+              "e"               true)))-[GOOD] (define-fun s3 () (Array (_ BitVec 8) Bool) ((as const (Array (_ BitVec 8) Bool)) true))+[GOOD] (define-fun s3 () (Array String Bool) ((as const (Array String Bool)) true)) [GOOD] (define-fun s4 () Bool (= s0 s3)) [SEND] (get-value (s4)) [RECV] ((s4 false))-[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (complement s0))+[GOOD] (define-fun s5 () (Array String Bool) (complement s0)) [GOOD] (define-fun s6 () Bool (= s5 s3)) [SEND] (get-value (s6)) [RECV] ((s6 false))
SBVTestSuite/GoldFiles/set_insert1.gold view
@@ -13,11 +13,13 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (_ BitVec 8) #x65)-[GOOD] (define-fun s4 () (Array (_ BitVec 8) Bool) (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false) #x6f true) #x6c true) #x68 true) #x65 true))+[GOOD] (define-fun s2 () String (_ char #x65))+[GOOD] (define-fun s4 () (Array String Bool) (store (store (store (store ((as const (Array String Bool)) false) (_ char #x6f) true) (_ char #x6c) true) (_ char #x68) true) (_ char #x65) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () String) ; tracks user variable "a"+[GOOD] (assert (= 1 (str.len s0)))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -31,43 +33,33 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 #x65))+[RECV] ((s0 "e")) [SEND] (get-value (s1))-[RECV] ((s1 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                   #x65-                                   true)-                            #x68+[RECV] ((s1 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6c+                     "h"                      true)-              #x6f+              "e"               true)))-[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (store s1 s0 true))+[GOOD] (define-fun s6 () (Array String Bool) (store s1 s0 true)) [SEND] (get-value (s6))-[RECV] ((s6 (store (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                          #x65-                                          true)-                                   #x68-                                   true)-                            #x6c+[RECV] ((s6 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6f+                     "h"                      true)-              #x65+              "e"               true)))-[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (complement s1))-[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (store s7 s0 true))+[GOOD] (define-fun s7 () (Array String Bool) (complement s1))+[GOOD] (define-fun s8 () (Array String Bool) (store s7 s0 true)) [SEND] (get-value (s8))-[RECV] ((s8 (store (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) true)-                                          #x65-                                          false)-                                   #x68-                                   false)-                            #x6c+[RECV] ((s8 (store (store (store (store ((as const (Array String Bool)) true) "o" false)+                            "l"                             false)-                     #x6f+                     "h"                      false)-              #x65+              "e"               true))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/set_intersect1.gold view
@@ -13,10 +13,12 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (Array (_ BitVec 8) Bool) (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))+[GOOD] (define-fun s2 () (Array String Bool) (store ((as const (Array String Bool)) false) (_ char #x61) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0)))))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -30,23 +32,23 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))+[RECV] ((s0 (store ((as const (Array String Bool)) false) "a" true))) [SEND] (get-value (s1))-[RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))-[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (intersection s0 s1))+[RECV] ((s1 (store ((as const (Array String Bool)) false) "a" true)))+[GOOD] (define-fun s5 () (Array String Bool) (intersection s0 s1)) [SEND] (get-value (s5))-[RECV] ((s5 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))-[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (complement s1))-[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (intersection s0 s6))+[RECV] ((s5 (store ((as const (Array String Bool)) false) "a" true)))+[GOOD] (define-fun s6 () (Array String Bool) (complement s1))+[GOOD] (define-fun s7 () (Array String Bool) (intersection s0 s6)) [SEND] (get-value (s7))-[RECV] ((s7 ((as const (Array (_ BitVec 8) Bool)) false)))-[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s0))-[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (intersection s8 s1))+[RECV] ((s7 ((as const (Array String Bool)) false)))+[GOOD] (define-fun s8 () (Array String Bool) (complement s0))+[GOOD] (define-fun s9 () (Array String Bool) (intersection s8 s1)) [SEND] (get-value (s9))-[RECV] ((s9 ((as const (Array (_ BitVec 8) Bool)) false)))-[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) (intersection s8 s6))+[RECV] ((s9 ((as const (Array String Bool)) false)))+[GOOD] (define-fun s10 () (Array String Bool) (intersection s8 s6)) [SEND] (get-value (s10))-[RECV] ((s10 (store ((as const (Array (_ BitVec 8) Bool)) true) #x61 false)))+[RECV] ((s10 (store ((as const (Array String Bool)) true) "a" false))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/set_member1.gold view
@@ -13,11 +13,13 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (_ BitVec 8) #x65)-[GOOD] (define-fun s4 () (Array (_ BitVec 8) Bool) (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false) #x6f true) #x6c true) #x68 true) #x65 true))+[GOOD] (define-fun s2 () String (_ char #x65))+[GOOD] (define-fun s4 () (Array String Bool) (store (store (store (store ((as const (Array String Bool)) false) (_ char #x6f) true) (_ char #x6c) true) (_ char #x68) true) (_ char #x65) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () String) ; tracks user variable "a"+[GOOD] (assert (= 1 (str.len s0)))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -31,21 +33,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 #x65))+[RECV] ((s0 "e")) [SEND] (get-value (s1))-[RECV] ((s1 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                   #x65-                                   true)-                            #x68+[RECV] ((s1 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6c+                     "h"                      true)-              #x6f+              "e"               true))) [GOOD] (define-fun s6 () Bool (select s1 s0)) [SEND] (get-value (s6)) [RECV] ((s6 true))-[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (complement s1))+[GOOD] (define-fun s7 () (Array String Bool) (complement s1)) [GOOD] (define-fun s8 () Bool (select s7 s0)) [SEND] (get-value (s8)) [RECV] ((s8 false))
SBVTestSuite/GoldFiles/set_notMember1.gold view
@@ -13,11 +13,13 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (_ BitVec 8) #x65)-[GOOD] (define-fun s4 () (Array (_ BitVec 8) Bool) (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false) #x6f true) #x6c true) #x68 true) #x65 true))+[GOOD] (define-fun s2 () String (_ char #x65))+[GOOD] (define-fun s4 () (Array String Bool) (store (store (store (store ((as const (Array String Bool)) false) (_ char #x6f) true) (_ char #x6c) true) (_ char #x68) true) (_ char #x65) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () String) ; tracks user variable "a"+[GOOD] (assert (= 1 (str.len s0)))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -31,22 +33,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 #x65))+[RECV] ((s0 "e")) [SEND] (get-value (s1))-[RECV] ((s1 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false)-                                   #x65-                                   true)-                            #x68+[RECV] ((s1 (store (store (store (store ((as const (Array String Bool)) false) "o" true)+                            "l"                             true)-                     #x6c+                     "h"                      true)-              #x6f+              "e"               true))) [GOOD] (define-fun s6 () Bool (select s1 s0)) [GOOD] (define-fun s7 () Bool (not s6)) [SEND] (get-value (s7)) [RECV] ((s7 false))-[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s1))+[GOOD] (define-fun s8 () (Array String Bool) (complement s1)) [GOOD] (define-fun s9 () Bool (select s8 s0)) [GOOD] (define-fun s10 () Bool (not s9)) [SEND] (get-value (s10))
SBVTestSuite/GoldFiles/set_psubset1.gold view
@@ -13,10 +13,12 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (Array (_ BitVec 8) Bool) (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))+[GOOD] (define-fun s2 () (Array String Bool) (store ((as const (Array String Bool)) false) (_ char #x61) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0)))))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -30,23 +32,23 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))+[RECV] ((s0 (store ((as const (Array String Bool)) false) "a" true))) [SEND] (get-value (s1))-[RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))+[RECV] ((s1 (store ((as const (Array String Bool)) false) "a" true))) [GOOD] (define-fun s5 () Bool (subset s0 s1)) [GOOD] (define-fun s6 () Bool (= s0 s1)) [GOOD] (define-fun s7 () Bool (not s6)) [GOOD] (define-fun s8 () Bool (and s5 s7)) [SEND] (get-value (s8)) [RECV] ((s8 false))-[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (complement s1))+[GOOD] (define-fun s9 () (Array String Bool) (complement s1)) [GOOD] (define-fun s10 () Bool (subset s0 s9)) [GOOD] (define-fun s11 () Bool (= s0 s9)) [GOOD] (define-fun s12 () Bool (not s11)) [GOOD] (define-fun s13 () Bool (and s10 s12)) [SEND] (get-value (s13)) [RECV] ((s13 false))-[GOOD] (define-fun s14 () (Array (_ BitVec 8) Bool) (complement s0))+[GOOD] (define-fun s14 () (Array String Bool) (complement s0)) [GOOD] (define-fun s15 () Bool (subset s14 s1)) [GOOD] (define-fun s16 () Bool (= s14 s1)) [GOOD] (define-fun s17 () Bool (not s16))
SBVTestSuite/GoldFiles/set_subset1.gold view
@@ -13,10 +13,12 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (Array (_ BitVec 8) Bool) (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))+[GOOD] (define-fun s2 () (Array String Bool) (store ((as const (Array String Bool)) false) (_ char #x61) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0)))))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -30,17 +32,17 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))+[RECV] ((s0 (store ((as const (Array String Bool)) false) "a" true))) [SEND] (get-value (s1))-[RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))+[RECV] ((s1 (store ((as const (Array String Bool)) false) "a" true))) [GOOD] (define-fun s5 () Bool (subset s0 s1)) [SEND] (get-value (s5)) [RECV] ((s5 true))-[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (complement s1))+[GOOD] (define-fun s6 () (Array String Bool) (complement s1)) [GOOD] (define-fun s7 () Bool (subset s0 s6)) [SEND] (get-value (s7)) [RECV] ((s7 false))-[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s0))+[GOOD] (define-fun s8 () (Array String Bool) (complement s0)) [GOOD] (define-fun s9 () Bool (subset s8 s1)) [SEND] (get-value (s9)) [RECV] ((s9 false))
SBVTestSuite/GoldFiles/set_union1.gold view
@@ -13,10 +13,12 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ----[GOOD] (define-fun s2 () (Array (_ BitVec 8) Bool) (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))+[GOOD] (define-fun s2 () (Array String Bool) (store ((as const (Array String Bool)) false) (_ char #x61) true)) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (Array (_ BitVec 8) Bool)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (Array (_ BitVec 8) Bool)) ; tracks user variable "b"+[GOOD] (declare-fun s0 () (Array String Bool)) ; tracks user variable "a"+[GOOD] (assert (forall ((set0 String)) (=> (select s0 set0) (= 1 (str.len set0)))))+[GOOD] (declare-fun s1 () (Array String Bool)) ; tracks user variable "b"+[GOOD] (assert (forall ((set0 String)) (=> (select s1 set0) (= 1 (str.len set0))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -30,23 +32,23 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))+[RECV] ((s0 (store ((as const (Array String Bool)) false) "a" true))) [SEND] (get-value (s1))-[RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))-[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (union s0 s1))+[RECV] ((s1 (store ((as const (Array String Bool)) false) "a" true)))+[GOOD] (define-fun s5 () (Array String Bool) (union s0 s1)) [SEND] (get-value (s5))-[RECV] ((s5 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true)))-[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (complement s1))-[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (union s0 s6))+[RECV] ((s5 (store ((as const (Array String Bool)) false) "a" true)))+[GOOD] (define-fun s6 () (Array String Bool) (complement s1))+[GOOD] (define-fun s7 () (Array String Bool) (union s0 s6)) [SEND] (get-value (s7))-[RECV] ((s7 ((as const (Array (_ BitVec 8) Bool)) true)))-[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s0))-[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (union s8 s1))+[RECV] ((s7 ((as const (Array String Bool)) true)))+[GOOD] (define-fun s8 () (Array String Bool) (complement s0))+[GOOD] (define-fun s9 () (Array String Bool) (union s8 s1)) [SEND] (get-value (s9))-[RECV] ((s9 ((as const (Array (_ BitVec 8) Bool)) true)))-[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) (union s8 s6))+[RECV] ((s9 ((as const (Array String Bool)) true)))+[GOOD] (define-fun s10 () (Array String Bool) (union s8 s6)) [SEND] (get-value (s10))-[RECV] ((s10 (store ((as const (Array (_ BitVec 8) Bool)) true) #x61 false)))+[RECV] ((s10 (store ((as const (Array String Bool)) true) "a" false))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/sumLiftEither.gold view
@@ -18,18 +18,19 @@ [GOOD] ; --- literal constants --- [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "i"-[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "c"+[GOOD] (declare-fun s1 () String) ; tracks user variable "c"+[GOOD] (assert (= 1 (str.len s1))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula ----[GOOD] (define-fun s2 () (SBVEither Int (_ BitVec 8)) ((as left_SBVEither (SBVEither Int (_ BitVec 8))) s0))-[GOOD] (define-fun s3 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s2))+[GOOD] (define-fun s2 () (SBVEither Int String) ((as left_SBVEither (SBVEither Int String)) s0))+[GOOD] (define-fun s3 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int String))) s2)) [GOOD] (define-fun s4 () Bool (ite s3 true false))-[GOOD] (define-fun s5 () (SBVEither Int (_ BitVec 8)) ((as right_SBVEither (SBVEither Int (_ BitVec 8))) s1))-[GOOD] (define-fun s6 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s5))+[GOOD] (define-fun s5 () (SBVEither Int String) ((as right_SBVEither (SBVEither Int String)) s1))+[GOOD] (define-fun s6 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int String))) s5)) [GOOD] (define-fun s7 () Bool (ite s6 false true)) [GOOD] (assert s4) [GOOD] (assert s7)@@ -38,8 +39,8 @@ [SEND] (get-value (s0)) [RECV] ((s0 0)) [SEND] (get-value (s1))-[RECV] ((s1 #x00))+[RECV] ((s1 "A")) -MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("i",0 :: Integer),("c",'\NUL' :: Char)], modelUIFuns = []}+MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("i",0 :: Integer),("c",'A' :: Char)], modelUIFuns = []} DONE.*** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/sumMaybeBoth.gold view
@@ -37,10 +37,10 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (left_SBVEither 0)))+[RECV] ((s0 (left_SBVEither 2))) [SEND] (get-value (s1))-[RECV] ((s1 (just_SBVMaybe 1)))+[RECV] ((s1 (just_SBVMaybe 3))) -MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Left 0 :: Either Integer Integer),("s1",Just 1 :: Maybe Integer)], modelUIFuns = []}+MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Left 2 :: Either Integer Integer),("s1",Just 3 :: Maybe Integer)], modelUIFuns = []} DONE.*** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/sumMergeEither1.gold view
@@ -33,12 +33,12 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (left_SBVEither 0)))+[RECV] ((s0 (left_SBVEither 2))) [SEND] (get-value (s1))-[RECV] ((s1 (left_SBVEither 0)))+[RECV] ((s1 (left_SBVEither 2))) [SEND] (get-value (s2)) [RECV] ((s2 false)) -MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Left 0 :: Either Integer Bool),("s1",Left 0 :: Either Integer Bool),("s2",False :: Bool)], modelUIFuns = []}+MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Left 2 :: Either Integer Bool),("s1",Left 2 :: Either Integer Bool),("s2",False :: Bool)], modelUIFuns = []} DONE.*** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/sumMergeMaybe2.gold view
@@ -33,12 +33,12 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (just_SBVMaybe 0)))+[RECV] ((s0 (just_SBVMaybe 2))) [SEND] (get-value (s1))-[RECV] ((s1 (just_SBVMaybe 0)))+[RECV] ((s1 (just_SBVMaybe 2))) [SEND] (get-value (s2)) [RECV] ((s2 false)) -MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Just 0 :: Maybe Integer),("s1",Just 0 :: Maybe Integer),("s2",False :: Bool)], modelUIFuns = []}+MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Just 2 :: Maybe Integer),("s1",Just 2 :: Maybe Integer),("s2",False :: Bool)], modelUIFuns = []} DONE.*** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/tuple_enum.gold view
@@ -64,8 +64,9 @@                                            ((mkSBVTuple3 (proj_1_SBVTuple3 T1)                                                          (proj_2_SBVTuple3 T2)                                                          (proj_3_SBVTuple3 T3))))))-[GOOD] (declare-fun s24 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E (_ BitVec 8) (_ FloatingPoint  8 24))))-[GOOD] (define-fun s25 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E (_ BitVec 8) (_ FloatingPoint  8 24))) (mkSBVTuple2 #x05 (mkSBVTuple3 C #x41 ((_ to_fp 8 24) roundNearestTiesToEven (/ 8514437.0 1048576.0)))))+[GOOD] (declare-fun s24 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E String (_ FloatingPoint  8 24))))+[GOOD] (assert (= 1 (str.len (proj_2_SBVTuple3 (proj_2_SBVTuple2 s24)))))+[GOOD] (define-fun s25 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E String (_ FloatingPoint  8 24))) (mkSBVTuple2 #x05 (mkSBVTuple3 C (_ char #x41) ((_ to_fp 8 24) roundNearestTiesToEven (/ 8514437.0 1048576.0))))) [GOOD] (define-fun s26 () Bool (= s24 s25)) [GOOD] (assert s26) [GOOD] (define-fun s27 () (Seq (SBVTuple2 E (Seq Bool))) (seq.++ (seq.unit (mkSBVTuple2 B (as seq.empty (Seq Bool)))) (seq.unit (mkSBVTuple2 A (seq.++ (seq.unit true) (seq.unit false)))) (seq.unit (mkSBVTuple2 C (seq.++ (seq.unit false) (seq.unit false) (seq.unit false) (seq.unit false) (seq.unit true) (seq.unit false))))))@@ -83,7 +84,7 @@                                               (seq.unit false)                                               (seq.++ (seq.unit true) (seq.unit false)))))))) [SEND] (get-value (s24))-[RECV] ((s24 (mkSBVTuple2 #x05 (mkSBVTuple3 C #x41 (fp #b0 #x82 #b00000011110101110000101)))))+[RECV] ((s24 (mkSBVTuple2 #x05 (mkSBVTuple3 C "A" (fp #b0 #x82 #b00000011110101110000101))))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/tuple_nested.gold view
@@ -18,23 +18,24 @@ [GOOD] ; --- literal constants --- [GOOD] (define-fun s3 () Int 1) [GOOD] (define-fun s7 () String "foo")-[GOOD] (define-fun s10 () (_ BitVec 8) #x63)+[GOOD] (define-fun s10 () String (_ char #x63)) [GOOD] (define-fun s13 () (_ BitVec 8) #x00) [GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (SBVTuple2 (SBVTuple2 Int (SBVTuple2 String (_ BitVec 8))) (_ BitVec 8))) ; tracks user variable "abcd"+[GOOD] (declare-fun s0 () (SBVTuple2 (SBVTuple2 Int (SBVTuple2 String String)) (_ BitVec 8))) ; tracks user variable "abcd"+[GOOD] (assert (= 1 (str.len (proj_2_SBVTuple2 (proj_2_SBVTuple2 (proj_1_SBVTuple2 s0)))))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula ----[GOOD] (define-fun s1 () (SBVTuple2 Int (SBVTuple2 String (_ BitVec 8))) (proj_1_SBVTuple2 s0))+[GOOD] (define-fun s1 () (SBVTuple2 Int (SBVTuple2 String String)) (proj_1_SBVTuple2 s0)) [GOOD] (define-fun s2 () Int (proj_1_SBVTuple2 s1)) [GOOD] (define-fun s4 () Bool (= s2 s3))-[GOOD] (define-fun s5 () (SBVTuple2 String (_ BitVec 8)) (proj_2_SBVTuple2 s1))+[GOOD] (define-fun s5 () (SBVTuple2 String String) (proj_2_SBVTuple2 s1)) [GOOD] (define-fun s6 () String (proj_1_SBVTuple2 s5)) [GOOD] (define-fun s8 () Bool (= s6 s7))-[GOOD] (define-fun s9 () (_ BitVec 8) (proj_2_SBVTuple2 s5))+[GOOD] (define-fun s9 () String (proj_2_SBVTuple2 s5)) [GOOD] (define-fun s11 () Bool (= s9 s10)) [GOOD] (define-fun s12 () (_ BitVec 8) (proj_2_SBVTuple2 s0)) [GOOD] (define-fun s14 () Bool (= s12 s13))@@ -45,7 +46,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (mkSBVTuple2 (mkSBVTuple2 1 (mkSBVTuple2 "foo" #x63)) #x00)))+[RECV] ((s0 (mkSBVTuple2 (mkSBVTuple2 1 (mkSBVTuple2 "foo" "c")) #x00))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/tuple_twoTwo.gold view
@@ -17,10 +17,11 @@ [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s3 () Int 1)-[GOOD] (define-fun s6 () (_ BitVec 8) #x63)+[GOOD] (define-fun s6 () String (_ char #x63)) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (SBVTuple2 Int String)) ; tracks user variable "ab"-[GOOD] (declare-fun s1 () (SBVTuple2 (_ BitVec 8) (_ BitVec 8))) ; tracks user variable "cd"+[GOOD] (declare-fun s1 () (SBVTuple2 String (_ BitVec 8))) ; tracks user variable "cd"+[GOOD] (assert (= 1 (str.len (proj_1_SBVTuple2 s1)))) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays ---@@ -29,7 +30,7 @@ [GOOD] ; --- formula --- [GOOD] (define-fun s2 () Int (proj_1_SBVTuple2 s0)) [GOOD] (define-fun s4 () Bool (= s2 s3))-[GOOD] (define-fun s5 () (_ BitVec 8) (proj_1_SBVTuple2 s1))+[GOOD] (define-fun s5 () String (proj_1_SBVTuple2 s1)) [GOOD] (define-fun s7 () Bool (= s5 s6)) [GOOD] (assert s4) [GOOD] (assert s7)@@ -38,7 +39,7 @@ [SEND] (get-value (s0)) [RECV] ((s0 (mkSBVTuple2 1 ""))) [SEND] (get-value (s1))-[RECV] ((s1 (mkSBVTuple2 #x63 #x00)))+[RECV] ((s1 (mkSBVTuple2 "c" #x00))) *** Solver   : Z3 *** Exit code: ExitSuccess
SBVTestSuite/SBVConnectionTest.hs view
@@ -54,7 +54,7 @@             models "t2" t2 (== ([2,62,66,126,130,190,194,254]::[Word8]))             models "t3" t3 (== ([]::[Word8]))             models "t4" t4 (== [4::Word8])-  where models m p f = (extractModels <$> allSat p) >>= decide s m f . sort+  where models m p f = allSat p >>= (decide s m f . sort) . extractModels         t0 x = x   .== x+(1::SWord8)         t1 x = x*2 .== x+(x::SWord8)         t2 x = x*x .== (4::SWord8)
SBVTestSuite/SBVDocTest.hs view
@@ -25,6 +25,14 @@  import System.Random (randomRIO) +-- For temporarily testing only a few files+testOnly :: FilePath -> Bool+testOnly f = case only of+               Nothing -> True+               Just xs -> any (`isSuffixOf` f) xs+  where only :: Maybe [FilePath]+        only = Nothing+ main :: IO () main = do (testEnv, testPercentage) <- getTestEnvironment @@ -42,7 +50,7 @@  where runDocTest onWindows onRemote tp = do srcFiles <- glob "Data/SBV/**/*.hs"                                              docFiles <- glob "Documentation/SBV/**/*.hs" -                                             let allFiles  = srcFiles ++ docFiles+                                             let allFiles  = [f | f <- srcFiles ++ docFiles, testOnly f]                                                  testFiles = filter (\nm -> not (skipWindows nm || skipRemote nm || skipLocal nm)) allFiles                                                   packages = [ "async"
SBVTestSuite/SBVTest.hs view
@@ -57,6 +57,7 @@ import qualified TestSuite.BitPrecise.Legato import qualified TestSuite.BitPrecise.MergeSort import qualified TestSuite.BitPrecise.PrefixSum+import qualified TestSuite.Char.Char import qualified TestSuite.CodeGeneration.AddSub import qualified TestSuite.CodeGeneration.CgTests import qualified TestSuite.CodeGeneration.CRC_USB5@@ -209,6 +210,7 @@                , TestSuite.BitPrecise.Legato.tests                , TestSuite.BitPrecise.MergeSort.tests                , TestSuite.BitPrecise.PrefixSum.tests+               , TestSuite.Char.Char.tests                , TestSuite.CodeGeneration.AddSub.tests                , TestSuite.CodeGeneration.CgTests.tests                , TestSuite.CodeGeneration.CRC_USB5.tests
SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs view
@@ -457,31 +457,31 @@                      ]  genChars :: [TestTree]-genChars = map mkTest $  [("ord",           show c, check SC.ord           cord            c) | c <- cs]-                      ++ [("toLower",       show c, check SC.toLower       C.toLower       c) | c <- cs]-                      ++ [("toUpper",       show c, check SC.toUpper       C.toUpper       c) | c <- cs, toUpperExceptions c]-                      ++ [("digitToInt",    show c, check SC.digitToInt    dig2Int         c) | c <- cs, digitToIntRange c]-                      ++ [("intToDigit",    show c, check SC.intToDigit    int2Dig         c) | c <- [0 .. 15]]-                      ++ [("isControl",     show c, check SC.isControl     C.isControl     c) | c <- cs]-                      ++ [("isSpace",       show c, check SC.isSpace       C.isSpace       c) | c <- cs]-                      ++ [("isLower",       show c, check SC.isLower       C.isLower       c) | c <- cs]-                      ++ [("isUpper",       show c, check SC.isUpper       C.isUpper       c) | c <- cs]-                      ++ [("isAlpha",       show c, check SC.isAlpha       C.isAlpha       c) | c <- cs]-                      ++ [("isAlphaNum",    show c, check SC.isAlphaNum    C.isAlphaNum    c) | c <- cs]-                      ++ [("isPrint",       show c, check SC.isPrint       C.isPrint       c) | c <- cs]-                      ++ [("isDigit",       show c, check SC.isDigit       C.isDigit       c) | c <- cs]-                      ++ [("isOctDigit",    show c, check SC.isOctDigit    C.isOctDigit    c) | c <- cs]-                      ++ [("isHexDigit",    show c, check SC.isHexDigit    C.isHexDigit    c) | c <- cs]-                      ++ [("isLetter",      show c, check SC.isLetter      C.isLetter      c) | c <- cs]-                      ++ [("isMark",        show c, check SC.isMark        C.isMark        c) | c <- cs]-                      ++ [("isNumber",      show c, check SC.isNumber      C.isNumber      c) | c <- cs]-                      ++ [("isPunctuation", show c, check SC.isPunctuation C.isPunctuation c) | c <- cs]-                      ++ [("isSymbol",      show c, check SC.isSymbol      C.isSymbol      c) | c <- cs]-                      ++ [("isSeparator",   show c, check SC.isSeparator   C.isSeparator   c) | c <- cs]-                      ++ [("isAscii",       show c, check SC.isAscii       C.isAscii       c) | c <- cs]-                      ++ [("isLatin1",      show c, check SC.isLatin1      C.isLatin1      c) | c <- cs]-                      ++ [("isAsciiUpper",  show c, check SC.isAsciiUpper  C.isAsciiUpper  c) | c <- cs]-                      ++ [("isAsciiLower",  show c, check SC.isAsciiLower  C.isAsciiLower  c) | c <- cs]+genChars = map mkTest $  [("ord",           show c, check SC.ord             cord            c) | c <- cs]+                      ++ [("toLower",       show c, check SC.toLowerL1       C.toLower       c) | c <- cs]+                      ++ [("toUpper",       show c, check SC.toUpperL1       C.toUpper       c) | c <- cs, toUpperExceptions c]+                      ++ [("digitToInt",    show c, check SC.digitToInt      dig2Int         c) | c <- cs, digitToIntRange c]+                      ++ [("intToDigit",    show c, check SC.intToDigit      int2Dig         c) | c <- [0 .. 15]]+                      ++ [("isControl",     show c, check SC.isControlL1     C.isControl     c) | c <- cs]+                      ++ [("isSpace",       show c, check SC.isSpaceL1       C.isSpace       c) | c <- cs]+                      ++ [("isLower",       show c, check SC.isLowerL1       C.isLower       c) | c <- cs]+                      ++ [("isUpper",       show c, check SC.isUpperL1       C.isUpper       c) | c <- cs]+                      ++ [("isAlpha",       show c, check SC.isAlphaL1       C.isAlpha       c) | c <- cs]+                      ++ [("isAlphaNum",    show c, check SC.isAlphaNumL1    C.isAlphaNum    c) | c <- cs]+                      ++ [("isPrint",       show c, check SC.isPrintL1       C.isPrint       c) | c <- cs]+                      ++ [("isDigit",       show c, check SC.isDigit         C.isDigit       c) | c <- cs]+                      ++ [("isOctDigit",    show c, check SC.isOctDigit      C.isOctDigit    c) | c <- cs]+                      ++ [("isHexDigit",    show c, check SC.isHexDigit      C.isHexDigit    c) | c <- cs]+                      ++ [("isLetter",      show c, check SC.isLetterL1      C.isLetter      c) | c <- cs]+                      ++ [("isMark",        show c, check SC.isMarkL1        C.isMark        c) | c <- cs]+                      ++ [("isNumber",      show c, check SC.isNumberL1      C.isNumber      c) | c <- cs]+                      ++ [("isPunctuation", show c, check SC.isPunctuationL1 C.isPunctuation c) | c <- cs]+                      ++ [("isSymbol",      show c, check SC.isSymbolL1      C.isSymbol      c) | c <- cs]+                      ++ [("isSeparator",   show c, check SC.isSeparatorL1   C.isSeparator   c) | c <- cs]+                      ++ [("isAscii",       show c, check SC.isAscii         C.isAscii       c) | c <- cs]+                      ++ [("isLatin1",      show c, check SC.isLatin1        C.isLatin1      c) | c <- cs]+                      ++ [("isAsciiUpper",  show c, check SC.isAsciiUpper    C.isAsciiUpper  c) | c <- cs]+                      ++ [("isAsciiLower",  show c, check SC.isAsciiLower    C.isAsciiLower  c) | c <- cs]   where toUpperExceptions = (`notElem` "\181\255")         digitToIntRange   = (`elem` "0123456789abcdefABCDEF")         cord :: Char -> Integer@@ -736,7 +736,7 @@ sds :: [SDouble] sds = map literal ds --- Currently we test over all latin-1 characters. But when Unicode comes along, we'll have to be more selective.+-- Currently we test over all latin-1 characters. Maybe we should add some unicode here. Oh well. cs :: String cs = map C.chr [0..255]
SBVTestSuite/TestSuite/Basics/ArithSolver.hs view
@@ -346,12 +346,8 @@                ++ [("fpIsEqualObject", show x, show y, mkThm2P fpIsEqualObject  x y (fpIsEqualObjectH x y)) | x <- vs, y <- vs]                ++ [("fpRem",           show x, show y, mkThm2  fpRem            x y (fpRemH           x y)) | x <- vsFPRem, y <- vsFPRem] -        -- Turning off fpRem tests for the time being. See: https://github.com/LeventErkok/sbv/issues/482-        issue482 = True-         -- TODO: For doubles fpRem takes too long, so we only do a subset         vsFPRem-          | issue482               = []           | origin == "genDoubles" = [nan, infinity, 0, 0.5, -infinity, -0, -0.5]           | True                   = vs @@ -546,31 +542,31 @@         noOverflow x y = not (x == minBound && y == -1)  genChars :: [TestTree]-genChars = map mkTest $  [("ord",           show c, mkThm SC.ord           cord            c) | c <- cs]-                      ++ [("toLower",       show c, mkThm SC.toLower       C.toLower       c) | c <- cs]-                      ++ [("toUpper",       show c, mkThm SC.toUpper       C.toUpper       c) | c <- cs, toUpperExceptions c]-                      ++ [("digitToInt",    show c, mkThm SC.digitToInt    dig2Int         c) | c <- cs, digitToIntRange c]-                      ++ [("intToDigit",    show c, mkThm SC.intToDigit    int2Dig         c) | c <- [0 .. 15]]-                      ++ [("isControl",     show c, mkThm SC.isControl     C.isControl     c) | c <- cs]-                      ++ [("isSpace",       show c, mkThm SC.isSpace       C.isSpace       c) | c <- cs]-                      ++ [("isLower",       show c, mkThm SC.isLower       C.isLower       c) | c <- cs]-                      ++ [("isUpper",       show c, mkThm SC.isUpper       C.isUpper       c) | c <- cs]-                      ++ [("isAlpha",       show c, mkThm SC.isAlpha       C.isAlpha       c) | c <- cs]-                      ++ [("isAlphaNum",    show c, mkThm SC.isAlphaNum    C.isAlphaNum    c) | c <- cs]-                      ++ [("isPrint",       show c, mkThm SC.isPrint       C.isPrint       c) | c <- cs]-                      ++ [("isDigit",       show c, mkThm SC.isDigit       C.isDigit       c) | c <- cs]-                      ++ [("isOctDigit",    show c, mkThm SC.isOctDigit    C.isOctDigit    c) | c <- cs]-                      ++ [("isHexDigit",    show c, mkThm SC.isHexDigit    C.isHexDigit    c) | c <- cs]-                      ++ [("isLetter",      show c, mkThm SC.isLetter      C.isLetter      c) | c <- cs]-                      ++ [("isMark",        show c, mkThm SC.isMark        C.isMark        c) | c <- cs]-                      ++ [("isNumber",      show c, mkThm SC.isNumber      C.isNumber      c) | c <- cs]-                      ++ [("isPunctuation", show c, mkThm SC.isPunctuation C.isPunctuation c) | c <- cs]-                      ++ [("isSymbol",      show c, mkThm SC.isSymbol      C.isSymbol      c) | c <- cs]-                      ++ [("isSeparator",   show c, mkThm SC.isSeparator   C.isSeparator   c) | c <- cs]-                      ++ [("isAscii",       show c, mkThm SC.isAscii       C.isAscii       c) | c <- cs]-                      ++ [("isLatin1",      show c, mkThm SC.isLatin1      C.isLatin1      c) | c <- cs]-                      ++ [("isAsciiUpper",  show c, mkThm SC.isAsciiUpper  C.isAsciiUpper  c) | c <- cs]-                      ++ [("isAsciiLower",  show c, mkThm SC.isAsciiLower  C.isAsciiLower  c) | c <- cs]+genChars = map mkTest $  [("ord",           show c, mkThm SC.ord             cord            c) | c <- cs]+                      ++ [("toLower",       show c, mkThm SC.toLowerL1       C.toLower       c) | c <- cs]+                      ++ [("toUpper",       show c, mkThm SC.toUpperL1       C.toUpper       c) | c <- cs, toUpperExceptions c]+                      ++ [("digitToInt",    show c, mkThm SC.digitToInt      dig2Int         c) | c <- cs, digitToIntRange c]+                      ++ [("intToDigit",    show c, mkThm SC.intToDigit      int2Dig         c) | c <- [0 .. 15]]+                      ++ [("isControl",     show c, mkThm SC.isControlL1     C.isControl     c) | c <- cs]+                      ++ [("isSpace",       show c, mkThm SC.isSpaceL1       C.isSpace       c) | c <- cs]+                      ++ [("isLower",       show c, mkThm SC.isLowerL1       C.isLower       c) | c <- cs]+                      ++ [("isUpper",       show c, mkThm SC.isUpperL1       C.isUpper       c) | c <- cs]+                      ++ [("isAlpha",       show c, mkThm SC.isAlphaL1       C.isAlpha       c) | c <- cs]+                      ++ [("isAlphaNum",    show c, mkThm SC.isAlphaNumL1    C.isAlphaNum    c) | c <- cs]+                      ++ [("isPrint",       show c, mkThm SC.isPrintL1       C.isPrint       c) | c <- cs]+                      ++ [("isDigit",       show c, mkThm SC.isDigit         C.isDigit       c) | c <- cs]+                      ++ [("isOctDigit",    show c, mkThm SC.isOctDigit      C.isOctDigit    c) | c <- cs]+                      ++ [("isHexDigit",    show c, mkThm SC.isHexDigit      C.isHexDigit    c) | c <- cs]+                      ++ [("isLetter",      show c, mkThm SC.isLetterL1      C.isLetter      c) | c <- cs]+                      ++ [("isMark",        show c, mkThm SC.isMarkL1        C.isMark        c) | c <- cs]+                      ++ [("isNumber",      show c, mkThm SC.isNumberL1      C.isNumber      c) | c <- cs]+                      ++ [("isPunctuation", show c, mkThm SC.isPunctuationL1 C.isPunctuation c) | c <- cs]+                      ++ [("isSymbol",      show c, mkThm SC.isSymbolL1      C.isSymbol      c) | c <- cs]+                      ++ [("isSeparator",   show c, mkThm SC.isSeparatorL1   C.isSeparator   c) | c <- cs]+                      ++ [("isAscii",       show c, mkThm SC.isAscii         C.isAscii       c) | c <- cs]+                      ++ [("isLatin1",      show c, mkThm SC.isLatin1        C.isLatin1      c) | c <- cs]+                      ++ [("isAsciiUpper",  show c, mkThm SC.isAsciiUpper    C.isAsciiUpper  c) | c <- cs]+                      ++ [("isAsciiLower",  show c, mkThm SC.isAsciiLower    C.isAsciiLower  c) | c <- cs]   where toUpperExceptions = (`notElem` "\181\255")         digitToIntRange   = (`elem` "0123456789abcdefABCDEF")         cord :: Char -> Integer@@ -804,8 +800,8 @@ ds = xs ++ map (* (-1)) (filter (not . isNaN) xs) -- -nan is the same as nan   where xs = [nan, infinity, 0, 0.5, 2.516632060108026e-2, 0.8601891300751106, 5.0e-324] --- Currently we test over all latin-1 characters. But when Unicode comes along, we'll have to be more selective.--- TODO: Unicode update here.+-- Currently we test over all latin-1 characters. Maybe we should add some unicode when the+-- underlying operation is supported. Oh well. cs :: String cs = map C.chr [0..255]
SBVTestSuite/TestSuite/Basics/String.hs view
@@ -21,6 +21,7 @@  import Data.SBV.String ((.!!), (.++)) import qualified Data.SBV.String as S+import qualified Data.SBV.Char   as SC import qualified Data.SBV.RegExp as R  import Control.Monad (unless)@@ -176,9 +177,12 @@    constrain $ s .== "13"    constrain $ sNot $ S.strToNat s .== 13 --- Generate all length one strings, to enumerate all and making sure we can parse correctly+-- Generate all length one strings consisting of letters A-Z, to enumerate all and making sure we can parse correctly strExamples14 :: IO Bool strExamples14 = do m <- allSat $ do s <- sString "s"+                                    let c = SC.ord (S.head s)+                                    constrain $ c .>= SC.ord (literal 'A')+                                    constrain $ c .<= SC.ord (literal 'Z')                                     return $ S.length s .== 1                    let dicts = getModelDictionaries m @@ -186,5 +190,5 @@                        vals = map C.ord $ concat $ sort $ map (fromCV . snd) (concatMap M.assocs dicts)                     case length dicts of-                     256 -> return $ vals == [0 .. 255]+                     26 -> return $ vals == map C.ord ['A' .. 'Z']                      _   -> return False
SBVTestSuite/TestSuite/Basics/UISat.hs view
@@ -8,6 +8,7 @@ -- -- Testing UI function sat examples -----------------------------------------------------------------------------+{-# LANGUAGE OverloadedStrings #-}  {-# OPTIONS_GHC -Wall -Werror #-}
+ SBVTestSuite/TestSuite/Char/Char.hs view
@@ -0,0 +1,111 @@+-----------------------------------------------------------------------------+-- |+-- Module    : TestSuite.Char.Char+-- Copyright : (c) Levent Erkok+-- License   : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Testing SChar constraints (as modeled thru strings in SMTLib)+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module TestSuite.Char.Char(tests) where++import Utils.SBVTestFramework+import Data.SBV.Control++import qualified Data.SBV.List   as L+import qualified Data.SBV.Set    as S+import qualified Data.SBV.Maybe  as M+import qualified Data.SBV.Either as E+import Data.SBV.Tuple++tests :: TestTree+tests =+  testGroup "Char" [+      goldenCapturedIO "charConstr00" $ \rf -> checkWith rf t00+    , goldenCapturedIO "charConstr01" $ \rf -> checkWith rf t01+    , goldenCapturedIO "charConstr02" $ \rf -> checkWith rf t02+    , goldenCapturedIO "charConstr03" $ \rf -> checkWith rf t03+    , goldenCapturedIO "charConstr04" $ \rf -> checkWith rf t04+    , goldenCapturedIO "charConstr05" $ \rf -> checkWith rf t05+    , goldenCapturedIO "charConstr06" $ \rf -> checkWith rf t06+    , goldenCapturedIO "charConstr07" $ \rf -> checkWith rf t07+    , goldenCapturedIO "charConstr08" $ \rf -> checkWith rf t08+    , goldenCapturedIO "charConstr09" $ \rf -> checkWith rf t09+    , goldenCapturedIO "charConstr10" $ \rf -> checkWith rf t10+    , goldenCapturedIO "charConstr11" $ \rf -> checkWith rf t11+    ]++checkWith :: FilePath -> Symbolic () -> IO ()+checkWith rf props = runSMTWith z3{verbose=True, redirectVerbose = Just rf} $ do+        _ <- props+        query $ do cs <- checkSat+                   case cs of+                     Unsat  -> io $ appendFile rf "\nUNSAT"+                     DSat{} -> io $ appendFile rf "\nDSAT"+                     Sat{}  -> getModel         >>= \m -> io $ appendFile rf $ "\nMODEL: "   ++ show m ++ "\nDONE."+                     Unk    -> getUnknownReason >>= \r -> io $ appendFile rf $ "\nUNKNOWN: " ++ show r ++ "\nDONE."++cf :: SInteger -> SChar+cf  = uninterpret "cf"++cf3 :: SInteger -> STuple3 Char Char Char+cf3 = uninterpret "cf3"++t00 :: Symbolic ()+t00 = do x <- sChar "x"+         constrain $ x ./= literal 'A'++t01 :: Symbolic ()+t01 = constrain $ cf 4 ./= literal 'A'++t02 :: Symbolic ()+t02 = constrain $ cf3 4 ./= literal ('A', 'B', 'C')++t03 :: Symbolic ()+t03 = do x::SEither Char Char <- free "x"+         constrain $ x ./= E.sLeft (literal 'A')++t04 :: Symbolic ()+t04 = do x::SEither Integer Char <- free "x"+         constrain $ x ./= E.sRight (literal 'A')++t05 :: Symbolic ()+t05 = do x::SEither Char Integer <- free "x"+         constrain $ x ./= E.sLeft (literal 'A')++t06 :: Symbolic ()+t06 = do x::SEither Char (Either Char Integer) <- free "x"+         constrain $ x ./= E.sLeft (literal 'A')++t07 :: Symbolic ()+t07 = do x::SMaybe Char <- free "x"+         constrain $ M.isJust x .&& x ./= M.sJust (literal 'A')++t08 :: Symbolic ()+t08 = do x :: SSet Char <- free "x"+         constrain $ S.member (literal 'A') x .&& sNot (S.member (literal 'B') x)++t09 :: Symbolic ()+t09 = do x :: SList ((Char, Char), [Integer]) <- free "x"+         constrain $ L.length x .== 1++t10 :: Symbolic ()+t10 = do x :: SList ((Char, Char), [Integer]) <- free "x"+         constrain $ L.length x .== 1+         constrain $ (x L..!! 0)^._1^._1 .== literal 'B'++cf4 :: SInteger -> SChar -> SList ((Char, Char), [Integer])+cf4 = uninterpret "cf4"++t11 :: Symbolic ()+t11 = do x <- sInteger "x"+         c <- sChar "c"+         constrain $ L.length (cf4 x c) .== 1++{-# ANN module ("HLint: ignore Redundant ^." :: String) #-}
SBVTestSuite/TestSuite/Queries/UISat.hs view
@@ -8,6 +8,7 @@ -- -- Testing UI function sat examples via queries -----------------------------------------------------------------------------+{-# LANGUAGE OverloadedStrings #-}  {-# OPTIONS_GHC -Wall -Werror #-}
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2  Name        : sbv-Version     : 8.9+Version     : 8.10 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@@ -9,7 +9,7 @@                .                For details, please see: <http://leventerkok.github.com/sbv/> -Copyright          : Levent Erkok, 2010-2020+Copyright          : Levent Erkok, 2010-2021 License            : BSD-3-Clause License-file       : LICENSE Stability          : Experimental@@ -83,7 +83,7 @@   build-depends   : crackNum                   , QuickCheck, template-haskell                   , array, async, containers, deepseq, directory, filepath, time-                  , pretty, process, mtl, random, syb, transformers, uniplate+                  , pretty, process, mtl, random, syb, text, transformers, uniplate   Exposed-modules : Data.SBV                   , Data.SBV.Control                   , Data.SBV.Dynamic@@ -133,6 +133,7 @@                   , Documentation.SBV.Examples.Misc.Enumerate                   , Documentation.SBV.Examples.Misc.Floating                   , Documentation.SBV.Examples.Misc.ModelExtract+                  , Documentation.SBV.Examples.Misc.NestedArray                   , Documentation.SBV.Examples.Misc.Auxiliary                   , Documentation.SBV.Examples.Misc.NoDiv0                   , Documentation.SBV.Examples.Misc.Newtypes@@ -167,6 +168,7 @@                   , Documentation.SBV.Examples.Puzzles.HexPuzzle                   , Documentation.SBV.Examples.Puzzles.LadyAndTigers                   , Documentation.SBV.Examples.Puzzles.MagicSquare+                  , Documentation.SBV.Examples.Puzzles.Murder                   , Documentation.SBV.Examples.Puzzles.NQueens                   , Documentation.SBV.Examples.Puzzles.SendMoreMoney                   , Documentation.SBV.Examples.Puzzles.Sudoku@@ -212,13 +214,13 @@                   , Data.SBV.SMT.SMTLibNames                   , Data.SBV.SMT.Utils                   , Data.SBV.Provers.Prover+                  , Data.SBV.Provers.ABC                   , Data.SBV.Provers.Boolector                   , Data.SBV.Provers.CVC4-                  , Data.SBV.Provers.Yices                   , Data.SBV.Provers.DReal-                  , Data.SBV.Provers.Z3                   , Data.SBV.Provers.MathSAT-                  , Data.SBV.Provers.ABC+                  , Data.SBV.Provers.Yices+                  , Data.SBV.Provers.Z3                   , Data.SBV.Utils.ExtractIO                   , Data.SBV.Utils.Numeric                   , Data.SBV.Utils.TDiff@@ -282,6 +284,7 @@                   , TestSuite.Basics.TOut                   , TestSuite.Basics.Tuple                   , TestSuite.Basics.UISat+                  , TestSuite.Char.Char                   , TestSuite.BitPrecise.BitTricks                   , TestSuite.BitPrecise.Legato                   , TestSuite.BitPrecise.MergeSort@@ -429,7 +432,7 @@                     TemplateHaskell                     TupleSections                     TypeApplications-  build-depends   : filepath, syb, crackNum+  build-depends   : filepath, syb, crackNum, text                   , sbv, directory, random, mtl, containers, time                   , gauge, process, deepseq, bench-show, silently   hs-source-dirs  : SBVBenchSuite