diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,22 @@ * Hackage: * GitHub: +### Version 13.5, 2026-01-26 + + * Replace internal SMT-lib program representation from plain String to Text. This + should improve performance and memory behavior in certain cases. Since solver time + dominates for most cases, this is not going to be noticable by end-users, except + for very large programs. In any case, it should at least improve memory usage. + NB. Historical note: Most of these transformations were done by Claude code; the + era of AI coding had its first contributions to SBV. I' duly impressed by Claude's + ability to understand and manipulate Haskell. (I also tried Gemini, which was less + successful, compared to Claude.) I, for one, welcome our new computer overlords. + + * Added Documentation.SBV.Examples.TP.UpDown.hs, demonstrating proof of a a couple of + list-processing functions together with naturals using TP. The problem itself is inspired + by a midterm exam question for an ACL2-class taught by J Moore at UT Austin back in 2011; + a minor tribute to J's amazing legacy. + ### Version 13.4, 2026-01-09 * Remove Eq constraint on readArray, generalizing it to arbitrary types for array-reads. diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -1164,7 +1164,7 @@ @ eval :: SExpr -> SInteger -eval = go SL.nil +eval = go [] where go :: SList (String, Integer) -> SExpr -> SInteger go = smtFunction "eval" $ \env expr -> [sCase|Expr expr of Num i -> i @@ -1357,15 +1357,15 @@ Q.E.D. >>> prove $ roundTrip @Int32 Falsifiable. Counter-example: - s0 = RoundTowardPositive :: RoundingMode - s1 = 1104019333 :: Int32 + s0 = RoundNearestTiesToAway :: RoundingMode + s1 = 22049281 :: Int32 Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float: ->>> toRational (1104019333 :: Float) -1104019328 % 1 +>>> toRational (22049281 :: Float) +22049280 % 1 -Note how the numerator is different, it is off by 5. This is hardly surprising, since floats become sparser as +Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable. >>> :{ @@ -1388,15 +1388,15 @@ >>> prove $ roundTrip @Int64 Falsifiable. Counter-example: s0 = RoundNearestTiesToEven :: RoundingMode - s1 = -2305843042984656748 :: Int64 + s1 = 2305843026393563113 :: Int64 Just like in the `SFloat` case, once we reach 64-bits, we no longer can exactly represent the integer value for all possible values: ->>> toRational (fromIntegral (-2305843042984656748 :: Int64) :: Double) -(-2305843042984656896) % 1 +>>> toRational (fromIntegral (2305843026393563113 :: Int64) :: Double) +2305843026393563136 % 1 -In this case the numerator is off by 148. +In this case the numerator is off by 23. -} -- | An implementation of rotate-left, using a barrel shifter like design. Only works when both 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 @@ -21,6 +21,7 @@ import Data.Maybe (isJust, isNothing, fromJust) import qualified Data.Foldable as F (toList) import qualified Data.Set as Set (member, union, unions, empty, toList, singleton, fromList) +import qualified Data.Text as T import System.FilePath (takeBaseName, replaceExtension) import System.Random @@ -255,15 +256,15 @@ showSizedConst :: Bool -> Integer -> (Bool, Int) -> Doc showSizedConst _ i (False, 1) = text (if i == 0 then "false" else "true") showSizedConst u8h i t@(False, 8) - | u8h = text (chex False True t i) + | u8h = text $ T.unpack (chex False True t i) | True = integer i showSizedConst _ i (True, 8) = integer i -showSizedConst _ i t@(False, 16) = text $ chex False True t i -showSizedConst _ i t@(True, 16) = text $ chex False True t i -showSizedConst _ i t@(False, 32) = text $ chex False True t i -showSizedConst _ i t@(True, 32) = text $ chex False True t i -showSizedConst _ i t@(False, 64) = text $ chex False True t i -showSizedConst _ i t@(True, 64) = text $ chex False True t i +showSizedConst _ i t@(False, 16) = text $ T.unpack $ chex False True t i +showSizedConst _ i t@(True, 16) = text $ T.unpack $ chex False True t i +showSizedConst _ i t@(False, 32) = text $ T.unpack $ chex False True t i +showSizedConst _ i t@(True, 32) = text $ T.unpack $ chex False True t i +showSizedConst _ i t@(False, 64) = text $ T.unpack $ chex False True t i +showSizedConst _ i t@(True, 64) = text $ T.unpack $ chex False True t i showSizedConst _ i (s, sz) = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz -- | Generate a makefile. The first argument is True if we have a driver. 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 @@ -129,7 +129,7 @@ , "*** Hint: Move the call to 'setOption' before the query." ] | True = do State{stCfg} <- contextState - send True $ setSMTOption stCfg o + send True $ T.unpack $ setSMTOption stCfg o -- | Adding a constraint, possibly with attributes and possibly soft. Only used internally. -- Use 'constrain' and 'namedConstraint' from user programs. @@ -138,7 +138,7 @@ sbvToSV st b) unless (null atts && sv == trueSV) $ - send True $ "(" ++ asrt ++ " " ++ addAnnotations atts (show sv) ++ ")" + send True $ "(" ++ asrt ++ " " ++ T.unpack (addAnnotations atts (T.pack (show sv))) ++ ")" where asrt | isSoft = "assert-soft" | True = "assert" @@ -189,7 +189,7 @@ let cnsts = sortBy cmp . map swap . Map.toList $ newConsts - return $ toIncSMTLib cfg progInfo inps ks (allConsts, cnsts) tbls uis as constraints cfg + return $ map T.unpack $ toIncSMTLib cfg progInfo inps ks (allConsts, cnsts) tbls uis as constraints cfg mapM_ (send True) $ mergeSExpr ls diff --git a/Data/SBV/Core/Concrete.hs b/Data/SBV/Core/Concrete.hs --- a/Data/SBV/Core/Concrete.hs +++ b/Data/SBV/Core/Concrete.hs @@ -28,6 +28,7 @@ import Data.Char (chr, isSpace) import Data.List (intercalate) +import qualified Data.Text as T import Data.SBV.Core.Kind import Data.SBV.Core.AlgReals @@ -242,8 +243,8 @@ where par v | parens = '(' : v ++ ")" | True = v withKind isInterval v | not shk = v - | isInterval = v ++ " :: [" ++ showBaseKind (kindOf extCV) ++ "]" - | True = v ++ " :: " ++ showBaseKind (kindOf extCV) + | isInterval = v ++ " :: [" ++ T.unpack (showBaseKind (kindOf extCV)) ++ "]" + | True = v ++ " :: " ++ T.unpack (showBaseKind (kindOf extCV)) add :: String -> String -> String add n ('-':v) = n ++ " - " ++ v @@ -367,7 +368,7 @@ showCV :: Bool -> CV -> String showCV shk w | isBoolean w = show (cvToBool w) ++ (if shk then " :: Bool" else "") showCV shk w = sh (cvVal w) ++ kInfo - where kInfo | shk = " :: " ++ showBaseKind wk + where kInfo | shk = " :: " ++ T.unpack (showBaseKind wk) | True = "" wk = kindOf w 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 @@ -40,6 +40,8 @@ import Data.Int import Data.Word import Data.SBV.Core.AlgReals +import Data.Text (Text) +import qualified Data.Text as T import Data.Proxy import Data.Kind @@ -128,8 +130,8 @@ show (KBounded True n) = pickType n "SInt" "SInt " ++ show n show KUnbounded = "SInteger" show KReal = "SReal" - show (KApp c ks) = unwords (c : map (kindParen . showBaseKind ) ks) - show (KADT s pks _) = unwords (s : map (kindParen . showBaseKind . snd) pks) + show (KApp c ks) = unwords (c : map (T.unpack . kindParen . showBaseKind ) ks) + show (KADT s pks _) = unwords (s : map (T.unpack . kindParen . showBaseKind . snd) pks) show KFloat = "SFloat" show KDouble = "SDouble" show (KFP eb sb) = "SFloatingPoint " ++ show eb ++ " " ++ show sb @@ -139,33 +141,34 @@ show (KSet e) = "{" ++ show e ++ "}" show (KTuple m) = "(" ++ intercalate ", " (show <$> m) ++ ")" show KRational = "SRational" - show (KArray k1 k2) = "SArray " ++ kindParen (showBaseKind k1) ++ " " ++ kindParen (showBaseKind k2) + show (KArray k1 k2) = "SArray " ++ T.unpack (kindParen (showBaseKind k1)) ++ " " ++ T.unpack (kindParen (showBaseKind k2)) -- | A version of show for kinds that says Bool instead of SBool, Float instead of SFloat, etc. -showBaseKind :: Kind -> String +showBaseKind :: Kind -> Text showBaseKind = sh - where sh (KVar s) = s - sh k@KBool = noS (show k) - sh (KBounded False n) = pickType n "Word" "WordN " ++ show n - sh (KBounded True n) = pickType n "Int" "IntN " ++ show n - sh (KApp s ks) = unwords (s : map (kindParen . sh) ks) - sh k@KUnbounded = noS (show k) - sh k@KReal = noS (show k) - sh k@KADT{} = show k -- Leave user-sorts untouched! - sh k@KFloat = noS (show k) - sh k@KDouble = noS (show k) - sh k@KFP{} = noS (show k) - sh k@KChar = noS (show k) - sh k@KString = noS (show k) - sh KRational = "Rational" - sh (KList k) = "[" ++ sh k ++ "]" - sh (KSet k) = "{" ++ sh k ++ "}" - sh (KTuple ks) = "(" ++ intercalate ", " (map sh ks) ++ ")" - sh (KArray k1 k2) = "Array " ++ kindParen (sh k1) ++ " " ++ kindParen (sh k2) + where sh (KVar s) = T.pack s + sh k@KBool = noS (T.pack $ show k) + sh (KBounded False n) = T.pack (pickType n "Word" "WordN ") <> T.pack (show n) + sh (KBounded True n) = T.pack (pickType n "Int" "IntN ") <> T.pack (show n) + sh (KApp s ks) = T.pack $ unwords (s : map (T.unpack . kindParen . sh) ks) + sh k@KUnbounded = noS (T.pack $ show k) + sh k@KReal = noS (T.pack $ show k) + sh k@KADT{} = T.pack $ show k -- Leave user-sorts untouched! + sh k@KFloat = noS (T.pack $ show k) + sh k@KDouble = noS (T.pack $ show k) + sh k@KFP{} = noS (T.pack $ show k) + sh k@KChar = noS (T.pack $ show k) + sh k@KString = noS (T.pack $ show k) + sh KRational = T.pack "Rational" + sh (KList k) = T.pack "[" <> sh k <> T.pack "]" + sh (KSet k) = T.pack "{" <> sh k <> T.pack "}" + sh (KTuple ks) = T.pack "(" <> T.pack (intercalate ", " (map (T.unpack . sh) ks)) <> T.pack ")" + sh (KArray k1 k2) = T.pack "Array " <> kindParen (sh k1) <> T.pack " " <> kindParen (sh k2) -- Drop the initial S if it's there - noS ('S':s) = s - noS s = s + noS s = case T.uncons s of + Just ('S', rest) -> rest + _ -> s -- For historical reasons, we show 8-16-32-64 bit values with no space; others with a space. pickType :: Int -> String -> String -> String @@ -174,12 +177,21 @@ | True = other -- | Put parens if necessary. This test is rather crummy, but seems to work ok -kindParen :: String -> String -kindParen s@('[':_) = s -kindParen s@('(':_) = s -kindParen s | any isSpace s = '(' : s ++ ")" - | True = s +kindParen :: Text -> Text +kindParen s = case T.uncons s of + Just ('[', _) -> s + Just ('(', _) -> s + _ -> if T.any isSpace s + then T.singleton '(' <> s <> T.singleton ')' + else s +-- | String version of kindParen for backward compatibility +kindParenStr :: String -> String +kindParenStr s@('[':_) = s +kindParenStr s@('(':_) = s +kindParenStr s | any isSpace s = '(' : s ++ ")" + | True = s + -- | How the type maps to SMT land smtType :: Kind -> String smtType (KVar s) = s @@ -194,8 +206,8 @@ smtType KChar = "String" smtType (KList k) = "(Seq " ++ smtType k ++ ")" smtType (KSet k) = "(Array " ++ smtType k ++ " Bool)" -smtType (KApp s ks) = kindParen $ unwords (s : map smtType ks) -smtType (KADT s pks _) = kindParen $ unwords (s : map (smtType . snd) pks) +smtType (KApp s ks) = kindParenStr $ unwords (s : map smtType ks) +smtType (KADT s pks _) = kindParenStr $ unwords (s : map (smtType . snd) pks) smtType (KTuple []) = "SBVTuple0" smtType (KTuple kinds) = "(SBVTuple" ++ show (length kinds) ++ " " ++ unwords (smtType <$> kinds) ++ ")" smtType KRational = "SBVRational" 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 @@ -97,6 +97,7 @@ import qualified Data.Foldable as F (toList) import qualified Data.Sequence as S (Seq, empty, (|>), (<|), lookup, elemIndexL) import qualified Data.Text as T +import Data.Text (Text) import System.Mem.StableName import System.Random @@ -2098,15 +2099,15 @@ smtLibVersionExtension :: SMTLibVersion -> String smtLibVersionExtension SMTLib2 = "smt2" --- | Representation of an SMT-Lib program. The second [String] are the function definitions, +-- | Representation of an SMT-Lib program. The second Text are the function definitions, -- which is *replicated* in the first one. There are cases where that we need the second part on its own. -data SMTLibPgm = SMTLibPgm SMTLibVersion [String] [String] +data SMTLibPgm = SMTLibPgm SMTLibVersion Text Text instance NFData SMTLibVersion where rnf a = a `seq` () instance NFData SMTLibPgm where rnf (SMTLibPgm v p d) = rnf v `seq` rnf p `seq` rnf d instance Show SMTLibPgm where - show (SMTLibPgm _ pgm _) = intercalate "\n" pgm + show (SMTLibPgm _ pgm _) = T.unpack pgm -- Other Technicalities.. instance NFData GeneralizedCV where diff --git a/Data/SBV/Lambda.hs b/Data/SBV/Lambda.hs --- a/Data/SBV/Lambda.hs +++ b/Data/SBV/Lambda.hs @@ -27,6 +27,8 @@ import Control.Monad (join) import Control.Monad.Trans (liftIO, MonadIO) +import qualified Data.Text as T + import Data.SBV.Core.Data import Data.SBV.Core.Kind import Data.SBV.SMT.SMTLib2 @@ -392,8 +394,8 @@ svBindings :: [((SV, String), Maybe String)] svBindings = map mkAsgn assignments - where mkAsgn (sv, e@(SBVApp (Label l) _)) = ((sv, converter e), Just l) - mkAsgn (sv, e) = ((sv, converter e), Nothing) + where mkAsgn (sv, e@(SBVApp (Label l) _)) = ((sv, T.unpack $ converter e), Just l) + mkAsgn (sv, e) = ((sv, T.unpack $ converter e), Nothing) converter = cvtExp cfg curProgInfo (capabilities (solver cfg)) rm tableMap @@ -418,7 +420,7 @@ lambdaTable :: String -> Kind -> Kind -> [SV] -> String lambdaTable extraSpace ak rk elts = "(lambda ((" ++ lv ++ " " ++ smtType ak ++ "))" ++ space ++ chain 0 elts ++ ")" - where cnst k i = cvtCV rm (mkConstCV k (i::Integer)) + where cnst k i = T.unpack $ cvtCV rm (mkConstCV k (i::Integer)) lv = "idx" 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 @@ -550,7 +550,7 @@ -- | Given a satisfiability problem, extract the function definitions in it defs2smt :: SatisfiableM m a => a -> m String defs2smt = generateSMTBenchMarkGen True satArgReduce defs - where defs (SMTLibPgm _ _ ds) = intercalate "\n" ds + where defs (SMTLibPgm _ _ ds) = T.unpack ds -- | Create an SMT-Lib2 benchmark, for a SAT query. generateSMTBenchmarkSat :: SatisfiableM m a => a -> m String 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 @@ -601,7 +601,7 @@ trim = reverse . dropWhile isSpace . reverse - (ats, rt) = case map showBaseKind ts of + (ats, rt) = case map (T.unpack . showBaseKind) ts of [] -> error $ "showModelUI: Unexpected type: " ++ show (SBVType ts) tss -> (init tss, last tss) @@ -638,9 +638,9 @@ -- NB. We'll ignore crackNum here. Seems to be overkill while displaying an -- uninterpreted function. scv = sh (printBase cfg) - where sh 2 = binP + where sh 2 = T.unpack . binP sh 10 = showCV False - sh 16 = hexP + sh 16 = T.unpack . hexP sh _ = show -- NB. If we have a float NaN/Infinity/+0/-0 etc. these will @@ -660,9 +660,9 @@ -- | Show a constant value, in the user-specified base shCV :: SMTConfig -> String -> CV -> String shCV SMTConfig{printBase, crackNum, verbose, crackNumSurfaceVals} nm cv = cracked (sh printBase cv) - where sh 2 = binS + where sh 2 = T.unpack . binS sh 10 = show - sh 16 = hexS + sh 16 = T.unpack . hexS sh n = \w -> show w ++ " -- Ignoring unsupported printBase " ++ show n ++ ", use 2, 10, or 16." cracked def diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs --- a/Data/SBV/SMT/SMTLib.hs +++ b/Data/SBV/SMT/SMTLib.hs @@ -23,6 +23,7 @@ import Data.SBV.SMT.Utils import qualified Data.SBV.SMT.SMTLib2 as SMT2 +import Data.Text (Text) -- | Convert to SMT-Lib, in a full program context. toSMTLib :: SMTConfig -> SMTLibConverter SMTLibPgm @@ -30,7 +31,7 @@ SMTLib2 -> toSMTLib2 -- | Convert to SMT-Lib, in an incremental query context. -toIncSMTLib :: SMTConfig -> SMTLibIncConverter [String] +toIncSMTLib :: SMTConfig -> SMTLibIncConverter [Text] toIncSMTLib SMTConfig{smtLibVersion} = case smtLibVersion of SMTLib2 -> toIncSMTLib2 -- | Convert to SMTLib-2 format @@ -42,6 +43,6 @@ (pgm, defs) = converter ctx progInfo kindInfo isSat comments qinps consts tbls uis axs asgnsSeq cstrs out config -- | Convert to SMTLib-2 format -toIncSMTLib2 :: SMTLibIncConverter [String] +toIncSMTLib2 :: SMTLibIncConverter [Text] toIncSMTLib2 = cvt SMTLib2 where cvt SMTLib2 = SMT2.cvtInc 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 @@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} @@ -25,6 +26,8 @@ import qualified Data.IntMap.Strict as IM import Data.Set (Set) import qualified Data.Set as Set +import qualified Data.Text as T +import Data.Text (Text) import Data.SBV.Core.Data import Data.SBV.Core.Kind (smtType, needsFlattening, expandKinds, substituteADTVars) @@ -54,31 +57,32 @@ _ -> f plu | length xs > 1 = "s are" | True = " is" - in Just $ unlines $ [ - "Data.SBV.mkSymbolic: Impossible happened! Unregistered subkinds." - , "***" - , "*** The following kind" ++ plu ++ " not registered: " ++ unwords (map fst xs) - , "***" - , "*** Please report this as a bug." - , "***" - , "*** As a workaround, you can try registering each ADT subfield, using: " - , "***" - , "*** {-# LANGUAGE TypeApplications #-}" - , "***" - , "*** import Data.Proxy" - , "*** registerType (Proxy @" ++ mkProxy h cnt ++ ")" - ] - ++ extras cnt - ++ [ "***" - , "*** Even if the workaround does the trick for you, it should not" - , "*** be needed. Please report this as a bug!" - ] + msg = T.unlines $ [ + "Data.SBV.mkSymbolic: Impossible happened! Unregistered subkinds." + , "***" + , "*** The following kind" <> plu <> " not registered: " <> T.unwords (map (T.pack . fst) xs) + , "***" + , "*** Please report this as a bug." + , "***" + , "*** As a workaround, you can try registering each ADT subfield, using: " + , "***" + , "*** {-# LANGUAGE TypeApplications #-}" + , "***" + , "*** import Data.Proxy" + , "*** registerType (Proxy @" <> mkProxy h cnt <> ")" + ] + ++ extras cnt + ++ [ "***" + , "*** Even if the workaround does the trick for you, it should not" + , "*** be needed. Please report this as a bug!" + ] + in Just $ T.unpack msg where apps = nub [(n, length as) | KApp n as <- concatMap expandKinds ks] defs = nub [n | KADT n _ _ <- ks] - mkProxy h 0 = h - mkProxy h n = '(' : unwords (h : replicate n "Integer") ++ ")" + mkProxy h 0 = T.pack h + mkProxy h n = "(" <> T.unwords (T.pack h : replicate n "Integer") <> ")" extras 0 = [] extras _ = [ "***" @@ -88,12 +92,12 @@ ] -- | Translate a problem into an SMTLib2 script -cvt :: SMTLibConverter ([String], [String]) +cvt :: SMTLibConverter (Text, Text) cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs (SBVPgm asgnsSeq) cstrs out cfg | Just s <- checkKinds allKinds = error s | True - = (pgm, exportedDefs) + = (T.intercalate "\n" pgm, T.intercalate "\n" exportedDefs) where allKinds = Set.toList kindInfo -- Below can simply be defined as: nub (sort (G.universeBi asgnsSeq)) @@ -141,12 +145,12 @@ , ("has data-types/sorts", supportsADTs, not (null adtsNoRM)) ] - nope w = [ "*** Given problem requires support for " ++ w - , "*** But the chosen solver (" ++ show (name (solver cfg)) ++ ") doesn't support this feature." + nope w = [ "*** Given problem requires support for " <> T.pack w + , "*** But the chosen solver (" <> T.pack (show (name (solver cfg))) <> ") doesn't support this feature." ] -- Some cases require all, some require none. - setAll reason = ["(set-logic " ++ showLogic Logic_ALL ++ ") ; " ++ reason ++ ", using catch-all."] + setAll reason = ["(set-logic " <> T.pack (showLogic Logic_ALL) <> ") ; " <> T.pack reason <> ", using catch-all."] isCVC5 = case name (solver cfg) of CVC5 -> True @@ -157,29 +161,32 @@ showLogic l = show l -- Determining the logic is surprisingly tricky! + logic :: [Text] logic -- user told us what to do: so just take it: | Just l <- case [l | SetLogic l <- solverSetOptions cfg] of [] -> Nothing [l] -> Just l - ls -> error $ unlines [ "" - , "*** Only one setOption call to 'setLogic' is allowed, found: " ++ show (length ls) - , "*** " ++ unwords (map show ls) + ls -> let msg = T.unlines [ "" + , "*** Only one setOption call to 'setLogic' is allowed, found: " <> T.pack (show (length ls)) + , "*** " <> T.unwords (map (T.pack . show) ls) ] + in error $ T.unpack msg = case l of Logic_NONE -> ["; NB. Not setting the logic per user request of Logic_NONE"] - _ -> ["(set-logic " ++ showLogic l ++ ") ; NB. User specified."] + _ -> ["(set-logic " <> T.pack (showLogic l) <> ") ; NB. User specified."] -- There's a reason why we can't handle this problem: | Just cantDo <- doesntHandle - = error $ unlines $ [ "" + = let msg = T.unlines $ [ "" , "*** SBV is unable to choose a proper solver configuration:" , "***" ] - ++ cantDo - ++ [ "***" + <> cantDo + <> [ "***" , "*** Please report this as a feature request, either for SBV or the backend solver." ] + in error $ T.unpack msg -- Otherwise, we try to determine the most suitable logic. -- NB. This isn't really fool proof! @@ -217,7 +224,7 @@ = case ctx of QueryExternal -> ["(set-logic ALL) ; external query, using all logics."] QueryInternal -> if supportsBitVectors solverCaps - then ["(set-logic " ++ qs ++ as ++ ufs ++ "BV)"] + then ["(set-logic " <> T.pack (T.unpack qs <> T.unpack as <> T.unpack ufs) <> "BV)"] else ["(set-logic ALL)"] -- fall-thru where qs | not needsQuantifiers = "QF_" | True = "" @@ -227,8 +234,9 @@ | True = "UF" -- SBV always requires the production of models! + getModels :: [Text] getModels = "(set-option :produce-models true)" - : concat [flattenConfig | any needsFlattening kindInfo, Just flattenConfig <- [supportsFlattenedModels solverCaps]] + : concat [map T.pack flattenConfig | any needsFlattening kindInfo, Just flattenConfig <- [supportsFlattenedModels solverCaps]] -- process all other settings we're given. If an option cannot be repeated, we only take the last one. userSettings = map (setSMTOption cfg) $ filter (not . isLogic) $ foldr comb [] $ solverSetOptions cfg @@ -246,8 +254,8 @@ | True = o : rest settings = userSettings -- NB. Make sure this comes first! - ++ getModels - ++ logic + <> getModels + <> logic (inputs, trackerVars) = case allInputs of @@ -258,34 +266,34 @@ , "*** Saw: " ++ show ps ] - pgm = map ("; " ++) comments - ++ settings - ++ [ "; --- tuples ---" ] - ++ concatMap declTuple tupleArities - ++ [ "; --- sums ---" ] - ++ (if containsRationals kindInfo then declRationals else []) - ++ [ "; --- ADTs --- " | not (null adtsNoRM)] - ++ declADT adtsNoRM - ++ [ "; --- literal constants ---" ] - ++ concatMap (declConst cfg) consts - ++ [ "; --- top level inputs ---"] - ++ concat [declareFun s (SBVType [kindOf s]) (userName s) | var <- inputs, let s = getSV var] - ++ [ "; --- optimization tracker variables ---" | not (null trackerVars) ] - ++ concat [declareFun s (SBVType [kindOf s]) (Just ("tracks " <> nm)) | var <- trackerVars, let s = getSV var, let nm = getUserName' var] - ++ [ "; --- constant tables ---" ] - ++ concatMap (uncurry (:) . mkTable) constTables - ++ [ "; --- non-constant tables ---" ] - ++ map nonConstTable nonConstTables - ++ [ "; --- uninterpreted constants ---" ] - ++ concatMap (declUI curProgInfo) uis - ++ [ "; --- user defined functions ---"] - ++ userDefs - ++ [ "; --- assignments ---" ] - ++ concatMap (declDef curProgInfo cfg tableMap) asgns - ++ [ "; --- delayedEqualities ---" ] - ++ map (\s -> "(assert " ++ s ++ ")") delayedEqualities - ++ [ "; --- formula ---" ] - ++ finalAssert + pgm = map (T.pack . ("; " <>)) comments + <> settings + <> [ "; --- tuples ---" ] + <> concatMap declTuple tupleArities + <> [ "; --- sums ---" ] + <> (if containsRationals kindInfo then declRationals else []) + <> [ "; --- ADTs --- " | not (null adtsNoRM)] + <> declADT adtsNoRM + <> [ "; --- literal constants ---" ] + <> concatMap (declConst cfg) consts + <> [ "; --- top level inputs ---"] + <> concat [declareFun s (SBVType [kindOf s]) (userName s) | var <- inputs, let s = getSV var] + <> [ "; --- optimization tracker variables ---" | not (null trackerVars) ] + <> concat [declareFun s (SBVType [kindOf s]) (Just ("tracks " <> T.pack nm)) | var <- trackerVars, let s = getSV var, let nm = getUserName' var] + <> [ "; --- constant tables ---" ] + <> concatMap (uncurry (:) . mkTable) constTables + <> [ "; --- non-constant tables ---" ] + <> map nonConstTable nonConstTables + <> [ "; --- uninterpreted constants ---" ] + <> concatMap (declUI curProgInfo) uis + <> [ "; --- user defined functions ---"] + <> userDefs + <> [ "; --- assignments ---" ] + <> concatMap (declDef curProgInfo cfg tableMap) asgns + <> [ "; --- delayedEqualities ---" ] + <> map (\s -> "(assert " <> s <> ")") delayedEqualities + <> [ "; --- formula ---" ] + <> finalAssert userDefs = declUserFuns defs exportedDefs @@ -301,10 +309,10 @@ finalAssert | noConstraints = [] - | True = map (\(attr, v) -> "(assert " ++ addAnnotations attr (mkLiteral v) ++ ")") hardAsserts - ++ map (\(attr, v) -> "(assert-soft " ++ addAnnotations attr (mkLiteral v) ++ ")") softAsserts + | True = map (\(attr, v) -> "(assert " <> addAnnotations attr (mkLiteral v) <> ")") hardAsserts + <> map (\(attr, v) -> "(assert-soft " <> addAnnotations attr (mkLiteral v) <> ")") softAsserts where mkLiteral (Left v) = cvtSV v - mkLiteral (Right v) = "(not " ++ cvtSV v ++ ")" + mkLiteral (Right v) = "(not " <> cvtSV v <> ")" (noConstraints, assertions) = finalAssertions @@ -338,11 +346,11 @@ userNameMap = M.fromList $ map (\nSymVar -> (getSV nSymVar, getUserName' nSymVar)) inputs userName s = case M.lookup s userNameMap of - Just u | show s /= u -> Just $ "tracks user variable " ++ show u + Just u | show s /= u -> Just $ "tracks user variable " <> T.pack (show u) _ -> Nothing -- | Declare ADTs -declADT :: [(String, [(String, Kind)], [(String, [Kind])])] -> [String] +declADT :: [(String, [(String, Kind)], [(String, [Kind])])] -> [Text] declADT = concatMap declGroup . DG.stronglyConnComp . map mkNode where mkNode adt@(n, pks, cstrs) = (adt, n, [s | KApp s _ <- concatMap expandKinds (map snd pks ++ concatMap snd cstrs)]) @@ -353,36 +361,36 @@ [d] -> singleADT d _ -> multiADT ds - parParens :: [(String, Kind)] -> (String, String) + parParens :: [(String, Kind)] -> (Text, Text) parParens [] = ("", "") - parParens ps = (" (par (" ++ unwords (map fst ps) ++ ")", ")") + parParens ps = (" (par (" <> T.unwords (map (T.pack . fst) ps) <> ")", ")") - mkC (nm, []) = nm - mkC (nm, ts) = nm ++ " " ++ unwords ['(' : mkF (nm ++ "_" ++ show i) t ++ ")" | (i, t) <- zip [(1::Int)..] ts] - where mkF a t = "get" ++ a ++ " " ++ smtType t + mkC (nm, []) = T.pack nm + mkC (nm, ts) = T.pack nm <> " " <> T.unwords ['(' `T.cons` mkF (nm <> "_" <> show i) t <> ")" | (i, t) <- zip [(1::Int)..] ts] + where mkF a t = "get" <> T.pack a <> " " <> T.pack (smtType t) - singleADT :: (String, [(String, Kind)], [(String, [Kind])]) -> [String] - singleADT (tName, [], []) = ["(declare-sort " ++ tName ++ " 0) ; N.B. Uninterpreted sort."] - singleADT (tName, pks, cstrs) = ("; User defined ADT: " ++ tName) : decl - where decl = ("(declare-datatype " ++ tName ++ parOpen ++ " (") - : [" (" ++ mkC c ++ ")" | c <- cstrs] - ++ ["))" ++ parClose] + singleADT :: (String, [(String, Kind)], [(String, [Kind])]) -> [Text] + singleADT (tName, [], []) = ["(declare-sort " <> T.pack tName <> " 0) ; N.B. Uninterpreted sort."] + singleADT (tName, pks, cstrs) = ("; User defined ADT: " <> T.pack tName) : decl + where decl = ("(declare-datatype " <> T.pack tName <> parOpen <> " (") + : [" (" <> mkC c <> ")" | c <- cstrs] + <> ["))" <> parClose] (parOpen, parClose) = parParens pks - multiADT :: [(String, [(String, Kind)], [(String, [Kind])])] -> [String] - multiADT adts = ("; User defined mutually-recursive ADTs: " ++ intercalate ", " (map (\(a, _, _) -> a) adts)) : decl - where decl = ("(declare-datatypes (" ++ typeDecls ++ ") (") + multiADT :: [(String, [(String, Kind)], [(String, [Kind])])] -> [Text] + multiADT adts = ("; User defined mutually-recursive ADTs: " <> T.intercalate ", " (map (\(a, _, _) -> T.pack a) adts)) : decl + where decl = ("(declare-datatypes (" <> typeDecls <> ") (") : concatMap adtBody adts - ++ ["))"] + <> ["))"] - typeDecls = unwords ['(' : name ++ " " ++ show (length pks) ++ ")" | (name, pks, _) <- adts] + typeDecls = T.unwords ['(' `T.cons` T.pack name <> " " <> T.pack (show (length pks)) <> ")" | (name, pks, _) <- adts] adtBody (_, pks, cstrs) = body where (parOpen, parClose) = parParens pks - body = (" " ++ parOpen ++ " (") - : [" (" ++ mkC c ++ ")" | c <- cstrs] - ++ [" )" ++ parClose] + body = (" " <> parOpen <> " (") + : [" (" <> mkC c <> ")" | c <- cstrs] + <> [" )" <> parClose] -- | Declare tuple datatypes -- @@ -393,24 +401,24 @@ -- ((mkSBVTuple2 (proj_1_SBVTuple2 T1) -- (proj_2_SBVTuple2 T2)))))) -- @ -declTuple :: Int -> [String] +declTuple :: Int -> [Text] declTuple arity | arity == 0 = ["(declare-datatypes ((SBVTuple0 0)) (((mkSBVTuple0))))"] | arity == 1 = error "Data.SBV.declTuple: Unexpected one-tuple" - | True = (l1 ++ "(par (" ++ unwords [param i | i <- [1..arity]] ++ ")") - : [pre i ++ proj i ++ post i | i <- [1..arity]] - where l1 = "(declare-datatypes ((SBVTuple" ++ show arity ++ " " ++ show arity ++ ")) (" - l2 = replicate (length l1) ' ' ++ "((mkSBVTuple" ++ show arity ++ " " - tab = replicate (length l2) ' ' + | True = (l1 <> "(par (" <> T.unwords [param i | i <- [1..arity]] <> ")") + : [pre i <> proj i <> post i | i <- [1..arity]] + where l1 = "(declare-datatypes ((SBVTuple" <> T.pack (show arity) <> " " <> T.pack (show arity) <> ")) (" + l2 = T.replicate (T.length l1) " " <> "((mkSBVTuple" <> T.pack (show arity) <> " " + tab = T.replicate (T.length l2) " " pre 1 = l2 pre _ = tab - proj i = "(proj_" ++ show i ++ "_SBVTuple" ++ show arity ++ " " ++ param i ++ ")" + proj i = "(proj_" <> T.pack (show i) <> "_SBVTuple" <> T.pack (show arity) <> " " <> param i <> ")" post i = if i == arity then ")))))" else "" - param i = "T" ++ show i + param i = "T" <> T.pack (show i) -- | Find the set of tuple sizes to declare, eg (2-tuple, 5-tuple). -- NB. We do *not* need to recursively go into list/tuple kinds here, @@ -427,7 +435,7 @@ -- Internally, we do *not* keep the rationals in reduced form! So, the boolean operators explicitly do the math -- to make sure equivalent values are treated correctly. -declRationals :: [String] +declRationals :: [Text] declRationals = [ "(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))" , "" , "(define-fun sbv.rat.eq ((x SBVRational) (y SBVRational)) Bool" @@ -445,35 +453,35 @@ -- to do as an extra in the incremental context. See `Data.SBV.Core.Symbolic.registerKind` -- for a list of what we include, in case something doesn't show up -- and you need it! -cvtInc :: SMTLibIncConverter [String] +cvtInc :: SMTLibIncConverter [Text] cvtInc curProgInfo inps newKs (_, consts) tbls uis (SBVPgm asgnsSeq) cstrs cfg = -- any new settings? settings -- sorts - ++ declADT [(s, pks, cs) | k@(KADT s pks cs) <- newKinds, not (isRoundingMode k)] + <> declADT [(s, pks, cs) | k@(KADT s pks cs) <- newKinds, not (isRoundingMode k)] -- tuples. NB. Only declare the new sizes, old sizes persist. - ++ concatMap declTuple (findTupleArities newKs) + <> concatMap declTuple (findTupleArities newKs) -- constants - ++ concatMap (declConst cfg) consts + <> concatMap (declConst cfg) consts -- inputs - ++ concatMap declInp inps + <> concatMap declInp inps -- uninterpreteds - ++ concatMap (declUI curProgInfo) uis + <> concatMap (declUI curProgInfo) uis -- table declarations - ++ tableDecls + <> tableDecls -- expressions - ++ concatMap (declDef curProgInfo cfg tableMap) asgnsSeq + <> concatMap (declDef curProgInfo cfg tableMap) asgnsSeq -- table setups - ++ concat tableAssigns + <> concat tableAssigns -- extra constraints - ++ map (\(isSoft, attr, v) -> "(assert" ++ (if isSoft then "-soft " else " ") ++ addAnnotations attr (cvtSV v) ++ ")") (F.toList cstrs) + <> map (\(isSoft, attr, v) -> "(assert" <> (if isSoft then "-soft " else " ") <> addAnnotations attr (cvtSV v) <> ")") (F.toList cstrs) where rm = roundingMode cfg newKinds = Set.toList newKs declInp (getSV -> s) = declareFun s (SBVType [kindOf s]) Nothing - (tableMap, allTables) = (tm, ct ++ nct) + (tableMap, allTables) = (tm, ct <> nct) where (tm, ct, nct) = constructTables rm consts tbls (tableDecls, tableAssigns) = unzip $ map mkTable allTables @@ -481,33 +489,33 @@ -- If we need flattening in models, do emit the required lines if preset settings | any needsFlattening newKinds - = concat (catMaybes [supportsFlattenedModels solverCaps]) + = concat (catMaybes [map T.pack <$> supportsFlattenedModels solverCaps]) | True = [] where solverCaps = capabilities (solver cfg) -declDef :: ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [String] +declDef :: ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [Text] declDef curProgInfo cfg tableMap (s, expr) = case expr of - SBVApp (Label m) [e] -> defineFun cfg (s, cvtSV e) (Just m) + SBVApp (Label m) [e] -> defineFun cfg (s, cvtSV e) (Just $ T.pack m) e -> defineFun cfg (s, cvtExp cfg curProgInfo caps rm tableMap e) Nothing where caps = capabilities (solver cfg) rm = roundingMode cfg -defineFun :: SMTConfig -> (SV, String) -> Maybe String -> [String] +defineFun :: SMTConfig -> (SV, Text) -> Maybe Text -> [Text] defineFun cfg (s, def) mbComment - | hasDefFun = ["(define-fun " ++ varT ++ " " ++ def ++ ")" ++ cmnt] - | True = [ "(declare-fun " ++ varT ++ ")" ++ cmnt - , "(assert (= " ++ var ++ " " ++ def ++ "))" + | hasDefFun = ["(define-fun " <> varT <> " " <> def <> ")" <> cmnt] + | True = [ "(declare-fun " <> varT <> ")" <> cmnt + , "(assert (= " <> var <> " " <> def <> "))" ] - where var = show s - varT = var ++ " " ++ svFunType [] s - cmnt = maybe "" (" ; " ++) mbComment + where var = T.pack $ show s + varT = var <> " " <> svFunType [] s + cmnt = maybe "" (" ; " <>) mbComment hasDefFun = supportsDefineFun $ capabilities (solver cfg) -- Declare constants. NB. We don't declare true/false; but just inline those as necessary -declConst :: SMTConfig -> (SV, CV) -> [String] +declConst :: SMTConfig -> (SV, CV) -> [Text] declConst cfg (s, c) | s == falseSV || s == trueSV = [] @@ -515,34 +523,34 @@ = defineFun cfg (s, cvtCV (roundingMode cfg) c) Nothing -- Make a function equality of nm against the internal function fun -mkRelEq :: String -> (String, String) -> Kind -> String +mkRelEq :: Text -> (Text, Text) -> Kind -> Text mkRelEq nm (fun, order) ak = res - where lhs = "(" ++ nm ++ " x y)" - rhs = "((_ " ++ fun ++ " " ++ order ++ ") x y)" - tk = smtType ak - res = "(forall ((x " ++ tk ++ ") (y " ++ tk ++ ")) (= " ++ lhs ++ " " ++ rhs ++ "))" + where lhs = "(" <> nm <> " x y)" + rhs = "((_ " <> fun <> " " <> order <> ") x y)" + tk = T.pack $ smtType ak + res = "(forall ((x " <> tk <> ") (y " <> tk <> ")) (= " <> lhs <> " " <> rhs <> "))" -declUI :: ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [String] -declUI ProgInfo{progTransClosures} (i, (_, _, t)) = declareName i t Nothing ++ declClosure +declUI :: ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [Text] +declUI ProgInfo{progTransClosures} (i, (_, _, t)) = declareName (T.pack i) t Nothing <> declClosure where declClosure | Just external <- lookup i progTransClosures - = declareName external t Nothing - ++ ["(assert " ++ mkRelEq external ("transitive-closure", i) (argKind t) ++ ")"] + = declareName (T.pack external) t Nothing + <> ["(assert " <> mkRelEq (T.pack external) ("transitive-closure", T.pack i) (argKind t) <> ")"] | True = [] argKind (SBVType [ka, _, KBool]) = ka - argKind _ = error $ "declUI: Unexpected type for name: " ++ show (i, t) + argKind _ = error $ "declUI: Unexpected type for name: " <> show (i, t) -- Note that even though we get all user defined-functions here (i.e., lambda and axiom), we can only have defined-functions -- and axioms. We spit axioms as is; and topologically sort the definitions. -declUserFuns :: [(String, (SMTDef, SBVType))] -> [String] +declUserFuns :: [(String, (SMTDef, SBVType))] -> [Text] declUserFuns ds = map declGroup sorted where mkNode d = (d, fst d, getDeps d) getDeps (_, (SMTDef _ d _ _, _)) = d - mkDecl Nothing rt = "() " ++ rt - mkDecl (Just p) rt = p ++ " " ++ rt + mkDecl Nothing rt = "() " <> rt + mkDecl (Just p) rt = T.pack p <> " " <> rt sorted = DG.stronglyConnComp (map mkNode ds) @@ -552,73 +560,74 @@ [x] -> declUserDef True x xs -> declUserDefMulti xs - declUserDef isRec (nm, (SMTDef fk deps param body, ty)) = ("; " ++ nm ++ " :: " ++ show ty ++ recursive ++ frees ++ "\n") ++ s + declUserDef isRec (nm, (SMTDef fk deps param body, ty)) = + "; " <> T.pack nm <> " :: " <> T.pack (show ty) <> recursive <> frees <> "\n" <> s where (recursive, definer) | isRec = (" [Recursive]", "define-fun-rec") | True = ("", "define-fun") otherDeps = filter (/= nm) deps frees | null otherDeps = "" - | True = " [Refers to: " ++ intercalate ", " otherDeps ++ "]" + | True = " [Refers to: " <> T.intercalate ", " (map T.pack otherDeps) <> "]" - decl = mkDecl param (smtType fk) + decl = mkDecl param (T.pack $ smtType fk) - s = "(" ++ definer ++ " " ++ nm ++ " " ++ decl ++ "\n" ++ body 2 ++ ")" + s = "(" <> definer <> " " <> T.pack nm <> " " <> decl <> "\n" <> T.pack (body 2) <> ")" -- declare a bunch of mutually-recursive functions declUserDefMulti bs = render $ map collect bs - where collect (nm, (SMTDef fk deps param body, ty)) = (deps, nm, ty, '(' : nm ++ " " ++ decl ++ ")", body 3) - where decl = mkDecl param (smtType fk) + where collect (nm, (SMTDef fk deps param body, ty)) = (deps, nm, ty, "(" <> T.pack nm <> " " <> decl <> ")", body 3) + where decl = mkDecl param (T.pack $ smtType fk) - render defs = intercalate "\n" $ - [ "; " ++ intercalate ", " [n ++ " :: " ++ show ty | (_, n, ty, _, _) <- defs] + render defs = T.intercalate "\n" $ + [ "; " <> T.intercalate ", " [T.pack n <> " :: " <> T.pack (show ty) | (_, n, ty, _, _) <- defs] , "(define-funs-rec" ] - ++ [ open i ++ param d ++ close1 i | (i, d) <- zip [1..] defs] - ++ [ open i ++ dump d ++ close2 i | (i, d) <- zip [1..] defs] + <> [ open i <> param d <> close1 i | (i, d) <- zip [1..] defs] + <> [ open i <> dump d <> close2 i | (i, d) <- zip [1..] defs] where open 1 = " (" open _ = " " param (_deps, _nm, _ty, p, _body) = p - dump (deps, nm, ty, _, body) = "; Definition of: " ++ nm ++ " :: " ++ show ty ++ ". [Refers to: " ++ intercalate ", " deps ++ "]" - ++ "\n" ++ body + dump (deps, nm, ty, _, body) = "; Definition of: " <> T.pack nm <> " :: " <> T.pack (show ty) <> ". [Refers to: " <> T.intercalate ", " (map T.pack deps) <> "]" + <> "\n" <> T.pack body ld = length defs close1 n = if n == ld then ")" else "" close2 n = if n == ld then "))" else "" -mkTable :: (((Int, Kind, Kind), [SV]), [String]) -> (String, [String]) -mkTable (((i, ak, rk), _elts), is) = (decl, zipWith wrap [(0::Int)..] is ++ setup) - where t = "table" ++ show i - decl = "(declare-fun " ++ t ++ " (" ++ smtType ak ++ ") " ++ smtType rk ++ ")" +mkTable :: (((Int, Kind, Kind), [SV]), [Text]) -> (Text, [Text]) +mkTable (((i, ak, rk), _elts), is) = (decl, zipWith wrap [(0::Int)..] is <> setup) + where t = "table" <> T.pack (show i) + decl = "(declare-fun " <> t <> " (" <> T.pack (smtType ak) <> ") " <> T.pack (smtType rk) <> ")" -- Arrange for initializers - mkInit idx = "table" ++ show i ++ "_initializer_" ++ show (idx :: Int) - initializer = "table" ++ show i ++ "_initializer" + mkInit idx = "table" <> T.pack (show i) <> "_initializer_" <> T.pack (show (idx :: Int)) + initializer = "table" <> T.pack (show i) <> "_initializer" - wrap index s = "(define-fun " ++ mkInit index ++ " () Bool " ++ s ++ ")" + wrap index s = "(define-fun " <> mkInit index <> " () Bool " <> s <> ")" lis = length is setup - | lis == 0 = [ "(define-fun " ++ initializer ++ " () Bool true) ; no initialization needed" + | lis == 0 = [ "(define-fun " <> initializer <> " () Bool true) ; no initialization needed" ] - | lis == 1 = [ "(define-fun " ++ initializer ++ " () Bool " ++ mkInit 0 ++ ")" - , "(assert " ++ initializer ++ ")" + | lis == 1 = [ "(define-fun " <> initializer <> " () Bool " <> mkInit 0 <> ")" + , "(assert " <> initializer <> ")" ] - | True = [ "(define-fun " ++ initializer ++ " () Bool (and " ++ unwords (map mkInit [0..lis - 1]) ++ "))" - , "(assert " ++ initializer ++ ")" + | True = [ "(define-fun " <> initializer <> " () Bool (and " <> T.unwords (map mkInit [0..lis - 1]) <> "))" + , "(assert " <> initializer <> ")" ] -nonConstTable :: (((Int, Kind, Kind), [SV]), [String]) -> String +nonConstTable :: (((Int, Kind, Kind), [SV]), [Text]) -> Text nonConstTable (((i, ak, rk), _elts), _) = decl - where t = "table" ++ show i - decl = "(declare-fun " ++ t ++ " (" ++ smtType ak ++ ") " ++ smtType rk ++ ")" + where t = "table" <> T.pack (show i) + decl = "(declare-fun " <> t <> " (" <> T.pack (smtType ak) <> ") " <> T.pack (smtType rk) <> ")" constructTables :: RoundingMode -> [(SV, CV)] -> [((Int, Kind, Kind), [SV])] - -> ( IM.IntMap String -- table enumeration - , [(((Int, Kind, Kind), [SV]), [String])] -- constant tables - , [(((Int, Kind, Kind), [SV]), [String])] -- non-constant tables + -> ( IM.IntMap Text -- table enumeration + , [(((Int, Kind, Kind), [SV]), [Text])] -- constant tables + , [(((Int, Kind, Kind), [SV]), [Text])] -- non-constant tables ) constructTables rm consts tbls = (tableMap, constTables, nonConstTables) where allTables = [(t, genTableData rm (map fst consts) t) | t <- tbls] @@ -626,50 +635,51 @@ nonConstTables = [(t, d) | (t, Right d) <- allTables] tableMap = IM.fromList $ map grab allTables - grab (((t, _, _), _), _) = (t, "table" ++ show t) + grab (((t, _, _), _), _) = (t, "table" <> T.pack (show t)) -- Left if all constants, Right if otherwise -genTableData :: RoundingMode -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String] +genTableData :: RoundingMode -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [Text] [Text] genTableData rm consts ((i, aknd, _), elts) | null post = Left (map (mkEntry . snd) pre) | True = Right (map (mkEntry . snd) (pre ++ post)) where (pre, post) = partition fst (zipWith mkElt elts [(0::Int)..]) - t = "table" ++ show i + t = "table" <> T.pack (show i) mkElt x k = (isReady, (idx, cvtSV x)) where idx = cvtCV rm (mkConstCV aknd k) isReady = x `Set.member` constsSet - mkEntry (idx, v) = "(= (" ++ t ++ " " ++ idx ++ ") " ++ v ++ ")" + mkEntry (idx, v) = "(= (" <> t <> " " <> idx <> ") " <> v <> ")" constsSet = Set.fromList consts -svType :: SV -> String -svType s = smtType (kindOf s) +svType :: SV -> Text +svType s = T.pack $ smtType (kindOf s) -svFunType :: [SV] -> SV -> String -svFunType ss s = "(" ++ unwords (map svType ss) ++ ") " ++ svType s +svFunType :: [SV] -> SV -> Text +svFunType ss s = "(" <> T.unwords (map svType ss) <> ") " <> svType s -cvtType :: SBVType -> String +cvtType :: SBVType -> Text cvtType (SBVType []) = error "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!" -cvtType (SBVType xs) = "(" ++ unwords (map smtType body) ++ ") " ++ smtType ret +cvtType (SBVType xs) = "(" <> T.unwords (map (T.pack . smtType) body) <> ") " <> T.pack (smtType ret) where (body, ret) = (init xs, last xs) -type TableMap = IM.IntMap String +type TableMap = IM.IntMap Text -- Present an SV, simply show -cvtSV :: SV -> String -cvtSV = show +cvtSV :: SV -> Text +cvtSV = T.pack . show -cvtCV :: RoundingMode -> CV -> String -cvtCV = cvToSMTLib +cvtCV :: RoundingMode -> CV -> Text +cvtCV = T.pack .* cvToSMTLib + where (.*) = (.) . (.) -getTable :: TableMap -> Int -> String +getTable :: TableMap -> Int -> Text getTable m i | Just tn <- i `IM.lookup` m = tn - | True = "table" ++ show i -- constant tables are always named this way + | True = "table" <> T.pack (show i) -cvtExp :: SMTConfig -> ProgInfo -> SolverCapabilities -> RoundingMode -> TableMap -> SBVExpr -> String +cvtExp :: SMTConfig -> ProgInfo -> SolverCapabilities -> RoundingMode -> TableMap -> SBVExpr -> Text cvtExp cfg curProgInfo caps rm tableMap expr@(SBVApp _ arguments) = sh expr where hasPB = supportsPseudoBooleans caps hasDistinct = supportsDistinct caps @@ -682,7 +692,7 @@ fpOp = any (\a -> isDouble a || isFloat a || isFP a) arguments boolOp = all isBoolean arguments charOp = any isChar arguments - stringOp = any isString arguments + stringOp = any isString arguments listOp = any isList arguments bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr @@ -691,7 +701,7 @@ ensureBVOrBool = bvOp || boolOp || bad ensureBV = bvOp || bad - addRM s = s ++ " " ++ smtRoundingMode rm + addRM s = s <> " " <> T.pack (smtRoundingMode rm) isZ3 = case name (solver cfg) of Z3 -> True @@ -705,11 +715,11 @@ hd w [] = error $ "Impossible: " ++ w ++ ": Received empty list of args!" -- lift a binary op - lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" - lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs) + lift2 o _ [x, y] = "(" <> o <> " " <> x <> " " <> y <> ")" + lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs) -- lift an arbitrary arity operator - liftN o _ xs = "(" ++ o ++ " " ++ unwords xs ++ ")" + liftN o _ xs = "(" <> o <> " " <> T.unwords xs <> ")" -- lift a binary operation with rounding-mode added; used for floating-point arithmetic lift2WM o fo | fpOp = lift2 (addRM fo) @@ -724,9 +734,9 @@ | bvOp = fArg | True = mkAbs fArg "<" "-" where fArg = hd "liftAbs" args - mkAbs x cmp neg = "(ite " ++ ltz ++ " " ++ nx ++ " " ++ x ++ ")" - where ltz = "(" ++ cmp ++ " " ++ x ++ " " ++ z ++ ")" - nx = "(" ++ neg ++ " " ++ x ++ ")" + mkAbs x cmp neg = "(ite " <> ltz <> " " <> nx <> " " <> x <> ")" + where ltz = "(" <> cmp <> " " <> x <> " " <> z <> ")" + nx = "(" <> neg <> " " <> x <> ")" z = cvtCV rm (mkConstCV (kindOf (hd "liftAbs.arguments" arguments)) (0::Integer)) lift2B bOp vOp @@ -749,11 +759,11 @@ notEqual sgn sbvs | fpOp || not hasDistinct = liftP sbvs | True = liftN "distinct" sgn sbvs - where liftP xs@[_, _] = "(not " ++ equal sgn xs ++ ")" - liftP args = "(and " ++ unwords (walk args) ++ ")" + where liftP xs@[_, _] = "(not " <> equal sgn xs <> ")" + liftP args = "(and " <> T.unwords (walk args) <> ")" walk [] = [] - walk (e:es) = map (\e' -> liftP [e, e']) es ++ walk es + walk (e:es) = map (\e' -> liftP [e, e']) es <> walk es lift2S oU oS sgn = lift2 (if sgn then oS else oU) sgn liftNS oU oS sgn = liftN (if sgn then oS else oU) sgn @@ -768,7 +778,7 @@ | stringOrChar (kindOf (hd "stringCmp" arguments)) = let (a1, a2) | swap = (b, a) | True = (a, b) - in "(" ++ o ++ " " ++ a1 ++ " " ++ a2 ++ ")" + in "(" <> o <> " " <> a1 <> " " <> a2 <> ")" stringCmp _ o sbvs = error $ "SBV.SMT.SMTLib2.sh.stringCmp: Unexpected arguments: " ++ show (o, sbvs) -- NB. Likewise for sequences @@ -776,16 +786,16 @@ | KList{} <- kindOf (hd "seqCmp" arguments) = let (a1, a2) | swap = (b, a) | True = (a, b) - in "(" ++ o ++ " " ++ a1 ++ " " ++ a2 ++ ")" + in "(" <> o <> " " <> a1 <> " " <> a2 <> ")" seqCmp _ o sbvs = error $ "SBV.SMT.SMTLib2.sh.seqCmp: Unexpected arguments: " ++ show (o, sbvs) - lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")" - lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) + lift1 o _ [x] = "(" <> o <> " " <> x <> ")" + lift1 o _ sbvs = error $ "SBV.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) - sh (SBVApp Ite [a, b, c]) = "(ite " ++ cvtSV a ++ " " ++ cvtSV b ++ " " ++ cvtSV c ++ ")" + sh (SBVApp Ite [a, b, c]) = "(ite " <> cvtSV a <> " " <> cvtSV b <> " " <> cvtSV c <> ")" sh (SBVApp (LkUp (t, aKnd, _, l) i e) []) - | needsCheck = "(ite " ++ cond ++ cvtSV e ++ " " ++ lkUp ++ ")" + | needsCheck = "(ite " <> cond <> cvtSV e <> " " <> lkUp <> ")" | True = lkUp where unexpected = error $ "SBV.SMT.SMTLib2.cvtExp: Unexpected: " ++ show aKnd needsCheck = case aKnd of @@ -807,11 +817,11 @@ KTuple _ -> unexpected KArray _ _ -> unexpected - lkUp = "(" ++ getTable tableMap t ++ " " ++ cvtSV i ++ ")" + lkUp = "(" <> getTable tableMap t <> " " <> cvtSV i <> ")" cond - | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") " - | True = gtl ++ " " + | hasSign i = "(or " <> le0 <> " " <> gtl <> ") " + | True = gtl <> " " (less, leq) = case aKnd of KVar{} -> error "SBV.SMT.SMTLib2.cvtExp: unexpected variable index" @@ -833,22 +843,22 @@ KArray k1 k2 -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected array valued index: " ++ show (k1, k2) mkCnst = cvtCV rm . mkConstCV (kindOf i) - le0 = "(" ++ less ++ " " ++ cvtSV i ++ " " ++ mkCnst 0 ++ ")" - gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ cvtSV i ++ ")" + le0 = "(" <> less <> " " <> cvtSV i <> " " <> mkCnst 0 <> ")" + gtl = "(" <> leq <> " " <> mkCnst l <> " " <> cvtSV i <> ")" sh (SBVApp (KindCast f t) [a]) = handleKindCast f t (cvtSV a) - sh (SBVApp (ArrayInit (Left (f, t))) [a]) = "((as const (Array " ++ smtType f ++ " " ++ smtType t ++ ")) " ++ cvtSV a ++ ")" - sh (SBVApp (ArrayInit (Right s)) []) = show s - sh (SBVApp ReadArray [a, i]) = "(select " ++ cvtSV a ++ " " ++ cvtSV i ++ ")" - sh (SBVApp WriteArray [a, i, e]) = "(store " ++ cvtSV a ++ " " ++ cvtSV i ++ " " ++ cvtSV e ++ ")" + sh (SBVApp (ArrayInit (Left (f, t))) [a]) = "((as const (Array " <> T.pack (smtType f) <> " " <> T.pack (smtType t) <> ")) " <> cvtSV a <> ")" + sh (SBVApp (ArrayInit (Right s)) []) = T.pack $ show s + sh (SBVApp ReadArray [a, i]) = "(select " <> cvtSV a <> " " <> cvtSV i <> ")" + sh (SBVApp WriteArray [a, i, e]) = "(store " <> cvtSV a <> " " <> cvtSV i <> " " <> cvtSV e <> ")" - sh (SBVApp (Uninterpreted nm) []) = nm - sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp (Uninterpreted nm) []) = T.pack nm + sh (SBVApp (Uninterpreted nm) args) = "(" <> T.pack nm <> " " <> T.unwords (map cvtSV args) <> ")" sh (SBVApp (ADTOp aop) args) = handleADT caps aop args - sh (SBVApp (QuantifiedBool i) []) = i + sh (SBVApp (QuantifiedBool i) []) = T.pack i sh (SBVApp (QuantifiedBool i) args) = error $ "SBV.SMT.SMTLib2.cvtExp: unexpected arguments to quantified boolean: " ++ show (i, args) sh a@(SBVApp (SpecialRelOp k o) args) @@ -860,16 +870,16 @@ Nothing -> error $ unlines [ "SBV.SMT.SMTLib2.cvtExp: Cannot find " ++ show o ++ " in the special-relations list." , "Known relations: " ++ intercalate ", " (map show specialRels) ] - asrt nm fun = mkRelEq nm (fun, show order) k + asrt nm fun = mkRelEq (T.pack nm) (T.pack fun, T.pack $ show order) k in case o of IsPartialOrder nm -> asrt nm "partial-order" IsLinearOrder nm -> asrt nm "linear-order" IsTreeOrder nm -> asrt nm "tree-order" IsPiecewiseLinearOrder nm -> asrt nm "piecewise-linear-order" - sh (SBVApp (Divides n) [a]) = "((_ divisible " ++ show n ++ ") " ++ cvtSV a ++ ")" + sh (SBVApp (Divides n) [a]) = "((_ divisible " <> T.pack (show n) <> ") " <> cvtSV a <> ")" - sh (SBVApp (Extract i j) [a]) | ensureBV = "((_ extract " ++ show i ++ " " ++ show j ++ ") " ++ cvtSV a ++ ")" + sh (SBVApp (Extract i j) [a]) | ensureBV = "((_ extract " <> T.pack (show i) <> " " <> T.pack (show j) <> ") " <> cvtSV a <> ")" sh (SBVApp (Rol i) [a]) | bvOp = rot "rotate_left" i a @@ -888,11 +898,11 @@ | True = bad sh (SBVApp (ZeroExtend i) [a]) - | bvOp = "((_ zero_extend " ++ show i ++ ") " ++ cvtSV a ++ ")" + | bvOp = "((_ zero_extend " <> T.pack (show i) <> ") " <> cvtSV a <> ")" | True = bad sh (SBVApp (SignExtend i) [a]) - | bvOp = "((_ sign_extend " ++ show i ++ ") " ++ cvtSV a ++ ")" + | bvOp = "((_ sign_extend " <> T.pack (show i) <> ") " <> cvtSV a <> ")" | True = bad sh (SBVApp op args) @@ -910,54 +920,54 @@ sh (SBVApp (Label _) [a]) = cvtSV a -- This won't be reached; but just in case! - sh (SBVApp (IEEEFP (FP_Cast kFrom kTo m)) args) = handleFPCast kFrom kTo (cvtSV m) (unwords (map cvtSV args)) - sh (SBVApp (IEEEFP w ) args) = "(" ++ show w ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp (IEEEFP (FP_Cast kFrom kTo m)) args) = handleFPCast kFrom kTo (cvtSV m) (T.unwords (map cvtSV args)) + sh (SBVApp (IEEEFP w ) args) = "(" <> T.pack (show w) <> " " <> T.unwords (map cvtSV args) <> ")" -- Some non-linear operators are supported by z3/CVC5 specifically, so do the custom translation Otherwise -- we pass them along. - sh (SBVApp (NonLinear NR_Sqrt) [a]) | isZ3 = "(^ " ++ cvtSV a ++ " 0.5)" - | isCVC5 = "(sqrt " ++ cvtSV a ++ ")" + sh (SBVApp (NonLinear NR_Sqrt) [a]) | isZ3 = "(^ " <> cvtSV a <> " 0.5)" + | isCVC5 = "(sqrt " <> cvtSV a <> ")" - sh (SBVApp (NonLinear NR_Pow) [a, b]) | isZ3 || isCVC5 = "(^ " ++ cvtSV a ++ " " ++ cvtSV b ++ ")" + sh (SBVApp (NonLinear NR_Pow) [a, b]) | isZ3 || isCVC5 = "(^ " <> cvtSV a <> " " <> cvtSV b <> ")" - sh (SBVApp (NonLinear w) args) = "(" ++ show w ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp (NonLinear w) args) = "(" <> T.pack (show w) <> " " <> T.unwords (map cvtSV args) <> ")" sh (SBVApp (PseudoBoolean pb) args) | hasPB = handlePB pb args' | True = reducePB pb args' where args' = map cvtSV args - sh (SBVApp (OverflowOp op) args) = "(" ++ show op ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp (OverflowOp op) args) = "(" <> T.pack (show op) <> " " <> T.unwords (map cvtSV args) <> ")" -- Note the unfortunate reversal in StrInRe.. - sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in_re " ++ unwords (map cvtSV args) ++ " " ++ regExpToSMTString r ++ ")" - sh (SBVApp (StrOp op) args) = "(" ++ show op ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in_re " <> T.unwords (map cvtSV args) <> " " <> T.pack (regExpToSMTString r) <> ")" + sh (SBVApp (StrOp op) args) = "(" <> T.pack (show op) <> " " <> T.unwords (map cvtSV args) <> ")" - sh (SBVApp (RegExOp o@RegExEq{}) []) = show o - sh (SBVApp (RegExOp o@RegExNEq{}) []) = show o + sh (SBVApp (RegExOp o@RegExEq{}) []) = T.pack (show o) + sh (SBVApp (RegExOp o@RegExNEq{}) []) = T.pack (show o) -- Sequences. The only interesting thing here is that unit over KChar is a no-op since SMTLib doesn't distinguish -- Strings and Characters, but SBV does. sh (SBVApp (SeqOp (SeqUnit KChar)) [a]) = cvtSV a - sh (SBVApp (SeqOp op) args) = "(" ++ show op ++ " " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp (SeqOp op) args) = "(" <> T.pack (show op) <> " " <> T.unwords (map cvtSV args) <> ")" - sh (SBVApp (SetOp SetEqual) args) = "(= " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp (SetOp SetMember) [e, s]) = "(select " ++ cvtSV s ++ " " ++ cvtSV e ++ ")" - sh (SBVApp (SetOp SetInsert) [e, s]) = "(store " ++ cvtSV s ++ " " ++ cvtSV e ++ " true)" - sh (SBVApp (SetOp SetDelete) [e, s]) = "(store " ++ cvtSV s ++ " " ++ cvtSV e ++ " false)" - sh (SBVApp (SetOp SetIntersect) args) = "(intersection " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp (SetOp SetUnion) args) = "(union " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp (SetOp SetSubset) args) = "(subset " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp (SetOp SetDifference) args) = "(setminus " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp (SetOp SetComplement) args) = "(complement " ++ unwords (map cvtSV args) ++ ")" + sh (SBVApp (SetOp SetEqual) args) = "(= " <> T.unwords (map cvtSV args) <> ")" + sh (SBVApp (SetOp SetMember) [e, s]) = "(select " <> cvtSV s <> " " <> cvtSV e <> ")" + sh (SBVApp (SetOp SetInsert) [e, s]) = "(store " <> cvtSV s <> " " <> cvtSV e <> " true)" + sh (SBVApp (SetOp SetDelete) [e, s]) = "(store " <> cvtSV s <> " " <> cvtSV e <> " false)" + sh (SBVApp (SetOp SetIntersect) args) = "(intersection " <> T.unwords (map cvtSV args) <> ")" + sh (SBVApp (SetOp SetUnion) args) = "(union " <> T.unwords (map cvtSV args) <> ")" + sh (SBVApp (SetOp SetSubset) args) = "(subset " <> T.unwords (map cvtSV args) <> ")" + sh (SBVApp (SetOp SetDifference) args) = "(setminus " <> T.unwords (map cvtSV args) <> ")" + sh (SBVApp (SetOp SetComplement) args) = "(complement " <> T.unwords (map cvtSV args) <> ")" sh (SBVApp (TupleConstructor 0) []) = "mkSBVTuple0" - sh (SBVApp (TupleConstructor n) args) = "((as mkSBVTuple" ++ show n ++ " " ++ smtType (KTuple (map kindOf args)) ++ ") " ++ unwords (map cvtSV args) ++ ")" - sh (SBVApp (TupleAccess i n) [tup]) = "(proj_" ++ show i ++ "_SBVTuple" ++ show n ++ " " ++ cvtSV tup ++ ")" + sh (SBVApp (TupleConstructor n) args) = "((as mkSBVTuple" <> T.pack (show n) <> " " <> T.pack (smtType (KTuple (map kindOf args))) <> ") " <> T.unwords (map cvtSV args) <> ")" + sh (SBVApp (TupleAccess i n) [tup]) = "(proj_" <> T.pack (show i) <> "_SBVTuple" <> T.pack (show n) <> " " <> cvtSV tup <> ")" - sh (SBVApp RationalConstructor [t, b]) = "(SBV.Rational " ++ cvtSV t ++ " " ++ cvtSV b ++ ")" + sh (SBVApp RationalConstructor [t, b]) = "(SBV.Rational " <> cvtSV t <> " " <> cvtSV b <> ")" - sh (SBVApp Implies [a, b]) = "(=> " ++ cvtSV a ++ " " ++ cvtSV b ++ ")" + sh (SBVApp Implies [a, b]) = "(=> " <> cvtSV a <> " " <> cvtSV b <> ")" sh inp@(SBVApp op args) | intOp, Just f <- lookup op smtOpIntTable @@ -1011,9 +1021,9 @@ , (LessEq, blq) , (GreaterEq, blq . swp) ] - where blt [x, y] = "(and (not " ++ x ++ ") " ++ y ++ ")" + where blt [x, y] = "(and (not " <> x <> ") " <> y <> ")" blt xs = error $ "SBV.SMT.SMTLib2.boolComps.blt: Impossible happened, incorrect arity (expected 2): " ++ show xs - blq [x, y] = "(or (not " ++ x ++ ") " ++ y ++ ")" + blq [x, y] = "(or (not " <> x <> ") " <> y <> ")" blq xs = error $ "SBV.SMT.SMTLib2.boolComps.blq: Impossible happened, incorrect arity (expected 2): " ++ show xs swp [x, y] = [y, x] swp xs = error $ "SBV.SMT.SMTLib2.boolComps.swp: Impossible happened, incorrect arity (expected 2): " ++ show xs @@ -1048,8 +1058,8 @@ , (Equal False, lift2Rat "sbv.rat.eq") , (NotEqual, lift2Rat "sbv.rat.notEq") ] - where lift2Rat o [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" - lift2Rat o sbvs = error $ "SBV.SMTLib2.sh.lift2Rat: Unexpected arguments: " ++ show (o, sbvs) + where lift2Rat o [x, y] = "(" <> o <> " " <> x <> " " <> y <> ")" + lift2Rat o sbvs = error $ "SBV.SMTLib2.sh.lift2Rat: Unexpected arguments: " ++ show (o, sbvs) -- equality and comparisons are the only thing that works on uninterpreted sorts and pretty much everything else uninterpretedTable = [ (Equal True, lift2S "=" "=" True) @@ -1077,18 +1087,18 @@ , (GreaterEq, seqCmp True "seq.<=") ] -declareFun :: SV -> SBVType -> Maybe String -> [String] -declareFun = declareName . show +declareFun :: SV -> SBVType -> Maybe Text -> [Text] +declareFun sv = declareName (T.pack $ show sv) -- If we have a char, we have to make sure it's and SMTLib string of length exactly one -- If we have a rational, we have to make sure the denominator is > 0 -- Otherwise, we just declare the name -declareName :: String -> SBVType -> Maybe String -> [String] +declareName :: Text -> SBVType -> Maybe Text -> [Text] declareName s t@(SBVType inputKS) mbCmnt = decl : restrict - where decl = "(declare-fun " ++ s ++ " " ++ cvtType t ++ ")" ++ maybe "" (" ; " ++) mbCmnt + where decl = "(declare-fun " <> s <> " " <> cvtType t <> ")" <> maybe "" (" ; " <>) mbCmnt (args, result) = case inputKS of - [] -> error $ "SBV.declareName: Unexpected empty type for: " ++ show s + [] -> error $ "SBV.declareName: Unexpected empty type for: " ++ T.unpack s _ -> (init inputKS, last inputKS) -- Does the kind KChar and KRational *not* occur in the kind anywhere? @@ -1103,38 +1113,38 @@ 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 ++ ")" + argList = ["a" <> T.pack (show i) | (i, _) <- zip [1::Int ..] args] + argTList = ["(" <> a <> " " <> T.pack (smtType k) <> ")" | (a, k) <- zip argList args] + resultExp = "(" <> s <> " " <> T.unwords argList <> ")" restrict | noCharOrRat = [] - | needsQuant = [ "(assert (forall (" ++ unwords argTList ++ ")" - , " (let ((" ++ resultVar ++ " " ++ resultExp ++ "))" + | needsQuant = [ "(assert (forall (" <> T.unwords argTList <> ")" + , " (let ((" <> resultVar <> " " <> resultExp <> "))" ] - ++ (case constraints of + <> (case constraints of [] -> [ " true"] - [x] -> [ " " ++ x] - (x:xs) -> ( " (and " ++ x) - : [ " " ++ c | c <- xs] - ++ [ " )"]) - ++ [ " )))"] + [x] -> [ " " <> x] + (x:xs) -> ( " (and " <> x) + : [ " " <> c | c <- xs] + <> [ " )"]) + <> [ " )))"] | True = case constraints of [] -> [] - [x] -> ["(assert " ++ x ++ ")"] - (x:xs) -> ( "(assert (and " ++ x) - : [ " " ++ c | c <- xs] - ++ [ " ))"] + [x] -> ["(assert " <> x <> ")"] + (x:xs) -> ( "(assert (and " <> x) + : [ " " <> c | c <- xs] + <> [ " ))"] constraints = walk 0 resultVar cstr result - where cstr KChar nm = ["(= 1 (str.len " ++ nm ++ "))"] - cstr KRational nm = ["(< 0 (sbv.rat.denominator " ++ nm ++ "))"] + where cstr KChar nm = ["(= 1 (str.len " <> nm <> "))"] + cstr KRational nm = ["(< 0 (sbv.rat.denominator " <> nm <> "))"] cstr _ _ = [] mkAnd [] _context = [] mkAnd [c] context = context c - mkAnd cs context = context $ "(and " ++ unwords cs ++ ")" + mkAnd cs context = context $ "(and " <> T.unwords cs <> ")" - walk :: Int -> String -> (Kind -> String -> [String]) -> Kind -> [String] + walk :: Int -> Text -> (Kind -> Text -> [Text]) -> Kind -> [Text] walk _d nm f k@KVar {} = f k nm walk _d nm f k@KBool {} = f k nm walk _d nm f k@KBounded {} = f k nm @@ -1149,25 +1159,25 @@ walk _d nm f k@KString {} = f k nm walk d nm f (KList k) | charRatFree k = [] - | True = let fnm = "seq" ++ show d - cstrs = walk (d+1) ("(seq.nth " ++ nm ++ " " ++ fnm ++ ")") f k - in mkAnd cstrs $ \hole -> ["(forall ((" ++ fnm ++ " " ++ smtType KUnbounded ++ ")) (=> (and (>= " ++ fnm ++ " 0) (< " ++ fnm ++ " (seq.len " ++ nm ++ "))) " ++ hole ++ "))"] + | True = let fnm = "seq" <> T.pack (show d) + cstrs = walk (d+1) ("(seq.nth " <> nm <> " " <> fnm <> ")") f k + in mkAnd cstrs $ \hole -> ["(forall ((" <> fnm <> " " <> T.pack (smtType KUnbounded) <> ")) (=> (and (>= " <> fnm <> " 0) (< " <> fnm <> " (seq.len " <> nm <> "))) " <> hole <> "))"] walk d nm f (KSet k) | charRatFree k = [] - | True = let fnm = "set" ++ show d - cstrs = walk (d+1) nm (\sk snm -> ["(=> (select " ++ snm ++ " " ++ fnm ++ ") " ++ c ++ ")" | c <- f sk fnm]) k - in mkAnd cstrs $ \hole -> ["(forall ((" ++ fnm ++ " " ++ smtType k ++ ")) " ++ hole ++ ")"] - walk d nm f (KTuple ks) = let tt = "SBVTuple" ++ show (length ks) - project i = "(proj_" ++ show i ++ "_" ++ tt ++ " " ++ nm ++ ")" + | True = let fnm = "set" <> T.pack (show d) + cstrs = walk (d+1) nm (\sk snm -> ["(=> (select " <> snm <> " " <> fnm <> ") " <> c <> ")" | c <- f sk fnm]) k + in mkAnd cstrs $ \hole -> ["(forall ((" <> fnm <> " " <> T.pack (smtType k) <> ")) " <> hole <> ")"] + walk d nm f (KTuple ks) = let tt = "SBVTuple" <> T.pack (show (length ks)) + project i = "(proj_" <> T.pack (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 (KArray k1 k2) | all charRatFree [k1, k2] = [] - | True = let fnm = "array" ++ show d - cstrs = walk (d+1) ("(select " ++ nm ++ " " ++ fnm ++ ")") f k2 - in mkAnd cstrs $ \hole -> ["(forall ((" ++ fnm ++ " " ++ smtType k1 ++ ")) " ++ hole ++ ")"] + | True = let fnm = "array" <> T.pack (show d) + cstrs = walk (d+1) ("(select " <> nm <> " " <> fnm <> ")") f k2 + in mkAnd cstrs $ \hole -> ["(forall ((" <> fnm <> " " <> T.pack (smtType k1) <> ")) " <> hole <> ")"] walk d nm f (KADT ty dict pureFS) = let fs = [(c, map (substituteADTVars ty dict) ks) | (c, ks) <- pureFS] - nmks = [("(get" ++ c ++ "_" ++ show i ++ " " ++ nm ++ ")", k) | (c, ks) <- fs, (i, k) <- zip [(1::Int)..] ks] + nmks = [("(get" <> T.pack c <> "_" <> T.pack (show i) <> " " <> nm <> ")", k) | (c, ks) <- fs, (i, k) <- zip [(1::Int)..] ks] in concatMap (\(n, k) -> walk (d+1) n f k) nmks ----------------------------------------------------------------------------------------------- @@ -1194,13 +1204,13 @@ -- (fp.to_real (_ FloatingPoint eb sb) Real) ----------------------------------------------------------------------------------------------- -handleFPCast :: Kind -> Kind -> String -> String -> String +handleFPCast :: Kind -> Kind -> Text -> Text -> Text handleFPCast kFromIn kToIn rm input | kFrom == kTo = input | True - = "(" ++ cast kFrom kTo input ++ ")" - where addRM a s = s ++ " " ++ rm ++ " " ++ a + = "(" <> cast kFrom kTo input <> ")" + where addRM a s = s <> " " <> rm <> " " <> a kFrom = simplify kFromIn kTo = simplify kToIn @@ -1209,51 +1219,51 @@ simplify KDouble = KFP 11 53 simplify k = k - size (eb, sb) = show eb ++ " " ++ show sb + size (eb, sb) = T.pack (show eb) <> " " <> T.pack (show sb) -- To go and back from Ints, we detour through reals - cast KUnbounded (KFP eb sb) a = "(_ to_fp " ++ size (eb, sb) ++ ") " ++ rm ++ " (to_real " ++ a ++ ")" - cast KFP{} KUnbounded a = "to_int (fp.to_real " ++ a ++ ")" + cast KUnbounded (KFP eb sb) a = "(_ to_fp " <> size (eb, sb) <> ") " <> rm <> " (to_real " <> a <> ")" + cast KFP{} KUnbounded a = "to_int (fp.to_real " <> a <> ")" -- To floats - cast (KBounded False _) (KFP eb sb) a = addRM a $ "(_ to_fp_unsigned " ++ size (eb, sb) ++ ")" - cast (KBounded True _) (KFP eb sb) a = addRM a $ "(_ to_fp " ++ size (eb, sb) ++ ")" - cast KReal (KFP eb sb) a = addRM a $ "(_ to_fp " ++ size (eb, sb) ++ ")" - cast KFP{} (KFP eb sb) a = addRM a $ "(_ to_fp " ++ size (eb, sb) ++ ")" + cast (KBounded False _) (KFP eb sb) a = addRM a $ "(_ to_fp_unsigned " <> size (eb, sb) <> ")" + cast (KBounded True _) (KFP eb sb) a = addRM a $ "(_ to_fp " <> size (eb, sb) <> ")" + cast KReal (KFP eb sb) a = addRM a $ "(_ to_fp " <> size (eb, sb) <> ")" + cast KFP{} (KFP eb sb) a = addRM a $ "(_ to_fp " <> size (eb, sb) <> ")" -- From float/double - cast KFP{} (KBounded False m) a = addRM a $ "(_ fp.to_ubv " ++ show m ++ ")" - cast KFP{} (KBounded True m) a = addRM a $ "(_ fp.to_sbv " ++ show m ++ ")" + cast KFP{} (KBounded False m) a = addRM a $ "(_ fp.to_ubv " <> T.pack (show m) <> ")" + cast KFP{} (KBounded True m) a = addRM a $ "(_ fp.to_sbv " <> T.pack (show m) <> ")" -- To real - cast KFP{} KReal a = "fp.to_real" ++ " " ++ a + cast KFP{} KReal a = "fp.to_real" <> " " <> a -- Nothing else should come up: cast f d _ = error $ "SBV.SMTLib2: Unexpected FPCast from: " ++ show f ++ " to " ++ show d -rot :: String -> Int -> SV -> String -rot o c x = "((_ " ++ o ++ " " ++ show c ++ ") " ++ cvtSV x ++ ")" +rot :: Text -> Int -> SV -> Text +rot o c x = "((_ " <> o <> " " <> T.pack (show c) <> ") " <> cvtSV x <> ")" -shft :: String -> String -> SV -> SV -> String -shft oW oS x c = "(" ++ o ++ " " ++ cvtSV x ++ " " ++ cvtSV c ++ ")" +shft :: Text -> Text -> SV -> SV -> Text +shft oW oS x c = "(" <> o <> " " <> cvtSV x <> " " <> cvtSV c <> ")" where o = if hasSign x then oS else oW -- ADT operations -handleADT :: SolverCapabilities -> ADTOp -> [SV] -> String +handleADT :: SolverCapabilities -> ADTOp -> [SV] -> Text handleADT caps op args = case args of [] -> f - _ -> "(" ++ f ++ " " ++ unwords (map cvtSV args) ++ ")" + _ -> "(" <> f <> " " <> T.unwords (map cvtSV args) <> ")" where f = case op of - ADTConstructor nm k -> ascribe nm k + ADTConstructor nm k -> ascribe (T.pack nm) k ADTTester nm k -> if supportsDirectTesters caps - then nm - else ascribe nm k - ADTAccessor nm _ -> nm + then T.pack nm + else ascribe (T.pack nm) k + ADTAccessor nm _ -> T.pack nm - ascribe nm k = "(as " ++ nm ++ " " ++ smtType k ++ ")" + ascribe nm k = "(as " <> nm <> " " <> T.pack (smtType k) <> ")" -- Various casts -handleKindCast :: Kind -> Kind -> String -> String +handleKindCast :: Kind -> Kind -> Text -> Text handleKindCast kFrom kTo a | kFrom == kTo = a @@ -1261,17 +1271,17 @@ = case kFrom of KBounded s m -> case kTo of KBounded _ n -> fromBV (if s then signExtend else zeroExtend) m n - KUnbounded -> if s then "(sbv_to_int " ++ a ++ ")" - else "(ubv_to_int " ++ a ++ ")" + KUnbounded -> if s then "(sbv_to_int " <> a <> ")" + else "(ubv_to_int " <> a <> ")" _ -> tryFPCast KUnbounded -> case kTo of - KReal -> "(to_real " ++ a ++ ")" - KBounded _ n -> "((_ int_to_bv " ++ show n ++ ") " ++ a ++ ")" + KReal -> "(to_real " <> a <> ")" + KBounded _ n -> "((_ int_to_bv " <> T.pack (show n) <> ") " <> a <> ")" _ -> tryFPCast KReal -> case kTo of - KUnbounded -> "(to_int " ++ a ++ ")" + KUnbounded -> "(to_int " <> a <> ")" _ -> tryFPCast _ -> tryFPCast @@ -1280,7 +1290,7 @@ -- Otherwise complain tryFPCast | any (\k -> isFloat k || isDouble k) [kFrom, kTo] - = handleFPCast kFrom kTo (smtRoundingMode RoundNearestTiesToEven) a + = handleFPCast kFrom kTo (T.pack $ smtRoundingMode RoundNearestTiesToEven) a | True = error $ "SBV.SMTLib2: Unexpected cast from: " ++ show kFrom ++ " to " ++ show kTo @@ -1289,36 +1299,36 @@ | m == n = a | True = extract (n - 1) - signExtend i = "((_ sign_extend " ++ show i ++ ") " ++ a ++ ")" - zeroExtend i = "((_ zero_extend " ++ show i ++ ") " ++ a ++ ")" - extract i = "((_ extract " ++ show i ++ " 0) " ++ a ++ ")" + signExtend i = "((_ sign_extend " <> T.pack (show i) <> ") " <> a <> ")" + zeroExtend i = "((_ zero_extend " <> T.pack (show i) <> ") " <> a <> ")" + extract i = "((_ extract " <> T.pack (show i) <> " 0) " <> a <> ")" -- Translation of pseudo-booleans, in case the solver supports them -handlePB :: PBOp -> [String] -> String -handlePB (PB_AtMost k) args = "((_ at-most " ++ show k ++ ") " ++ unwords args ++ ")" -handlePB (PB_AtLeast k) args = "((_ at-least " ++ show k ++ ") " ++ unwords args ++ ")" -handlePB (PB_Exactly k) args = "((_ pbeq " ++ unwords (map show (k : replicate (length args) 1)) ++ ") " ++ unwords args ++ ")" -handlePB (PB_Eq cs k) args = "((_ pbeq " ++ unwords (map show (k : cs)) ++ ") " ++ unwords args ++ ")" -handlePB (PB_Le cs k) args = "((_ pble " ++ unwords (map show (k : cs)) ++ ") " ++ unwords args ++ ")" -handlePB (PB_Ge cs k) args = "((_ pbge " ++ unwords (map show (k : cs)) ++ ") " ++ unwords args ++ ")" +handlePB :: PBOp -> [Text] -> Text +handlePB (PB_AtMost k) args = "((_ at-most " <> T.pack (show k) <> ") " <> T.unwords args <> ")" +handlePB (PB_AtLeast k) args = "((_ at-least " <> T.pack (show k) <> ") " <> T.unwords args <> ")" +handlePB (PB_Exactly k) args = "((_ pbeq " <> T.unwords (map (T.pack . show) (k : replicate (length args) 1)) <> ") " <> T.unwords args <> ")" +handlePB (PB_Eq cs k) args = "((_ pbeq " <> T.unwords (map (T.pack . show) (k : cs)) <> ") " <> T.unwords args <> ")" +handlePB (PB_Le cs k) args = "((_ pble " <> T.unwords (map (T.pack . show) (k : cs)) <> ") " <> T.unwords args <> ")" +handlePB (PB_Ge cs k) args = "((_ pbge " <> T.unwords (map (T.pack . show) (k : cs)) <> ") " <> T.unwords args <> ")" -- Translation of pseudo-booleans, in case the solver does *not* support them -reducePB :: PBOp -> [String] -> String +reducePB :: PBOp -> [Text] -> Text reducePB op args = case op of - PB_AtMost k -> "(<= " ++ addIf (repeat 1) ++ " " ++ show k ++ ")" - PB_AtLeast k -> "(>= " ++ addIf (repeat 1) ++ " " ++ show k ++ ")" - PB_Exactly k -> "(= " ++ addIf (repeat 1) ++ " " ++ show k ++ ")" - PB_Le cs k -> "(<= " ++ addIf cs ++ " " ++ show k ++ ")" - PB_Ge cs k -> "(>= " ++ addIf cs ++ " " ++ show k ++ ")" - PB_Eq cs k -> "(= " ++ addIf cs ++ " " ++ show k ++ ")" + PB_AtMost k -> "(<= " <> addIf (repeat 1) <> " " <> T.pack (show k) <> ")" + PB_AtLeast k -> "(>= " <> addIf (repeat 1) <> " " <> T.pack (show k) <> ")" + PB_Exactly k -> "(= " <> addIf (repeat 1) <> " " <> T.pack (show k) <> ")" + PB_Le cs k -> "(<= " <> addIf cs <> " " <> T.pack (show k) <> ")" + PB_Ge cs k -> "(>= " <> addIf cs <> " " <> T.pack (show k) <> ")" + PB_Eq cs k -> "(= " <> addIf cs <> " " <> T.pack (show k) <> ")" - where addIf :: [Int] -> String - addIf cs = "(+ " ++ unwords ["(ite " ++ a ++ " " ++ show c ++ " 0)" | (a, c) <- zip args cs] ++ ")" + where addIf :: [Int] -> Text + addIf cs = "(+ " <> T.unwords ["(ite " <> a <> " " <> T.pack (show c) <> " 0)" | (a, c) <- zip args cs] <> ")" -- | Translate an option setting to SMTLib. Note the SetLogic/SetInfo discrepancy. -setSMTOption :: SMTConfig -> SMTOption -> String +setSMTOption :: SMTConfig -> SMTOption -> Text setSMTOption cfg = set - where set (DiagnosticOutputChannel f) = opt [":diagnostic-output-channel", show f] + where set (DiagnosticOutputChannel f) = opt [":diagnostic-output-channel", T.pack $ show f] set (ProduceAssertions b) = opt [":produce-assertions", smtBool b] set (ProduceAssignments b) = opt [":produce-assignments", smtBool b] set (ProduceProofs b) = opt [":produce-proofs", smtBool b] @@ -1326,29 +1336,29 @@ set (ProduceUnsatAssumptions b) = opt [":produce-unsat-assumptions", smtBool b] set (ProduceUnsatCores b) = opt [":produce-unsat-cores", smtBool b] set (ProduceAbducts b) = opt [":produce-abducts", smtBool b] - set (RandomSeed i) = opt [":random-seed", show i] - set (ReproducibleResourceLimit i) = opt [":reproducible-resource-limit", show i] - set (SMTVerbosity i) = opt [":verbosity", show i] - set (OptionKeyword k as) = opt (k : as) + set (RandomSeed i) = opt [":random-seed", T.pack $ show i] + set (ReproducibleResourceLimit i) = opt [":reproducible-resource-limit", T.pack $ show i] + set (SMTVerbosity i) = opt [":verbosity", T.pack $ show i] + set (OptionKeyword k as) = opt (T.pack k : map T.pack as) set (SetLogic l) = logic l - set (SetInfo k as) = info (k : as) + set (SetInfo k as) = info (T.pack k : map T.pack as) set (SetTimeOut i) = opt $ timeOut i - opt xs = "(set-option " ++ unwords xs ++ ")" - info xs = "(set-info " ++ unwords xs ++ ")" + opt xs = "(set-option " <> T.unwords xs <> ")" + info xs = "(set-info " <> T.unwords xs <> ")" logic Logic_NONE = "; NB. not setting the logic per user request of Logic_NONE" - logic l = "(set-logic " ++ show l ++ ")" + logic l = "(set-logic " <> T.pack (show l) <> ")" -- timeout is not standard. We distinguish between CVC/Z3. All else follows z3 -- The value is in milliseconds, which is how z3/CVC interpret it timeOut i = case name (solver cfg) of - CVC4 -> [":tlimit-per", show i] - CVC5 -> [":tlimit-per", show i] - _ -> [":timeout", show i] + CVC4 -> [":tlimit-per", T.pack $ show i] + CVC5 -> [":tlimit-per", T.pack $ show i] + _ -> [":timeout", T.pack $ show i] -- SMTLib's True/False is spelled differently than Haskell's. - smtBool :: Bool -> String + smtBool :: Bool -> Text smtBool True = "true" smtBool False = "false" 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 @@ -9,7 +9,8 @@ -- A few internally used types/routines ----------------------------------------------------------------------------- -{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -53,6 +54,9 @@ import qualified Data.Set as Set (Set) import qualified Data.Sequence as S (Seq) +import qualified Data.Text as T +import Data.Text (Text) + import System.Directory (findExecutable) import System.Exit (ExitCode(..)) @@ -86,9 +90,9 @@ -> a -- | Create an annotated term -addAnnotations :: [(String, String)] -> String -> String +addAnnotations :: [(String, String)] -> Text -> Text addAnnotations [] x = x -addAnnotations atts x = "(! " ++ x ++ " " ++ unwords (map mkAttr atts) ++ ")" +addAnnotations atts x = "(! " <> x <> " " <> T.unwords (map (T.pack . mkAttr) atts) <> ")" where mkAttr (a, v) = a ++ " |" ++ concatMap sanitize v ++ "|" sanitize '|' = "_bar_" sanitize '\\' = "_backslash_" diff --git a/Data/SBV/TP/Kernel.hs b/Data/SBV/TP/Kernel.hs --- a/Data/SBV/TP/Kernel.hs +++ b/Data/SBV/TP/Kernel.hs @@ -13,6 +13,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -50,7 +51,7 @@ import Type.Reflection (typeRep) -import qualified Data.SBV.List as SL (nil, (.:)) +import qualified Data.SBV.List as SL ((.:)) -- | A proposition is something SBV is capable of proving/disproving in TP. type Proposition a = ( QNot a @@ -122,14 +123,14 @@ instance SymVal x => HasInductionSchema (Forall nm [x] -> SBool) where inductionSchema p = proofOf $ internalAxiom ("induct" ++ show (typeRep @[x])) ax where pf = p . Forall - ax = sAnd [pf SL.nil, quantifiedBool (\(Forall x) (Forall xs) -> pf xs .=> pf (x SL..: xs))] + ax = sAnd [pf [], quantifiedBool (\(Forall x) (Forall xs) -> pf xs .=> pf (x SL..: xs))] .=> quantifiedBool (\(Forall xs) -> pf xs) -- | Induction schema for lists with one extra argument instance (SymVal x, SymVal at) => HasInductionSchema (Forall nm [x] -> Forall an at -> SBool) where inductionSchema p = proofOf $ internalAxiom ("induct" ++ show (typeRep @[x]) ++ "1") ax where pf xs a = p (Forall xs) (Forall a) - ax = sAnd [ quantifiedBool (\ (Forall a) -> pf SL.nil a) + ax = sAnd [ quantifiedBool (\ (Forall a) -> pf [] a) , quantifiedBool (\(Forall x) (Forall xs) (Forall a) -> pf xs a .=> pf (x SL..: xs) a)] .=> quantifiedBool (\(Forall xs) (Forall a) -> pf xs a) @@ -137,7 +138,7 @@ instance (SymVal x, SymVal at, SymVal bt) => HasInductionSchema (Forall nm [x] -> Forall an at -> Forall bn bt -> SBool) where inductionSchema p = proofOf $ internalAxiom ("induct" ++ show (typeRep @[x]) ++ "2") ax where pf xs a b = p (Forall xs) (Forall a) (Forall b) - ax = sAnd [ quantifiedBool (\ (Forall a) (Forall b) -> pf SL.nil a b) + ax = sAnd [ quantifiedBool (\ (Forall a) (Forall b) -> pf [] a b) , quantifiedBool (\(Forall x) (Forall xs) (Forall a) (Forall b) -> pf xs a b .=> pf (x SL..: xs) a b)] .=> quantifiedBool (\(Forall xs) (Forall a) (Forall b) -> pf xs a b) @@ -145,7 +146,7 @@ instance (SymVal x, SymVal at, SymVal bt, SymVal ct) => HasInductionSchema (Forall nm [x] -> Forall an at -> Forall bn bt -> Forall cn ct -> SBool) where inductionSchema p = proofOf $ internalAxiom ("induct" ++ show (typeRep @[x]) ++ "3") ax where pf xs a b c = p (Forall xs) (Forall a) (Forall b) (Forall c) - ax = sAnd [ quantifiedBool (\ (Forall a) (Forall b) (Forall c) -> pf SL.nil a b c) + ax = sAnd [ quantifiedBool (\ (Forall a) (Forall b) (Forall c) -> pf [] a b c) , quantifiedBool (\(Forall x) (Forall xs) (Forall a) (Forall b) (Forall c) -> pf xs a b c .=> pf (x SL..: xs) a b c)] .=> quantifiedBool (\(Forall xs) (Forall a) (Forall b) (Forall c) -> pf xs a b c) @@ -153,7 +154,7 @@ instance (SymVal x, SymVal at, SymVal bt, SymVal ct, SymVal dt) => HasInductionSchema (Forall nm [x] -> Forall an at -> Forall bn bt -> Forall cn ct -> Forall dn dt -> SBool) where inductionSchema p = proofOf $ internalAxiom ("induct" ++ show (typeRep @[x]) ++ "4") ax where pf xs a b c d = p (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) - ax = sAnd [ quantifiedBool (\ (Forall a) (Forall b) (Forall c) (Forall d) -> pf SL.nil a b c d) + ax = sAnd [ quantifiedBool (\ (Forall a) (Forall b) (Forall c) (Forall d) -> pf [] a b c d) , quantifiedBool (\(Forall x) (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) -> pf xs a b c d .=> pf (x SL..: xs) a b c d)] .=> quantifiedBool (\(Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) -> pf xs a b c d) @@ -161,7 +162,7 @@ instance (SymVal x, SymVal at, SymVal bt, SymVal ct, SymVal dt, SymVal et) => HasInductionSchema (Forall nm [x] -> Forall an at -> Forall bn bt -> Forall cn ct -> Forall dn dt -> Forall en et -> SBool) where inductionSchema p = proofOf $ internalAxiom ("induct" ++ show (typeRep @[x]) ++ "5") ax where pf xs a b c d e = p (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) - ax = sAnd [ quantifiedBool (\ (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) -> pf SL.nil a b c d e) + ax = sAnd [ quantifiedBool (\ (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) -> pf [] a b c d e) , quantifiedBool (\(Forall x) (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) -> pf xs a b c d e .=> pf (x SL..: xs) a b c d e)] .=> quantifiedBool (\(Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) -> pf xs a b c d e) diff --git a/Data/SBV/TP/TP.hs b/Data/SBV/TP/TP.hs --- a/Data/SBV/TP/TP.hs +++ b/Data/SBV/TP/TP.hs @@ -12,6 +12,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} @@ -798,7 +799,7 @@ inductionStrategy result steps = do (x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs) - let bc = result (Forall SL.nil) + let bc = result (Forall []) ih = internalAxiom "IH" (result (Forall xs)) mkIndStrategy Nothing @@ -816,7 +817,7 @@ (x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs) (a, na) <- mkVar (Proxy @na) - let bc = result (Forall SL.nil) (Forall a) + let bc = result (Forall []) (Forall a) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) -> result (Forall xs) (Forall a')) mkIndStrategy Nothing @@ -835,7 +836,7 @@ (a, na) <- mkVar (Proxy @na) (b, nb) <- mkVar (Proxy @nb) - let bc = result (Forall SL.nil) (Forall a) (Forall b) + let bc = result (Forall []) (Forall a) (Forall b) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> result (Forall xs) (Forall a') (Forall b')) mkIndStrategy Nothing @@ -855,7 +856,7 @@ (b, nb) <- mkVar (Proxy @nb) (c, nc) <- mkVar (Proxy @nc) - let bc = result (Forall SL.nil) (Forall a) (Forall b) (Forall c) + let bc = result (Forall []) (Forall a) (Forall b) (Forall c) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> result (Forall xs) (Forall a') (Forall b') (Forall c')) mkIndStrategy Nothing @@ -876,7 +877,7 @@ (c, nc) <- mkVar (Proxy @nc) (d, nd) <- mkVar (Proxy @nd) - let bc = result (Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) + let bc = result (Forall []) (Forall a) (Forall b) (Forall c) (Forall d) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> result (Forall xs) (Forall a') (Forall b') (Forall c') (Forall d')) mkIndStrategy Nothing @@ -898,7 +899,7 @@ (d, nd) <- mkVar (Proxy @nd) (e, ne) <- mkVar (Proxy @ne) - let bc = result (Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) + let bc = result (Forall []) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> result (Forall xs) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e')) mkIndStrategy Nothing @@ -916,7 +917,7 @@ (x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs) (y, ys, ny, nys, nyys) <- mkLVar (Proxy @nys) - let bc = result (Forall SL.nil, Forall SL.nil) .&& result (Forall SL.nil, Forall (y SL..: ys)) .&& result (Forall (x SL..: xs), Forall SL.nil) + let bc = result (Forall [], Forall []) .&& result (Forall [], Forall (y SL..: ys)) .&& result (Forall (x SL..: xs), Forall []) ih = internalAxiom "IH" (result (Forall xs, Forall ys)) mkIndStrategy Nothing @@ -935,7 +936,7 @@ (y, ys, ny, nys, nyys) <- mkLVar (Proxy @nys) (a, na) <- mkVar (Proxy @na) - let bc = result (Forall SL.nil, Forall SL.nil) (Forall a) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) + let bc = result (Forall [], Forall []) (Forall a) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) .&& result (Forall (x SL..: xs), Forall []) (Forall a) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) -> result (Forall xs, Forall ys) (Forall a')) mkIndStrategy Nothing @@ -955,7 +956,7 @@ (a, na) <- mkVar (Proxy @na) (b, nb) <- mkVar (Proxy @nb) - let bc = result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) + let bc = result (Forall [], Forall []) (Forall a) (Forall b) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) (Forall b) .&& result (Forall (x SL..: xs), Forall []) (Forall a) (Forall b) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> result (Forall xs, Forall ys) (Forall a') (Forall b')) mkIndStrategy Nothing @@ -976,7 +977,7 @@ (b, nb) <- mkVar (Proxy @nb) (c, nc) <- mkVar (Proxy @nc) - let bc = result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) + let bc = result (Forall [], Forall []) (Forall a) (Forall b) (Forall c) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) .&& result (Forall (x SL..: xs), Forall []) (Forall a) (Forall b) (Forall c) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c')) mkIndStrategy Nothing @@ -998,7 +999,7 @@ (c, nc) <- mkVar (Proxy @nc) (d, nd) <- mkVar (Proxy @nd) - let bc = result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) + let bc = result (Forall [], Forall []) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall (x SL..: xs), Forall []) (Forall a) (Forall b) (Forall c) (Forall d) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c') (Forall d')) mkIndStrategy Nothing @@ -1021,7 +1022,7 @@ (d, nd) <- mkVar (Proxy @nd) (e, ne) <- mkVar (Proxy @ne) - let bc = result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) + let bc = result (Forall [], Forall []) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall (x SL..: xs), Forall []) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e')) mkIndStrategy Nothing 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 @@ -23,6 +23,7 @@ import Data.Function (on) import Data.List (intercalate, groupBy) import Data.Maybe (fromMaybe) +import qualified Data.Text as T import Data.SBV.Core.AlgReals import Data.SBV.Core.Data @@ -146,8 +147,8 @@ s cv = case kindOf cv of KVar{} -> error $ "SBV.renderTest: Unexpected: " ++ show (kindOf cv) KBool -> take 5 (show (cvToBool cv) ++ repeat ' ') - KBounded sgn sz -> let CInteger w = cvVal cv in shex False True (sgn, sz) w - KUnbounded -> let CInteger w = cvVal cv in shexI False True w + KBounded sgn sz -> let CInteger w = cvVal cv in T.unpack $ shex False True (sgn, sz) w + KUnbounded -> let CInteger w = cvVal cv in T.unpack $ shexI False True w KFloat -> let CFloat w = cvVal cv in showHFloat w KDouble -> let CDouble w = cvVal cv in showHDouble w KRational -> error "SBV.renderTest: Unsupported rational number" @@ -261,8 +262,8 @@ v cv = case kindOf cv of KVar{} -> error $ "SBV.renderTest: Unexpected: " ++ show (kindOf cv) KBool -> if cvToBool cv then "true " else "false" - KBounded sgn sz -> let CInteger w = cvVal cv in chex False True (sgn, sz) w - KUnbounded -> let CInteger w = cvVal cv in shexI False True w + KBounded sgn sz -> let CInteger w = cvVal cv in T.unpack $ chex False True (sgn, sz) w + KUnbounded -> let CInteger w = cvVal cv in T.unpack $ shexI False True w KFloat -> let CFloat w = cvVal cv in showCFloat w KDouble -> let CDouble w = cvVal cv in showCDouble w KRational -> error "SBV.renderTest: Unsupported rational number" diff --git a/Data/SBV/Tools/Overflow.hs b/Data/SBV/Tools/Overflow.hs --- a/Data/SBV/Tools/Overflow.hs +++ b/Data/SBV/Tools/Overflow.hs @@ -23,7 +23,6 @@ {-# OPTIONS_GHC -Wall -Werror #-} module Data.SBV.Tools.Overflow ( - -- * Arithmetic overflows ArithOverflow(..), CheckedArithmetic(..) @@ -31,8 +30,7 @@ , signedMulOverflow -- * Cast overflows - , sFromIntegralO, sFromIntegralChecked - + , sFromIntegralO, sFromIntegralChecked ) where import Data.SBV.Core.Data @@ -100,11 +98,11 @@ instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SInt n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} instance ArithOverflow SVal where - bvAddO = signPick2 (svMkOverflow2 (PlusOv False)) (svMkOverflow2 (PlusOv True)) - bvSubO = signPick2 (svMkOverflow2 (SubOv False)) (svMkOverflow2 (SubOv True)) - bvMulO = signPick2 (svMkOverflow2 (MulOv False)) (svMkOverflow2 (MulOv True)) - bvDivO = signPick2 (const (const svFalse)) (svMkOverflow2 DivOv) -- unsigned division doesn't overflow - bvNegO = signPick1 (const svFalse) (svMkOverflow1 NegOv) -- unsigned unary negation doesn't overflow + bvAddO = signPick2 (svMkOverflow2 (PlusOv False)) (svMkOverflow2 (PlusOv True)) + bvSubO = signPick2 (svMkOverflow2 (SubOv False)) (svMkOverflow2 (SubOv True)) + bvMulO = signPick2 (svMkOverflow2 (MulOv False)) (svMkOverflow2 (MulOv True)) + bvDivO = signPick2 (const (const svFalse)) (svMkOverflow2 DivOv) -- unsigned division doesn't overflow + bvNegO = signPick1 (const svFalse) (svMkOverflow1 NegOv) -- unsigned unary negation doesn't overflow -- | A class of checked-arithmetic operations. These follow the usual arithmetic, -- except make calls to 'Data.SBV.sAssert' to ensure no overflow/underflow can occur. 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 @@ -28,6 +28,8 @@ import Data.Maybe (fromJust, fromMaybe, listToMaybe) import Data.Ratio (numerator, denominator) import Data.Word (Word8, Word16, Word32, Word64) +import Data.Text (Text) +import qualified Data.Text as T import qualified Data.Set as Set @@ -46,34 +48,34 @@ -- | PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers. class PrettyNum a where -- | Show a number in hexadecimal, starting with @0x@ and type. - hexS :: a -> String + hexS :: a -> Text -- | Show a number in binary, starting with @0b@ and type. - binS :: a -> String + binS :: a -> Text -- | Show a number in hexadecimal, starting with @0x@ but no type. - hexP :: a -> String + hexP :: a -> Text -- | Show a number in binary, starting with @0b@ but no type. - binP :: a -> String + binP :: a -> Text -- | Show a number in hex, without prefix, or types. - hex :: a -> String + hex :: a -> Text -- | Show a number in bin, without prefix, or types. - bin :: a -> String + bin :: a -> Text -- Why not default methods? Because defaults need "Integral a" but Bool is not.. instance PrettyNum Bool where - hexS = show - binS = show - hexP = show - binP = show - hex = show - bin = show + hexS = T.pack . show + binS = T.pack . show + hexP = T.pack . show + binP = T.pack . show + hex = T.pack . show + bin = T.pack . show instance PrettyNum String where - hexS = show - binS = show - hexP = show - binP = show - hex = show - bin = show + hexS = T.pack . show + binS = T.pack . show + hexP = T.pack . show + binP = T.pack . show + hex = T.pack . show + bin = T.pack . show instance PrettyNum Word8 where hexS = shex True True (False, 8) @@ -165,106 +167,106 @@ hex = shexI False False bin = sbinI False False -shBKind :: HasKind a => a -> String -shBKind a = " :: " ++ showBaseKind (kindOf a) +shBKind :: HasKind a => a -> Text +shBKind a = T.pack " :: " <> showBaseKind (kindOf a) instance PrettyNum CV where - hexS cv | isADT cv = shows cv $ shBKind cv - | isBoolean cv = hexS (cvToBool cv) ++ shBKind cv - | isFloat cv = let CFloat f = cvVal cv in N.showHFloat f $ shBKind cv - | isDouble cv = let CDouble d = cvVal cv in N.showHFloat d $ shBKind cv - | isFP cv = let CFP f = cvVal cv in bfToString 16 True True f ++ shBKind cv - | isReal cv = let CAlgReal r = cvVal cv in show r ++ shBKind cv - | isString cv = let CString s = cvVal cv in show s ++ shBKind cv + hexS cv | isADT cv = T.pack (show cv) <> shBKind cv + | isBoolean cv = hexS (cvToBool cv) <> shBKind cv + | isFloat cv = let CFloat f = cvVal cv in T.pack (N.showHFloat f "") <> shBKind cv + | isDouble cv = let CDouble d = cvVal cv in T.pack (N.showHFloat d "") <> shBKind cv + | isFP cv = let CFP f = cvVal cv in T.pack (bfToString 16 True True f) <> shBKind cv + | isReal cv = let CAlgReal r = cvVal cv in T.pack (show r) <> shBKind cv + | isString cv = let CString s = cvVal cv in T.pack (show s) <> shBKind cv | not (isBounded cv) = let CInteger i = cvVal cv in shexI True True i | True = let CInteger i = cvVal cv in shex True True (hasSign cv, intSizeOf cv) i - binS cv | isADT cv = shows cv $ shBKind cv - | isBoolean cv = binS (cvToBool cv) ++ shBKind cv - | isFloat cv = let CFloat f = cvVal cv in showBFloat f $ shBKind cv - | isDouble cv = let CDouble d = cvVal cv in showBFloat d $ shBKind cv - | isFP cv = let CFP f = cvVal cv in bfToString 2 True True f ++ shBKind cv - | isReal cv = let CAlgReal r = cvVal cv in shows r $ shBKind cv - | isString cv = let CString s = cvVal cv in shows s $ shBKind cv + binS cv | isADT cv = T.pack (show cv) <> shBKind cv + | isBoolean cv = binS (cvToBool cv) <> shBKind cv + | isFloat cv = let CFloat f = cvVal cv in T.pack (showBFloat f "") <> shBKind cv + | isDouble cv = let CDouble d = cvVal cv in T.pack (showBFloat d "") <> shBKind cv + | isFP cv = let CFP f = cvVal cv in T.pack (bfToString 2 True True f) <> shBKind cv + | isReal cv = let CAlgReal r = cvVal cv in T.pack (show r) <> shBKind cv + | isString cv = let CString s = cvVal cv in T.pack (show s) <> shBKind cv | not (isBounded cv) = let CInteger i = cvVal cv in sbinI True True i | True = let CInteger i = cvVal cv in sbin True True (hasSign cv, intSizeOf cv) i - hexP cv | isADT cv = show cv + hexP cv | isADT cv = T.pack (show cv) | isBoolean cv = hexS (cvToBool cv) - | isFloat cv = let CFloat f = cvVal cv in show f - | isDouble cv = let CDouble d = cvVal cv in show d - | isFP cv = let CFP f = cvVal cv in bfToString 16 True True f - | isReal cv = let CAlgReal r = cvVal cv in show r - | isString cv = let CString s = cvVal cv in show s + | isFloat cv = let CFloat f = cvVal cv in T.pack (show f) + | isDouble cv = let CDouble d = cvVal cv in T.pack (show d) + | isFP cv = let CFP f = cvVal cv in T.pack (bfToString 16 True True f) + | isReal cv = let CAlgReal r = cvVal cv in T.pack (show r) + | isString cv = let CString s = cvVal cv in T.pack (show s) | not (isBounded cv) = let CInteger i = cvVal cv in shexI False True i | True = let CInteger i = cvVal cv in shex False True (hasSign cv, intSizeOf cv) i - binP cv | isADT cv = show cv + binP cv | isADT cv = T.pack (show cv) | isBoolean cv = binS (cvToBool cv) - | isFloat cv = let CFloat f = cvVal cv in show f - | isDouble cv = let CDouble d = cvVal cv in show d - | isFP cv = let CFP f = cvVal cv in bfToString 2 True True f - | isReal cv = let CAlgReal r = cvVal cv in show r - | isString cv = let CString s = cvVal cv in show s + | isFloat cv = let CFloat f = cvVal cv in T.pack (show f) + | isDouble cv = let CDouble d = cvVal cv in T.pack (show d) + | isFP cv = let CFP f = cvVal cv in T.pack (bfToString 2 True True f) + | isReal cv = let CAlgReal r = cvVal cv in T.pack (show r) + | isString cv = let CString s = cvVal cv in T.pack (show s) | not (isBounded cv) = let CInteger i = cvVal cv in sbinI False True i | True = let CInteger i = cvVal cv in sbin False True (hasSign cv, intSizeOf cv) i - hex cv | isADT cv = show cv + hex cv | isADT cv = T.pack (show cv) | isBoolean cv = hexS (cvToBool cv) - | isFloat cv = let CFloat f = cvVal cv in show f - | isDouble cv = let CDouble d = cvVal cv in show d - | isFP cv = let CFP f = cvVal cv in bfToString 16 False True f - | isReal cv = let CAlgReal r = cvVal cv in show r - | isString cv = let CString s = cvVal cv in show s + | isFloat cv = let CFloat f = cvVal cv in T.pack (show f) + | isDouble cv = let CDouble d = cvVal cv in T.pack (show d) + | isFP cv = let CFP f = cvVal cv in T.pack (bfToString 16 False True f) + | isReal cv = let CAlgReal r = cvVal cv in T.pack (show r) + | isString cv = let CString s = cvVal cv in T.pack (show s) | not (isBounded cv) = let CInteger i = cvVal cv in shexI False False i | True = let CInteger i = cvVal cv in shex False False (hasSign cv, intSizeOf cv) i - bin cv | isADT cv = show cv + bin cv | isADT cv = T.pack (show cv) | isBoolean cv = binS (cvToBool cv) - | isFloat cv = let CFloat f = cvVal cv in show f - | isDouble cv = let CDouble d = cvVal cv in show d - | isFP cv = let CFP f = cvVal cv in bfToString 2 False True f - | isReal cv = let CAlgReal r = cvVal cv in show r - | isString cv = let CString s = cvVal cv in show s + | isFloat cv = let CFloat f = cvVal cv in T.pack (show f) + | isDouble cv = let CDouble d = cvVal cv in T.pack (show d) + | isFP cv = let CFP f = cvVal cv in T.pack (bfToString 2 False True f) + | isReal cv = let CAlgReal r = cvVal cv in T.pack (show r) + | isString cv = let CString s = cvVal cv in T.pack (show s) | not (isBounded cv) = let CInteger i = cvVal cv in sbinI False False i | True = let CInteger i = cvVal cv in sbin False False (hasSign cv, intSizeOf cv) i instance (SymVal a, PrettyNum a) => PrettyNum (SBV a) where - hexS s = maybe (show s) (hexS :: a -> String) $ unliteral s - binS s = maybe (show s) (binS :: a -> String) $ unliteral s + hexS s = maybe (T.pack $ show s) (hexS :: a -> Text) $ unliteral s + binS s = maybe (T.pack $ show s) (binS :: a -> Text) $ unliteral s - hexP s = maybe (show s) (hexP :: a -> String) $ unliteral s - binP s = maybe (show s) (binP :: a -> String) $ unliteral s + hexP s = maybe (T.pack $ show s) (hexP :: a -> Text) $ unliteral s + binP s = maybe (T.pack $ show s) (binP :: a -> Text) $ unliteral s - hex s = maybe (show s) (hex :: a -> String) $ unliteral s - bin s = maybe (show s) (bin :: a -> String) $ unliteral s + hex s = maybe (T.pack $ show s) (hex :: a -> Text) $ unliteral s + bin s = maybe (T.pack $ show s) (bin :: a -> Text) $ unliteral s -- | Show as a hexadecimal value. First bool controls whether type info is printed -- while the second boolean controls whether 0x prefix is printed. The tuple is -- the signedness and the bit-length of the input. The length of the string -- will /not/ depend on the value, but rather the bit-length. -shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String +shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> Text shex shType shPre (signed, size) a | a < 0 - = "-" ++ pre ++ pad l (s16 (abs (fromIntegral a :: Integer))) ++ t + = T.pack "-" <> pre <> T.pack (pad l (s16 (abs (fromIntegral a :: Integer)))) <> t | True - = pre ++ pad l (s16 a) ++ t - where t | shType = " :: " ++ (if signed then "Int" else "Word") ++ show size - | True = "" - pre | shPre = "0x" - | True = "" + = pre <> T.pack (pad l (s16 a)) <> t + where t | shType = T.pack " :: " <> T.pack (if signed then "Int" else "Word") <> T.pack (show size) + | True = T.empty + pre | shPre = T.pack "0x" + | True = T.empty l = (size + 3) `div` 4 -- | Show as hexadecimal, but for C programs. We have to be careful about -- printing min-bounds, since C does some funky casting, possibly losing -- the sign bit. In those cases, we use the defined constants in . -- We also properly append the necessary suffixes as needed. -chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String +chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> Text chex shType shPre (signed, size) a | Just s <- (signed, size, fromIntegral a) `lookup` specials - = s + = T.pack s | True - = shex shType shPre (signed, size) a ++ suffix + = shex shType shPre (signed, size) a <> T.pack suffix where specials :: [((Bool, Int, Integer), String)] specials = [ ((True, 8, fromIntegral (minBound :: Int8)), "INT8_MIN" ) , ((True, 16, fromIntegral (minBound :: Int16)), "INT16_MIN") @@ -285,40 +287,40 @@ -- | Show as a hexadecimal value, integer version. Almost the same as shex above -- except we don't have a bit-length so the length of the string will depend -- on the actual value. -shexI :: Bool -> Bool -> Integer -> String +shexI :: Bool -> Bool -> Integer -> Text shexI shType shPre a | a < 0 - = "-" ++ pre ++ s16 (abs a) ++ t + = T.pack "-" <> pre <> T.pack (s16 (abs a)) <> t | True - = pre ++ s16 a ++ t - where t | shType = " :: Integer" - | True = "" - pre | shPre = "0x" - | True = "" + = pre <> T.pack (s16 a) <> t + where t | shType = T.pack " :: Integer" + | True = T.empty + pre | shPre = T.pack "0x" + | True = T.empty -- | Similar to 'shex'; except in binary. -sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String +sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> Text sbin shType shPre (signed,size) a | a < 0 - = "-" ++ pre ++ pad size (s2 (abs (fromIntegral a :: Integer))) ++ t + = T.pack "-" <> pre <> T.pack (pad size (s2 (abs (fromIntegral a :: Integer)))) <> t | True - = pre ++ pad size (s2 a) ++ t - where t | shType = " :: " ++ (if signed then "Int" else "Word") ++ show size - | True = "" - pre | shPre = "0b" - | True = "" + = pre <> T.pack (pad size (s2 a)) <> t + where t | shType = T.pack " :: " <> T.pack (if signed then "Int" else "Word") <> T.pack (show size) + | True = T.empty + pre | shPre = T.pack "0b" + | True = T.empty -- | Similar to 'shexI'; except in binary. -sbinI :: Bool -> Bool -> Integer -> String +sbinI :: Bool -> Bool -> Integer -> Text sbinI shType shPre a | a < 0 - = "-" ++ pre ++ s2 (abs a) ++ t + = T.pack "-" <> pre <> T.pack (s2 (abs a)) <> t | True - = pre ++ s2 a ++ t - where t | shType = " :: Integer" - | True = "" - pre | shPre = "0b" - | True = "" + = pre <> T.pack (s2 a) <> t + where t | shType = T.pack " :: Integer" + | True = T.empty + pre | shPre = T.pack "0b" + | True = T.empty -- | Pad a string to a given length. If the string is longer, then we don't drop anything. pad :: Int -> String -> String diff --git a/Documentation/SBV/Examples/ADT/Expr.hs b/Documentation/SBV/Examples/ADT/Expr.hs --- a/Documentation/SBV/Examples/ADT/Expr.hs +++ b/Documentation/SBV/Examples/ADT/Expr.hs @@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} @@ -65,7 +66,7 @@ -- any number of upper-lower case letters and digits), and all expressions are closed; i.e., any -- variable referenced is introduced by an enclosing let expression. isValid :: SExpr -> SBool -isValid = go SL.nil +isValid = go [] where isId s = s `match` (asciiLower * KStar (asciiLetter + digit)) go :: SList String -> SExpr -> SBool go = smtFunction "valid" $ \env expr -> [sCase|Expr expr of @@ -78,7 +79,7 @@ -- | Evaluate an expression. eval :: SExpr -> SInteger -eval = go SL.nil +eval = go [] where go :: SList (String, Integer) -> SExpr -> SInteger go = smtFunction "eval" $ \env expr -> [sCase|Expr expr of Val i -> i diff --git a/Documentation/SBV/Examples/ADT/Param.hs b/Documentation/SBV/Examples/ADT/Param.hs --- a/Documentation/SBV/Examples/ADT/Param.hs +++ b/Documentation/SBV/Examples/ADT/Param.hs @@ -11,6 +11,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} @@ -74,7 +75,7 @@ -- any number of upper-lower case letters and digits), and all expressions are closed; i.e., any -- variable referenced is introduced by an enclosing let expression. isValid :: (SymVal nm, Eq nm, SymVal val) => (SBV nm -> SBool) -> SExpr nm val -> SBool -isValid nmChk = go SL.nil +isValid nmChk = go [] where go = smtFunction "valid" $ \env expr -> [sCase|Expr expr of Var s -> nmChk s .&& s `SL.elem` env Val _ -> sTrue @@ -85,7 +86,7 @@ -- | Evaluate an expression. eval :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val -eval = go SL.nil +eval = go [] where go = smtFunction "eval" $ \env expr -> [sCase|Expr expr of Val i -> i Var s -> get env s diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs --- a/Documentation/SBV/Examples/Misc/Floating.hs +++ b/Documentation/SBV/Examples/Misc/Floating.hs @@ -68,19 +68,19 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example: --- x = 1.9258643e-34 :: Float --- y = -1.925931e-34 :: Float --- z = -3.8518585e-34 :: Float +-- x = 2.5291315e20 :: Float +-- y = -2.9558926e20 :: Float +-- z = 1.1256507e20 :: Float -- -- Indeed, we have: -- --- >>> let x = 1.9258643e-34 :: Float --- >>> let y = -1.925931e-34 :: Float --- >>> let z = -3.8518585e-34 :: Float +-- >>> let x = 2.5291315e20 :: Float +-- >>> let y = -2.9558926e20 :: Float +-- >>> let z = 1.1256507e20 :: Float -- >>> x + (y + z) --- -3.8519256e-34 +-- 6.988897e19 -- >>> (x + y) + z --- -3.851925e-34 +-- 6.988896e19 -- -- Note the significant difference in the results! assocPlusRegular :: IO ThmResult @@ -131,11 +131,11 @@ -- -- >>> multInverse -- Falsifiable. Counter-example: --- a = -1.0669042e-38 :: Float +-- a = -2.372672e38 :: Float -- -- Indeed, we have: -- --- >>> let a = -1.0669042e-38 :: Float +-- >>> let a = -2.372672e38 :: Float -- >>> a * (1/a) -- 0.99999994 multInverse :: IO ThmResult diff --git a/Documentation/SBV/Examples/TP/InsertionSort.hs b/Documentation/SBV/Examples/TP/InsertionSort.hs --- a/Documentation/SBV/Examples/TP/InsertionSort.hs +++ b/Documentation/SBV/Examples/TP/InsertionSort.hs @@ -44,7 +44,7 @@ -- | Insertion sort, using 'insert' above to successively insert the elements. insertionSort :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SList a -insertionSort = smtFunction "insertionSort" $ \l -> ite (null l) nil +insertionSort = smtFunction "insertionSort" $ \l -> ite (null l) [] $ let (x, xs) = uncons l in insert x (insertionSort xs) @@ -52,7 +52,7 @@ -- | Remove the first occurrence of an number from a list, if any. removeFirst :: (Eq a, SymVal a) => SBV a -> SList a -> SList a removeFirst = smtFunction "removeFirst" $ \e l -> ite (null l) - nil + [] (let (x, xs) = uncons l in ite (e .== x) xs (x .: removeFirst e xs)) diff --git a/Documentation/SBV/Examples/TP/Lists.hs b/Documentation/SBV/Examples/TP/Lists.hs --- a/Documentation/SBV/Examples/TP/Lists.hs +++ b/Documentation/SBV/Examples/TP/Lists.hs @@ -99,7 +99,7 @@ -- [Proven] appendNull :: Ɐxs ∷ [Integer] → Bool appendNull :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) appendNull = lemma "appendNull" - (\(Forall xs) -> xs ++ nil .== xs) + (\(Forall xs) -> xs ++ [] .== xs) [] -- | @(x : xs) ++ ys == x : (xs ++ ys)@ @@ -1527,14 +1527,14 @@ (\(Forall n) (Forall xs) -> length xs .<= n .=> take n xs .== xs) [] --- | @length xs \<= n ==\> drop n xs == nil@ +-- | @length xs \<= n ==\> drop n xs == []@ -- -- >>> runTP $ drop_all @Integer -- Lemma: drop_all Q.E.D. -- [Proven] drop_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool drop_all :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) drop_all = lemma "drop_all" - (\(Forall n) (Forall xs) -> length xs .<= n .=> drop n xs .== nil) + (\(Forall n) (Forall xs) -> length xs .<= n .=> drop n xs .== []) [] -- | @take n (xs ++ ys) == (take n xs ++ take (n - length xs) ys)@ @@ -1705,7 +1705,7 @@ -- | Uninterleave the elements of two lists. We roughly split it into two, of alternating elements. uninterleave :: SymVal a => SList a -> STuple [a] [a] -uninterleave lst = uninterleaveGen lst (tuple (nil, nil)) +uninterleave lst = uninterleaveGen lst (tuple ([], [])) -- | Generalized form of uninterleave with the auxilary lists made explicit. uninterleaveGen :: SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a] @@ -1778,9 +1778,9 @@ (\(Forall xs) (Forall ys) -> length xs .== length ys .=> uninterleave (interleave xs ys) .== tuple (xs, ys)) $ \xs ys -> [length xs .== length ys] |- uninterleave (interleave xs ys) - =: uninterleaveGen (interleave xs ys) (tuple (nil, nil)) - ?? roundTripGen `at` (Inst @"xs" xs, Inst @"ys" ys, Inst @"alts" (tuple (nil, nil))) - =: tuple (reverse nil ++ xs, reverse nil ++ ys) + =: uninterleaveGen (interleave xs ys) (tuple ([], [])) + ?? roundTripGen `at` (Inst @"xs" xs, Inst @"ys" ys, Inst @"alts" (tuple ([], []))) + =: tuple (reverse [] ++ xs, reverse [] ++ ys) =: qed -- | @count e (xs ++ ys) == count e xs + count e ys@ diff --git a/Documentation/SBV/Examples/TP/QuickSort.hs b/Documentation/SBV/Examples/TP/QuickSort.hs --- a/Documentation/SBV/Examples/TP/QuickSort.hs +++ b/Documentation/SBV/Examples/TP/QuickSort.hs @@ -45,7 +45,7 @@ -- | Quick-sort, using the first element as pivot. quickSort :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SList a quickSort = smtFunction "quickSort" $ \l -> ite (null l) - nil + [] (let (x, xs) = uncons l (lo, hi) = untuple (partition x xs) in quickSort lo ++ [x] ++ quickSort hi) @@ -55,7 +55,7 @@ -- with a free-variable captured, which isn't supported due to higher-order limitations in SMTLib. partition :: (OrdSymbolic (SBV a), SymVal a) => SBV a -> SList a -> STuple [a] [a] partition = smtFunction "partition" $ \pivot xs -> ite (null xs) - (tuple (nil, nil)) + (tuple ([], [])) (let (a, as) = uncons xs (lo, hi) = untuple (partition pivot as) in ite (a .< pivot) diff --git a/Documentation/SBV/Examples/TP/UpDown.hs b/Documentation/SBV/Examples/TP/UpDown.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/TP/UpDown.hs @@ -0,0 +1,111 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.TP.UpDown +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Proves @reverse (down n) = up n@. +-- +-- This problem is motivated by an ACL2 midterm exam question, from Fall 2011. +-- See: . +----------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeApplications #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.TP.UpDown where + +import Prelude hiding (reverse, (++)) + +import Data.SBV +import Data.SBV.TP +import Data.SBV.List + +import Documentation.SBV.Examples.TP.Lists +import Documentation.SBV.Examples.TP.Peano + +#ifdef DOCTEST +-- $setup +-- >>> import Data.SBV.TP +#endif + +-- | Construct a list of size @n@, containing numbers @1@ to @n@. +-- +-- >>> up 0 +-- [] :: [SInteger] +-- >>> up 5 +-- [1,2,3,4,5] :: [SInteger] +up :: SNat -> SList Integer +up n = upAcc n [] + +-- | Keep consing the first argument on to the accumulator, until we hit zero. After that, return the second argument. +-- Normally, we'd define this as a local function, but the definition needs to be visible for the proofs. +upAcc :: SNat -> SList Integer -> SList Integer +upAcc = smtFunction "up" $ \n lst -> [sCase|Nat n of + Zero -> lst + Succ p -> upAcc p (n2i n .: lst) + |] + +-- | Construct a list of size @n@, containing numbers @n-1@ down to @0@. +-- +-- >>> down 0 +-- [] :: [SInteger] +-- >>> down 5 +-- [5,4,3,2,1] :: [SInteger] +down :: SNat -> SList Integer +down = smtFunction "down" $ \n -> [sCase|Nat n of + Zero -> [] + Succ p -> n2i n .: down p + |] + +-- | Prove that @reverse (down n)@ is the same as @up n@ +-- +-- >>> runTP upDown +-- Lemma: n2iNonNeg Q.E.D. +-- Lemma: revCons Q.E.D. +-- Inductive lemma (strong): upDownGen +-- Step: Measure is non-negative Q.E.D. +-- Step: 1 (2 way case split) +-- Step: 1.1 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.2.3 Q.E.D. +-- Step: 1.2.4 Q.E.D. +-- Step: 1.Completeness Q.E.D. +-- Result: Q.E.D. +-- Lemma: upDown Q.E.D. +-- [Proven] upDown :: Ɐn ∷ Nat → Bool +upDown :: TP (Proof (Forall "n" Nat -> SBool)) +upDown = do + n2inn <- recall "n2iNonNeg" n2iNonNeg + rc <- recall "revCons" (revCons @Integer) + + -- We first generalize the theorem, to make it inductive + upDownGen <- sInduct "upDownGen" + (\(Forall @"n" n) (Forall @"xs" xs) -> reverse (down n) ++ xs .== upAcc n xs) + (\n _ -> n2i n, [proofOf n2inn]) $ + \ih n xs -> [] |- cases [ isZero n ==> trivial + , isSucc n ==> let p = getSucc_1 n + in reverse (down (sSucc p)) ++ xs + =: reverse (n2i n .: down p) ++ xs + ?? rc + =: reverse (down p) ++ (n2i n .: xs) + ?? ih `at` (Inst @"n" p, Inst @"xs" (n2i n .: xs)) + =: upAcc p (n2i n .: xs) + =: upAcc n xs + =: qed + ] + + -- The theorem we want to prove follows by instantiating the list at empty, and + -- the SMT solver can figure it out by itself + lemma "upDown" + (\(Forall n) -> reverse (down n) .== up n) + [proofOf upDownGen] diff --git a/SBVTestSuite/GoldFiles/doctest_sanity.gold b/SBVTestSuite/GoldFiles/doctest_sanity.gold --- a/SBVTestSuite/GoldFiles/doctest_sanity.gold +++ b/SBVTestSuite/GoldFiles/doctest_sanity.gold @@ -1,3 +1,3 @@ -Total: 1089; Tried: 1089; Skipped: 0; Success: 1089; Errors: 0; Failures 0 -Examples: 971; Tried: 971; Skipped: 0; Success: 971; Errors: 0; Failures 0 -Setup: 118; Tried: 118; Skipped: 0; Success: 118; Errors: 0; Failures 0 +Total: 1095; Tried: 1095; Skipped: 0; Success: 1095; Errors: 0; Failures 0 +Examples: 976; Tried: 976; Skipped: 0; Success: 976; Errors: 0; Failures 0 +Setup: 119; Tried: 119; Skipped: 0; Success: 119; Errors: 0; Failures 0 diff --git a/SBVTestSuite/GoldFiles/validate_2.gold b/SBVTestSuite/GoldFiles/validate_2.gold --- a/SBVTestSuite/GoldFiles/validate_2.gold +++ b/SBVTestSuite/GoldFiles/validate_2.gold @@ -25,11 +25,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (fp #b0 #x00 #b00000001001110100110010))) +[RECV] ((s0 (fp #b0 #x00 #b00000000000000011001101))) *** Solver : Z3 *** Exit code: ExitSuccess [VALIDATE] Validating the model. Assignment: -[VALIDATE] x = 5.6391e-41 :: Float +[VALIDATE] x = 2.87e-43 :: Float [VALIDATE] There are no constraints to check. [VALIDATE] Validating outputs. @@ -38,7 +38,7 @@ *** *** Assignment: *** -*** x = 5.6391e-41 :: Float +*** x = 2.87e-43 :: Float *** *** Floating point FMA operation is not supported concretely. *** @@ -48,4 +48,4 @@ *** Alleged model: *** *** Satisfiable. Model: -*** x = 5.6391e-41 :: Float +*** x = 2.87e-43 :: Float diff --git a/SBVTestSuite/TestSuite/ADT/MutRec.hs b/SBVTestSuite/TestSuite/ADT/MutRec.hs --- a/SBVTestSuite/TestSuite/ADT/MutRec.hs +++ b/SBVTestSuite/TestSuite/ADT/MutRec.hs @@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} @@ -78,7 +79,7 @@ -- any number of upper-lower case letters and digits), and all expressions are closed; i.e., any -- variable referenced is assigned by a prior assignment expression. isValid :: forall val. SymVal val => SStmt String val -> SBool -isValid = ST.fst . goS SL.nil +isValid = ST.fst . goS [] where isId s = s `match` (asciiLower * KStar (asciiLetter + digit)) goE :: SList String -> SExpr String val -> SBool diff --git a/SBVTestSuite/TestSuite/Basics/Lambda.hs b/SBVTestSuite/TestSuite/Basics/Lambda.hs --- a/SBVTestSuite/TestSuite/Basics/Lambda.hs +++ b/SBVTestSuite/TestSuite/Basics/Lambda.hs @@ -444,7 +444,7 @@ xs <- free_ ys <- free_ - pure $ map (ae xs) ys .== nil + pure $ map (ae xs) ys .== [] -- This one is ok, because we're using the global xs. (i.e., no free vars) filterHead :: Symbolic String diff --git a/SBVTestSuite/TestSuite/Basics/Tuple.hs b/SBVTestSuite/TestSuite/Basics/Tuple.hs --- a/SBVTestSuite/TestSuite/Basics/Tuple.hs +++ b/SBVTestSuite/TestSuite/Basics/Tuple.hs @@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} @@ -97,7 +98,7 @@ vTup1 :: SList (E, [Bool]) <- sList "v1" q <- sBool "q" constrain $ sNot q - constrain $ (vTup1 !! 1)^._2 .== sTrue .: q .: L.nil + constrain $ (vTup1 !! 1)^._2 .== sTrue .: q .: [] constrain $ L.length vTup1 .== 3 case untuple (vTup1 !! 2) of 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 : 13.4 +Version : 13.5 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 @@ -262,6 +262,7 @@ , Documentation.SBV.Examples.TP.StrongInduction , Documentation.SBV.Examples.TP.SumReverse , Documentation.SBV.Examples.TP.Tao + , Documentation.SBV.Examples.TP.UpDown , Documentation.SBV.Examples.TP.VM , Documentation.SBV.Examples.Transformers.SymbolicEval , Documentation.SBV.Examples.Uninterpreted.AUF