diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,28 @@ * Hackage: * GitHub: -* 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 diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -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 diff --git a/Data/SBV/Char.hs b/Data/SBV/Char.hs --- a/Data/SBV/Char.hs +++ b/Data/SBV/Char.hs @@ -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 diff --git a/Data/SBV/Client.hs b/Data/SBV/Client.hs --- a/Data/SBV/Client.hs +++ b/Data/SBV/Client.hs @@ -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] diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -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 diff --git a/Data/SBV/Control/BaseIO.hs b/Data/SBV/Control/BaseIO.hs --- a/Data/SBV/Control/BaseIO.hs +++ b/Data/SBV/Control/BaseIO.hs @@ -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. diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs --- a/Data/SBV/Control/Query.hs +++ b/Data/SBV/Control/Query.hs @@ -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 [ "" diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -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: - 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" diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs --- a/Data/SBV/Core/Data.hs +++ b/Data/SBV/Core/Data.hs @@ -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: . 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: +-- | A symbolic character. Note that this is the full unicode character set. +-- see: +-- for details. type SChar = SBV Char -- | A symbolic string. Note that a symbolic string is /not/ a list of symbolic characters, diff --git a/Data/SBV/Core/Kind.hs b/Data/SBV/Core/Kind.hs --- a/Data/SBV/Core/Kind.hs +++ b/Data/SBV/Core/Kind.hs @@ -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 diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -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 diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -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: 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 -- 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 diff --git a/Data/SBV/Either.hs b/Data/SBV/Either.hs --- a/Data/SBV/Either.hs +++ b/Data/SBV/Either.hs @@ -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 diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -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 diff --git a/Data/SBV/Maybe.hs b/Data/SBV/Maybe.hs --- a/Data/SBV/Maybe.hs +++ b/Data/SBV/Maybe.hs @@ -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 diff --git a/Data/SBV/Provers/Boolector.hs b/Data/SBV/Provers/Boolector.hs --- a/Data/SBV/Provers/Boolector.hs +++ b/Data/SBV/Provers/Boolector.hs @@ -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 diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs --- a/Data/SBV/Provers/CVC4.hs +++ b/Data/SBV/Provers/CVC4.hs @@ -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 diff --git a/Data/SBV/Provers/MathSAT.hs b/Data/SBV/Provers/MathSAT.hs --- a/Data/SBV/Provers/MathSAT.hs +++ b/Data/SBV/Provers/MathSAT.hs @@ -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 diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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, "") diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -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 diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -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 diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -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 diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -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." , ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;" diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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: ) diff --git a/Data/SBV/SMT/Utils.hs b/Data/SBV/SMT/Utils.hs --- a/Data/SBV/SMT/Utils.hs +++ b/Data/SBV/SMT/Utils.hs @@ -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 diff --git a/Data/SBV/Set.hs b/Data/SBV/Set.hs --- a/Data/SBV/Set.hs +++ b/Data/SBV/Set.hs @@ -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} diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs --- a/Data/SBV/String.hs +++ b/Data/SBV/String.hs @@ -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 diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs --- a/Data/SBV/Tools/GenTest.hs +++ b/Data/SBV/Tools/GenTest.hs @@ -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 diff --git a/Data/SBV/Utils/Lib.hs b/Data/SBV/Utils/Lib.hs --- a/Data/SBV/Utils/Lib.hs +++ b/Data/SBV/Utils/Lib.hs @@ -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 diff --git a/Data/SBV/Utils/PrettyNum.hs b/Data/SBV/Utils/PrettyNum.hs --- a/Data/SBV/Utils/PrettyNum.hs +++ b/Data/SBV/Utils/PrettyNum.hs @@ -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 diff --git a/Documentation/SBV/Examples/Existentials/Diophantine.hs b/Documentation/SBV/Examples/Existentials/Diophantine.hs --- a/Documentation/SBV/Examples/Existentials/Diophantine.hs +++ b/Documentation/SBV/Examples/Existentials/Diophantine.hs @@ -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, diff --git a/Documentation/SBV/Examples/Misc/Auxiliary.hs b/Documentation/SBV/Examples/Misc/Auxiliary.hs --- a/Documentation/SBV/Examples/Misc/Auxiliary.hs +++ b/Documentation/SBV/Examples/Misc/Auxiliary.hs @@ -15,6 +15,8 @@ -- considering them explicitly in model construction. ----------------------------------------------------------------------------- +{-# LANGUAGE OverloadedStrings #-} + {-# OPTIONS_GHC -Wall -Werror #-} module Documentation.SBV.Examples.Misc.Auxiliary where diff --git a/Documentation/SBV/Examples/Misc/NestedArray.hs b/Documentation/SBV/Examples/Misc/NestedArray.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/Misc/NestedArray.hs @@ -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 diff --git a/Documentation/SBV/Examples/Misc/SetAlgebra.hs b/Documentation/SBV/Examples/Misc/SetAlgebra.hs --- a/Documentation/SBV/Examples/Misc/SetAlgebra.hs +++ b/Documentation/SBV/Examples/Misc/SetAlgebra.hs @@ -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} -} diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs --- a/Documentation/SBV/Examples/ProofTools/BMC.hs +++ b/Documentation/SBV/Examples/ProofTools/BMC.hs @@ -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 diff --git a/Documentation/SBV/Examples/Puzzles/Garden.hs b/Documentation/SBV/Examples/Puzzles/Garden.hs --- a/Documentation/SBV/Examples/Puzzles/Garden.hs +++ b/Documentation/SBV/Examples/Puzzles/Garden.hs @@ -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 diff --git a/Documentation/SBV/Examples/Puzzles/Murder.hs b/Documentation/SBV/Examples/Puzzles/Murder.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/Puzzles/Murder.hs @@ -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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/SBVBenchSuite/BenchSuite/Puzzles/Garden.hs b/SBVBenchSuite/BenchSuite/Puzzles/Garden.hs --- a/SBVBenchSuite/BenchSuite/Puzzles/Garden.hs +++ b/SBVBenchSuite/BenchSuite/Puzzles/Garden.hs @@ -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 diff --git a/SBVBenchSuite/SBVBenchmark.hs b/SBVBenchSuite/SBVBenchmark.hs --- a/SBVBenchSuite/SBVBenchmark.hs +++ b/SBVBenchSuite/SBVBenchmark.hs @@ -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 diff --git a/SBVBenchSuite/Utils/SBVBenchFramework.hs b/SBVBenchSuite/Utils/SBVBenchFramework.hs --- a/SBVBenchSuite/Utils/SBVBenchFramework.hs +++ b/SBVBenchSuite/Utils/SBVBenchFramework.hs @@ -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 diff --git a/SBVTestSuite/GoldFiles/charConstr00.gold b/SBVTestSuite/GoldFiles/charConstr00.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr00.gold @@ -0,0 +1,32 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-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 diff --git a/SBVTestSuite/GoldFiles/charConstr01.gold b/SBVTestSuite/GoldFiles/charConstr01.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr01.gold @@ -0,0 +1,40 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-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 diff --git a/SBVTestSuite/GoldFiles/charConstr02.gold b/SBVTestSuite/GoldFiles/charConstr02.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr02.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/charConstr03.gold b/SBVTestSuite/GoldFiles/charConstr03.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr03.gold @@ -0,0 +1,40 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-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 diff --git a/SBVTestSuite/GoldFiles/charConstr04.gold b/SBVTestSuite/GoldFiles/charConstr04.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr04.gold @@ -0,0 +1,38 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-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 diff --git a/SBVTestSuite/GoldFiles/charConstr05.gold b/SBVTestSuite/GoldFiles/charConstr05.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr05.gold @@ -0,0 +1,38 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-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 diff --git a/SBVTestSuite/GoldFiles/charConstr06.gold b/SBVTestSuite/GoldFiles/charConstr06.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr06.gold @@ -0,0 +1,40 @@ +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-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 diff --git a/SBVTestSuite/GoldFiles/charConstr07.gold b/SBVTestSuite/GoldFiles/charConstr07.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr07.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/charConstr08.gold b/SBVTestSuite/GoldFiles/charConstr08.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr08.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/charConstr09.gold b/SBVTestSuite/GoldFiles/charConstr09.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr09.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/charConstr10.gold b/SBVTestSuite/GoldFiles/charConstr10.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr10.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/charConstr11.gold b/SBVTestSuite/GoldFiles/charConstr11.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/charConstr11.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/exceptionLocal1.gold b/SBVTestSuite/GoldFiles/exceptionLocal1.gold --- a/SBVTestSuite/GoldFiles/exceptionLocal1.gold +++ b/SBVTestSuite/GoldFiles/exceptionLocal1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/freshVars.gold b/SBVTestSuite/GoldFiles/freshVars.gold --- a/SBVTestSuite/GoldFiles/freshVars.gold +++ b/SBVTestSuite/GoldFiles/freshVars.gold @@ -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)))) diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -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) diff --git a/SBVTestSuite/GoldFiles/query_Chars1.gold b/SBVTestSuite/GoldFiles/query_Chars1.gold --- a/SBVTestSuite/GoldFiles/query_Chars1.gold +++ b/SBVTestSuite/GoldFiles/query_Chars1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/query_ListOfMaybe.gold b/SBVTestSuite/GoldFiles/query_ListOfMaybe.gold --- a/SBVTestSuite/GoldFiles/query_ListOfMaybe.gold +++ b/SBVTestSuite/GoldFiles/query_ListOfMaybe.gold @@ -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] diff --git a/SBVTestSuite/GoldFiles/query_ListOfSum.gold b/SBVTestSuite/GoldFiles/query_ListOfSum.gold --- a/SBVTestSuite/GoldFiles/query_ListOfSum.gold +++ b/SBVTestSuite/GoldFiles/query_ListOfSum.gold @@ -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'] diff --git a/SBVTestSuite/GoldFiles/query_SumMaybeBoth.gold b/SBVTestSuite/GoldFiles/query_SumMaybeBoth.gold --- a/SBVTestSuite/GoldFiles/query_SumMaybeBoth.gold +++ b/SBVTestSuite/GoldFiles/query_SumMaybeBoth.gold @@ -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) diff --git a/SBVTestSuite/GoldFiles/query_Sums.gold b/SBVTestSuite/GoldFiles/query_Sums.gold --- a/SBVTestSuite/GoldFiles/query_Sums.gold +++ b/SBVTestSuite/GoldFiles/query_Sums.gold @@ -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) diff --git a/SBVTestSuite/GoldFiles/query_Tuples1.gold b/SBVTestSuite/GoldFiles/query_Tuples1.gold --- a/SBVTestSuite/GoldFiles/query_Tuples1.gold +++ b/SBVTestSuite/GoldFiles/query_Tuples1.gold @@ -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') diff --git a/SBVTestSuite/GoldFiles/query_Tuples2.gold b/SBVTestSuite/GoldFiles/query_Tuples2.gold --- a/SBVTestSuite/GoldFiles/query_Tuples2.gold +++ b/SBVTestSuite/GoldFiles/query_Tuples2.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/query_badOption.gold b/SBVTestSuite/GoldFiles/query_badOption.gold --- a/SBVTestSuite/GoldFiles/query_badOption.gold +++ b/SBVTestSuite/GoldFiles/query_badOption.gold @@ -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) diff --git a/SBVTestSuite/GoldFiles/query_boolector.gold b/SBVTestSuite/GoldFiles/query_boolector.gold --- a/SBVTestSuite/GoldFiles/query_boolector.gold +++ b/SBVTestSuite/GoldFiles/query_boolector.gold @@ -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 --- diff --git a/SBVTestSuite/GoldFiles/query_sumMergeEither1.gold b/SBVTestSuite/GoldFiles/query_sumMergeEither1.gold --- a/SBVTestSuite/GoldFiles/query_sumMergeEither1.gold +++ b/SBVTestSuite/GoldFiles/query_sumMergeEither1.gold @@ -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) diff --git a/SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold b/SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold --- a/SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold +++ b/SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold @@ -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) diff --git a/SBVTestSuite/GoldFiles/query_uisatex1.gold b/SBVTestSuite/GoldFiles/query_uisatex1.gold --- a/SBVTestSuite/GoldFiles/query_uisatex1.gold +++ b/SBVTestSuite/GoldFiles/query_uisatex1.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/query_uisatex2.gold b/SBVTestSuite/GoldFiles/query_uisatex2.gold --- a/SBVTestSuite/GoldFiles/query_uisatex2.gold +++ b/SBVTestSuite/GoldFiles/query_uisatex2.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/query_yices.gold b/SBVTestSuite/GoldFiles/query_yices.gold --- a/SBVTestSuite/GoldFiles/query_yices.gold +++ b/SBVTestSuite/GoldFiles/query_yices.gold @@ -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 --- diff --git a/SBVTestSuite/GoldFiles/set_compl1.gold b/SBVTestSuite/GoldFiles/set_compl1.gold --- a/SBVTestSuite/GoldFiles/set_compl1.gold +++ b/SBVTestSuite/GoldFiles/set_compl1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/set_delete1.gold b/SBVTestSuite/GoldFiles/set_delete1.gold --- a/SBVTestSuite/GoldFiles/set_delete1.gold +++ b/SBVTestSuite/GoldFiles/set_delete1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/set_diff1.gold b/SBVTestSuite/GoldFiles/set_diff1.gold --- a/SBVTestSuite/GoldFiles/set_diff1.gold +++ b/SBVTestSuite/GoldFiles/set_diff1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/set_disj1.gold b/SBVTestSuite/GoldFiles/set_disj1.gold --- a/SBVTestSuite/GoldFiles/set_disj1.gold +++ b/SBVTestSuite/GoldFiles/set_disj1.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/set_empty1.gold b/SBVTestSuite/GoldFiles/set_empty1.gold --- a/SBVTestSuite/GoldFiles/set_empty1.gold +++ b/SBVTestSuite/GoldFiles/set_empty1.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/set_full1.gold b/SBVTestSuite/GoldFiles/set_full1.gold --- a/SBVTestSuite/GoldFiles/set_full1.gold +++ b/SBVTestSuite/GoldFiles/set_full1.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/set_insert1.gold b/SBVTestSuite/GoldFiles/set_insert1.gold --- a/SBVTestSuite/GoldFiles/set_insert1.gold +++ b/SBVTestSuite/GoldFiles/set_insert1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/set_intersect1.gold b/SBVTestSuite/GoldFiles/set_intersect1.gold --- a/SBVTestSuite/GoldFiles/set_intersect1.gold +++ b/SBVTestSuite/GoldFiles/set_intersect1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/set_member1.gold b/SBVTestSuite/GoldFiles/set_member1.gold --- a/SBVTestSuite/GoldFiles/set_member1.gold +++ b/SBVTestSuite/GoldFiles/set_member1.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/set_notMember1.gold b/SBVTestSuite/GoldFiles/set_notMember1.gold --- a/SBVTestSuite/GoldFiles/set_notMember1.gold +++ b/SBVTestSuite/GoldFiles/set_notMember1.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/set_psubset1.gold b/SBVTestSuite/GoldFiles/set_psubset1.gold --- a/SBVTestSuite/GoldFiles/set_psubset1.gold +++ b/SBVTestSuite/GoldFiles/set_psubset1.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/set_subset1.gold b/SBVTestSuite/GoldFiles/set_subset1.gold --- a/SBVTestSuite/GoldFiles/set_subset1.gold +++ b/SBVTestSuite/GoldFiles/set_subset1.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/set_union1.gold b/SBVTestSuite/GoldFiles/set_union1.gold --- a/SBVTestSuite/GoldFiles/set_union1.gold +++ b/SBVTestSuite/GoldFiles/set_union1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/sumLiftEither.gold b/SBVTestSuite/GoldFiles/sumLiftEither.gold --- a/SBVTestSuite/GoldFiles/sumLiftEither.gold +++ b/SBVTestSuite/GoldFiles/sumLiftEither.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/sumMaybeBoth.gold b/SBVTestSuite/GoldFiles/sumMaybeBoth.gold --- a/SBVTestSuite/GoldFiles/sumMaybeBoth.gold +++ b/SBVTestSuite/GoldFiles/sumMaybeBoth.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/sumMergeEither1.gold b/SBVTestSuite/GoldFiles/sumMergeEither1.gold --- a/SBVTestSuite/GoldFiles/sumMergeEither1.gold +++ b/SBVTestSuite/GoldFiles/sumMergeEither1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/sumMergeMaybe2.gold b/SBVTestSuite/GoldFiles/sumMergeMaybe2.gold --- a/SBVTestSuite/GoldFiles/sumMergeMaybe2.gold +++ b/SBVTestSuite/GoldFiles/sumMergeMaybe2.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/tuple_enum.gold b/SBVTestSuite/GoldFiles/tuple_enum.gold --- a/SBVTestSuite/GoldFiles/tuple_enum.gold +++ b/SBVTestSuite/GoldFiles/tuple_enum.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/tuple_nested.gold b/SBVTestSuite/GoldFiles/tuple_nested.gold --- a/SBVTestSuite/GoldFiles/tuple_nested.gold +++ b/SBVTestSuite/GoldFiles/tuple_nested.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/tuple_twoTwo.gold b/SBVTestSuite/GoldFiles/tuple_twoTwo.gold --- a/SBVTestSuite/GoldFiles/tuple_twoTwo.gold +++ b/SBVTestSuite/GoldFiles/tuple_twoTwo.gold @@ -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 diff --git a/SBVTestSuite/SBVConnectionTest.hs b/SBVTestSuite/SBVConnectionTest.hs --- a/SBVTestSuite/SBVConnectionTest.hs +++ b/SBVTestSuite/SBVConnectionTest.hs @@ -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) diff --git a/SBVTestSuite/SBVDocTest.hs b/SBVTestSuite/SBVDocTest.hs --- a/SBVTestSuite/SBVDocTest.hs +++ b/SBVTestSuite/SBVDocTest.hs @@ -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" diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs @@ -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] diff --git a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs @@ -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] diff --git a/SBVTestSuite/TestSuite/Basics/String.hs b/SBVTestSuite/TestSuite/Basics/String.hs --- a/SBVTestSuite/TestSuite/Basics/String.hs +++ b/SBVTestSuite/TestSuite/Basics/String.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Basics/UISat.hs b/SBVTestSuite/TestSuite/Basics/UISat.hs --- a/SBVTestSuite/TestSuite/Basics/UISat.hs +++ b/SBVTestSuite/TestSuite/Basics/UISat.hs @@ -8,6 +8,7 @@ -- -- Testing UI function sat examples ----------------------------------------------------------------------------- +{-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wall -Werror #-} diff --git a/SBVTestSuite/TestSuite/Char/Char.hs b/SBVTestSuite/TestSuite/Char/Char.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Char/Char.hs @@ -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) #-} diff --git a/SBVTestSuite/TestSuite/Queries/UISat.hs b/SBVTestSuite/TestSuite/Queries/UISat.hs --- a/SBVTestSuite/TestSuite/Queries/UISat.hs +++ b/SBVTestSuite/TestSuite/Queries/UISat.hs @@ -8,6 +8,7 @@ -- -- Testing UI function sat examples via queries ----------------------------------------------------------------------------- +{-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wall -Werror #-} diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 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: -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