diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,17 @@ * Hackage: * GitHub: -* Latest Hackage released version: 7.5, 2018-01-13 +* Latest Hackage released version: 7.6, 2018-03-18 + +### Version 7.6, Released 2018-03-18 + + * GHC 8.4.1 compatibility: Work around compilation issues. SBV + now compiles cleanly with GHC 8.4.1. + + * Define and export sWordN, sWordN_, sIntN_, from the Dynamic + interface, which simplifies creation of variables of arbitrary + bit sizes. These are similar to sWord8, sInt8, etc.; except + they create dynamic counterparts that can be of arbitrary bit size. ### Version 7.5, Released 2018-01-13 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -283,8 +283,8 @@ -- problems with constraints, like the following: -- -- @ --- do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"] --- solve [x .> 5, y + z .< x] +-- sat $ do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"] +-- solve [x .> 5, y + z .< x] -- @ solve :: [SBool] -> Symbolic SBool solve = return . bAnd @@ -492,7 +492,7 @@ types, along with those produce 'SReal's. That is, it can find models satisfying all the constraints while minimizing or maximizing user given metrics. Currently, optimization requires the use of the z3 SMT solver as the backend, and a good review of these features is given - in this paper: . + in this paper: . Goals can be lexicographically (default), independently, or pareto-front optimized. The relevant functions are: @@ -570,7 +570,7 @@ Note that 'assertSoft' works well with optimization goals ('minimize'/'maximize' etc.), and are most useful when we are optimizing a metric and thus some of the constraints can be relaxed with a penalty to obtain a good solution. Again - see + see for a good overview of the features in Z3 that SBV is providing the bridge for. A soft assertion can be specified in one of the following three main ways: 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 @@ -22,7 +22,10 @@ import qualified Data.Set as Set (member, union, unions, empty, toList, singleton, fromList) import System.FilePath (takeBaseName, replaceExtension) import System.Random + +-- Work around the fact that GHC 8.4.1 started exporting <>.. Hmm.. import Text.PrettyPrint.HughesPJ +import qualified Text.PrettyPrint.HughesPJ as P ((<>)) import Data.SBV.Core.Data import Data.SBV.Compilers.CodeGen @@ -129,7 +132,7 @@ -- as a function that returns that value. Otherwise, we compile it as a void function -- that takes return values as pointers to be updated. pprCFunHeader :: String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -pprCFunHeader fn ins outs mbRet = retType <+> text fn <> parens (fsep (punctuate comma (map mkParam ins ++ map mkPParam outs))) +pprCFunHeader fn ins outs mbRet = retType <+> text fn P.<> parens (fsep (punctuate comma (map mkParam ins ++ map mkPParam outs))) where retType = case mbRet of Nothing -> text "void" Just sw -> pprCWord False sw @@ -137,10 +140,10 @@ mkParam, mkPParam :: (String, CgVal) -> Doc mkParam (n, CgAtomic sw) = pprCWord True sw <+> text n mkParam (_, CgArray []) = die "mkParam: CgArray with no elements!" -mkParam (n, CgArray (sw:_)) = pprCWord True sw <+> text "*" <> text n -mkPParam (n, CgAtomic sw) = pprCWord False sw <+> text "*" <> text n +mkParam (n, CgArray (sw:_)) = pprCWord True sw <+> text "*" P.<> text n +mkPParam (n, CgAtomic sw) = pprCWord False sw <+> text "*" P.<> text n mkPParam (_, CgArray []) = die "mPkParam: CgArray with no elements!" -mkPParam (n, CgArray (sw:_)) = pprCWord False sw <+> text "*" <> text n +mkPParam (n, CgArray (sw:_)) = pprCWord False sw <+> text "*" P.<> text n -- | Renders as "const SWord8 s0", etc. the first parameter is the width of the typefield declSW :: Int -> SW -> Doc @@ -201,7 +204,7 @@ -- There are many options here, using binary, decimal, etc. We simply use decimal for values 8-bits or less, -- and hex otherwise. mkConst :: CgConfig -> CW -> Doc -mkConst cfg (CW KReal (CWAlgReal (AlgRational _ r))) = double (fromRational r :: Double) <> sRealSuffix (fromJust (cgReal cfg)) +mkConst cfg (CW KReal (CWAlgReal (AlgRational _ r))) = double (fromRational r :: Double) P.<> sRealSuffix (fromJust (cgReal cfg)) where sRealSuffix CgFloat = text "F" sRealSuffix CgDouble = empty sRealSuffix CgLongDouble = text "L" @@ -216,12 +219,12 @@ showSizedConst i (False, 1) = text (if i == 0 then "false" else "true") showSizedConst i (False, 8) = integer i showSizedConst i (True, 8) = integer i -showSizedConst i t@(False, 16) = text (shex False True t i) <> text "U" +showSizedConst i t@(False, 16) = text (shex False True t i) P.<> text "U" showSizedConst i t@(True, 16) = text (shex False True t i) -showSizedConst i t@(False, 32) = text (shex False True t i) <> text "UL" -showSizedConst i t@(True, 32) = text (shex False True t i) <> text "L" -showSizedConst i t@(False, 64) = text (shex False True t i) <> text "ULL" -showSizedConst i t@(True, 64) = text (shex False True t i) <> text "LL" +showSizedConst i t@(False, 32) = text (shex False True t i) P.<> text "UL" +showSizedConst i t@(True, 32) = text (shex False True t i) P.<> text "L" +showSizedConst i t@(False, 64) = text (shex False True t i) P.<> text "ULL" +showSizedConst i t@(True, 64) = text (shex False True t i) P.<> text "LL" showSizedConst i (True, 1) = die $ "Signed 1-bit value " ++ show i showSizedConst i (s, sz) = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz @@ -231,24 +234,24 @@ where ifld = not (null ldFlags) ld | ifld = text "${LDFLAGS}" | True = empty - lns = [ (True, text "# Makefile for" <+> nm <> text ". Automatically generated by SBV. Do not edit!") + lns = [ (True, text "# Makefile for" <+> nm P.<> text ". Automatically generated by SBV. Do not edit!") , (True, text "") , (True, text "# include any user-defined .mk file in the current directory.") , (True, text "-include *.mk") , (True, text "") , (True, text "CC?=gcc") , (True, text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer") - , (ifld, text "LDFLAGS?=" <> text (unwords ldFlags)) + , (ifld, text "LDFLAGS?=" P.<> text (unwords ldFlags)) , (True, text "") , (ifdr, text "all:" <+> nmd) , (ifdr, text "") - , (True, nmo <> text (": " ++ ppSameLine (hsep [nmc, nmh]))) + , (True, nmo P.<> text (": " ++ ppSameLine (hsep [nmc, nmh]))) , (True, text "\t${CC} ${CCFLAGS}" <+> text "-c $< -o $@") , (True, text "") - , (ifdr, nmdo <> text ":" <+> nmdc) + , (ifdr, nmdo P.<> text ":" <+> nmdc) , (ifdr, text "\t${CC} ${CCFLAGS}" <+> text "-c $< -o $@") , (ifdr, text "") - , (ifdr, nmd <> text (": " ++ ppSameLine (hsep [nmo, nmdo]))) + , (ifdr, nmd P.<> text (": " ++ ppSameLine (hsep [nmo, nmdo]))) , (ifdr, text "\t${CC} ${CCFLAGS}" <+> text "$^ -o $@" <+> ld) , (ifdr, text "") , (True, text "clean:") @@ -260,16 +263,16 @@ ] nm = text fn nmd = text dn - nmh = nm <> text ".h" - nmc = nm <> text ".c" - nmo = nm <> text ".o" - nmdc = nmd <> text ".c" - nmdo = nmd <> text ".o" + nmh = nm P.<> text ".h" + nmc = nm P.<> text ".c" + nmo = nm P.<> text ".o" + nmdc = nmd P.<> text ".c" + nmdo = nmd P.<> text ".o" -- | Generate the header genHeader :: (Maybe Int, Maybe CgSRealType) -> String -> [Doc] -> Doc -> Doc genHeader (ik, rk) fn sigs protos = - text "/* Header file for" <+> nm <> text ". Automatically generated by SBV. Do not edit! */" + text "/* Header file for" <+> nm P.<> text ". Automatically generated by SBV. Do not edit! */" $$ text "" $$ text "#ifndef" <+> tag $$ text "#define" <+> tag @@ -306,13 +309,13 @@ $$ imapping $$ rmapping $$ text ("/* Entry point prototype" ++ plu ++ ": */") - $$ vcat (map (<> semi) sigs) + $$ vcat (map (P.<> semi) sigs) $$ text "" $$ protos $$ text "#endif /*" <+> tag <+> text "*/" $$ text "" where nm = text fn - tag = text "__" <> nm <> text "__HEADER_INCLUDED__" + tag = text "__" P.<> nm P.<> text "__HEADER_INCLUDED__" plu = if length sigs /= 1 then "s" else "" imapping = case ik of Nothing -> empty @@ -333,11 +336,11 @@ -- | Generate an example driver program genDriver :: CgConfig -> [Integer] -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> [Doc] genDriver cfg randVals fn inps outs mbRet = [pre, header, body, post] - where pre = text "/* Example driver program for" <+> nm <> text ". */" + where pre = text "/* Example driver program for" <+> nm P.<> text ". */" $$ text "/* Automatically generated by SBV. Edit as you see fit! */" $$ text "" $$ text "#include " - header = text "#include" <+> doubleQuotes (nm <> text ".h") + header = text "#include" <+> doubleQuotes (nm P.<> text ".h") $$ text "" $$ text "int main(void)" $$ text "{" @@ -348,13 +351,13 @@ $$ call $$ text "" $$ (case mbRet of - Just sw -> text "printf" <> parens (printQuotes (fcall <+> text "=" <+> specifier cfg sw <> text "\\n") - <> comma <+> resultVar) <> semi - Nothing -> text "printf" <> parens (printQuotes (fcall <+> text "->\\n")) <> semi) + Just sw -> text "printf" P.<> parens (printQuotes (fcall <+> text "=" <+> specifier cfg sw P.<> text "\\n") + P.<> comma <+> resultVar) P.<> semi + Nothing -> text "printf" P.<> parens (printQuotes (fcall <+> text "->\\n")) P.<> semi) $$ vcat (map display outs) ) post = text "" - $+$ nest 2 (text "return 0" <> semi) + $+$ nest 2 (text "return 0" P.<> semi) $$ text "}" $$ text "" nm = text fn @@ -371,36 +374,36 @@ mkRVal sw r = mkConst cfg $ mkConstCW (kindOf sw) r mkInp (_, _, CgAtomic{}) = empty -- constant, no need to declare mkInp (_, n, CgArray []) = die $ "Unsupported empty array value for " ++ show n - mkInp (vs, n, CgArray sws@(sw:_)) = pprCWord True sw <+> text n <> brackets (int (length sws)) <+> text "= {" + mkInp (vs, n, CgArray sws@(sw:_)) = pprCWord True sw <+> text n P.<> brackets (int (length sws)) <+> text "= {" $$ nest 4 (fsep (punctuate comma (align vs))) $$ text "};" $$ text "" - $$ text "printf" <> parens (printQuotes (text "Contents of input array" <+> text n <> text ":\\n")) <> semi + $$ text "printf" P.<> parens (printQuotes (text "Contents of input array" <+> text n P.<> text ":\\n")) P.<> semi $$ display (n, CgArray sws) $$ text "" - mkOut (v, CgAtomic sw) = pprCWord False sw <+> text v <> semi + mkOut (v, CgAtomic sw) = pprCWord False sw <+> text v P.<> semi mkOut (v, CgArray []) = die $ "Unsupported empty array value for " ++ show v - mkOut (v, CgArray sws@(sw:_)) = pprCWord False sw <+> text v <> brackets (int (length sws)) <> semi + mkOut (v, CgArray sws@(sw:_)) = pprCWord False sw <+> text v P.<> brackets (int (length sws)) P.<> semi resultVar = text "__result" call = case mbRet of - Nothing -> fcall <> semi - Just sw -> pprCWord True sw <+> resultVar <+> text "=" <+> fcall <> semi - fcall = nm <> parens (fsep (punctuate comma (map mkCVal pairedInputs ++ map mkOVal outs))) + Nothing -> fcall P.<> semi + Just sw -> pprCWord True sw <+> resultVar <+> text "=" <+> fcall P.<> semi + fcall = nm P.<> parens (fsep (punctuate comma (map mkCVal pairedInputs ++ map mkOVal outs))) mkCVal ([v], _, CgAtomic{}) = v mkCVal (vs, n, CgAtomic{}) = die $ "Unexpected driver value computed for " ++ show n ++ render (hcat vs) mkCVal (_, n, CgArray{}) = text n - mkOVal (n, CgAtomic{}) = text "&" <> text n + mkOVal (n, CgAtomic{}) = text "&" P.<> text n mkOVal (n, CgArray{}) = text n - display (n, CgAtomic sw) = text "printf" <> parens (printQuotes (text " " <+> text n <+> text "=" <+> specifier cfg sw - <> text "\\n") <> comma <+> text n) <> semi + display (n, CgAtomic sw) = text "printf" P.<> parens (printQuotes (text " " <+> text n <+> text "=" <+> specifier cfg sw + P.<> text "\\n") P.<> comma <+> text n) P.<> semi display (n, CgArray []) = die $ "Unsupported empty array value for " ++ show n - display (n, CgArray sws@(sw:_)) = text "int" <+> nctr <> semi - $$ text "for(" <> nctr <+> text "= 0;" <+> nctr <+> text "<" <+> int (length sws) <+> text "; ++" <> nctr <> text ")" - $$ nest 2 (text "printf" <> parens (printQuotes (text " " <+> entrySpec <+> text "=" <+> spec <> text "\\n") - <> comma <+> nctr <+> comma <> entry) <> semi) - where nctr = text n <> text "_ctr" - entry = text n <> text "[" <> nctr <> text "]" - entrySpec = text n <> text "[%d]" + display (n, CgArray sws@(sw:_)) = text "int" <+> nctr P.<> semi + $$ text "for(" P.<> nctr <+> text "= 0;" <+> nctr <+> text "<" <+> int (length sws) <+> text "; ++" P.<> nctr P.<> text ")" + $$ nest 2 (text "printf" P.<> parens (printQuotes (text " " <+> entrySpec <+> text "=" <+> spec P.<> text "\\n") + P.<> comma <+> nctr <+> comma P.<> entry) P.<> semi) + where nctr = text n P.<> text "_ctr" + entry = text n P.<> text "[" P.<> nctr P.<> text "]" + entrySpec = text n P.<> text "[%d]" spec = specifier cfg sw -- | Generate the C program @@ -427,10 +430,10 @@ usorts = [s | KUserSort s _ <- Set.toList kindInfo, s /= "RoundingMode"] -- No support for any sorts other than RoundingMode! - pre = text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */" + pre = text "/* File:" <+> doubleQuotes (nm P.<> text ".c") P.<> text ". Automatically generated by SBV. Do not edit! */" $$ text "" - header = text "#include" <+> doubleQuotes (nm <> text ".h") + header = text "#include" <+> doubleQuotes (nm P.<> text ".h") post = text "" $$ vcat (map codeSeg cgs) @@ -490,18 +493,18 @@ isAlive (_, _) = True genIO :: Bool -> (Bool, (String, CgVal)) -> [Doc] - genIO True (alive, (cNm, CgAtomic sw)) = [declSW typeWidth sw <+> text "=" <+> text cNm <> semi | alive] - genIO False (alive, (cNm, CgAtomic sw)) = [text "*" <> text cNm <+> text "=" <+> showSW cfg consts sw <> semi | alive] + genIO True (alive, (cNm, CgAtomic sw)) = [declSW typeWidth sw <+> text "=" <+> text cNm P.<> semi | alive] + genIO False (alive, (cNm, CgAtomic sw)) = [text "*" P.<> text cNm <+> text "=" <+> showSW cfg consts sw P.<> semi | alive] genIO isInp (_, (cNm, CgArray sws)) = zipWith genElt sws [(0::Int)..] where genElt sw i - | isInp = declSW typeWidth sw <+> text "=" <+> text entry <> semi - | True = text entry <+> text "=" <+> showSW cfg consts sw <> semi + | isInp = declSW typeWidth sw <+> text "=" <+> text entry P.<> semi + | True = text entry <+> text "=" <+> showSW cfg consts sw P.<> semi where entry = cNm ++ "[" ++ show i ++ "]" - mkRet sw = text "return" <+> showSW cfg consts sw <> semi + mkRet sw = text "return" <+> showSW cfg consts sw P.<> semi genTbl :: ((Int, Kind, Kind), [SW]) -> (Int, Doc) - genTbl ((i, _, k), elts) = (location, static <+> text "const" <+> text (show k) <+> text ("table" ++ show i) <> text "[] = {" + genTbl ((i, _, k), elts) = (location, static <+> text "const" <+> text (show k) <+> text ("table" ++ show i) P.<> text "[] = {" $$ nest 4 (fsep (punctuate comma (align (map (showSW cfg consts) elts)))) $$ text "};") where static = if location == -1 then text "static" else empty @@ -511,7 +514,7 @@ | True = n genAsgn :: (SW, SBVExpr) -> (Int, Doc) - genAsgn (sw, n) = (getNodeId sw, ppExpr cfg consts n (declSW typeWidth sw) (declSWNoConst typeWidth sw) <> semi) + genAsgn (sw, n) = (getNodeId sw, ppExpr cfg consts n (declSW typeWidth sw) (declSWNoConst typeWidth sw) P.<> semi) -- merge tables intermixed with assignments and assertions, paying attention to putting tables as -- early as possible and tables right after.. Note that the assignment list (second argument) is sorted on its order @@ -527,7 +530,7 @@ where doc = text "/* ASSERTION:" <+> text msg $$ maybe empty (vcat . map text) (locInfo (getCallStack `fmap` cs)) $$ text " */" - $$ text "if" <> parens (showSW cfg consts sw) + $$ text "if" P.<> parens (showSW cfg consts sw) $$ text "{" $+$ nest 2 (vcat [errOut, text "exit(-1);"]) $$ text "}" @@ -556,9 +559,9 @@ where same f = (f, f) named fnm dnm f = (f fnm, f dnm) - castToUnsigned f to = parens (text "!isnan" <> parens a <+> text "&&" <+> text "signbit" <> parens a) <+> text "?" <+> cvt1 <+> text ":" <+> cvt2 + castToUnsigned f to = parens (text "!isnan" P.<> parens a <+> text "&&" <+> text "signbit" P.<> parens a) <+> text "?" <+> cvt1 <+> text ":" <+> cvt2 where [a] = map snd fpArgs - absA = text (if f == KFloat then "fabsf" else "fabs") <> parens a + absA = text (if f == KFloat then "fabsf" else "fabs") P.<> parens a cvt1 = parens (text "-" <+> parens (parens (text (show to)) <+> absA)) cvt2 = parens (parens (text (show to)) <+> a) @@ -574,35 +577,35 @@ (KFloat, KBounded False 32) -> cast $ cpy "sizeof(SWord32)" (KDouble, KBounded False 64) -> cast $ cpy "sizeof(SWord64)" _ -> die $ "Reinterpretation from : " ++ show f ++ " to " ++ show t - where cpy sz = \[a] -> let alhs = text "&" <> var - arhs = text "&" <> a - in text "memcpy" <> parens (fsep (punctuate comma [alhs, arhs, text sz])) - cvt FP_Abs = dispatch $ named "fabsf" "fabs" $ \nm _ [a] -> text nm <> parens a - cvt FP_Neg = dispatch $ same $ \_ [a] -> text "-" <> a + where cpy sz = \[a] -> let alhs = text "&" P.<> var + arhs = text "&" P.<> a + in text "memcpy" P.<> parens (fsep (punctuate comma [alhs, arhs, text sz])) + cvt FP_Abs = dispatch $ named "fabsf" "fabs" $ \nm _ [a] -> text nm P.<> parens a + cvt FP_Neg = dispatch $ same $ \_ [a] -> text "-" P.<> a cvt FP_Add = dispatch $ same $ \_ [a, b] -> a <+> text "+" <+> b cvt FP_Sub = dispatch $ same $ \_ [a, b] -> a <+> text "-" <+> b cvt FP_Mul = dispatch $ same $ \_ [a, b] -> a <+> text "*" <+> b cvt FP_Div = dispatch $ same $ \_ [a, b] -> a <+> text "/" <+> b - cvt FP_FMA = dispatch $ named "fmaf" "fma" $ \nm _ [a, b, c] -> text nm <> parens (fsep (punctuate comma [a, b, c])) - cvt FP_Sqrt = dispatch $ named "sqrtf" "sqrt" $ \nm _ [a] -> text nm <> parens a - cvt FP_Rem = dispatch $ named "fmodf" "fmod" $ \nm _ [a, b] -> text nm <> parens (fsep (punctuate comma [a, b])) - cvt FP_RoundToIntegral = dispatch $ named "rintf" "rint" $ \nm _ [a] -> text nm <> parens a - cvt FP_Min = dispatch $ named "fminf" "fmin" $ \nm k [a, b] -> wrapMinMax k a b (text nm <> parens (fsep (punctuate comma [a, b]))) - cvt FP_Max = dispatch $ named "fmaxf" "fmax" $ \nm k [a, b] -> wrapMinMax k a b (text nm <> parens (fsep (punctuate comma [a, b]))) + cvt FP_FMA = dispatch $ named "fmaf" "fma" $ \nm _ [a, b, c] -> text nm P.<> parens (fsep (punctuate comma [a, b, c])) + cvt FP_Sqrt = dispatch $ named "sqrtf" "sqrt" $ \nm _ [a] -> text nm P.<> parens a + cvt FP_Rem = dispatch $ named "fmodf" "fmod" $ \nm _ [a, b] -> text nm P.<> parens (fsep (punctuate comma [a, b])) + cvt FP_RoundToIntegral = dispatch $ named "rintf" "rint" $ \nm _ [a] -> text nm P.<> parens a + cvt FP_Min = dispatch $ named "fminf" "fmin" $ \nm k [a, b] -> wrapMinMax k a b (text nm P.<> parens (fsep (punctuate comma [a, b]))) + cvt FP_Max = dispatch $ named "fmaxf" "fmax" $ \nm k [a, b] -> wrapMinMax k a b (text nm P.<> parens (fsep (punctuate comma [a, b]))) cvt FP_ObjEqual = let mkIte x y z = x <+> text "?" <+> y <+> text ":" <+> z - chkNaN x = text "isnan" <> parens x - signbit x = text "signbit" <> parens x + chkNaN x = text "isnan" P.<> parens x + signbit x = text "signbit" P.<> parens x eq x y = parens (x <+> text "==" <+> y) eqZero x = eq x (text "0") negZero x = parens (signbit x <+> text "&&" <+> eqZero x) in dispatch $ same $ \_ [a, b] -> mkIte (chkNaN a) (chkNaN b) (mkIte (negZero a) (negZero b) (mkIte (negZero b) (negZero a) (eq a b))) - cvt FP_IsNormal = dispatch $ same $ \_ [a] -> text "isnormal" <> parens a - cvt FP_IsSubnormal = dispatch $ same $ \_ [a] -> text "FP_SUBNORMAL == fpclassify" <> parens a - cvt FP_IsZero = dispatch $ same $ \_ [a] -> text "FP_ZERO == fpclassify" <> parens a - cvt FP_IsInfinite = dispatch $ same $ \_ [a] -> text "isinf" <> parens a - cvt FP_IsNaN = dispatch $ same $ \_ [a] -> text "isnan" <> parens a - cvt FP_IsNegative = dispatch $ same $ \_ [a] -> text "!isnan" <> parens a <+> text "&&" <+> text "signbit" <> parens a - cvt FP_IsPositive = dispatch $ same $ \_ [a] -> text "!isnan" <> parens a <+> text "&&" <+> text "!signbit" <> parens a + cvt FP_IsNormal = dispatch $ same $ \_ [a] -> text "isnormal" P.<> parens a + cvt FP_IsSubnormal = dispatch $ same $ \_ [a] -> text "FP_SUBNORMAL == fpclassify" P.<> parens a + cvt FP_IsZero = dispatch $ same $ \_ [a] -> text "FP_ZERO == fpclassify" P.<> parens a + cvt FP_IsInfinite = dispatch $ same $ \_ [a] -> text "isinf" P.<> parens a + cvt FP_IsNaN = dispatch $ same $ \_ [a] -> text "isnan" P.<> parens a + cvt FP_IsNegative = dispatch $ same $ \_ [a] -> text "!isnan" P.<> parens a <+> text "&&" <+> text "signbit" P.<> parens a + cvt FP_IsPositive = dispatch $ same $ \_ [a] -> text "!isnan" P.<> parens a <+> text "&&" <+> text "!signbit" P.<> parens a -- grab the rounding-mode, if present, and make sure it's RoundNearestTiesToEven. Otherwise skip. fpArgs = case as of @@ -640,14 +643,14 @@ -- There's really no good choice here. wrapMinMax k a b s = parens cond <+> text "?" <+> zero <+> text ":" <+> s where zero = text $ if k == KFloat then showCFloat 0 else showCDouble 0 - cond = parens (text "FP_ZERO == fpclassify" <> parens a) -- a is zero - <+> text "&&" <+> parens (text "FP_ZERO == fpclassify" <> parens b) -- b is zero - <+> text "&&" <+> parens (text "signbit" <> parens a <+> text "!=" <+> text "signbit" <> parens b) -- a and b differ in sign + cond = parens (text "FP_ZERO == fpclassify" P.<> parens a) -- a is zero + <+> text "&&" <+> parens (text "FP_ZERO == fpclassify" P.<> parens b) -- b is zero + <+> text "&&" <+> parens (text "signbit" P.<> parens a <+> text "!=" <+> text "signbit" P.<> parens b) -- a and b differ in sign ppExpr :: CgConfig -> [(SW, CW)] -> SBVExpr -> Doc -> (Doc, Doc) -> Doc ppExpr cfg consts (SBVApp op opArgs) lhs (typ, var) | doNotAssign op - = typ <+> var <> semi <+> rhs + = typ <+> var P.<> semi <+> rhs | True = lhs <+> text "=" <+> rhs where doNotAssign (IEEEFP FP_Reinterpret{}) = True -- generates a memcpy instead; no simple assignment @@ -676,7 +679,7 @@ p (PseudoBoolean pb) as = handlePB pb as p (KindCast _ to) [a] = parens (text (show to)) <+> a p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s - p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as)) + p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s P.<> parens (fsep (punctuate comma as)) p (Extract i j) [a] = extract i j (head opArgs) a p Join [a, b] = join (let (s1 : s2 : _) = opArgs in (s1, s2, a, b)) p (Rol i) [a] = rotate True i a (head opArgs) @@ -685,8 +688,8 @@ p Shr [a, i] = shift False (getShiftAmnt i opArgs) a -- intentional and historical (from the days when Shl/Shr had a constant parameter.) p Not [a] = case kindOf (head opArgs) of -- be careful about booleans, bitwise complement is not correct for them! - KBool -> text "!" <> a - _ -> text "~" <> a + KBool -> text "!" P.<> a + _ -> text "~" P.<> a p Ite [a, b, c] = a <+> text "?" <+> b <+> text ":" <+> c p (LkUp (t, k, _, len) ind def) [] | not rtc = lkUp -- ignore run-time-checks per user request @@ -695,7 +698,7 @@ | needsCheckR = cndLkUp checkRight | True = lkUp where [index, defVal] = map (showSW cfg consts) [ind, def] - lkUp = text "table" <> int t <> brackets (showSW cfg consts ind) + lkUp = text "table" P.<> int t P.<> brackets (showSW cfg consts ind) cndLkUp cnd = cnd <+> text "?" <+> defVal <+> text ":" <+> lkUp checkLeft = index <+> text "< 0" checkRight = index <+> text ">=" <+> int len @@ -724,7 +727,7 @@ KFloat -> text "fabsf" KDouble -> text "fabs" _ -> text "abs" - in f <> parens a + in f P.<> parens a -- for And/Or, translate to boolean versions if on boolean kind p And [a, b] | kindOf (head opArgs) == KBool = a <+> text "&&" <+> b p Or [a, b] | kindOf (head opArgs) == KBool = a <+> text "||" <+> b @@ -852,24 +855,24 @@ where ifld = not (null ldFlags) ld | ifld = text "${LDFLAGS}" | True = empty - lns = [ (True, text "# Makefile for" <+> nm <> text ". Automatically generated by SBV. Do not edit!") + lns = [ (True, text "# Makefile for" <+> nm P.<> text ". Automatically generated by SBV. Do not edit!") , (True, text "") , (True, text "# include any user-defined .mk file in the current directory.") , (True, text "-include *.mk") , (True, text "") , (True, text "CC?=gcc") , (True, text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer") - , (ifld, text "LDFLAGS?=" <> text (unwords ldFlags)) + , (ifld, text "LDFLAGS?=" P.<> text (unwords ldFlags)) , (True, text "AR?=ar") , (True, text "ARFLAGS?=cr") , (True, text "") , (not ifdr, text ("all: " ++ liba)) , (ifdr, text ("all: " ++ unwords [liba, libd])) , (True, text "") - , (True, text liba <> text (": " ++ unwords os)) + , (True, text liba P.<> text (": " ++ unwords os)) , (True, text "\t${AR} ${ARFLAGS} $@ $^") , (True, text "") - , (ifdr, text libd <> text (": " ++ unwords [libd ++ ".c", libh])) + , (ifdr, text libd P.<> text (": " ++ unwords [libd ++ ".c", libh])) , (ifdr, text ("\t${CC} ${CCFLAGS} $< -o $@ " ++ liba) <+> ld) , (ifdr, text "") , (True, vcat (zipWith mkObj os fs)) @@ -886,14 +889,14 @@ libh = libName ++ ".h" libd = libName ++ "_driver" os = map (`replaceExtension` ".o") fs - mkObj o f = text o <> text (": " ++ unwords [f, libh]) + mkObj o f = text o P.<> text (": " ++ unwords [f, libh]) $$ text "\t${CC} ${CCFLAGS} -c $< -o $@" $$ text "" -- | Create a driver for a library mergeDrivers :: String -> Doc -> [(FilePath, [Doc])] -> [Doc] mergeDrivers libName inc ds = pre : concatMap mkDFun ds ++ [callDrivers (map fst ds)] - where pre = text "/* Example driver program for" <+> text libName <> text ". */" + where pre = text "/* Example driver program for" <+> text libName P.<> text ". */" $$ text "/* Automatically generated by SBV. Edit as you see fit! */" $$ text "" $$ text "#include " diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs --- a/Data/SBV/Control/Query.hs +++ b/Data/SBV/Control/Query.hs @@ -309,8 +309,7 @@ inputs <- map snd <$> getQuantifiedInputs - parse r bad $ \case EApp (ECon "objectives" : es) -> do mbVals <- mapM (getObjValue (bad r) inputs) es - return $ catMaybes mbVals + parse r bad $ \case EApp (ECon "objectives" : es) -> catMaybes <$> mapM (getObjValue (bad r) inputs) es _ -> bad r Nothing where -- | Parse an objective value out. 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 @@ -133,7 +133,7 @@ ks <- readIORef (rNewKinds is) cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rNewConsts is) arrs <- IMap.toAscList <$> readIORef (rNewArrs is) - tbls <- (map arrange . sortBy cmp . map swap . Map.toList) <$> readIORef (rNewTbls is) + tbls <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef (rNewTbls is) as <- readIORef (rNewAsgns is) return $ toIncSMTLib cfg inps ks cnsts arrs tbls as cfg mapM_ (send True) $ mergeSExpr ls diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs --- a/Data/SBV/Core/Data.hs +++ b/Data/SBV/Core/Data.hs @@ -447,11 +447,9 @@ -- | Declare a new symbolic array, with a potential initial value declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Symbolic (SArray a b) -declNewSArray mkNm = do - let aknd = kindOf (undefined :: a) +declNewSArray mkNm = SArray <$> newSArr (aknd, bknd) mkNm + where aknd = kindOf (undefined :: a) bknd = kindOf (undefined :: b) - arr <- newSArr (aknd, bknd) mkNm - return (SArray arr) -- | Declare a new functional symbolic array. Note that a read from an uninitialized cell will result in an error. declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe String -> Symbolic (SFunArray a b) diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -1748,7 +1748,7 @@ -- Minimal complete definition: minimize/maximize. -- -- A good reference on these features is given in the following paper: --- . +-- . class Metric a where -- | Minimize a named metric minimize :: String -> a -> Symbolic () @@ -1805,7 +1805,7 @@ return (SBV s :: SBool) -- | Explicit sharing combinator. The SBV library has internal caching/hash-consing mechanisms --- built in, based on Andy Gill's type-safe obervable sharing technique (see: ). +-- built in, based on Andy Gill's type-safe obervable sharing technique (see: ). -- However, there might be times where being explicit on the sharing can help, especially in experimental code. The 'slet' combinator -- ensures that its first argument is computed once and passed on to its continuation, explicitly indicating the intent of sharing. Most -- use cases of the SBV library should simply use Haskell's @let@ construct for this purpose. 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 @@ -32,7 +32,7 @@ , RoundingMode(..) , SBVType(..), newUninterpreted, addAxiom , SVal(..) - , svMkSymVar + , svMkSymVar, sWordN, sWordN_, sIntN, sIntN_ , ArrayContext(..), ArrayInfo , svToSW, svToSymSW, forceSWArg , SBVExpr(..), newExpr, isCodeGenMode @@ -813,6 +813,22 @@ svMkTrackerVar :: Kind -> String -> State -> IO SVal svMkTrackerVar k nm = svMkSymVarGen True (Just EX) k (Just nm) +-- | Create an N-bit symbolic unsigned named variable +sWordN :: Int -> String -> Symbolic SVal +sWordN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) (Just nm) + +-- | Create an N-bit symbolic unsigned unnamed variable +sWordN_ :: Int -> Symbolic SVal +sWordN_ w = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) Nothing + +-- | Create an N-bit symbolic signed named variable +sIntN :: Int -> String -> Symbolic SVal +sIntN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded True w) (Just nm) + +-- | Create an N-bit symbolic signed unnamed variable +sIntN_ :: Int -> Symbolic SVal +sIntN_ w = ask >>= liftIO . svMkSymVar Nothing (KBounded True w) Nothing + -- | Create a symbolic value, based on the quantifier we have. If an -- explicit quantifier is given, we just use that. If not, then we -- pick the quantifier appropriately based on the run-mode. @@ -967,8 +983,8 @@ swapc ((_, a), b) = (b, a) cmp (a, _) (b, _) = a `compare` b arrange (i, (at, rt, es)) = ((i, at, rt), es) - cnsts <- (sortBy cmp . map swapc . Map.toList) <$> readIORef (rconstMap st) - tbls <- (map arrange . sortBy cmp . map swap . Map.toList) <$> readIORef tables + cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rconstMap st) + tbls <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef tables arrs <- IMap.toAscList <$> readIORef arrays unint <- Map.toList <$> readIORef uis axs <- reverse <$> readIORef axioms @@ -1118,7 +1134,7 @@ -- takes into the account of how symbolic simulation executes. -- -- See Andy Gill's type-safe obervable sharing trick for the inspiration behind --- this technique: +-- this technique: -- -- Note that this is *not* a general memo utility! newtype Cached a = Cached (State -> IO a) diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -26,6 +26,7 @@ , Symbolic , Quantifier(..) , svMkSymVar + , sWordN, sWordN_, sIntN, sIntN_ -- ** Operations on symbolic values -- *** Boolean literals , svTrue, svFalse, svBool, svAsBool diff --git a/Data/SBV/Examples/Misc/Floating.hs b/Data/SBV/Examples/Misc/Floating.hs --- a/Data/SBV/Examples/Misc/Floating.hs +++ b/Data/SBV/Examples/Misc/Floating.hs @@ -146,29 +146,29 @@ -- >>> roundingAdd -- Satisfiable. Model: -- rm = RoundTowardPositive :: RoundingMode --- x = -256.0 :: Float --- y = 4.6475088e-10 :: Float +-- x = 1.0 :: Float +-- y = -6.1035094e-5 :: Float -- -- (Note that depending on your version of Z3, you might get a different result.) -- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports -- 'RoundNearestTiesToEven'. We have: -- --- >>> (-256.0 + 4.6475088e-10) :: Float --- -256.0 +-- >>> (1 + (-6.1035094e-5)) :: Float +-- 0.99993896 -- -- While we cannot directly see the result when the mode is 'RoundTowardPositive' in Haskell, we can use -- SBV to provide us with that result thusly: -- --- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive (-256.0) (4.6475088e-10 :: SFloat) +-- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive 1 (-6.1035094e-5 :: SFloat) -- Satisfiable. Model: --- s0 = -255.99998 :: Float +-- s0 = 0.999939 :: Float -- -- We can see why these two resuls are indeed different: The 'RoundTowardsPositive' -- (which rounds towards positive-infinity) produces a larger result. Indeed, if we treat these numbers -- as 'Double' values, we get: -- --- >>> (-256.0 + 4.6475088e-10) :: Double --- -255.99999999953525 +-- >>> (1 + (-6.1035094e-5)) :: Double +-- 0.999938964906 -- -- we see that the "more precise" result is larger than what the 'Float' value is, justifying the -- larger value with 'RoundTowardPositive'. A more detailed study is beyond our current scope, so we'll diff --git a/Data/SBV/Examples/Puzzles/U2Bridge.hs b/Data/SBV/Examples/Puzzles/U2Bridge.hs --- a/Data/SBV/Examples/Puzzles/U2Bridge.hs +++ b/Data/SBV/Examples/Puzzles/U2Bridge.hs @@ -129,8 +129,7 @@ -- | Read the state via an accessor function peek :: (Status -> a) -> Move a -peek f = do s <- get - return (f s) +peek f = f <$> get -- | Given an arbitrary member, return his location whereIs :: SU2Member -> Move SLocation diff --git a/Data/SBV/Examples/Uninterpreted/AUF.hs b/Data/SBV/Examples/Uninterpreted/AUF.hs --- a/Data/SBV/Examples/Uninterpreted/AUF.hs +++ b/Data/SBV/Examples/Uninterpreted/AUF.hs @@ -88,5 +88,4 @@ proveThm2 = prove $ do x <- free "x" y <- free "y" - a <- newArray "b" - return $ thm2 x y a + thm2 x y <$> newArray "b" diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -7,9 +7,9 @@ ### Build Status - Linux: - - GHC 8.0.2 [![Build1][3]][1] - - GHC 8.2.1 [![Build1][4]][1] - - GHC 8.2.2 [![Build1][5]][1] + - GHC 8.2.1 [![Build1][3]][1] + - GHC 8.2.2 [![Build1][4]][1] + - GHC 8.4.1 [![Build1][5]][1] - Mac OSX: - GHC 8.2.1 [![Build1][6]][1] - Windows: diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -76,7 +76,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version) -[RECV] (:version "4.6.1") +[RECV] (:version "4.6.2") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -107,7 +107,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.6.1") +[RECV] (:version "4.6.2") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) diff --git a/SBVTestSuite/TestSuite/Basics/Exceptions.hs b/SBVTestSuite/TestSuite/Basics/Exceptions.hs --- a/SBVTestSuite/TestSuite/Basics/Exceptions.hs +++ b/SBVTestSuite/TestSuite/Basics/Exceptions.hs @@ -61,7 +61,6 @@ x <- sInteger "x" y <- sInteger "y" query $ do constrain $ x*y .== x*x - cs <- checkSat - return $ show cs + show <$> checkSat {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} diff --git a/SBVTestSuite/TestSuite/Basics/GenBenchmark.hs b/SBVTestSuite/TestSuite/Basics/GenBenchmark.hs --- a/SBVTestSuite/TestSuite/Basics/GenBenchmark.hs +++ b/SBVTestSuite/TestSuite/Basics/GenBenchmark.hs @@ -20,7 +20,5 @@ [ goldenString "genBenchMark1" $ gen False (\x -> x .== (x+1::SWord8)) , goldenString "genBenchMark2" $ gen True (\x -> x .== (x+1::SWord8)) ] - where gen b f = do r <- generateSMTBenchmark b f - -- the first line is time-stamp, get rid of it so test - -- is repeatable - return $ unlines $ tail $ lines r + where gen b f = -- the first line is time-stamp, get rid of it so test is repeatable + unlines . tail . lines <$> generateSMTBenchmark b f diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 7.5 +Version: 7.6 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