diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,33 @@ * Hackage: * GitHub: -* Latest Hackage released version: 8.9, 2021-02-13 +* Latest Hackage released version: 8.11, 2021-03-09 + +### Version 8.11, 2021-03-09 + + * SBV now supports floating-point numbers with arbitrary exponent and + significand sizes. The type is `SFloatingPoint eb sb`, where `eb` + and `sb` are type-level naturals. In particular, SBV can now reason about + half-floats, which are used much more frequently in ML applications. Through + the LibBF binding, you can also use these concretely, so if you have a use + case for computing with floats, you can use SBV as a vehicle for doing so. + The exponent/significand sizes are limited to those supported by the LibBF + bindings, though the allowed range is rather large and should not be a limitation + in practice. (In particular, you'll most likely run out of memory before you + hit precision limits!) + + * We now support a separate `crackNum` parameter in model display. If set to True + (default is False), SBV will display numeric values of bounded integers, words, + and all floats (SDouble, SFloat, and the new SFloatingPoint) in models in detail, + showing how they are laid out in memory. Numbers follow the usual 2's-complement + notation if they are signed, bit-vectors if they are not signed, and the floats + follow the usual IEEE754 binary layout rules. Similarly, there's now a function + crack :: SBV a -> String that does the same for non-model printing contexts. + + * Changed the isNonModelVar config param to take a String (instead of Text). + Simplifies programming. + + * Changes to make SBV compile with GHC9.0. Thanks to Ryan Scott for the patch. ### Version 8.10, 2021-02-13 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -52,6 +52,9 @@ -- -- * 'SDouble': IEEE-754 double-precision floating point values -- +-- * 'SFloatingPoint': Generalized IEEE-754 floating point values, with user specified exponent and +-- mantissa widths. +-- -- * 'SChar', 'SString', 'RegExp': Characters, strings and regular expressions -- -- * 'SList': Symbolic lists (which can be nested) @@ -149,13 +152,18 @@ -- *** Signed bit-vectors , SInt8, SInt16, SInt32, SInt64, SInt, IntN -- *** Converting between fixed-size and arbitrary bitvectors - , IsNonZero, FromSized, ToSized, fromSized, toSized + , BVIsNonZero, FromSized, ToSized, fromSized, toSized -- ** Unbounded integers -- $unboundedLimitations , SInteger -- ** Floating point numbers -- $floatingPoints - , SFloat, SDouble + , ValidFloat, SFloat, SDouble + , SFloatingPoint, FloatingPoint + , SFPHalf, FPHalf + , SFPSingle, FPSingle + , SFPDouble, FPDouble + , SFPQuad, FPQuad -- ** Algebraic reals -- $algReals , SReal, AlgReal(..), sRealToSInteger, algRealToRational, RealPoint(..), realPoint, RationalCV(..) @@ -185,6 +193,11 @@ , sReal, sReal_ , sFloat, sFloat_ , sDouble, sDouble_ + , sFloatingPoint, sFloatingPoint_ + , sFPHalf, sFPHalf_ + , sFPSingle, sFPSingle_ + , sFPDouble, sFPDouble_ + , sFPQuad, sFPQuad_ , sChar, sChar_ , sString, sString_ , sList, sList_ @@ -202,6 +215,11 @@ , sReals , sFloats , sDoubles + , sFloatingPoints + , sFPHalfs + , sFPSingles + , sFPDoubles + , sFPQuads , sChars , sStrings , sLists @@ -237,9 +255,20 @@ , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ -- ** Conversion to/from floats , IEEEFloatConvertible(..) + -- ** Bit-pattern conversions - , sFloatAsSWord32, sWord32AsSFloat, sDoubleAsSWord64, sWord64AsSDouble, blastSFloat, blastSDouble + , sFloatAsSWord32, sWord32AsSFloat + , sDoubleAsSWord64, sWord64AsSDouble + , sFloatingPointAsSWord, sWordAsSFloatingPoint + -- ** Extracting bit patterns from floats + , blastSFloat + , blastSDouble + , blastSFloatingPoint + + -- ** Showing values in detail + , crack + -- * Enumerations -- $enumerations , mkSymbolicEnumeration @@ -363,6 +392,9 @@ forall, forall_, exists, exists_, solve, sBool, sBool_, sBools, sChar, sChar_, sChars, sDouble, sDouble_, sDoubles, sFloat, sFloat_, sFloats, + sFloatingPoint, sFloatingPoint_, sFloatingPoints, + sFPHalf, sFPHalf_, sFPHalfs, sFPSingle, sFPSingle_, sFPSingles, + sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads, sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s, sInt64, sInt64_, sInt64s, sInteger, sInteger_, sIntegers, sList, sList_, sLists, sTuple, sTuple_, sTuples, @@ -371,7 +403,10 @@ sWord32, sWord32_, sWord32s, sWord64, sWord64_, sWord64s, sMaybe, sMaybe_, sMaybes, sEither, sEither_, sEithers, sSet, sSet_, sSets) import Data.SBV.Core.Sized hiding (sWord, sWord_, sWords, sInt, sInt_, sInts) +import Data.SBV.Core.Kind +import Data.SBV.Core.SizedFloats + import Data.SBV.Core.Floating import Data.SBV.Core.Symbolic (MonadSymbolic(..), SymbolicT) @@ -396,6 +431,14 @@ import Data.SBV.SMT.Utils (SBVException(..)) import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..)) + +import qualified Data.SBV.Utils.CrackNum as CN + +-- | Show a value in detailed (cracked) form, if possible. +-- This makes most sense with numbers, and especially floating-point types. +crack :: SBV a -> String +crack (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv = s +crack (SBV sv) = show sv -- Haddock section documentation {- $progIntro diff --git a/Data/SBV/Char.hs b/Data/SBV/Char.hs --- a/Data/SBV/Char.hs +++ b/Data/SBV/Char.hs @@ -13,11 +13,12 @@ -- symbolic-strings when working with symbolic characters -- and strings. -- --- Note that currently 'SChar' type only covers Latin1 (i.e., the first 256 --- characters), as opposed to Haskell's Unicode character support. However, --- there is a pending SMTLib proposal to extend this set to Unicode, at --- which point we will update these functions to match the implementations. --- For details, see: +-- 'SChar' type only covers all unicode characters, following the specification +-- in . +-- However, some of the recognizers only support the Latin1 subset, suffixed +-- by @L1@. The reason for this is that there is no performant way of performing +-- these functions for the entire unicode set. As SMTLib's capabilities increase, +-- we will provide full unicode versions as well. ----------------------------------------------------------------------------- {-# LANGUAGE OverloadedStrings #-} @@ -108,7 +109,8 @@ -- | Lift a char function to a symbolic version. If the given char is -- not in the class recognized by predicate, the output is the same as the input. --- Only works for the Latin1 set, i.e., the first 256 characters. +-- Only works for the Latin1 set, i.e., the first 256 characters. If the given +-- character is outside this range, it's returned unchanged. liftFunL1 :: (Char -> Char) -> SChar -> SChar liftFunL1 f c = walk kernel where kernel = [g | g <- map C.chr [0 .. 255], g /= f g] diff --git a/Data/SBV/Client/BaseIO.hs b/Data/SBV/Client/BaseIO.hs --- a/Data/SBV/Client/BaseIO.hs +++ b/Data/SBV/Client/BaseIO.hs @@ -25,10 +25,12 @@ import Data.SBV.Core.Data (HasKind, Kind, Outputtable, Penalty, SymArray, SymVal, SBool, SBV, SChar, SDouble, SFloat, + SFPHalf, SFPSingle, SFPDouble, SFPQuad, SFloatingPoint, SInt8, SInt16, SInt32, SInt64, SInteger, SList, SReal, SString, SV, SWord8, SWord16, SWord32, SWord64, SEither, SMaybe, SSet) -import Data.SBV.Core.Sized (SInt, SWord, IntN, WordN, IsNonZero) +import Data.SBV.Core.Sized (SInt, SWord, IntN, WordN) +import Data.SBV.Core.Kind (BVIsNonZero, ValidFloat) import Data.SBV.Core.Model (Metric(..), SymTuple) import Data.SBV.Core.Symbolic (Objective, OptimizeStyle, Result, VarContext, Symbolic, SBVRunMode, SMTConfig, SVal) @@ -448,19 +450,19 @@ -- | Declare a named 'SWord' -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord' -sWord :: (KnownNat n, IsNonZero n) => String -> Symbolic (SWord n) +sWord :: (KnownNat n, BVIsNonZero n) => String -> Symbolic (SWord n) sWord = Trans.sWord -- | Declare an unnamed 'SWord' -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWord_' -sWord_ :: (KnownNat n, IsNonZero n) => Symbolic (SWord n) +sWord_ :: (KnownNat n, BVIsNonZero n) => Symbolic (SWord n) sWord_ = Trans.sWord_ -- | Declare a list of 'SWord8's -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sWords' -sWords :: (KnownNat n, IsNonZero n) => [String] -> Symbolic [SWord n] +sWords :: (KnownNat n, BVIsNonZero n) => [String] -> Symbolic [SWord n] sWords = Trans.sWords -- | Declare a named 'SInt8' @@ -538,19 +540,19 @@ -- | Declare a named 'SInt' -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt' -sInt :: (KnownNat n, IsNonZero n) => String -> Symbolic (SInt n) +sInt :: (KnownNat n, BVIsNonZero n) => String -> Symbolic (SInt n) sInt = Trans.sInt -- | Declare an unnamed 'SInt' -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInt_' -sInt_ :: (KnownNat n, IsNonZero n) => Symbolic (SInt n) +sInt_ :: (KnownNat n, BVIsNonZero n) => Symbolic (SInt n) sInt_ = Trans.sInt_ -- | Declare a list of 'SInt's -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sInts' -sInts :: (KnownNat n, IsNonZero n) => [String] -> Symbolic [SInt n] +sInts :: (KnownNat n, BVIsNonZero n) => [String] -> Symbolic [SInt n] sInts = Trans.sInts -- | Declare a named 'SInteger' @@ -624,6 +626,96 @@ -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sDoubles' sDoubles :: [String] -> Symbolic [SDouble] sDoubles = Trans.sDoubles + +-- | Declare a named 'SFloatingPoint eb sb' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloatingPoint' +sFloatingPoint :: ValidFloat eb sb => String -> Symbolic (SFloatingPoint eb sb) +sFloatingPoint = Trans.sFloatingPoint + +-- | Declare an unnamed 'SFloatingPoint' @eb@ @sb@ +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloatingPoint_' +sFloatingPoint_ :: ValidFloat eb sb => Symbolic (SFloatingPoint eb sb) +sFloatingPoint_ = Trans.sFloatingPoint_ + +-- | Declare a list of 'SFloatingPoint' @eb@ @sb@'s +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFloatingPoints' +sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb] +sFloatingPoints = Trans.sFloatingPoints + +-- | Declare a named 'SFPHalf' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPHalf' +sFPHalf :: String -> Symbolic SFPHalf +sFPHalf = Trans.sFPHalf + +-- | Declare an unnamed 'SFPHalf' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPHalf_' +sFPHalf_ :: Symbolic SFPHalf +sFPHalf_ = Trans.sFPHalf_ + +-- | Declare a list of 'SFPHalf's +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPHalfs' +sFPHalfs :: [String] -> Symbolic [SFPHalf] +sFPHalfs = Trans.sFPHalfs + +-- | Declare a named 'SFPSingle' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPSingle' +sFPSingle :: String -> Symbolic SFPSingle +sFPSingle = Trans.sFPSingle + +-- | Declare an unnamed 'SFPSingle' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPSingle_' +sFPSingle_ :: Symbolic SFPSingle +sFPSingle_ = Trans.sFPSingle_ + +-- | Declare a list of 'SFPSingle's +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPSingles' +sFPSingles :: [String] -> Symbolic [SFPSingle] +sFPSingles = Trans.sFPSingles + +-- | Declare a named 'SFPDouble' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPDouble' +sFPDouble :: String -> Symbolic SFPDouble +sFPDouble = Trans.sFPDouble + +-- | Declare an unnamed 'SFPDouble' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPDouble_' +sFPDouble_ :: Symbolic SFPDouble +sFPDouble_ = Trans.sFPDouble_ + +-- | Declare a list of 'SFPDouble's +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPDoubles' +sFPDoubles :: [String] -> Symbolic [SFPDouble] +sFPDoubles = Trans.sFPDoubles + +-- | Declare a named 'SFPQuad' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPQuad' +sFPQuad :: String -> Symbolic SFPQuad +sFPQuad = Trans.sFPQuad + +-- | Declare an unnamed 'SFPQuad' +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPQuad_' +sFPQuad_ :: Symbolic SFPQuad +sFPQuad_ = Trans.sFPQuad_ + +-- | Declare a list of 'SFPQuad's +-- +-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sFPQuads' +sFPQuads :: [String] -> Symbolic [SFPQuad] +sFPQuads = Trans.sFPQuads -- | Declare a named 'SChar' -- 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 @@ -201,6 +201,7 @@ KDouble -> specF CgDouble KString -> text "%s" KChar -> text "%c" + KFP{} -> die "arbitrary float sort" KList k -> die $ "list sort: " ++ show k KSet k -> die $ "set sort: " ++ show k KUserSort s _ -> die $ "user sort: " ++ s @@ -520,6 +521,7 @@ len KBool = 5 -- SBool len (KBounded False n) = 5 + length (show n) -- SWordN len (KBounded True n) = 4 + length (show n) -- SIntN + len KFP{} = die "Arbitrary float." len (KList s) = die $ "List sort: " ++ show s len (KSet s) = die $ "Set sort: " ++ show s len (KTuple s) = die $ "Tuple sort: " ++ show s @@ -776,6 +778,7 @@ KReal -> die "array index with real value" KFloat -> die "array index with float value" KDouble -> die "array index with double value" + KFP{} -> die "array index with arbitrary float value" KString -> die "array index with string value" KChar -> die "array index with character value" KUnbounded -> case cgInteger cfg of 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 @@ -87,23 +87,25 @@ -- Collect strings appearing, used in 'getOption' only stringsOf :: SExpr -> [String] -stringsOf (ECon s) = [s] -stringsOf (ENum (i, _)) = [show i] -stringsOf (EReal r) = [show r] -stringsOf (EFloat f) = [show f] -stringsOf (EDouble d) = [show d] -stringsOf (EApp ss) = concatMap stringsOf ss +stringsOf (ECon s) = [s] +stringsOf (ENum (i, _)) = [show i] +stringsOf (EReal r) = [show r] +stringsOf (EFloat f) = [show f] +stringsOf (EFloatingPoint f) = [show f] +stringsOf (EDouble d) = [show d] +stringsOf (EApp ss) = concatMap stringsOf ss -- Sort of a light-hearted show for SExprs, for better consumption at the user level. serialize :: Bool -> SExpr -> String serialize removeQuotes = go - where go (ECon s) = if removeQuotes then unQuote s else s - go (ENum (i, _)) = shNN i - go (EReal r) = shNN r - go (EFloat f) = shNN f - go (EDouble d) = shNN d - go (EApp [x]) = go x - go (EApp ss) = "(" ++ unwords (map go ss) ++ ")" + where go (ECon s) = if removeQuotes then unQuote s else s + go (ENum (i, _)) = shNN i + go (EReal r) = shNN r + go (EFloat f) = shNN f + go (EDouble d) = shNN d + go (EFloatingPoint f) = show f + go (EApp [x]) = go x + go (EApp ss) = "(" ++ unwords (map go ss) ++ ")" -- be careful with negative number printing in SMT-Lib.. shNN :: (Show a, Num a, Ord a) => a -> String @@ -341,12 +343,12 @@ let name = fst . snd removeSV = snd - prepare = S.unstableSort . S.filter (not . isNonModelVar cfg . name) + prepare = S.unstableSort . S.filter (not . isNonModelVar cfg . T.unpack . name) assocs = S.fromList (sortOn fst obsvs) <> fmap removeSV (prepare inputAssocs) -- collect UIs, and UI functions if requested - let uiFuns = [ui | ui@(T.pack -> nm, SBVType as) <- uis, length as > 1, satTrackUFs cfg, not (isNonModelVar cfg nm)] -- functions have at least two things in their type! - uiRegs = [ui | ui@(T.pack -> nm, SBVType as) <- uis, length as == 1, not (isNonModelVar cfg nm)] + let uiFuns = [ui | ui@(nm, SBVType as) <- uis, length as > 1, satTrackUFs cfg, not (isNonModelVar cfg nm)] -- functions have at least two things in their type! + uiRegs = [ui | ui@(nm, SBVType as) <- uis, length as == 1, not (isNonModelVar cfg nm)] -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out -- as cex's tend to get larger 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 @@ -88,9 +88,10 @@ , getUserName', Name, CnstMap ) -import Data.SBV.Core.AlgReals (mergeAlgReals, AlgReal(..), RealPoint(..)) -import Data.SBV.Core.Kind (smtType, hasUninterpretedSorts) -import Data.SBV.Core.Operations (svNot, svNotEqual, svOr) +import Data.SBV.Core.AlgReals (mergeAlgReals, AlgReal(..), RealPoint(..)) +import Data.SBV.Core.SizedFloats (fpZero, fpFromInteger, fpFromFloat, fpFromDouble) +import Data.SBV.Core.Kind (smtType, hasUninterpretedSorts) +import Data.SBV.Core.Operations (svNot, svNotEqual, svOr) import Data.SBV.SMT.SMT (showModel, parseCVs, SatModel, AllSatResult(..)) import Data.SBV.SMT.SMTLib (toIncSMTLib, toSMTLib) @@ -728,6 +729,7 @@ cvt (KUserSort _ ui) = uninterp ui cvt KFloat = Just $ CFloat 0 cvt KDouble = Just $ CDouble 0 + cvt (KFP eb sb) = Just $ CFP (fpZero False eb sb) cvt KChar = Just $ CChar '\NUL' -- why not? cvt KString = Just $ CString "" cvt (KList _) = Just $ CList [] @@ -748,46 +750,52 @@ -- | Recover a given solver-printed value with a possible interpretation recoverKindedValue :: Kind -> SExpr -> Maybe CV recoverKindedValue k e = case k of - KBool | ENum (i, _) <- e -> Just $ mkConstCV k i - | True -> Nothing + KBool | ENum (i, _) <- e -> Just $ mkConstCV k i + | True -> Nothing - KBounded{} | ENum (i, _) <- e -> Just $ mkConstCV k i - | True -> Nothing + KBounded{} | ENum (i, _) <- e -> Just $ mkConstCV k i + | True -> Nothing - KUnbounded | ENum (i, _) <- e -> Just $ mkConstCV k i - | True -> Nothing + KUnbounded | ENum (i, _) <- e -> Just $ mkConstCV k i + | True -> Nothing - KReal | ENum (i, _) <- e -> Just $ mkConstCV k i - | EReal i <- e -> Just $ CV KReal (CAlgReal i) - | True -> interpretInterval e + KReal | ENum (i, _) <- e -> Just $ mkConstCV k i + | EReal i <- e -> Just $ CV KReal (CAlgReal i) + | True -> interpretInterval e - KUserSort{} | ECon s <- e -> Just $ CV k $ CUserSort (getUIIndex k s, s) - | True -> Nothing + KUserSort{} | ECon s <- e -> Just $ CV k $ CUserSort (getUIIndex k s, s) + | True -> Nothing - KFloat | ENum (i, _) <- e -> Just $ mkConstCV k i - | EFloat i <- e -> Just $ CV KFloat (CFloat i) - | True -> Nothing + KFloat | ENum (i, _) <- e -> Just $ mkConstCV k i + | EFloat i <- e -> Just $ CV KFloat (CFloat i) + | True -> Nothing - KDouble | ENum (i, _) <- e -> Just $ mkConstCV k i - | EDouble i <- e -> Just $ CV KDouble (CDouble i) - | True -> Nothing + KDouble | ENum (i, _) <- e -> Just $ mkConstCV k i + | EDouble i <- e -> Just $ CV KDouble (CDouble i) + | True -> Nothing - KChar | ECon s <- e -> Just $ CV KChar $ CChar $ interpretChar s - | True -> Nothing + KFP eb sb | ENum (i, _) <- e -> Just $ CV k $ CFP $ fpFromInteger eb sb i + | EFloat f <- e -> Just $ CV k $ CFP $ fpFromFloat eb sb f + | EDouble d <- e -> Just $ CV k $ CFP $ fpFromDouble eb sb d + | EFloatingPoint c <- e -> Just $ CV k $ CFP c + | True -> Nothing - KString | ECon s <- e -> Just $ CV KString $ CString $ interpretString s - | True -> Nothing + KChar | ECon s <- e -> Just $ CV KChar $ CChar $ interpretChar s + | True -> Nothing - KList ek -> Just $ CV k $ CList $ interpretList ek e + KString | ECon s <- e -> Just $ CV KString $ CString $ interpretString s + | True -> Nothing - KSet ek -> Just $ CV k $ CSet $ interpretSet ek e + KList ek -> Just $ CV k $ CList $ interpretList ek e - KTuple{} -> Just $ CV k $ CTuple $ interpretTuple e + KSet ek -> Just $ CV k $ CSet $ interpretSet ek e - KMaybe{} -> Just $ CV k $ CMaybe $ interpretMaybe k e + KTuple{} -> Just $ CV k $ CTuple $ interpretTuple e - KEither{} -> Just $ CV k $ CEither $ interpretEither k e + KMaybe{} -> Just $ CV k $ CMaybe $ interpretMaybe k e + KEither{} -> Just $ CV k $ CEither $ interpretEither k e + where getUIIndex (KUserSort _ (Just xs)) i = i `elemIndex` xs getUIIndex _ _ = Nothing @@ -1106,11 +1114,11 @@ -- Functions have at least two kinds in their type and all components must be "interpreted" let allUiFuns = [u | satTrackUFs cfg -- config says consider UIFs , u@(nm, SBVType as) <- allUninterpreteds, length as > 1 -- get the function ones - , not (isNonModelVar cfg (T.pack nm)) -- make sure they aren't explicitly ignored + , not (isNonModelVar cfg nm) -- make sure they aren't explicitly ignored ] allUiRegs = [u | u@(nm, SBVType as) <- allUninterpreteds, length as == 1 -- non-function ones - , not (isNonModelVar cfg (T.pack nm)) -- make sure not ignored + , not (isNonModelVar cfg nm) -- make sure not ignored ] -- We can only "allSat" if all component types themselves are interpreted. (Otherwise @@ -1151,7 +1159,7 @@ vars = let mkSVal :: NamedSymVar -> (SVal, NamedSymVar) mkSVal nm@(getSV -> sv) = (SVal (kindOf sv) (Right (cache (const (return sv)))), nm) - ignored n = isNonModelVar cfg n || "__internal_sbv" `T.isPrefixOf` n + ignored n = isNonModelVar cfg (T.unpack n) || "__internal_sbv" `T.isPrefixOf` n in fmap (mkSVal . namedSymVar) . S.filter (not . ignored . getUserName . namedSymVar) @@ -1257,8 +1265,10 @@ interpretedEqs :: [SVal] interpretedEqs = [mkNotEq (kindOf sv) sv (SVal (kindOf sv) (Left cv)) | (sv, cv) <- interpretedRegUiSVs <> F.toList interpreteds] where mkNotEq k a b - | isDouble k || isFloat k = svNot (a `fpNotEq` b) - | True = a `svNotEqual` b + | isDouble k || isFloat k || isFP k + = svNot (a `fpNotEq` b) + | True + = a `svNotEqual` b fpNotEq a b = SVal KBool $ Right $ cache r where r st = do sva <- svToSV st a diff --git a/Data/SBV/Core/AlgReals.hs b/Data/SBV/Core/AlgReals.hs --- a/Data/SBV/Core/AlgReals.hs +++ b/Data/SBV/Core/AlgReals.hs @@ -235,7 +235,7 @@ data RationalCV = RatIrreducible AlgReal -- ^ Root of a polynomial, cannot be reduced | RatExact Rational -- ^ An exact rational | RatApprox Rational -- ^ An approximated value - | RatInterval (RealPoint Rational) (RealPoint Rational) -- ^ Interval. If bool is 'True' then closed, otherwise open. + | RatInterval (RealPoint Rational) (RealPoint Rational) -- ^ Interval. Can be open/closed on both ends. deriving Show -- | Convert an 'AlgReal' to a 'Rational'. If the 'AlgReal' is exact, then you get a 'Left' value. Otherwise, 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 @@ -11,6 +11,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE Rank2Types #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -28,6 +29,7 @@ import Data.SBV.Core.Kind import Data.SBV.Core.AlgReals +import Data.SBV.Core.SizedFloats import Data.Proxy @@ -69,18 +71,19 @@ kindOf _ = KSet (kindOf (Proxy @a)) -- | A constant value -data CVal = CAlgReal !AlgReal -- ^ Algebraic real - | CInteger !Integer -- ^ Bit-vector/unbounded integer - | CFloat !Float -- ^ Float - | CDouble !Double -- ^ Double - | CChar !Char -- ^ Character - | CString !String -- ^ String - | CList ![CVal] -- ^ List - | CSet !(RCSet CVal) -- ^ Set. Can be regular or complemented. - | CUserSort !(Maybe Int, String) -- ^ Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations - | CTuple ![CVal] -- ^ Tuple - | CMaybe !(Maybe CVal) -- ^ Maybe - | CEither !(Either CVal CVal) -- ^ Disjoint union +data CVal = CAlgReal !AlgReal -- ^ Algebraic real + | CInteger !Integer -- ^ Bit-vector/unbounded integer + | CFloat !Float -- ^ Float + | CDouble !Double -- ^ Double + | CFP !FP -- ^ Arbitrary float + | CChar !Char -- ^ Character + | CString !String -- ^ String + | CList ![CVal] -- ^ List + | CSet !(RCSet CVal) -- ^ Set. Can be regular or complemented. + | CUserSort !(Maybe Int, String) -- ^ Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations + | CTuple ![CVal] -- ^ Tuple + | CMaybe !(Maybe CVal) -- ^ Maybe + | CEither !(Either CVal CVal) -- ^ Disjoint union -- | Assign a rank to constant values, this is structural and helps with ordering cvRank :: CVal -> Int @@ -88,14 +91,15 @@ cvRank CInteger {} = 1 cvRank CFloat {} = 2 cvRank CDouble {} = 3 -cvRank CChar {} = 4 -cvRank CString {} = 5 -cvRank CList {} = 6 -cvRank CSet {} = 7 -cvRank CUserSort {} = 8 -cvRank CTuple {} = 9 -cvRank CMaybe {} = 10 -cvRank CEither {} = 11 +cvRank CFP {} = 4 +cvRank CChar {} = 5 +cvRank CString {} = 6 +cvRank CList {} = 7 +cvRank CSet {} = 8 +cvRank CUserSort {} = 9 +cvRank CTuple {} = 10 +cvRank CMaybe {} = 11 +cvRank CEither {} = 12 -- | Eq instance for CVVal. Note that we cannot simply derive Eq/Ord, since CVAlgReal doesn't have proper -- instances for these when values are infinitely precise reals. However, we do @@ -125,18 +129,19 @@ -- | Ord instance for VWVal. Same comments as the 'Eq' instance why this cannot be derived. instance Ord CVal where - CAlgReal a `compare` CAlgReal b = a `algRealStructuralCompare` b - CInteger a `compare` CInteger b = a `compare` b - CFloat a `compare` CFloat b = a `fpCompareObjectH` b - CDouble a `compare` CDouble b = a `fpCompareObjectH` b - CChar a `compare` CChar b = a `compare` b - CString a `compare` CString b = a `compare` b - CList a `compare` CList b = a `compare` b - CSet a `compare` CSet b = a `compareRCSet` b - CUserSort a `compare` CUserSort b = a `compare` b - CTuple a `compare` CTuple b = a `compare` b - CMaybe a `compare` CMaybe b = a `compare` b - CEither a `compare` CEither b = a `compare` b + CAlgReal a `compare` CAlgReal b = a `algRealStructuralCompare` b + CInteger a `compare` CInteger b = a `compare` b + CFloat a `compare` CFloat b = a `fpCompareObjectH` b + CDouble a `compare` CDouble b = a `fpCompareObjectH` b + CFP a `compare` CFP b = a `fprCompareObject` b + CChar a `compare` CChar b = a `compare` b + CString a `compare` CString b = a `compare` b + CList a `compare` CList b = a `compare` b + CSet a `compare` CSet b = a `compareRCSet` b + CUserSort a `compare` CUserSort b = a `compare` b + CTuple a `compare` CTuple b = a `compare` b + CMaybe a `compare` CMaybe b = a `compare` b + CEither a `compare` CEither b = a `compare` b a `compare` b = let ra = cvRank a rb = cvRank b in if ra == rb @@ -271,6 +276,7 @@ -> (Integer -> b) -> (Float -> b) -> (Double -> b) + -> (FP -> b) -> (Char -> b) -> (String -> b) -> ((Maybe Int, String) -> b) @@ -281,24 +287,26 @@ -> (Either CVal CVal -> b) -> CV -> b -liftCV f _ _ _ _ _ _ _ _ _ _ _ (CV _ (CAlgReal v)) = f v -liftCV _ f _ _ _ _ _ _ _ _ _ _ (CV _ (CInteger v)) = f v -liftCV _ _ f _ _ _ _ _ _ _ _ _ (CV _ (CFloat v)) = f v -liftCV _ _ _ f _ _ _ _ _ _ _ _ (CV _ (CDouble v)) = f v -liftCV _ _ _ _ f _ _ _ _ _ _ _ (CV _ (CChar v)) = f v -liftCV _ _ _ _ _ f _ _ _ _ _ _ (CV _ (CString v)) = f v -liftCV _ _ _ _ _ _ f _ _ _ _ _ (CV _ (CUserSort v)) = f v -liftCV _ _ _ _ _ _ _ f _ _ _ _ (CV _ (CList v)) = f v -liftCV _ _ _ _ _ _ _ _ f _ _ _ (CV _ (CSet v)) = f v -liftCV _ _ _ _ _ _ _ _ _ f _ _ (CV _ (CTuple v)) = f v -liftCV _ _ _ _ _ _ _ _ _ _ f _ (CV _ (CMaybe v)) = f v -liftCV _ _ _ _ _ _ _ _ _ _ _ f (CV _ (CEither v)) = f v +liftCV f _ _ _ _ _ _ _ _ _ _ _ _ (CV _ (CAlgReal v)) = f v +liftCV _ f _ _ _ _ _ _ _ _ _ _ _ (CV _ (CInteger v)) = f v +liftCV _ _ f _ _ _ _ _ _ _ _ _ _ (CV _ (CFloat v)) = f v +liftCV _ _ _ f _ _ _ _ _ _ _ _ _ (CV _ (CDouble v)) = f v +liftCV _ _ _ _ f _ _ _ _ _ _ _ _ (CV _ (CFP v)) = f v +liftCV _ _ _ _ _ f _ _ _ _ _ _ _ (CV _ (CChar v)) = f v +liftCV _ _ _ _ _ _ f _ _ _ _ _ _ (CV _ (CString v)) = f v +liftCV _ _ _ _ _ _ _ f _ _ _ _ _ (CV _ (CUserSort v)) = f v +liftCV _ _ _ _ _ _ _ _ f _ _ _ _ (CV _ (CList v)) = f v +liftCV _ _ _ _ _ _ _ _ _ f _ _ _ (CV _ (CSet v)) = f v +liftCV _ _ _ _ _ _ _ _ _ _ f _ _ (CV _ (CTuple v)) = f v +liftCV _ _ _ _ _ _ _ _ _ _ _ f _ (CV _ (CMaybe v)) = f v +liftCV _ _ _ _ _ _ _ _ _ _ _ _ f (CV _ (CEither v)) = f v -- | Lift a binary function through a 'CV'. liftCV2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) + -> (FP -> FP -> b) -> (Char -> Char -> b) -> (String -> String -> b) -> ([CVal] -> [CVal] -> b) @@ -307,68 +315,73 @@ -> (Either CVal CVal -> Either CVal CVal -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CV -> CV -> b -liftCV2 r i f d c s u v m e w x y = case (cvVal x, cvVal y) of - (CAlgReal a, CAlgReal b) -> r a b - (CInteger a, CInteger b) -> i a b - (CFloat a, CFloat b) -> f a b - (CDouble a, CDouble b) -> d a b - (CChar a, CChar b) -> c a b - (CString a, CString b) -> s a b - (CList a, CList b) -> u a b - (CTuple a, CTuple b) -> v a b - (CMaybe a, CMaybe b) -> m a b - (CEither a, CEither b) -> e a b - (CUserSort a, CUserSort b) -> w a b - _ -> error $ "SBV.liftCV2: impossible, incompatible args received: " ++ show (x, y) +liftCV2 r i f d af c s u v m e w x y = case (cvVal x, cvVal y) of + (CAlgReal a, CAlgReal b) -> r a b + (CInteger a, CInteger b) -> i a b + (CFloat a, CFloat b) -> f a b + (CDouble a, CDouble b) -> d a b + (CFP a, CFP b) -> af a b + (CChar a, CChar b) -> c a b + (CString a, CString b) -> s a b + (CList a, CList b) -> u a b + (CTuple a, CTuple b) -> v a b + (CMaybe a, CMaybe b) -> m a b + (CEither a, CEither b) -> e a b + (CUserSort a, CUserSort b) -> w a b + _ -> error $ "SBV.liftCV2: impossible, incompatible args received: " ++ show (x, y) -- | Map a unary function through a 'CV'. mapCV :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) + -> (FP -> FP) -> (Char -> Char) -> (String -> String) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CV -> CV -mapCV r i f d c s u x = normCV $ CV (kindOf x) $ case cvVal x of - CAlgReal a -> CAlgReal (r a) - CInteger a -> CInteger (i a) - CFloat a -> CFloat (f a) - CDouble a -> CDouble (d a) - CChar a -> CChar (c a) - CString a -> CString (s a) - CUserSort a -> CUserSort (u a) - CList{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with lists!" - CSet{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with sets!" - CTuple{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with tuples!" - CMaybe{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with maybe!" - CEither{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with either!" +mapCV r i f d af c s u x = normCV $ CV (kindOf x) $ case cvVal x of + CAlgReal a -> CAlgReal (r a) + CInteger a -> CInteger (i a) + CFloat a -> CFloat (f a) + CDouble a -> CDouble (d a) + CFP a -> CFP (af a) + CChar a -> CChar (c a) + CString a -> CString (s a) + CUserSort a -> CUserSort (u a) + CList{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with lists!" + CSet{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with sets!" + CTuple{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with tuples!" + CMaybe{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with maybe!" + CEither{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with either!" -- | Map a binary function through a 'CV'. mapCV2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) + -> (FP -> FP -> FP) -> (Char -> Char -> Char) -> (String -> String -> String) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CV -> CV -> CV -mapCV2 r i f d c s u x y = case (cvSameType x y, cvVal x, cvVal y) of - (True, CAlgReal a, CAlgReal b) -> normCV $ CV (kindOf x) (CAlgReal (r a b)) - (True, CInteger a, CInteger b) -> normCV $ CV (kindOf x) (CInteger (i a b)) - (True, CFloat a, CFloat b) -> normCV $ CV (kindOf x) (CFloat (f a b)) - (True, CDouble a, CDouble b) -> normCV $ CV (kindOf x) (CDouble (d a b)) - (True, CChar a, CChar b) -> normCV $ CV (kindOf x) (CChar (c a b)) - (True, CString a, CString b) -> normCV $ CV (kindOf x) (CString (s a b)) - (True, CUserSort a, CUserSort b) -> normCV $ CV (kindOf x) (CUserSort (u a b)) - (True, CList{}, CList{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with lists!" - (True, CTuple{}, CTuple{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with tuples!" - (True, CMaybe{}, CMaybe{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with maybes!" - (True, CEither{}, CEither{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with eithers!" - _ -> error $ "SBV.mapCV2: impossible, incompatible args received: " ++ show (x, y) +mapCV2 r i f d af c s u x y = case (cvSameType x y, cvVal x, cvVal y) of + (True, CAlgReal a, CAlgReal b) -> normCV $ CV (kindOf x) (CAlgReal (r a b)) + (True, CInteger a, CInteger b) -> normCV $ CV (kindOf x) (CInteger (i a b)) + (True, CFloat a, CFloat b) -> normCV $ CV (kindOf x) (CFloat (f a b)) + (True, CDouble a, CDouble b) -> normCV $ CV (kindOf x) (CDouble (d a b)) + (True, CFP a, CFP b) -> normCV $ CV (kindOf x) (CFP (af a b)) + (True, CChar a, CChar b) -> normCV $ CV (kindOf x) (CChar (c a b)) + (True, CString a, CString b) -> normCV $ CV (kindOf x) (CString (s a b)) + (True, CUserSort a, CUserSort b) -> normCV $ CV (kindOf x) (CUserSort (u a b)) + (True, CList{}, CList{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with lists!" + (True, CTuple{}, CTuple{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with tuples!" + (True, CMaybe{}, CMaybe{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with maybes!" + (True, CEither{}, CEither{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with eithers!" + _ -> error $ "Data.SBV.mapCV2: impossible, incompatible args received: " ++ show (x, y) -- | Show instance for 'CV'. instance Show CV where @@ -382,7 +395,7 @@ -- | Show a CV, with kind info if bool is True showCV :: Bool -> CV -> String showCV shk w | isBoolean w = show (cvToBool w) ++ (if shk then " :: Bool" else "") -showCV shk w = liftCV show show show show show show snd shL shS shT shMaybe shEither w ++ kInfo +showCV shk w = liftCV show show show show show show show snd shL shS shT shMaybe shEither w ++ kInfo where kw = kindOf w kInfo | shk = " :: " ++ showBaseKind kw @@ -439,7 +452,8 @@ mkConstCV KReal a = normCV $ CV KReal (CAlgReal (fromInteger (toInteger a))) mkConstCV KFloat a = normCV $ CV KFloat (CFloat (fromInteger (toInteger a))) mkConstCV KDouble a = normCV $ CV KDouble (CDouble (fromInteger (toInteger a))) -mkConstCV KChar a = error $ "Unexpected call to mkConstCV (Char) with value: " ++ show (toInteger a) +mkConstCV k@KFP{} a = normCV $ CV k (CFP (fromInteger (toInteger a))) +mkConstCV KChar a = error $ "Unexpected call to mkConstCV (Char) with value: " ++ show (toInteger a) mkConstCV KString a = error $ "Unexpected call to mkConstCV (String) with value: " ++ show (toInteger a) mkConstCV (KUserSort s _) a = error $ "Unexpected call to mkConstCV with user kind: " ++ s ++ " with value: " ++ show (toInteger a) mkConstCV k@KList{} a = error $ "Unexpected call to mkConstCV (" ++ show k ++ ") with value: " ++ show (toInteger a) @@ -458,6 +472,14 @@ KReal -> CAlgReal <$> randomIO KFloat -> CFloat <$> randomIO KDouble -> CDouble <$> randomIO + + -- Rather bad, but OK + KFP eb sb -> do sgn <- randomRIO (0 :: Integer, 1) + let sign = sgn == 1 + e <- randomRIO (0 :: Integer, 2^eb-1) + s <- randomRIO (0 :: Integer, 2^sb-1) + pure $ CFP $ fpFromRawRep sign (e, eb) (s, sb) + -- TODO: KString/KChar currently only go for 0..255; include unicode? KString -> do l <- randomRIO (0, 100) CString <$> replicateM l (chr <$> randomRIO (0, 255)) 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 @@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} @@ -26,7 +27,9 @@ module Data.SBV.Core.Data ( SBool, SWord8, SWord16, SWord32, SWord64 - , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble, SChar, SString, SList + , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble + , SFloatingPoint, SFPHalf, SFPSingle, SFPDouble, SFPQuad + , SChar, SString, SList , SEither, SMaybe , STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8 , RCSet(..), SSet @@ -58,6 +61,8 @@ , QueryState(..), QueryT(..), SMTProblem(..) ) where +import GHC.TypeLits + import GHC.Generics (Generic) import GHC.Exts (IsList(..)) @@ -79,6 +84,7 @@ import System.Random import Data.SBV.Core.AlgReals +import Data.SBV.Core.SizedFloats import Data.SBV.Core.Kind import Data.SBV.Core.Concrete import Data.SBV.Core.Symbolic @@ -142,6 +148,21 @@ -- | IEEE-754 double-precision floating point numbers type SDouble = SBV Double +-- | A symbolic arbitrary precision floating point value +type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb) + +-- | A symbolic half-precision float +type SFPHalf = SBV FPHalf + +-- | A symbolic single-precision float +type SFPSingle = SBV FPSingle + +-- | A symbolic double-precision float +type SFPDouble = SBV FPDouble + +-- | A symbolic quad-precision float +type SFPQuad = SBV FPQuad + -- | A symbolic character. Note that this is the full unicode character set. -- see: -- for details. @@ -211,13 +232,13 @@ infinity :: Floating a => a infinity = 1/0 --- | Symbolic variant of Not-A-Number. This value will inhabit both --- 'SDouble' and 'SFloat'. +-- | Symbolic variant of Not-A-Number. This value will inhabit +-- 'SFloat', 'SDouble' and 'SFloatingPoint'. types. sNaN :: (Floating a, SymVal a) => SBV a sNaN = literal nan -- | Symbolic variant of infinity. This value will inhabit both --- 'SDouble' and 'SFloat'. +-- 'SFloat', 'SDouble' and 'SFloatingPoint'. types. sInfinity :: (Floating a, SymVal a) => SBV a sInfinity = literal infinity diff --git a/Data/SBV/Core/Floating.hs b/Data/SBV/Core/Floating.hs --- a/Data/SBV/Core/Floating.hs +++ b/Data/SBV/Core/Floating.hs @@ -10,36 +10,50 @@ ----------------------------------------------------------------------------- {-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} module Data.SBV.Core.Floating ( IEEEFloating(..), IEEEFloatConvertible(..) - , sFloatAsSWord32, sDoubleAsSWord64, sWord32AsSFloat, sWord64AsSDouble - , blastSFloat, blastSDouble - , sFloatAsComparableSWord32, sDoubleAsComparableSWord64 + , sFloatAsSWord32, sDoubleAsSWord64, sFloatingPointAsSWord + , sWord32AsSFloat, sWord64AsSDouble, sWordAsSFloatingPoint + , blastSFloat, blastSDouble, blastSFloatingPoint + , sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord + , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint + , ) where -import qualified Data.Numbers.CrackNum as CN (wordToFloat, wordToDouble, floatToWord, doubleToWord) - -import Data.Int (Int8, Int16, Int32, Int64) -import Data.Word (Word8, Word16, Word32, Word64) +import Data.Bits (testBit) +import Data.Int (Int8, Int16, Int32, Int64) +import Data.Word (Word8, Word16, Word32, Word64) import Data.Proxy import Data.SBV.Core.AlgReals (isExactRational) +import Data.SBV.Core.Sized +import Data.SBV.Core.SizedFloats import Data.SBV.Core.Data +import Data.SBV.Core.Kind import Data.SBV.Core.Model import Data.SBV.Core.Symbolic (addSValOptGoal) import Data.SBV.Utils.Numeric +import Data.Ratio + +import GHC.TypeLits + +import LibBF + -- For doctest use only -- -- $setup @@ -162,9 +176,10 @@ -- -- Conversions to float: 'toSFloat' and 'toSDouble' simply return the -- nearest representable float from the given type based on the rounding --- mode provided. +-- mode provided. Similarly, 'toSFloatingPoint' converts to a generalized +-- floating-point number with specified exponent and significand bith widths. -- --- Conversions from float: 'fromSFloat' and 'fromSDouble' functions do +-- Conversions from float: 'fromSFloat', 'fromSDouble', 'fromSFloatingPoint' functions do -- the reverse conversion. However some care is needed when given values -- that are not representable in the integral target domain. For instance, -- converting an 'SFloat' to an 'SInt8' is problematic. The rules are as follows: @@ -236,7 +251,7 @@ -- default definition if we have an integral like default toSFloat :: Integral a => SRoundingMode -> SBV a -> SFloat - toSFloat = genericToFloat (Just . fromRational . fromIntegral) + toSFloat = genericToFloat (onlyWhenRNE (Just . fromRational . fromIntegral)) -- | Convert from an IEEE74 double precision float. fromSDouble :: SRoundingMode -> SDouble -> SBV a @@ -277,8 +292,24 @@ -- default definition if we have an integral like default toSDouble :: Integral a => SRoundingMode -> SBV a -> SDouble - toSDouble = genericToFloat (Just . fromRational . fromIntegral) + toSDouble = genericToFloat (onlyWhenRNE (Just . fromRational . fromIntegral)) + -- | Convert from an arbitrary floating point. + fromSFloatingPoint :: ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV a + fromSFloatingPoint = genericFromFloat + + -- | Convert to an arbitrary floating point. + toSFloatingPoint :: ValidFloat eb sb => SRoundingMode -> SBV a -> SFloatingPoint eb sb + + -- -- default definition if we have an integral like + default toSFloatingPoint :: (Integral a, ValidFloat eb sb) => SRoundingMode -> SBV a -> SFloatingPoint eb sb + toSFloatingPoint = genericToFloat (const (Just . fromRational . fromIntegral)) + +-- Run the function if the conversion is in RNE. Otherwise return Nothing. +onlyWhenRNE :: (a -> Maybe b) -> RoundingMode -> a -> Maybe b +onlyWhenRNE f RoundNearestTiesToEven v = f v +onlyWhenRNE _ _ _ = Nothing + -- | A generic from-float converter. Note that this function does no constant folding since -- it's behavior is undefined when the input float is out-of-bounds or not a point. genericFromFloat :: forall a r. (IEEEFloating a, IEEEFloatConvertible r) @@ -292,14 +323,14 @@ xsv <- sbvToSV st f newExpr st kTo (SBVApp (IEEEFP (FP_Cast kFrom kTo msv)) [xsv]) --- | A generic to-float converter, which will constant-fold as necessary, but only in the sRNE mode. +-- | A generic to-float converter, which will constant-fold as necessary, but only in the sRNE mode for regular floats. genericToFloat :: forall a r. (IEEEFloatConvertible a, IEEEFloating r) - => (a -> Maybe r) -- How to convert concretely, if possible - -> SRoundingMode -- Rounding mode - -> SBV a -- Input convertible + => (RoundingMode -> a -> Maybe r) -- How to convert concretely, if possible + -> SRoundingMode -- Rounding mode + -> SBV a -- Input convertible -> SBV r genericToFloat converter rm i - | Just w <- unliteral i, Just RoundNearestTiesToEven <- unliteral rm, Just result <- converter w + | Just w <- unliteral i, Just crm <- unliteral rm, Just result <- converter crm w = literal result | True = SBV (SVal kTo (Right (cache r))) @@ -322,8 +353,10 @@ -- For float and double, skip the conversion if the same and do the constant folding, unlike all others. instance IEEEFloatConvertible Float where toSFloat _ f = f - toSDouble = genericToFloat (Just . fp2fp) + toSDouble = genericToFloat (onlyWhenRNE (Just . fp2fp)) + toSFloatingPoint rm f = toSFloatingPoint rm $ toSDouble rm f + fromSFloat _ f = f fromSDouble rm f | Just RoundNearestTiesToEven <- unliteral rm @@ -333,9 +366,22 @@ = genericFromFloat rm f instance IEEEFloatConvertible Double where - toSFloat = genericToFloat (Just . fp2fp) + toSFloat = genericToFloat (onlyWhenRNE (Just . fp2fp)) toSDouble _ d = d + toSFloatingPoint rm sd + | Just d <- unliteral sd, Just brm <- rmToRM rm + = literal $ FloatingPoint $ FP ei si $ fst (bfRoundFloat (mkBFOpts ei si brm) (bfFromDouble d)) + | True + = res + where (k, ei, si) = case kindOf res of + kr@(KFP eb sb) -> (kr, eb, sb) + kr -> error $ "Unexpected kind in toSFloatingPoint: " ++ show (kr, rm, sd) + res = SBV $ SVal k $ Right $ cache r + r st = do msv <- sbvToSV st rm + xsv <- sbvToSV st sd + newExpr st k (SBVApp (IEEEFP (FP_Cast KDouble k msv)) [xsv]) + fromSDouble _ d = d fromSFloat rm d | Just RoundNearestTiesToEven <- unliteral rm @@ -344,39 +390,90 @@ | True = genericFromFloat rm d +convertWhenExactRational :: Fractional a => AlgReal -> Maybe a +convertWhenExactRational r + | isExactRational r = Just (fromRational (toRational r)) + | True = Nothing + -- For AlgReal; be careful to only process exact rationals concretely instance IEEEFloatConvertible AlgReal where - toSFloat = genericToFloat (\r -> if isExactRational r then Just (fromRational (toRational r)) else Nothing) - toSDouble = genericToFloat (\r -> if isExactRational r then Just (fromRational (toRational r)) else Nothing) + toSFloat = genericToFloat (onlyWhenRNE convertWhenExactRational) + toSDouble = genericToFloat (onlyWhenRNE convertWhenExactRational) + toSFloatingPoint = genericToFloat (const convertWhenExactRational) +-- Arbitrary floats can handle all rounding modes in concrete mode +instance ValidFloat eb sb => IEEEFloatConvertible (FloatingPoint eb sb) where + toSFloat rm i + | Just (FloatingPoint (FP _ _ v)) <- unliteral i, Just brm <- rmToRM rm + = literal $ fp2fp $ fst (bfToDouble brm (fst (bfRoundFloat (mkBFOpts ei si brm) v))) + | True + = genericToFloat (\_ _ -> Nothing) rm i + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + + fromSFloat rm i + | Just f <- unliteral i, Just brm <- rmToRM rm + = literal $ FloatingPoint $ FP ei si $ fst (bfRoundFloat (mkBFOpts ei si brm) (bfFromDouble (fp2fp f :: Double))) + | True + = genericFromFloat rm i + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + + toSDouble rm i + | Just (FloatingPoint (FP _ _ v)) <- unliteral i, Just brm <- rmToRM rm + = literal $ fst (bfToDouble brm (fst (bfRoundFloat (mkBFOpts ei si brm) v))) + | True + = genericToFloat (\_ _ -> Nothing) rm i + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + + fromSDouble rm i + | Just f <- unliteral i, Just brm <- rmToRM rm + = literal $ FloatingPoint $ FP ei si $ fst (bfRoundFloat (mkBFOpts ei si brm) (bfFromDouble f)) + | True + = genericFromFloat rm i + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + + toSFloatingPoint rm i + | Just (FloatingPoint (FP _ _ v)) <- unliteral i, Just brm <- rmToRM rm + = literal $ FloatingPoint $ FP ei si $ fst (bfRoundFloat (mkBFOpts ei si brm) v) + | True + = genericToFloat (\_ _ -> Nothing) rm i + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + + -- From and To are the same when the source is an arbitrary float! + fromSFloatingPoint = toSFloatingPoint + -- | Concretely evaluate one arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data concEval1 :: SymVal a => Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a) concEval1 mbOp mbRm a = do op <- mbOp v <- unliteral a case unliteral =<< mbRm of - Nothing -> (Just . literal) (op v) - Just RoundNearestTiesToEven -> (Just . literal) (op v) - _ -> Nothing + Nothing -> (Just . literal) (op v) + Just RoundNearestTiesToEven -> (Just . literal) (op v) + _ -> Nothing -- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data concEval2 :: SymVal a => Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a) -concEval2 mbOp mbRm a b = do op <- mbOp - v1 <- unliteral a - v2 <- unliteral b - case unliteral =<< mbRm of - Nothing -> (Just . literal) (v1 `op` v2) - Just RoundNearestTiesToEven -> (Just . literal) (v1 `op` v2) - _ -> Nothing +concEval2 mbOp mbRm a b = do op <- mbOp + v1 <- unliteral a + v2 <- unliteral b + case unliteral =<< mbRm of + Nothing -> (Just . literal) (v1 `op` v2) + Just RoundNearestTiesToEven -> (Just . literal) (v1 `op` v2) + _ -> Nothing -- | Concretely evaluate a bool producing two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data concEval2B :: SymVal a => Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool -concEval2B mbOp mbRm a b = do op <- mbOp - v1 <- unliteral a - v2 <- unliteral b - case unliteral =<< mbRm of - Nothing -> (Just . literal) (v1 `op` v2) - Just RoundNearestTiesToEven -> (Just . literal) (v1 `op` v2) - _ -> Nothing +concEval2B mbOp mbRm a b = do op <- mbOp + v1 <- unliteral a + v2 <- unliteral b + case unliteral =<< mbRm of + Nothing -> (Just . literal) (v1 `op` v2) + Just RoundNearestTiesToEven -> (Just . literal) (v1 `op` v2) + _ -> Nothing -- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data concEval3 :: SymVal a => Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a) @@ -385,9 +482,9 @@ v2 <- unliteral b v3 <- unliteral c case unliteral =<< mbRm of - Nothing -> (Just . literal) (op v1 v2 v3) - Just RoundNearestTiesToEven -> (Just . literal) (op v1 v2 v3) - _ -> Nothing + Nothing -> (Just . literal) (op v1 v2 v3) + Just RoundNearestTiesToEven -> (Just . literal) (op v1 v2 v3) + _ -> Nothing -- | Add the converted rounding mode if given as an argument addRM :: State -> Maybe SRoundingMode -> [SV] -> IO [SV] @@ -485,7 +582,7 @@ sFloatAsSWord32 :: SFloat -> SWord32 sFloatAsSWord32 fVal | Just f <- unliteral fVal, not (isNaN f) - = literal (CN.floatToWord f) + = literal (floatToWord f) | True = SBV (SVal w32 (Right (cache y))) where w32 = KBounded False 32 @@ -506,7 +603,7 @@ sDoubleAsSWord64 :: SDouble -> SWord64 sDoubleAsSWord64 fVal | Just f <- unliteral fVal, not (isNaN f) - = literal (CN.doubleToWord f) + = literal (doubleToWord f) | True = SBV (SVal w64 (Right (cache y))) where w64 = KBounded False 64 @@ -531,10 +628,19 @@ blastSDouble = extract . sDoubleAsSWord64 where extract x = (sTestBit x 63, sExtractBits x [62, 61 .. 52], sExtractBits x [51, 50 .. 0]) +-- | Extract the sign\/exponent\/mantissa of an arbitrary precision float. The output will have +-- @eb@ bits in the second argument for exponent, and @sb-1@ bits in the third for mantissa. +blastSFloatingPoint :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) + => SFloatingPoint eb sb -> (SBool, [SBool], [SBool]) +blastSFloatingPoint = extract . sFloatingPointAsSWord + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + extract x = (sTestBit x (ei + si - 1), sExtractBits x [ei + si - 2, ei + si - 3 .. si - 1], sExtractBits x [si - 2, si - 3 .. 0]) + -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number sWord32AsSFloat :: SWord32 -> SFloat sWord32AsSFloat fVal - | Just f <- unliteral fVal = literal $ CN.wordToFloat f + | Just f <- unliteral fVal = literal $ wordToFloat f | True = SBV (SVal KFloat (Right (cache y))) where y st = do xsv <- sbvToSV st fVal newExpr st KFloat (SBVApp (IEEEFP (FP_Reinterpret (kindOf fVal) KFloat)) [xsv]) @@ -542,7 +648,7 @@ -- | Reinterpret the bits in a 32-bit word as a single-precision floating point number sWord64AsSDouble :: SWord64 -> SDouble sWord64AsSDouble dVal - | Just d <- unliteral dVal = literal $ CN.wordToDouble d + | Just d <- unliteral dVal = literal $ wordToDouble d | True = SBV (SVal KDouble (Right (cache y))) where y st = do xsv <- sbvToSV st dVal newExpr st KDouble (SBVApp (IEEEFP (FP_Reinterpret (kindOf dVal) KDouble)) [xsv]) @@ -555,6 +661,17 @@ sFloatAsComparableSWord32 f = ite (fpIsNegativeZero f) (sFloatAsComparableSWord32 0) (fromBitsBE $ sNot sb : ite sb (map sNot rest) rest) where (sb : rest) = blastBE $ sFloatAsSWord32 f +-- | Inverse transformation to 'sFloatAsComparableSWord32'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@. +-- Otherwise, it's faithful: +-- +-- >>> prove $ \x -> let f = sComparableSWord32AsSFloat x in fpIsNaN f .|| fpIsNegativeZero f .|| sFloatAsComparableSWord32 f .== x +-- Q.E.D. +-- >>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWord32AsSFloat (sFloatAsComparableSWord32 x) `fpIsEqualObject` x +-- Q.E.D. +sComparableSWord32AsSFloat :: SWord32 -> SFloat +sComparableSWord32AsSFloat w = sWord32AsSFloat $ ite sb (fromBitsBE $ sFalse : rest) (fromBitsBE $ map sNot allBits) + where allBits@(sb : rest) = blastBE w + -- | Convert a double to a comparable 'SWord64'. The trick is to ignore the -- sign of -0, and if it's a negative value flip all the bits, and otherwise -- only flip the sign bit. This is known as the lexicographic ordering on doubles @@ -563,13 +680,24 @@ sDoubleAsComparableSWord64 d = ite (fpIsNegativeZero d) (sDoubleAsComparableSWord64 0) (fromBitsBE $ sNot sb : ite sb (map sNot rest) rest) where (sb : rest) = blastBE $ sDoubleAsSWord64 d +-- | Inverse transformation to 'sDoubleAsComparableSWord64'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@. +-- Otherwise, it's faithful: +-- +-- >>> prove $ \x -> let d = sComparableSWord64AsSDouble x in fpIsNaN d .|| fpIsNegativeZero d .|| sDoubleAsComparableSWord64 d .== x +-- Q.E.D. +-- >>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWord64AsSDouble (sDoubleAsComparableSWord64 x) `fpIsEqualObject` x +-- Q.E.D. +sComparableSWord64AsSDouble :: SWord64 -> SDouble +sComparableSWord64AsSDouble w = sWord64AsSDouble $ ite sb (fromBitsBE $ sFalse : rest) (fromBitsBE $ map sNot allBits) + where allBits@(sb : rest) = blastBE w + -- | 'Float' instance for 'Metric' goes through the lexicographic ordering on 'Word32'. -- It implicitly makes sure that the value is not @NaN@. instance Metric Float where type MetricSpace Float = Word32 toMetricSpace = sFloatAsComparableSWord32 - fromMetricSpace = sWord32AsSFloat + fromMetricSpace = sComparableSWord32AsSFloat msMinimize nm o = do constrain $ sNot $ fpIsNaN o addSValOptGoal $ unSBV `fmap` Minimize nm (toMetricSpace o) @@ -583,12 +711,219 @@ type MetricSpace Double = Word64 toMetricSpace = sDoubleAsComparableSWord64 - fromMetricSpace = sWord64AsSDouble + fromMetricSpace = sComparableSWord64AsSDouble msMinimize nm o = do constrain $ sNot $ fpIsNaN o addSValOptGoal $ unSBV `fmap` Minimize nm (toMetricSpace o) msMaximize nm o = do constrain $ sNot $ fpIsNaN o addSValOptGoal $ unSBV `fmap` Maximize nm (toMetricSpace o) + +-- | Real instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here. +instance ValidFloat eb sb => Real (FloatingPoint eb sb) where + toRational (FloatingPoint (FP _ _ r)) = case bfToRep r of + BFNaN -> toRational (0/0 :: Double) + BFRep s n -> case n of + Zero -> 0 % 1 + Inf -> (if s == Neg then -1 else 1) % 0 + Num x y -> -- The value here is x * 2^y + let v :: Integer + v = 2 ^ abs (fromIntegral y :: Integer) + sgn = if s == Neg then ((-1) *) else id + in if y > 0 + then sgn $ x * v % 1 + else sgn $ x % v + +-- | RealFrac instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here. +instance ValidFloat eb sb => RealFrac (FloatingPoint eb sb) where + properFraction (FloatingPoint f) = (a, FloatingPoint b) + where (a, b) = properFraction f + +-- | RealFloat instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here. +instance ValidFloat eb sb => RealFloat (FloatingPoint eb sb) where + floatRadix (FloatingPoint f) = floatRadix f + floatDigits (FloatingPoint f) = floatDigits f + floatRange (FloatingPoint f) = floatRange f + isNaN (FloatingPoint f) = isNaN f + isInfinite (FloatingPoint f) = isInfinite f + isDenormalized (FloatingPoint f) = isDenormalized f + isNegativeZero (FloatingPoint f) = isNegativeZero f + isIEEE (FloatingPoint f) = isIEEE f + decodeFloat (FloatingPoint f) = decodeFloat f + + encodeFloat m n = res + where res = FloatingPoint $ fpEncodeFloat ei si m n + ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + +-- | Convert a float to the word containing the corresponding bit pattern +sFloatingPointAsSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb) +sFloatingPointAsSWord fVal + | Just f@(FloatingPoint (FP eb sb v)) <- unliteral fVal, not (isNaN f) + = fromIntegral $ bfToBits (mkBFOpts eb sb NearEven) v + | True + = SBV (SVal kTo (Right (cache y))) + where ieb = intOfProxy (Proxy @eb) + isb = intOfProxy (Proxy @sb) + kFrom = KFP ieb isb + kTo = KBounded False (ieb + isb) + y st = do cg <- isCodeGenMode st + if cg + then do f <- sbvToSV st fVal + newExpr st kTo (SBVApp (IEEEFP (FP_Reinterpret kFrom kTo)) [f]) + else do n <- internalVariable st kTo + ysw <- newExpr st kFrom (SBVApp (IEEEFP (FP_Reinterpret kTo kFrom)) [n]) + internalConstraint st False [] $ unSBV $ fVal `fpIsEqualObject` SBV (SVal kFrom (Right (cache (\_ -> return ysw)))) + return n + +-- | Convert a float to the correct size word, that can be used in lexicographic ordering. Used in optimization. +sFloatingPointAsComparableSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb) +sFloatingPointAsComparableSWord f = ite (fpIsNegativeZero f) posZero (fromBitsBE $ sNot sb : ite sb (map sNot rest) rest) + where posZero = sFloatingPointAsComparableSWord (0 :: SFloatingPoint eb sb) + (sb : rest) = blastBE (sFloatingPointAsSWord f :: SWord (eb + sb)) + +-- | Inverse transformation to 'sFloatingPointAsComparableSWord'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@. +-- Otherwise, it's faithful: +-- +-- >>> prove $ \x -> let d = sComparableSWordAsSFloatingPoint x in fpIsNaN d .|| fpIsNegativeZero d .|| sFloatingPointAsComparableSWord (d :: SFPHalf) .== x +-- Q.E.D. +-- >>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWordAsSFloatingPoint (sFloatingPointAsComparableSWord x) `fpIsEqualObject` (x :: SFPHalf) +-- Q.E.D. +sComparableSWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb +sComparableSWordAsSFloatingPoint w = sWordAsSFloatingPoint $ ite signBit (fromBitsBE $ sFalse : rest) (fromBitsBE $ map sNot allBits) + where allBits@(signBit : rest) = blastBE w + +-- | Convert a word to an arbitrary float, by reinterpreting the bits of the word as the corresponding bits of the float. +sWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb +sWordAsSFloatingPoint sw + | Just (f :: WordN (eb + sb)) <- unliteral sw + = let ext i = f `testBit` i + exts = map ext + (s, ebits, sigbits) = (ext (ei + si - 1), exts [ei + si - 2, ei + si - 3 .. si - 1], exts [si - 2, si - 3 .. 0]) + + cvt :: [Bool] -> Integer + cvt = foldr (\b sofar -> 2 * sofar + if b then 1 else 0) 0 . reverse + + eIntV = cvt ebits + sIntV = cvt sigbits + fp = fpFromRawRep s (eIntV, ei) (sIntV, si) + in literal $ FloatingPoint fp + | True + = SBV (SVal kTo (Right (cache y))) + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + kTo = KFP ei si + y st = do xsv <- sbvToSV st sw + newExpr st kTo (SBVApp (IEEEFP (FP_Reinterpret (kindOf sw) kTo)) [xsv]) + +instance (BVIsNonZero (eb + sb), KnownNat (eb + sb), ValidFloat eb sb) => Metric (FloatingPoint eb sb) where + + type MetricSpace (FloatingPoint eb sb) = WordN (eb + sb) + toMetricSpace = sFloatingPointAsComparableSWord + fromMetricSpace = sComparableSWordAsSFloatingPoint + + msMinimize nm o = do constrain $ sNot $ fpIsNaN o + addSValOptGoal $ unSBV `fmap` Minimize nm (toMetricSpace o) + + msMaximize nm o = do constrain $ sNot $ fpIsNaN o + addSValOptGoal $ unSBV `fmap` Maximize nm (toMetricSpace o) + +-- Map SBV's rounding modes to LibBF's +rmToRM :: SRoundingMode -> Maybe RoundMode +rmToRM srm = cvt <$> unliteral srm + where cvt RoundNearestTiesToEven = NearEven + cvt RoundNearestTiesToAway = NearAway + cvt RoundTowardPositive = ToPosInf + cvt RoundTowardNegative = ToNegInf + cvt RoundTowardZero = ToZero + +-- | Lift a 1 arg Big-float op +lift1FP :: forall eb sb. ValidFloat eb sb => + (BFOpts -> BigFloat -> (BigFloat, Status)) + -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb) + -> SRoundingMode + -> SFloatingPoint eb sb + -> SFloatingPoint eb sb +lift1FP bfOp mkDef rm a + | Just (FloatingPoint (FP _ _ v)) <- unliteral a + , Just brm <- rmToRM rm + = literal $ FloatingPoint (FP ei si (fst (bfOp (mkBFOpts ei si brm) v))) + | True + = mkDef (Just rm) a + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + +-- | Lift a 2 arg Big-float op +lift2FP :: forall eb sb. ValidFloat eb sb => + (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) + -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb) + -> SRoundingMode + -> SFloatingPoint eb sb + -> SFloatingPoint eb sb + -> SFloatingPoint eb sb +lift2FP bfOp mkDef rm a b + | Just (FloatingPoint (FP _ _ v1)) <- unliteral a + , Just (FloatingPoint (FP _ _ v2)) <- unliteral b + , Just brm <- rmToRM rm + = literal $ FloatingPoint (FP ei si (fst (bfOp (mkBFOpts ei si brm) v1 v2))) + | True + = mkDef (Just rm) a b + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + +-- | Lift a 3 arg Big-float op +lift3FP :: forall eb sb. ValidFloat eb sb => + (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)) + -> (Maybe SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb) + -> SRoundingMode + -> SFloatingPoint eb sb + -> SFloatingPoint eb sb + -> SFloatingPoint eb sb + -> SFloatingPoint eb sb +lift3FP bfOp mkDef rm a b c + | Just (FloatingPoint (FP _ _ v1)) <- unliteral a + , Just (FloatingPoint (FP _ _ v2)) <- unliteral b + , Just (FloatingPoint (FP _ _ v3)) <- unliteral c + , Just brm <- rmToRM rm + = literal $ FloatingPoint (FP ei si (fst (bfOp (mkBFOpts ei si brm) v1 v2 v3))) + | True + = mkDef (Just rm) a b c + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + +-- Sized-floats have a special instance, since it can handle arbitrary rounding modes when it matters. +instance ValidFloat eb sb => IEEEFloating (FloatingPoint eb sb) where + fpAdd = lift2FP bfAdd (lift2 FP_Add (Just (+))) + fpSub = lift2FP bfSub (lift2 FP_Sub (Just (-))) + fpMul = lift2FP bfMul (lift2 FP_Mul (Just (*))) + fpDiv = lift2FP bfDiv (lift2 FP_Div (Just (/))) + fpFMA = lift3FP bfFMA (lift3 FP_FMA Nothing) + fpSqrt = lift1FP bfSqrt (lift1 FP_Sqrt (Just sqrt)) + + fpRoundToIntegral rm a + | Just (FloatingPoint (FP ei si v)) <- unliteral a + , Just brm <- rmToRM rm + = literal $ FloatingPoint (FP ei si (fst (bfRoundInt brm v))) + | True + = lift1 FP_RoundToIntegral (Just fpRoundToIntegralH) (Just rm) a + + -- All other operations are agnostic to the rounding mode, hence the defaults are sufficient: + -- + -- fpAbs :: SBV a -> SBV a + -- fpNeg :: SBV a -> SBV a + -- fpRem :: SBV a -> SBV a -> SBV a + -- fpMin :: SBV a -> SBV a -> SBV a + -- fpMax :: SBV a -> SBV a -> SBV a + -- fpIsEqualObject :: SBV a -> SBV a -> SBool + -- fpIsNormal :: SBV a -> SBool + -- fpIsSubnormal :: SBV a -> SBool + -- fpIsZero :: SBV a -> SBool + -- fpIsInfinite :: SBV a -> SBool + -- fpIsNaN :: SBV a -> SBool + -- fpIsNegative :: SBV a -> SBool + -- fpIsPositive :: SBV a -> SBool + -- fpIsNegativeZero :: SBV a -> SBool + -- fpIsPositiveZero :: SBV a -> SBool + -- fpIsPoint :: SBV a -> SBool {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} 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 @@ -9,17 +9,26 @@ -- Internal data-structures for the sbv library ----------------------------------------------------------------------------- -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} -module Data.SBV.Core.Kind (Kind(..), HasKind(..), constructUKind, smtType, hasUninterpretedSorts, showBaseKind, needsFlattening) where +module Data.SBV.Core.Kind ( + Kind(..), HasKind(..), constructUKind, smtType, hasUninterpretedSorts + , BVIsNonZero, ValidFloat, intOfProxy + , showBaseKind, needsFlattening, RoundingMode(..), smtRoundingMode + ) where import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields) @@ -30,11 +39,16 @@ import Data.SBV.Core.AlgReals import Data.Proxy +import Data.Kind import Data.List (isPrefixOf, intercalate) import Data.Typeable (Typeable) +import Data.Type.Bool +import Data.Type.Equality +import GHC.TypeLits + import Data.SBV.Utils.Lib (isKString) -- | Kind of symbolic value @@ -45,6 +59,7 @@ | KUserSort String (Maybe [String]) -- name. Uninterpreted, or enumeration constants. | KFloat | KDouble + | KFP !Int !Int | KChar | KString | KList Kind @@ -66,6 +81,7 @@ show (KUserSort s _) = s show KFloat = "SFloat" show KDouble = "SDouble" + show (KFP eb sb) = "SFloatingPoint " ++ show eb ++ " " ++ show sb show KString = "SString" show KChar = "SChar" show (KList e) = "[" ++ show e ++ "]" @@ -85,6 +101,7 @@ sh k@KUserSort{} = 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 (KList k) = "[" ++ sh k ++ "]" @@ -118,6 +135,7 @@ smtType KReal = "Real" smtType KFloat = "(_ FloatingPoint 8 24)" smtType KDouble = "(_ FloatingPoint 11 53)" +smtType (KFP eb sb) = "(_ FloatingPoint " ++ show eb ++ " " ++ show sb ++ ")" smtType KString = "String" smtType KChar = "String" smtType (KList k) = "(Seq " ++ smtType k ++ ")" @@ -142,6 +160,7 @@ KReal -> True KFloat -> True KDouble -> True + KFP{} -> True KUserSort{} -> False KString -> False KChar -> False @@ -196,6 +215,7 @@ isReal :: a -> Bool isFloat :: a -> Bool isDouble :: a -> Bool + isFP :: a -> Bool isUnbounded :: a -> Bool isUserSort :: a -> Bool isChar :: a -> Bool @@ -216,6 +236,7 @@ KReal -> error "SBV.HasKind.intSizeOf((S)Real)" KFloat -> error "SBV.HasKind.intSizeOf((S)Float)" KDouble -> error "SBV.HasKind.intSizeOf((S)Double)" + KFP{} -> error "SBV.HasKind.intSizeOf((S)FP)" KUserSort s _ -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s KString -> error "SBV.HasKind.intSizeOf((S)Double)" KChar -> error "SBV.HasKind.intSizeOf((S)Char)" @@ -240,6 +261,9 @@ isDouble (kindOf -> KDouble{}) = True isDouble _ = False + isFP (kindOf -> KFP{}) = True + isFP _ = False + isUnbounded (kindOf -> KUnbounded{}) = True isUnbounded _ = False @@ -293,6 +317,10 @@ instance HasKind Double where kindOf _ = KDouble instance HasKind Char where kindOf _ = KChar +-- | Grab the bit-size from the proxy +intOfProxy :: KnownNat n => Proxy n -> Int +intOfProxy = fromEnum . natVal + -- | Do we have a completely uninterpreted sort lying around anywhere? hasUninterpretedSorts :: Kind -> Bool hasUninterpretedSorts KBool = False @@ -303,6 +331,7 @@ hasUninterpretedSorts (KUserSort _ Nothing) = True -- These are the completely uninterpreted sorts, which we are looking for here hasUninterpretedSorts KFloat = False hasUninterpretedSorts KDouble = False +hasUninterpretedSorts KFP{} = False hasUninterpretedSorts KChar = False hasUninterpretedSorts KString = False hasUninterpretedSorts (KList k) = hasUninterpretedSorts k @@ -359,6 +388,7 @@ needsFlattening KUserSort{} = False needsFlattening KFloat = False needsFlattening KDouble = False +needsFlattening KFP{} = False needsFlattening KChar = False needsFlattening KString = False needsFlattening KList{} = True @@ -366,3 +396,95 @@ needsFlattening KTuple{} = True needsFlattening KMaybe{} = True needsFlattening KEither{} = True + +-- | Catch 0-width cases +type BVZeroWidth = 'Text "Zero-width bit-vectors are not allowed." + +-- | Type family to create the appropriate non-zero constraint +type family BVIsNonZero (arg :: Nat) :: Constraint where + BVIsNonZero 0 = TypeError BVZeroWidth + BVIsNonZero _ = () + +#include "MachDeps.h" + +-- Allowed sizes for floats, imposed by LibBF. +-- +-- NB. In LibBF bindings (and libbf itself as well), minimum number of exponent bits is specified as 3. But this +-- seems unnecessarily restrictive; that constant doesn't seem to be used anywhere, and furthermore my tests with sb = 2 +-- didn't reveal anything going wrong. I emailed the author of libbf regarding this, and he said: +-- +-- I had no clear reason to use BF_EXP_BITS_MIN = 3. So if "2" is OK then +-- why not. The important is that the basic operations are OK. It is likely +-- there are tricky cases in the transcendental operations but even with +-- large exponents libbf may have problems with them ! +-- +-- So, in SBV, we allow sb == 2. If this proves problematic, change the number below in definition of FP_MIN_EB to 3! +-- +-- NB. It would be nice if we could use the LibBF constants expBitsMin, expBitsMax, precBitsMin, precBitsMax +-- for determining the valid range. Unfortunately this doesn't seem to be possible. +-- See for a discussion. +-- So, we use CPP to work-around that. +#define FP_MIN_EB 2 +#define FP_MIN_SB 2 +#if WORD_SIZE_IN_BITS == 64 +#define FP_MAX_EB 61 +#define FP_MAX_SB 4611686018427387902 +#else +#define FP_MAX_EB 29 +#define FP_MAX_SB 1073741822 +#endif + +-- | Catch an invalid FP. +type InvalidFloat (eb :: Nat) (sb :: Nat) + = 'Text "Invalid floating point type `SFloatingPoint " ':<>: 'ShowType eb ':<>: 'Text " " ':<>: 'ShowType sb ':<>: 'Text "'" + ':$$: 'Text "" + ':$$: 'Text "A valid float of type 'SFloatingPoint eb sb' must satisfy:" + ':$$: 'Text " eb `elem` [" ':<>: 'ShowType FP_MIN_EB ':<>: 'Text " .. " ':<>: 'ShowType FP_MAX_EB ':<>: 'Text "]" + ':$$: 'Text " sb `elem` [" ':<>: 'ShowType FP_MIN_SB ':<>: 'Text " .. " ':<>: 'ShowType FP_MAX_SB ':<>: 'Text "]" + ':$$: 'Text "" + ':$$: 'Text "Given type falls outside of this range, or the sizes are not known naturals." + +-- | A valid float has restrictions on eb/sb values. +-- NB. In the below encoding, I found that CPP is very finicky about substitution of the machine-dependent +-- macros. If you try to put the conditionals in the same line, it fails to substitute for some reason. Hence the awkward spacing. +-- Filed this as a bug report for CPPHS at . +type family ValidFloat (eb :: Nat) (sb :: Nat) :: Constraint where + ValidFloat (eb :: Nat) (sb :: Nat) = ( KnownNat eb + , KnownNat sb + , If ( ( eb `CmpNat` FP_MIN_EB == 'EQ + || eb `CmpNat` FP_MIN_EB == 'GT) + && ( eb `CmpNat` FP_MAX_EB == 'EQ + || eb `CmpNat` FP_MAX_EB == 'LT) + && ( sb `CmpNat` FP_MIN_SB == 'EQ + || sb `CmpNat` FP_MIN_SB == 'GT) + && ( sb `CmpNat` FP_MAX_SB == 'EQ + || sb `CmpNat` FP_MAX_SB == 'LT)) + (() :: Constraint) + (TypeError (InvalidFloat eb sb)) + ) + +-- | Rounding mode to be used for the IEEE floating-point operations. +-- Note that Haskell's default is 'RoundNearestTiesToEven'. If you use +-- a different rounding mode, then the counter-examples you get may not +-- match what you observe in Haskell. +data RoundingMode = RoundNearestTiesToEven -- ^ Round to nearest representable floating point value. + -- If precisely at half-way, pick the even number. + -- (In this context, /even/ means the lowest-order bit is zero.) + | RoundNearestTiesToAway -- ^ Round to nearest representable floating point value. + -- If precisely at half-way, pick the number further away from 0. + -- (That is, for positive values, pick the greater; for negative values, pick the smaller.) + | RoundTowardPositive -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.) + | RoundTowardNegative -- ^ Round towards negative infinity. (Also known as rounding-down or floor.) + | RoundTowardZero -- ^ Round towards zero. (Also known as truncation.) + deriving (Eq, Ord, Show, Read, G.Data, Bounded, Enum) + +-- | 'RoundingMode' kind +instance HasKind RoundingMode + +-- | Convert a rounding mode to the format SMT-Lib2 understands. +smtRoundingMode :: RoundingMode -> String +smtRoundingMode RoundNearestTiesToEven = "roundNearestTiesToEven" +smtRoundingMode RoundNearestTiesToAway = "roundNearestTiesToAway" +smtRoundingMode RoundTowardPositive = "roundTowardPositive" +smtRoundingMode RoundTowardNegative = "roundTowardNegative" +smtRoundingMode RoundTowardZero = "roundTowardZero" 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 @@ -9,15 +9,17 @@ -- Instance declarations for our symbolic world ----------------------------------------------------------------------------- -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} @@ -29,6 +31,8 @@ , sBool, sBool_, sBools, sWord8, sWord8_, sWord8s, sWord16, sWord16_, sWord16s, sWord32, sWord32_, sWord32s , sWord64, sWord64_, sWord64s, sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s, sInt64, sInt64_ , sInt64s, sInteger, sInteger_, sIntegers, sReal, sReal_, sReals, sFloat, sFloat_, sFloats, sDouble, sDouble_, sDoubles + , sFPHalf, sFPHalf_, sFPHalfs, sFPSingle, sFPSingle_, sFPSingles, sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads + , sFloatingPoint, sFloatingPoint_, sFloatingPoints , sChar, sChar_, sChars, sString, sString_, sStrings, sList, sList_, sLists , SymTuple, sTuple, sTuple_, sTuples , sEither, sEither_, sEithers, sMaybe, sMaybe_, sMaybes @@ -57,6 +61,7 @@ import Data.Bits (Bits(..)) import Data.Char (toLower, isDigit) import Data.Int (Int8, Int16, Int32, Int64) +import Data.Kind (Type) import Data.List (genericLength, genericIndex, genericTake, unzip4, unzip5, unzip6, unzip7, intercalate, isPrefixOf) import Data.Maybe (fromMaybe, mapMaybe) import Data.String (IsString(..)) @@ -75,9 +80,11 @@ import qualified Data.Foldable as F (toList) import Data.SBV.Core.AlgReals +import Data.SBV.Core.SizedFloats import Data.SBV.Core.Data import Data.SBV.Core.Symbolic import Data.SBV.Core.Operations +import Data.SBV.Core.Kind import Data.SBV.Provers.Prover (defaultSMTCfg, SafeResult(..), prove) import Data.SBV.SMT.SMT (ThmResult, showModel) @@ -215,6 +222,16 @@ fromCV (CV _ (CList a)) = fromCV . CV (kindOf (Proxy @a)) <$> a fromCV c = error $ "SymVal.fromCV: Unexpected non-list value: " ++ show c +instance ValidFloat eb sb => HasKind (FloatingPoint eb sb) where + kindOf _ = KFP (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb)) + +instance ValidFloat eb sb => SymVal (FloatingPoint eb sb) where + mkSymVal = genMkSymVar (KFP (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb))) + literal (FloatingPoint r) = let k = KFP (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb)) + in SBV $ SVal k $ Left $ CV k (CFP r) + fromCV (CV _ (CFP r)) = FloatingPoint r + fromCV c = error $ "SymVal.FPR: Unexpected non-arbitrary-precision value: " ++ show c + toCV :: SymVal a => a -> CVal toCV a = case literal a of SBV (SVal _ (Left cv)) -> cvVal cv @@ -502,6 +519,66 @@ sDoubles :: MonadSymbolic m => [String] -> m [SDouble] sDoubles = symbolics +-- | Generalization of 'Data.SBV.sFPHalf' +sFPHalf :: String -> Symbolic SFPHalf +sFPHalf = symbolic + +-- | Generalization of 'Data.SBV.sFPHalf_' +sFPHalf_ :: Symbolic SFPHalf +sFPHalf_ = free_ + +-- | Generalization of 'Data.SBV.sFPHalfs' +sFPHalfs :: [String] -> Symbolic [SFPHalf] +sFPHalfs = symbolics + +-- | Generalization of 'Data.SBV.sFPSingle' +sFPSingle :: String -> Symbolic SFPSingle +sFPSingle = symbolic + +-- | Generalization of 'Data.SBV.sFPSingle_' +sFPSingle_ :: Symbolic SFPSingle +sFPSingle_ = free_ + +-- | Generalization of 'Data.SBV.sFPSingles' +sFPSingles :: [String] -> Symbolic [SFPSingle] +sFPSingles = symbolics + +-- | Generalization of 'Data.SBV.sFPDouble' +sFPDouble :: String -> Symbolic SFPDouble +sFPDouble = symbolic + +-- | Generalization of 'Data.SBV.sFPDouble_' +sFPDouble_ :: Symbolic SFPDouble +sFPDouble_ = free_ + +-- | Generalization of 'Data.SBV.sFPDoubles' +sFPDoubles :: [String] -> Symbolic [SFPDouble] +sFPDoubles = symbolics + +-- | Generalization of 'Data.SBV.sFPQuad' +sFPQuad :: String -> Symbolic SFPQuad +sFPQuad = symbolic + +-- | Generalization of 'Data.SBV.sFPQuad_' +sFPQuad_ :: Symbolic SFPQuad +sFPQuad_ = free_ + +-- | Generalization of 'Data.SBV.sFPQuads' +sFPQuads :: [String] -> Symbolic [SFPQuad] +sFPQuads = symbolics + +-- | Generalization of 'Data.SBV.sFloatingPoint' +sFloatingPoint :: ValidFloat eb sb => String -> Symbolic (SFloatingPoint eb sb) +sFloatingPoint = symbolic + +-- | Generalization of 'Data.SBV.sFloatingPoint_' +sFloatingPoint_ :: ValidFloat eb sb => Symbolic (SFloatingPoint eb sb) +sFloatingPoint_ = free_ + +-- | Generalization of 'Data.SBV.sFloatingPoints' +sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb] +sFloatingPoints = symbolics + -- | Generalization of 'Data.SBV.sChar' sChar :: MonadSymbolic m => String -> m SChar sChar = symbolic @@ -847,10 +924,7 @@ let incr x table = ite (x `sElem` ignored) zero (1 + readArray table x) - insert [] table = table - insert (x:xs) table = insert xs (writeArray table x (incr x table)) - - finalArray = insert es arr + finalArray = foldl (\table x -> writeArray table x (incr x table)) arr es sbvToSV st $ sAll (\e -> readArray finalArray e .<= 1) es @@ -888,6 +962,7 @@ KUserSort {} -> True KFloat -> True KDouble -> True + KFP {} -> True KChar -> True KString -> True KList {} -> nope -- Unfortunately, no way for us to desugar this @@ -1288,6 +1363,7 @@ div0 = case kindOf sy of KFloat -> False KDouble -> False + KFP{} -> False KReal -> True -- Following cases should not happen since these types should *not* be instances of Fractional k@KBounded{} -> error $ "Unexpected Fractional case for: " ++ show k @@ -1302,12 +1378,12 @@ k@KMaybe{} -> error $ "Unexpected Fractional case for: " ++ show k k@KEither{} -> error $ "Unexpected Fractional case for: " ++ show k --- | Define Floating instance on SBV's; only for base types that are already floating; i.e., SFloat, SDouble, and SReal. --- Note that unless you use delta-sat via dReal on SReal, most of the fields are "undefined" for symbolic values. We will --- add methods as they are supported by SMTLib. Currently, the only symbolically available function in this class is sqrt --- for SFloat and SDouble. +-- | Define Floating instance on SBV's; only for base types that are already floating; i.e., 'SFloat', 'SDouble', and 'SReal'. +-- (See the separate definition below for 'SFloatingPoint'.) Note that unless you use delta-sat via 'Data.SBV.Provers.dReal' on 'SReal', most +-- of the fields are "undefined" for symbolic values. We will add methods as they are supported by SMTLib. Currently, the +-- only symbolically available function in this class is 'sqrt' for 'SFloat', 'SDouble' and 'SFloatingPoint'. instance (Ord a, SymVal a, Fractional a, Floating a) => Floating (SBV a) where - pi = literal pi + pi = fromRational . toRational $ (pi :: Double) exp = lift1FNS "exp" exp log = lift1FNS "log" log sqrt = lift1F FP_Sqrt sqrt @@ -1326,6 +1402,44 @@ (**) = lift2FNS "**" (**) logBase = lift2FNS "logBase" logBase +unsupported :: String -> a +unsupported w = error $ "Data.SBV.FloatingPoint: Unsupported operation: " ++ w ++ ". Please request this as a feature!" + +-- | We give a specific instance for 'SFloatingPoint', because the underlying floating-point type doesn't support +-- fromRational directly. The overlap with the above instance is unfortunate. +instance {-# OVERLAPPING #-} ValidFloat eb sb => Floating (SFloatingPoint eb sb) where + -- Try from double; if there's enough precision this'll work, otherwise will bail out. + pi + | ei > 11 || si > 53 = unsupported $ "Floating.SFloatingPoint.pi (not-enough-precision for " ++ show (ei, si) ++ ")" + | True = literal $ FloatingPoint $ fpFromRational ei si (toRational (pi :: Double)) + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + + -- Likewise, exponentiation is again limited to precision of double + exp i + | ei > 11 || si > 53 = unsupported $ "Floating.SFloatingPoint.exp (not-enough-precision for " ++ show (ei, si) ++ ")" + | True = literal e ** i + where ei = intOfProxy (Proxy @eb) + si = intOfProxy (Proxy @sb) + e = FloatingPoint $ fpFromRational ei si (toRational (exp 1 :: Double)) + + log = lift1FNS "log" log + sqrt = lift1F FP_Sqrt sqrt + sin = lift1FNS "sin" sin + cos = lift1FNS "cos" cos + tan = lift1FNS "tan" tan + asin = lift1FNS "asin" asin + acos = lift1FNS "acos" acos + atan = lift1FNS "atan" atan + sinh = lift1FNS "sinh" sinh + cosh = lift1FNS "cosh" cosh + tanh = lift1FNS "tanh" tanh + asinh = lift1FNS "asinh" asinh + acosh = lift1FNS "acosh" acosh + atanh = lift1FNS "atanh" atanh + (**) = lift2FNS "**" (**) + logBase = lift2FNS "logBase" logBase + -- | Lift a 1 arg FP-op, using sRNE default lift1F :: SymVal a => FPOp -> (a -> a) -> SBV a -> SBV a lift1F w op a @@ -1355,7 +1469,7 @@ -- we do not constant fold these values (except for pi), as Haskell doesn't really have any means of computing -- them for arbitrary rationals. instance {-# OVERLAPPING #-} Floating SReal where - pi = fromRational . toRational $ (pi :: Double) + pi = fromRational . toRational $ (pi :: Double) -- Perhaps not good enough? exp = lift1SReal NR_Exp log = lift1SReal NR_Log sqrt = lift1SReal NR_Sqrt @@ -2400,7 +2514,7 @@ -- | The metric space we optimize the goal over. Usually the same as the type itself, but not always! -- For instance, signed bit-vectors are optimized over their unsigned counterparts, floats are -- optimized over their 'Word32' comparable counterparts, etc. - type MetricSpace a :: * + type MetricSpace a :: Type type MetricSpace a = a -- | Compute the metric value to optimize. diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs --- a/Data/SBV/Core/Operations.hs +++ b/Data/SBV/Core/Operations.hs @@ -17,7 +17,7 @@ ( -- ** Basic constructors svTrue, svFalse, svBool - , svInteger, svFloat, svDouble, svReal, svEnumFromThenTo, svString, svChar + , svInteger, svFloat, svDouble, svFloatingPoint, svReal, svEnumFromThenTo, svString, svChar -- ** Basic destructors , svAsBool, svAsInteger, svNumerator, svDenominator -- ** Basic operations @@ -60,6 +60,7 @@ import Data.SBV.Core.Kind import Data.SBV.Core.Concrete import Data.SBV.Core.Symbolic +import Data.SBV.Core.SizedFloats import Data.Ratio @@ -88,10 +89,15 @@ svFloat :: Float -> SVal svFloat f = SVal KFloat (Left $! CV KFloat (CFloat f)) --- | Convert from a Float +-- | Convert from a Double svDouble :: Double -> SVal svDouble d = SVal KDouble (Left $! CV KDouble (CDouble d)) +-- | Convert from a generalized floating point +svFloatingPoint :: FP -> SVal +svFloatingPoint f@(FP eb sb _) = SVal k (Left $! CV k (CFP f)) + where k = KFP eb sb + -- | Convert from a String svString :: String -> SVal svString s = SVal KString (Left $! CV KString (CString s)) @@ -148,7 +154,7 @@ svPlus x y | isConcreteZero x = y | isConcreteZero y = x - | True = liftSym2 (mkSymOp Plus) rationalCheck (+) (+) (+) (+) x y + | True = liftSym2 (mkSymOp Plus) [rationalCheck] (+) (+) (+) (+) (+) x y -- | Multiplication. svTimes :: SVal -> SVal -> SVal @@ -157,25 +163,25 @@ | isConcreteZero y = y | isConcreteOne x = y | isConcreteOne y = x - | True = liftSym2 (mkSymOp Times) rationalCheck (*) (*) (*) (*) x y + | True = liftSym2 (mkSymOp Times) [rationalCheck] (*) (*) (*) (*) (*) x y -- | Subtraction. svMinus :: SVal -> SVal -> SVal svMinus x y | isConcreteZero y = x - | True = liftSym2 (mkSymOp Minus) rationalCheck (-) (-) (-) (-) x y + | True = liftSym2 (mkSymOp Minus) [rationalCheck] (-) (-) (-) (-) (-) x y --- | Unary minus. +-- | Unary minus. We handle arbitrary-FP's specially here, just for the negated literals. svUNeg :: SVal -> SVal -svUNeg = liftSym1 (mkSymOp1 UNeg) negate negate negate negate +svUNeg = liftSym1 (mkSymOp1 UNeg) negate negate negate negate negate -- | Absolute value. svAbs :: SVal -> SVal -svAbs = liftSym1 (mkSymOp1 Abs) abs abs abs abs +svAbs = liftSym1 (mkSymOp1 Abs) abs abs abs abs abs -- | Division. svDivide :: SVal -> SVal -> SVal -svDivide = liftSym2 (mkSymOp Quot) rationalCheck (/) idiv (/) (/) +svDivide = liftSym2 (mkSymOp Quot) [rationalCheck] (/) idiv (/) (/) (/) where idiv x 0 = x idiv x y = x `div` y @@ -246,8 +252,8 @@ | isConcreteZero x = x | isConcreteZero y = svInteger (kindOf x) 0 | isConcreteOne y = x - | True = liftSym2 (mkSymOp Quot) nonzeroCheck - (noReal "quot") quot' (noFloat "quot") (noDouble "quot") x y + | True = liftSym2 (mkSymOp Quot) [nonzeroCheck] + (noReal "quot") quot' (noFloat "quot") (noDouble "quot") (noFP "quot") x y where quot' a b | kindOf x == KUnbounded = div a (abs b) * signum b | otherwise = quot a b @@ -263,8 +269,8 @@ | isConcreteZero x = x | isConcreteZero y = x | isConcreteOne y = svInteger (kindOf x) 0 - | True = liftSym2 (mkSymOp Rem) nonzeroCheck - (noReal "rem") rem' (noFloat "rem") (noDouble "rem") x y + | True = liftSym2 (mkSymOp Rem) [nonzeroCheck] + (noReal "rem") rem' (noFloat "rem") (noDouble "rem") (noFP "rem") x y where rem' a b | kindOf x == KUnbounded = mod a (abs b) | otherwise = rem a b @@ -289,7 +295,7 @@ | isSet a && isSet b = svSetEqual a b | True - = liftSym2B (mkSymOpSC (eqOptBool Equal trueSV) Equal) rationalCheck (==) (==) (==) (==) (==) (==) (==) (==) (==) (==) (==) a b + = liftSym2B (mkSymOpSC (eqOptBool Equal trueSV) Equal) rationalCheck (==) (==) (==) (==) (==) (==) (==) (==) (==) (==) (==) (==) a b -- | Inequality. svNotEqual :: SVal -> SVal -> SVal @@ -297,7 +303,7 @@ | isSet a && isSet b = svNot $ svEqual a b | True - = liftSym2B (mkSymOpSC (eqOptBool NotEqual falseSV) NotEqual) rationalCheck (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) a b + = liftSym2B (mkSymOpSC (eqOptBool NotEqual falseSV) NotEqual) rationalCheck (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) (/=) a b -- | Set equality. Note that we only do constant folding if we get both a regular or both a -- complement set. Otherwise we get a symbolic value even if they might be completely concrete. @@ -321,21 +327,20 @@ -- | Strong equality. Only matters on floats, where it says @NaN@ equals @NaN@ and @+0@ and @-0@ are different. -- Otherwise equivalent to `svEqual`. svStrongEqual :: SVal -> SVal -> SVal -svStrongEqual x y - | isFloat x, Just f1 <- getF x, Just f2 <- getF y - = svBool $ f1 `fpIsEqualObjectH` f2 - | isDouble x, Just f1 <- getD x, Just f2 <- getD y - = svBool $ f1 `fpIsEqualObjectH` f2 - | isFloat x || isDouble x - = SVal KBool $ Right $ cache r - | True - = svEqual x y +svStrongEqual x y | isFloat x, Just f1 <- getF x, Just f2 <- getF y = svBool $ f1 `fpIsEqualObjectH` f2 + | isDouble x, Just f1 <- getD x, Just f2 <- getD y = svBool $ f1 `fpIsEqualObjectH` f2 + | isFP x, Just f1 <- getFP x, Just f2 <- getFP y = svBool $ f1 `fpIsEqualObjectH` f2 + | isFloat x || isDouble x || isFP x = SVal KBool $ Right $ cache r + | True = svEqual x y where getF (SVal _ (Left (CV _ (CFloat f)))) = Just f getF _ = Nothing getD (SVal _ (Left (CV _ (CDouble d)))) = Just d getD _ = Nothing + getFP (SVal _ (Left (CV _ (CFP f)))) = Just f + getFP _ = Nothing + r st = do sx <- svToSV st x sy <- svToSV st y newExpr st KBool (SBVApp (IEEEFP FP_ObjEqual) [sx, sy]) @@ -345,28 +350,28 @@ svLessThan x y | isConcreteMax x = svFalse | isConcreteMin y = svFalse - | True = liftSym2B (mkSymOpSC (eqOpt falseSV) LessThan) rationalCheck (<) (<) (<) (<) (<) (<) (<) (<) (<) (<) (uiLift "<" (<)) x y + | True = liftSym2B (mkSymOpSC (eqOpt falseSV) LessThan) rationalCheck (<) (<) (<) (<) (<) (<) (<) (<) (<) (<) (<) (uiLift "<" (<)) x y -- | Greater than. svGreaterThan :: SVal -> SVal -> SVal svGreaterThan x y | isConcreteMin x = svFalse | isConcreteMax y = svFalse - | True = liftSym2B (mkSymOpSC (eqOpt falseSV) GreaterThan) rationalCheck (>) (>) (>) (>) (>) (>) (>) (>) (>) (>) (uiLift ">" (>)) x y + | True = liftSym2B (mkSymOpSC (eqOpt falseSV) GreaterThan) rationalCheck (>) (>) (>) (>) (>) (>) (>) (>) (>) (>) (>) (uiLift ">" (>)) x y -- | Less than or equal to. svLessEq :: SVal -> SVal -> SVal svLessEq x y | isConcreteMin x = svTrue | isConcreteMax y = svTrue - | True = liftSym2B (mkSymOpSC (eqOpt trueSV) LessEq) rationalCheck (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (uiLift "<=" (<=)) x y + | True = liftSym2B (mkSymOpSC (eqOpt trueSV) LessEq) rationalCheck (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (<=) (uiLift "<=" (<=)) x y -- | Greater than or equal to. svGreaterEq :: SVal -> SVal -> SVal svGreaterEq x y | isConcreteMax x = svTrue | isConcreteMin y = svTrue - | True = liftSym2B (mkSymOpSC (eqOpt trueSV) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (uiLift ">=" (>=)) x y + | True = liftSym2B (mkSymOpSC (eqOpt trueSV) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (>=) (uiLift ">=" (>=)) x y -- | Bitwise and. svAnd :: SVal -> SVal -> SVal @@ -375,7 +380,7 @@ | isConcreteOnes x = y | isConcreteZero y = y | isConcreteOnes y = x - | True = liftSym2 (mkSymOpSC opt And) (const (const True)) (noReal ".&.") (.&.) (noFloat ".&.") (noDouble ".&.") x y + | True = liftSym2 (mkSymOpSC opt And) [] (noReal ".&.") (.&.) (noFloat ".&.") (noDouble ".&.") (noFP ".&.") x y where opt a b | a == falseSV || b == falseSV = Just falseSV | a == trueSV = Just b @@ -389,8 +394,8 @@ | isConcreteOnes x = x | isConcreteZero y = x | isConcreteOnes y = y - | True = liftSym2 (mkSymOpSC opt Or) (const (const True)) - (noReal ".|.") (.|.) (noFloat ".|.") (noDouble ".|.") x y + | True = liftSym2 (mkSymOpSC opt Or) [] + (noReal ".|.") (.|.) (noFloat ".|.") (noDouble ".|.") (noFP ".|.") x y where opt a b | a == trueSV || b == trueSV = Just trueSV | a == falseSV = Just b @@ -404,8 +409,8 @@ | isConcreteOnes x = svNot y | isConcreteZero y = x | isConcreteOnes y = svNot x - | True = liftSym2 (mkSymOpSC opt XOr) (const (const True)) - (noReal "xor") xor (noFloat "xor") (noDouble "xor") x y + | True = liftSym2 (mkSymOpSC opt XOr) [] + (noReal "xor") xor (noFloat "xor") (noDouble "xor") (noFP "xor") x y where opt a b | a == b && swKind a == KBool = Just falseSV | a == falseSV = Just b @@ -416,7 +421,7 @@ svNot :: SVal -> SVal svNot = liftSym1 (mkSymOp1SC opt Not) (noRealUnary "complement") complement - (noFloatUnary "complement") (noDoubleUnary "complement") + (noFloatUnary "complement") (noDoubleUnary "complement") (noFPUnary "complement") where opt a | a == falseSV = Just trueSV | a == trueSV = Just falseSV @@ -469,7 +474,7 @@ = case kindOf x of KBounded _ sz -> liftSym1 (mkSymOp1 (Rol (i `mod` sz))) (noRealUnary "rotateL") (rot True sz i) - (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x + (noFloatUnary "rotateL") (noDoubleUnary "rotateL") (noFPUnary "rotateL") x _ -> svShl x i -- for unbounded Integers, rotateL is the same as shiftL in Haskell -- | Rotate-right, by a constant. @@ -484,7 +489,7 @@ = case kindOf x of KBounded _ sz -> liftSym1 (mkSymOp1 (Ror (i `mod` sz))) (noRealUnary "rotateR") (rot False sz i) - (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x + (noFloatUnary "rotateR") (noDoubleUnary "rotateR") (noFPUnary "rotateR") x _ -> svShr x i -- for unbounded integers, rotateR is the same as shiftR in Haskell -- | Generic rotation. Since the underlying representation is just Integers, rotations has to be @@ -1260,9 +1265,9 @@ noStringLift2 :: String -> String -> a noStringLift2 x y = error $ "Unexpected binary operation called on strings: " ++ show (x, y) -liftSym1 :: (State -> Kind -> SV -> IO SV) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> SVal -> SVal -liftSym1 _ opCR opCI opCF opCD (SVal k (Left a)) = SVal k . Left $! mapCV opCR opCI opCF opCD noCharLift noStringLift noUnint a -liftSym1 opS _ _ _ _ a@(SVal k _) = SVal k $ Right $ cache c +liftSym1 :: (State -> Kind -> SV -> IO SV) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (FP -> FP) -> SVal -> SVal +liftSym1 _ opCR opCI opCF opCD opFP (SVal k (Left a)) = SVal k . Left $! mapCV opCR opCI opCF opCD opFP noCharLift noStringLift noUnint a +liftSym1 opS _ _ _ _ _ a@(SVal k _) = SVal k $ Right $ cache c where c st = do sva <- svToSV st a opS st k sva @@ -1319,14 +1324,15 @@ opS st k sw1 sw2 liftSym2 :: (State -> Kind -> SV -> SV -> IO SV) - -> (CV -> CV -> Bool) + -> [CV -> CV -> Bool] -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) + -> (FP -> FP -> FP) -> SVal -> SVal -> SVal -liftSym2 _ okCV opCR opCI opCF opCD (SVal k (Left a)) (SVal _ (Left b)) | okCV a b = SVal k . Left $! mapCV2 opCR opCI opCF opCD noCharLift2 noStringLift2 noUnint2 a b -liftSym2 opS _ _ _ _ _ a@(SVal k _) b = SVal k $ Right $ liftSV2 opS k a b +liftSym2 _ okCV opCR opCI opCF opCD opFP (SVal k (Left a)) (SVal _ (Left b)) | and [f a b | f <- okCV] = SVal k . Left $! mapCV2 opCR opCI opCF opCD opFP noCharLift2 noStringLift2 noUnint2 a b +liftSym2 opS _ _ _ _ _ _ a@(SVal k _) b = SVal k $ Right $ liftSV2 opS k a b liftSym2B :: (State -> Kind -> SV -> SV -> IO SV) -> (CV -> CV -> Bool) @@ -1334,6 +1340,7 @@ -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) + -> (FP -> FP -> Bool) -> (Char -> Char -> Bool) -> (String -> String -> Bool) -> ([CVal] -> [CVal] -> Bool) @@ -1342,8 +1349,8 @@ -> (Either CVal CVal -> Either CVal CVal -> Bool) -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool) -> SVal -> SVal -> SVal -liftSym2B _ okCV opCR opCI opCF opCD opCC opCS opCSeq opCTup opCMaybe opCEither opUI (SVal _ (Left a)) (SVal _ (Left b)) | okCV a b = svBool (liftCV2 opCR opCI opCF opCD opCC opCS opCSeq opCTup opCMaybe opCEither opUI a b) -liftSym2B opS _ _ _ _ _ _ _ _ _ _ _ _ a b = SVal KBool $ Right $ liftSV2 opS KBool a b +liftSym2B _ okCV opCR opCI opCF opCD opAF opCC opCS opCSeq opCTup opCMaybe opCEither opUI (SVal _ (Left a)) (SVal _ (Left b)) | okCV a b = svBool (liftCV2 opCR opCI opCF opCD opAF opCC opCS opCSeq opCTup opCMaybe opCEither opUI a b) +liftSym2B opS _ _ _ _ _ _ _ _ _ _ _ _ _ a b = SVal KBool $ Right $ liftSV2 opS KBool a b -- | Create a symbolic two argument operation; with shortcut optimizations mkSymOpSC :: (SV -> SV -> Maybe SV) -> Op -> State -> Kind -> SV -> SV -> IO SV @@ -1360,13 +1367,14 @@ mkSymOp1 = mkSymOp1SC (const Nothing) -- | eqOpt says the references are to the same SV, thus we can optimize. Note that --- we explicitly disallow KFloat/KDouble here. Why? Because it's *NOT* true that +-- we explicitly disallow KFloat/KDouble/KFloat here. Why? Because it's *NOT* true that -- NaN == NaN, NaN >= NaN, and so-forth. So, we have to make sure we don't optimize -- floats and doubles, in case the argument turns out to be NaN. eqOpt :: SV -> SV -> SV -> Maybe SV eqOpt w x y = case swKind x of KFloat -> Nothing KDouble -> Nothing + KFP{} -> Nothing _ -> if x == y then Just w else Nothing -- For uninterpreted/enumerated values, we carefully lift through the constructor index for comparisons: @@ -1428,7 +1436,6 @@ _ -> True -- | Quot/Rem operations require a nonzero check on the divisor. --- nonzeroCheck :: CV -> CV -> Bool nonzeroCheck _ b = cvVal b /= CInteger 0 @@ -1446,6 +1453,9 @@ noDouble :: String -> Double -> Double -> Double noDouble o a b = error $ "SBV.Double." ++ o ++ ": Unexpected arguments: " ++ show (a, b) +noFP :: String -> FP -> FP -> FP +noFP o a b = error $ "SBV.FPR." ++ o ++ ": Unexpected arguments: " ++ show (a, b) + noRealUnary :: String -> AlgReal -> AlgReal noRealUnary o a = error $ "SBV.AlgReal." ++ o ++ ": Unexpected argument: " ++ show a @@ -1454,6 +1464,10 @@ noDoubleUnary :: String -> Double -> Double noDoubleUnary o a = error $ "SBV.Double." ++ o ++ ": Unexpected argument: " ++ show a + + +noFPUnary :: String -> FP -> FP +noFPUnary o a = error $ "SBV.FPR." ++ o ++ ": Unexpected argument: " ++ show a -- | Given a composite structure, figure out how to compare for less than svStructuralLessThan :: SVal -> SVal -> SVal diff --git a/Data/SBV/Core/Sized.hs b/Data/SBV/Core/Sized.hs --- a/Data/SBV/Core/Sized.hs +++ b/Data/SBV/Core/Sized.hs @@ -25,12 +25,10 @@ SWord, WordN, sWord, sWord_, sWords -- * Type-sized signed bit-vectors , SInt, IntN, sInt, sInt_, sInts - -- Bit-vector operations + -- * Bit-vector operations , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake - -- Splitting and reconstructing from bytes + -- * Splitting and reconstructing from bytes , ByteConverter(..) - -- Non-zero constraint - , IsNonZero ) where import Data.Bits @@ -38,9 +36,9 @@ import Data.Proxy (Proxy(..)) import GHC.TypeLits -import Data.Kind import Data.SBV.Core.Data +import Data.SBV.Core.Kind import Data.SBV.Core.Model import Data.SBV.Core.Operations import Data.SBV.Core.Symbolic @@ -63,24 +61,12 @@ instance Show (WordN n) where show (WordN v) = show v --- | Grab the bit-size from the proxy -intOfProxy :: KnownNat n => Proxy n -> Int -intOfProxy = fromEnum . natVal - --- | Catch 0-width cases -type ZeroWidth = 'Text "Zero-width BV's are not allowed." - --- | Type family to create the appropriate non-zero constraint -type family IsNonZero (arg :: Nat) :: Constraint where - IsNonZero 0 = TypeError ZeroWidth - IsNonZero _ = () - -- | 'WordN' has a kind -instance (KnownNat n, IsNonZero n) => HasKind (WordN n) where +instance (KnownNat n, BVIsNonZero n) => HasKind (WordN n) where kindOf _ = KBounded False (intOfProxy (Proxy @n)) -- | 'SymVal' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => SymVal (WordN n) where +instance (KnownNat n, BVIsNonZero n) => SymVal (WordN n) where literal x = genLiteral (kindOf x) x mkSymVal = genMkSymVar (kindOf (undefined :: WordN n)) fromCV = genFromCV @@ -96,17 +82,17 @@ show (IntN v) = show v -- | 'IntN' has a kind -instance (KnownNat n, IsNonZero n) => HasKind (IntN n) where +instance (KnownNat n, BVIsNonZero n) => HasKind (IntN n) where kindOf _ = KBounded True (intOfProxy (Proxy @n)) -- | 'SymVal' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => SymVal (IntN n) where +instance (KnownNat n, BVIsNonZero n) => SymVal (IntN n) where literal x = genLiteral (kindOf x) x mkSymVal = genMkSymVar (kindOf (undefined :: IntN n)) fromCV = genFromCV -- Lift a unary operation via SVal -lift1 :: (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal) -> bv n -> bv n +lift1 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal) -> bv n -> bv n lift1 nm op x = uc $ op (c x) where k = kindOf x c = SVal k . Left . CV k . CInteger . toInteger @@ -114,7 +100,7 @@ uc r = error $ "Impossible happened while lifting " ++ show nm ++ " over " ++ show (k, x, r) -- Lift a binary operation via SVal -lift2 :: (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n +lift2 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n lift2 nm op x y = uc $ c x `op` c y where k = kindOf x c = SVal k . Left . CV k . CInteger . toInteger @@ -122,7 +108,7 @@ uc r = error $ "Impossible happened while lifting " ++ show nm ++ " over " ++ show (k, x, y, r) -- Lift a binary operation via SVal where second argument is an Int -lift2I :: (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n +lift2I :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n lift2I nm op x i = uc $ c x `op` i where k = kindOf x c = SVal k . Left . CV k . CInteger . toInteger @@ -130,7 +116,7 @@ uc r = error $ "Impossible happened while lifting " ++ show nm ++ " over " ++ show (k, x, i, r) -- Lift a binary operation via SVal where second argument is an Int and returning a Bool -lift2IB :: (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool +lift2IB :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool lift2IB nm op x i = uc $ c x `op` i where k = kindOf x c = SVal k . Left . CV k . CInteger . toInteger @@ -138,17 +124,17 @@ uc r = error $ "Impossible happened while lifting " ++ show nm ++ " over " ++ show (k, x, i, r) -- | 'Bounded' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => Bounded (WordN n) where +instance (KnownNat n, BVIsNonZero n) => Bounded (WordN n) where minBound = WordN 0 maxBound = let sz = intOfProxy (Proxy @n) in WordN $ 2 ^ sz - 1 -- | 'Bounded' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => Bounded (IntN n) where +instance (KnownNat n, BVIsNonZero n) => Bounded (IntN n) where minBound = let sz1 = intOfProxy (Proxy @n) - 1 in IntN $ - (2 ^ sz1) maxBound = let sz1 = intOfProxy (Proxy @n) - 1 in IntN $ 2 ^ sz1 - 1 -- | 'Num' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => Num (WordN n) where +instance (KnownNat n, BVIsNonZero n) => Num (WordN n) where (+) = lift2 "(+)" svPlus (-) = lift2 "(*)" svMinus (*) = lift2 "(*)" svTimes @@ -158,7 +144,7 @@ fromInteger = WordN . fromJust . svAsInteger . svInteger (kindOf (undefined :: WordN n)) -- | 'Num' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => Num (IntN n) where +instance (KnownNat n, BVIsNonZero n) => Num (IntN n) where (+) = lift2 "(+)" svPlus (-) = lift2 "(*)" svMinus (*) = lift2 "(*)" svTimes @@ -168,35 +154,35 @@ fromInteger = IntN . fromJust . svAsInteger . svInteger (kindOf (undefined :: IntN n)) -- | 'Enum' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => Enum (WordN n) where +instance (KnownNat n, BVIsNonZero n) => Enum (WordN n) where toEnum = fromInteger . toInteger fromEnum = fromIntegral . toInteger -- | 'Enum' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => Enum (IntN n) where +instance (KnownNat n, BVIsNonZero n) => Enum (IntN n) where toEnum = fromInteger . toInteger fromEnum = fromIntegral . toInteger -- | 'Real' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => Real (WordN n) where +instance (KnownNat n, BVIsNonZero n) => Real (WordN n) where toRational (WordN x) = toRational x -- | 'Real' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => Real (IntN n) where +instance (KnownNat n, BVIsNonZero n) => Real (IntN n) where toRational (IntN x) = toRational x -- | 'Integral' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => Integral (WordN n) where +instance (KnownNat n, BVIsNonZero n) => Integral (WordN n) where toInteger (WordN x) = x quotRem (WordN x) (WordN y) = let (q, r) = quotRem x y in (WordN q, WordN r) -- | 'Integral' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => Integral (IntN n) where +instance (KnownNat n, BVIsNonZero n) => Integral (IntN n) where toInteger (IntN x) = x quotRem (IntN x) (IntN y) = let (q, r) = quotRem x y in (IntN q, IntN r) -- 'Bits' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => Bits (WordN n) where +instance (KnownNat n, BVIsNonZero n) => Bits (WordN n) where (.&.) = lift2 "(.&.)" svAnd (.|.) = lift2 "(.|.)" svOr xor = lift2 "xor" svXOr @@ -213,7 +199,7 @@ popCount = fromIntegral . popCount . toInteger -- 'Bits' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => Bits (IntN n) where +instance (KnownNat n, BVIsNonZero n) => Bits (IntN n) where (.&.) = lift2 "(.&.)" svAnd (.|.) = lift2 "(.|.)" svOr xor = lift2 "xor" svXOr @@ -230,94 +216,94 @@ popCount = fromIntegral . popCount . toInteger -- | 'SIntegral' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => SIntegral (WordN n) +instance (KnownNat n, BVIsNonZero n) => SIntegral (WordN n) -- | 'SIntegral' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => SIntegral (IntN n) +instance (KnownNat n, BVIsNonZero n) => SIntegral (IntN n) -- | 'SDivisible' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => SDivisible (WordN n) where +instance (KnownNat n, BVIsNonZero n) => SDivisible (WordN n) where sQuotRem x 0 = (0, x) sQuotRem x y = x `quotRem` y sDivMod x 0 = (0, x) sDivMod x y = x `divMod` y -- | 'SDivisible' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => SDivisible (IntN n) where +instance (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) where sQuotRem x 0 = (0, x) sQuotRem x y = x `quotRem` y sDivMod x 0 = (0, x) sDivMod x y = x `divMod` y -- | 'SDivisible' instance for 'SWord' -instance (KnownNat n, IsNonZero n) => SDivisible (SWord n) where +instance (KnownNat n, BVIsNonZero n) => SDivisible (SWord n) where sQuotRem = liftQRem sDivMod = liftDMod -- | 'SDivisible' instance for 'SInt' -instance (KnownNat n, IsNonZero n) => SDivisible (SInt n) where +instance (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) where sQuotRem = liftQRem sDivMod = liftDMod -- | 'SFiniteBits' instance for 'WordN' -instance (KnownNat n, IsNonZero n) => SFiniteBits (WordN n) where +instance (KnownNat n, BVIsNonZero n) => SFiniteBits (WordN n) where sFiniteBitSize _ = intOfProxy (Proxy @n) -- | 'SFiniteBits' instance for 'IntN' -instance (KnownNat n, IsNonZero n) => SFiniteBits (IntN n) where +instance (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN n) where sFiniteBitSize _ = intOfProxy (Proxy @n) -- | Constructing models for 'WordN' -instance (KnownNat n, IsNonZero n) => SatModel (WordN n) where +instance (KnownNat n, BVIsNonZero n) => SatModel (WordN n) where parseCVs = genParse (kindOf (undefined :: WordN n)) -- | Constructing models for 'IntN' -instance (KnownNat n, IsNonZero n) => SatModel (IntN n) where +instance (KnownNat n, BVIsNonZero n) => SatModel (IntN n) where parseCVs = genParse (kindOf (undefined :: IntN n)) -- | Optimizing 'WordN' -instance (KnownNat n, IsNonZero n) => Metric (WordN n) +instance (KnownNat n, BVIsNonZero n) => Metric (WordN n) -- | Optimizing 'IntN' -instance (KnownNat n, IsNonZero n) => Metric (IntN n) where +instance (KnownNat n, BVIsNonZero n) => Metric (IntN n) where type MetricSpace (IntN n) = WordN n toMetricSpace x = sFromIntegral x + 2 ^ (intOfProxy (Proxy @n) - 1) fromMetricSpace x = sFromIntegral x - 2 ^ (intOfProxy (Proxy @n) - 1) -- | Generalization of 'Data.SBV.sWord' -sWord :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SWord n) +sWord :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SWord n) sWord = symbolic -- | Generalization of 'Data.SBV.sWord_' -sWord_ :: (KnownNat n, IsNonZero n) => MonadSymbolic m => m (SWord n) +sWord_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SWord n) sWord_ = free_ -- | Generalization of 'Data.SBV.sWord64s' -sWords :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SWord n] +sWords :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SWord n] sWords = symbolics -- | Generalization of 'Data.SBV.sInt' -sInt :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SInt n) +sInt :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SInt n) sInt = symbolic -- | Generalization of 'Data.SBV.sInt_' -sInt_ :: (KnownNat n, IsNonZero n) => MonadSymbolic m => m (SInt n) +sInt_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SInt n) sInt_ = free_ -- | Generalization of 'Data.SBV.sInts' -sInts :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SInt n] +sInts :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SInt n] sInts = symbolics -- | Extract a portion of bits to form a smaller bit-vector. -- -- >>> prove $ \x -> bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x) -- Q.E.D. -bvExtract :: forall i j n bv proxy. ( KnownNat n, IsNonZero n, SymVal (bv n) +bvExtract :: forall i j n bv proxy. ( KnownNat n, BVIsNonZero n, SymVal (bv n) , KnownNat i , KnownNat j , i + 1 <= n , j <= i - , IsNonZero (i - j + 1) + , BVIsNonZero (i - j + 1) ) => proxy i -- ^ @i@: Start position, numbered from @n-1@ to @0@ -> proxy j -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold -> SBV (bv n) -- ^ Input bit vector of size @n@ @@ -330,8 +316,8 @@ -- -- >>> prove $ \x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71)) -- Q.E.D. -(#) :: ( KnownNat n, IsNonZero n, SymVal (bv n) - , KnownNat m, IsNonZero m, SymVal (bv m) +(#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n) + , KnownNat m, BVIsNonZero m, SymVal (bv m) ) => SBV (bv n) -- ^ First input, of size @n@, becomes the left side -> SBV (bv m) -- ^ Second input, of size @m@, becomes the right side -> SBV (bv (n + m)) -- ^ Concatenation, of size @n+m@ @@ -342,11 +328,11 @@ -- -- >>> prove $ \x -> bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0 -- Q.E.D. -zeroExtend :: forall n m bv. ( KnownNat n, IsNonZero n, SymVal (bv n) - , KnownNat m, IsNonZero m, SymVal (bv m) +zeroExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n) + , KnownNat m, BVIsNonZero m, SymVal (bv m) , n + 1 <= m , SIntegral (bv (m - n)) - , IsNonZero (m - n) + , BVIsNonZero (m - n) ) => SBV (bv n) -- ^ Input, of size @n@ -> SBV (bv m) -- ^ Output, of size @m@. @n < m@ must hold zeroExtend n = SBV $ svJoin (unSBV zero) (unSBV n) @@ -359,12 +345,12 @@ -- Q.E.D. -- >>> prove $ \x -> msb x .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== complement 0 -- Q.E.D. -signExtend :: forall n m bv. ( KnownNat n, IsNonZero n, SymVal (bv n) - , KnownNat m, IsNonZero m, SymVal (bv m) +signExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n) + , KnownNat m, BVIsNonZero m, SymVal (bv m) , n + 1 <= m , SFiniteBits (bv n) , SIntegral (bv (m - n)) - , IsNonZero (m - n) + , BVIsNonZero (m - n) ) => SBV (bv n) -- ^ Input, of size @n@ -> SBV (bv m) -- ^ Output, of size @m@. @n < m@ must hold signExtend n = SBV $ svJoin (unSBV ext) (unSBV n) @@ -379,11 +365,11 @@ -- Q.E.D. -- >>> prove $ \x -> bvDrop (Proxy @20) (x :: SWord 21) .== ite (lsb x) 1 0 -- Q.E.D. -bvDrop :: forall i n m bv proxy. ( KnownNat n, IsNonZero n +bvDrop :: forall i n m bv proxy. ( KnownNat n, BVIsNonZero n , KnownNat i , i + 1 <= n , i + m - n <= 0 - , IsNonZero (n - i) + , BVIsNonZero (n - i) ) => proxy i -- ^ @i@: Number of bits to drop. @i < n@ must hold. -> SBV (bv n) -- ^ Input, of size @n@ -> SBV (bv m) -- ^ Output, of size @m@. @m = n - i@ holds. @@ -399,8 +385,8 @@ -- Q.E.D. -- >>> prove $ \x -> bvTake (Proxy @4) x # bvDrop (Proxy @4) x .== (x :: SWord 23) -- Q.E.D. -bvTake :: forall i n bv proxy. ( KnownNat n, IsNonZero n - , KnownNat i, IsNonZero i +bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n + , KnownNat i, BVIsNonZero i , i <= n ) => proxy i -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold. -> SBV (bv n) -- ^ Input, of size @n@ diff --git a/Data/SBV/Core/SizedFloats.hs b/Data/SBV/Core/SizedFloats.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Core/SizedFloats.hs @@ -0,0 +1,343 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Core.Sized +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Type-level sized floats. +----------------------------------------------------------------------------- + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Data.SBV.Core.SizedFloats ( + -- * Type-sized floats + FloatingPoint(..), FP(..), FPHalf, FPSingle, FPDouble, FPQuad + + -- * Constructing values + , fpFromRawRep, fpNaN, fpInf, fpZero + + -- * Operations + , fpFromInteger, fpFromRational, fpFromFloat, fpFromDouble, fpEncodeFloat + + -- * Internal operations + , fprCompareObject, fprToSMTLib2, mkBFOpts, bfToString + ) where + +import Data.Char (intToDigit) +import Data.Proxy +import GHC.TypeLits + +import Data.Bits +import Data.Ratio +import Numeric + +import Data.SBV.Core.Kind +import Data.SBV.Utils.Numeric (floatToWord) + +import LibBF (BigFloat, BFOpts, RoundMode, Status) +import qualified LibBF as BF + +-- | A floating point value, indexed by its exponent and significand sizes. +-- +-- An IEEE SP is @FloatingPoint 8 24@ +-- DP is @FloatingPoint 11 53@ +-- etc. +newtype FloatingPoint (eb :: Nat) (sb :: Nat) = FloatingPoint FP + deriving (Eq, Ord) + +-- | Abbreviation for IEEE half precision float, bit width 16. +type FPHalf = FloatingPoint 5 11 + +-- | Abbreviation for IEEE single precision float, bit width 32. +type FPSingle = FloatingPoint 8 24 + +-- | Abbreviation for IEEE double precision float, bit width 64. +type FPDouble = FloatingPoint 11 53 + +-- | Abbreviation for IEEE quadruble precision float, bit width 128. +type FPQuad = FloatingPoint 15 113 + +-- | Show instance for Floats. By default we print in base 10, with standard scientific notation. +instance Show (FloatingPoint eb sb) where + show (FloatingPoint r) = show r + +-- | Internal representation of a parameterized float. +-- +-- A note on cardinality: If we have eb exponent bits, and sb significand bits, +-- then the total number of floats is 2^sb*(2^eb-1) + 3: All exponents except 11..11 +-- is allowed. So we get, 2^eb-1, different combinations, each with a sign, giving +-- us 2^sb*(2^eb-1) totals. Then we have two infinities, and one NaN, adding 3 more. +data FP = FP { fpExponentSize :: Int + , fpSignificandSize :: Int + , fpValue :: BigFloat + } + deriving (Ord, Eq) + +instance Show FP where + show = bfToString 10 False + +-- | Show a big float in the base given. +-- NB. Do not be tempted to use BF.showFreeMin below; it produces arguably correct +-- but very confusing results. See +-- for a discussion of the issues. +bfToString :: Int -> Bool -> FP -> String +bfToString b withPrefix (FP _ sb a) + | BF.bfIsNaN a = "NaN" + | BF.bfIsInf a = if BF.bfIsPos a then "Infinity" else "-Infinity" + | BF.bfIsZero a = if BF.bfIsPos a then "0.0" else "-0.0" + | True = trimZeros $ BF.bfToString b withP a + where opts = BF.showRnd BF.NearEven <> BF.showFree (Just (fromIntegral sb)) + withP + | withPrefix = BF.addPrefix <> opts + | True = opts + + trimZeros s + | '.' `elem` s = reverse $ case dropWhile (== '0') $ reverse s of + res@('.':_) -> '0' : res + res -> res + | True = s + +-- | Default options for BF options. +mkBFOpts :: Integral a => a -> a -> RoundMode -> BFOpts +mkBFOpts eb sb rm = BF.allowSubnormal <> BF.rnd rm <> BF.expBits (fromIntegral eb) <> BF.precBits (fromIntegral sb) + +-- | normFP the float to make sure it's within the required range +mkFP :: Int -> Int -> BigFloat -> FP +mkFP eb sb r = FP eb sb $ fst $ BF.bfRoundFloat (mkBFOpts eb sb BF.NearEven) r + +-- | Convert from an sign/exponent/mantissa representation to a float. The values are the integers +-- representing the bit-patterns of these values, i.e., the raw representation. We assume that these +-- integers fit into the ranges given, i.e., no overflow checking is done here. +fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP +fpFromRawRep sign (e, eb) (s, sb) = FP eb sb $ BF.bfFromBits (mkBFOpts eb sb BF.NearEven) val + where es, val :: Integer + es = (e `shiftL` (sb - 1)) .|. s + val | sign = (1 `shiftL` (eb + sb - 1)) .|. es + | True = es + +-- | Make NaN. Exponent is all 1s. Significand is non-zero. The sign is irrelevant. +fpNaN :: Int -> Int -> FP +fpNaN eb sb = mkFP eb sb BF.bfNaN + +-- | Make Infinity. Exponent is all 1s. Significand is 0. +fpInf :: Bool -> Int -> Int -> FP +fpInf sign eb sb = mkFP eb sb $ if sign then BF.bfNegInf else BF.bfPosInf + +-- | Make a signed zero. +fpZero :: Bool -> Int -> Int -> FP +fpZero sign eb sb = mkFP eb sb $ if sign then BF.bfNegZero else BF.bfPosZero + +-- | Make from an integer value. +fpFromInteger :: Int -> Int -> Integer -> FP +fpFromInteger eb sb iv = mkFP eb sb $ BF.bfFromInteger iv + +-- | Make a generalized floating-point value from a 'Rational'. +fpFromRational :: Int -> Int -> Rational -> FP +fpFromRational eb sb r = FP eb sb $ fst $ BF.bfDiv (mkBFOpts eb sb BF.NearEven) (BF.bfFromInteger (numerator r)) + (BF.bfFromInteger (denominator r)) + +-- | Represent the FP in SMTLib2 format +fprToSMTLib2 :: FP -> String +fprToSMTLib2 (FP eb sb r) + | BF.bfIsNaN r = as "NaN" + | BF.bfIsInf r = as $ if BF.bfIsPos r then "+oo" else "-oo" + | BF.bfIsZero r = as $ if BF.bfIsPos r then "+zero" else "-zero" + | True = generic + where e = show eb + s = show sb + + bits = BF.bfToBits (mkBFOpts eb sb BF.NearEven) r + significandMask = (1 :: Integer) `shiftL` (sb - 1) - 1 + exponentMask = (1 :: Integer) `shiftL` eb - 1 + + fpSign = bits `testBit` (eb + sb - 1) + fpExponent = (bits `shiftR` (sb - 1)) .&. exponentMask + fpSignificand = bits .&. significandMask + + generic = "(fp " ++ unwords [if fpSign then "#b1" else "#b0", mkB eb fpExponent, mkB (sb - 1) fpSignificand] ++ ")" + + as x = "(_ " ++ x ++ " " ++ e ++ " " ++ s ++ ")" + + mkB sz val = "#b" ++ pad sz (showBin val "") + showBin = showIntAtBase 2 intToDigit + pad l str = replicate (l - length str) '0' ++ str + +-- | Structural comparison only, for internal map indexes +fprCompareObject :: FP -> FP -> Ordering +fprCompareObject (FP eb sb a) (FP eb' sb' b) = case (eb, sb) `compare` (eb', sb') of + LT -> LT + GT -> GT + EQ -> a `BF.bfCompare` b + + +-- | Compute the signum of a big float +bfSignum :: BigFloat -> BigFloat +bfSignum r | BF.bfIsNaN r = r + | BF.bfIsZero r = r + | BF.bfIsPos r = BF.bfFromInteger 1 + | True = BF.bfFromInteger (-1) + +-- | Num instance for big-floats +instance Num FP where + (+) = lift2 BF.bfAdd + (-) = lift2 BF.bfSub + (*) = lift2 BF.bfMul + abs = lift1 BF.bfAbs + signum = lift1 bfSignum + fromInteger = error "FP.fromInteger: Not supported for arbitrary floats. Use fpFromInteger instead, specifying the precision" + negate = lift1 BF.bfNeg + +-- | Fractional instance for big-floats +instance Fractional FP where + fromRational = error "FP.fromRational: Not supported for arbitrary floats. Use fpFromRational instead, specifying the precision" + (/) = lift2 BF.bfDiv + +-- | Floating instance for big-floats +instance Floating FP where + sqrt (FP eb sb a) = FP eb sb $ fst $ BF.bfSqrt (mkBFOpts eb sb BF.NearEven) a + FP eb sb a ** FP _ _ b = FP eb sb $ fst $ BF.bfPow (mkBFOpts eb sb BF.NearEven) a b + + pi = unsupported "Floating.FP.pi" + exp = unsupported "Floating.FP.exp" + log = unsupported "Floating.FP.log" + sin = unsupported "Floating.FP.sin" + cos = unsupported "Floating.FP.cos" + tan = unsupported "Floating.FP.tan" + asin = unsupported "Floating.FP.asin" + acos = unsupported "Floating.FP.acos" + atan = unsupported "Floating.FP.atan" + sinh = unsupported "Floating.FP.sinh" + cosh = unsupported "Floating.FP.cosh" + tanh = unsupported "Floating.FP.tanh" + asinh = unsupported "Floating.FP.asinh" + acosh = unsupported "Floating.FP.acosh" + atanh = unsupported "Floating.FP.atanh" + +-- | Real-float instance for big-floats. Beware! Some of these aren't really all that well tested. +instance RealFloat FP where + floatRadix _ = 2 + floatDigits (FP _ sb _) = sb + floatRange (FP eb _ _) = (fromIntegral (-v+3), fromIntegral v) + where v :: Integer + v = 2 ^ ((fromIntegral eb :: Integer) - 1) + + isNaN (FP _ _ r) = BF.bfIsNaN r + isInfinite (FP _ _ r) = BF.bfIsInf r + isDenormalized (FP eb sb r) = BF.bfIsSubnormal (mkBFOpts eb sb BF.NearEven) r + isNegativeZero (FP _ _ r) = BF.bfIsZero r && BF.bfIsNeg r + isIEEE _ = True + + decodeFloat i@(FP _ _ r) = case BF.bfToRep r of + BF.BFNaN -> decodeFloat (0/0 :: Double) + BF.BFRep s n -> case n of + BF.Zero -> (0, 0) + BF.Inf -> let (_, m) = floatRange i + x = (2 :: Integer) ^ toInteger (m+1) + in (if s == BF.Neg then -x else x, 0) + BF.Num x y -> -- The value here is x * 2^y + (if s == BF.Neg then -x else x, fromIntegral y) + + encodeFloat = error "FP.encodeFloat: Not supported for arbitrary floats. Use fpEncodeFloat instead, specifying the precision" + +-- | Encode from exponent/mantissa form to a float representation. Corresponds to 'encodeFloat' in Haskell. +fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP +fpEncodeFloat eb sb m n | n < 0 = fpFromRational eb sb (m % n') + | True = fpFromRational eb sb (m * n' % 1) + where n' :: Integer + n' = (2 :: Integer) ^ abs (fromIntegral n :: Integer) + +-- | Real instance for big-floats. Beware, not that well tested! +instance Real FP where + toRational i + | n >= 0 = m * 2 ^ n % 1 + | True = m % 2 ^ abs n + where (m, n) = decodeFloat i + +-- | Real-frac instance for big-floats. Beware, not that well tested! +instance RealFrac FP where + properFraction (FP eb sb r) = case BF.bfRoundInt BF.ToNegInf r of + (r', BF.Ok) | BF.bfSign r == BF.bfSign r' -> (getInt r', FP eb sb r - FP eb sb r') + x -> error $ "RealFrac.FP.properFraction: Failed to convert: " ++ show (r, x) + where getInt x = case BF.bfToRep x of + BF.BFNaN -> error $ "Data.SBV.FloatingPoint.properFraction: Failed to convert: " ++ show (r, x) + BF.BFRep s n -> case n of + BF.Zero -> 0 + BF.Inf -> error $ "Data.SBV.FloatingPoint.properFraction: Failed to convert: " ++ show (r, x) + BF.Num v y -> -- The value here is x * 2^y, and is integer if y >= 0 + let e :: Integer + e = 2 ^ (fromIntegral y :: Integer) + sgn = if s == BF.Neg then ((-1) *) else id + in if y > 0 + then fromIntegral $ sgn $ v * e + else fromIntegral $ sgn v + +-- | Num instance for FloatingPoint +instance ValidFloat eb sb => Num (FloatingPoint eb sb) where + FloatingPoint a + FloatingPoint b = FloatingPoint $ a + b + FloatingPoint a * FloatingPoint b = FloatingPoint $ a * b + + abs (FloatingPoint fp) = FloatingPoint (abs fp) + signum (FloatingPoint fp) = FloatingPoint (signum fp) + negate (FloatingPoint fp) = FloatingPoint (negate fp) + + fromInteger = FloatingPoint . fpFromInteger (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb)) + +instance ValidFloat eb sb => Fractional (FloatingPoint eb sb) where + fromRational = FloatingPoint . fpFromRational (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb)) + + FloatingPoint a / FloatingPoint b = FloatingPoint (a / b) + +unsupported :: String -> a +unsupported w = error $ "Data.SBV.FloatingPoint: Unsupported operation: " ++ w ++ ". Please request this as a feature!" + +-- Float instance. Most methods are left unimplemented. +instance ValidFloat eb sb => Floating (FloatingPoint eb sb) where + pi = FloatingPoint pi + + exp (FloatingPoint i) = FloatingPoint (exp i) + sqrt (FloatingPoint i) = FloatingPoint (sqrt i) + + FloatingPoint a ** FloatingPoint b = FloatingPoint $ a ** b + + log (FloatingPoint i) = FloatingPoint (log i) + sin (FloatingPoint i) = FloatingPoint (sin i) + cos (FloatingPoint i) = FloatingPoint (cos i) + tan (FloatingPoint i) = FloatingPoint (tan i) + asin (FloatingPoint i) = FloatingPoint (asin i) + acos (FloatingPoint i) = FloatingPoint (acos i) + atan (FloatingPoint i) = FloatingPoint (atan i) + sinh (FloatingPoint i) = FloatingPoint (sinh i) + cosh (FloatingPoint i) = FloatingPoint (cosh i) + tanh (FloatingPoint i) = FloatingPoint (tanh i) + asinh (FloatingPoint i) = FloatingPoint (asinh i) + acosh (FloatingPoint i) = FloatingPoint (acosh i) + atanh (FloatingPoint i) = FloatingPoint (atanh i) + +-- | Lift a unary operation, simple case of function with no status. Here, we call mkFP since the big-float isn't size aware. +lift1 :: (BigFloat -> BigFloat) -> FP -> FP +lift1 f (FP eb sb a) = mkFP eb sb $ f a + +-- Lift a binary operation. Here we don't call mkFP, because the result is correctly rounded. +lift2 :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> FP -> FP -> FP +lift2 f (FP eb sb a) (FP _ _ b) = FP eb sb $ fst $ f (mkBFOpts eb sb BF.NearEven) a b + +-- | Convert from a IEEE float. +fpFromFloat :: Int -> Int -> Float -> FP +fpFromFloat 8 24 f = let fw = floatToWord f + (sgn, e, s) = (fw `testBit` 31, fromIntegral (fw `shiftR` 23) .&. 0xFF, fromIntegral fw .&. 0x7FFFFF) + in fpFromRawRep sgn (e, 8) (s, 24) +fpFromFloat eb sb f = error $ "SBV.fprFromFloat: Unexpected input: " ++ show (eb, sb, f) + +-- | Convert from a IEEE double. +fpFromDouble :: Int -> Int -> Double -> FP +fpFromDouble 11 54 d = FP 11 54 $ BF.bfFromDouble d +fpFromDouble eb sb d = error $ "SBV.fprFromDouble: Unexpected input: " ++ show (eb, sb, d) 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 @@ -238,10 +238,11 @@ -- is FP_Cast; where we handle different source/origins explicitly later on. instance Show FPOp where show (FP_Cast f t r) = "(FP_Cast: " ++ show f ++ " -> " ++ show t ++ ", using RM [" ++ show r ++ "])" - show (FP_Reinterpret f t) = case (f, t) of - (KBounded False 32, KFloat) -> "(_ to_fp 8 24)" - (KBounded False 64, KDouble) -> "(_ to_fp 11 53)" - _ -> error $ "SBV.FP_Reinterpret: Unexpected conversion: " ++ show f ++ " to " ++ show t + show (FP_Reinterpret f t) = case t of + KFloat -> "(_ to_fp 8 24)" + KDouble -> "(_ to_fp 11 53)" + KFP eb sb -> "(_ to_fp " ++ show eb ++ " " ++ show sb ++ ")" + _ -> error $ "SBV.FP_Reinterpret: Unexpected conversion: " ++ show f ++ " to " ++ show t show FP_Abs = "fp.abs" show FP_Neg = "fp.neg" show FP_Add = "fp.add" @@ -1168,11 +1169,11 @@ show (SVal k (Left c)) = showCV False c ++ " :: " ++ show k show (SVal k (Right _)) = " :: " ++ show k --- We really don't want an 'Eq' instance for 'SBV' or 'SVal'. As it really makes no sense. --- But since we do want the 'Bits' instance, we're forced to define equality. See --- . We simply error out. -- | This instance is only defined so that we can define an instance for -- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. +-- We really don't want an 'Eq' instance for 'Data.SBV.Core.SBV' or 'SVal'. As it really makes no sense. +-- But since we do want the 'Data.Bits.Bits' instance, we're forced to define equality. See +-- . We simply error out. instance Eq SVal where a == b = noEquals "==" ".==" (show a, show b) a /= b = noEquals "/=" "./=" (show a, show b) @@ -1358,6 +1359,7 @@ KUserSort {} -> return () KFloat {} -> return () KDouble {} -> return () + KFP {} -> return () KChar {} -> return () KString {} -> return () KList ek -> registerKind st ek @@ -1558,7 +1560,7 @@ (_ , Concrete Nothing) -> noUI (randomCV k >>= mkC) -- Model validation: - (_ , Concrete (Just (_isSat, env))) -> + (_ , Concrete (Just (_isSat, env))) -> do let bad why conc = error $ unlines [ "" , "*** Data.SBV: " ++ why , "***" @@ -1570,10 +1572,11 @@ cant = "Validation engine is not capable of handling this case. Failed to validate." report = "Please report this as a bug in SBV!" - in if isUserSort k - then bad ("Cannot validate models in the presence of user defined kinds, saw: " ++ show k) cant - else do (NamedSymVar sv internalName) <- newSV st k + case () of + () | isUserSort k -> bad ("Cannot validate models in the presence of user defined kinds, saw: " ++ show k) cant + _ -> do (NamedSymVar sv internalName) <- newSV st k + let nm = fromMaybe (T.unpack internalName) mbNm nsv = toNamedSV' sv nm @@ -1968,24 +1971,6 @@ , supportsFlattenedModels :: Maybe [String] -- ^ Supports flattened model output? (With given config lines.) } --- | Rounding mode to be used for the IEEE floating-point operations. --- Note that Haskell's default is 'RoundNearestTiesToEven'. If you use --- a different rounding mode, then the counter-examples you get may not --- match what you observe in Haskell. -data RoundingMode = RoundNearestTiesToEven -- ^ Round to nearest representable floating point value. - -- If precisely at half-way, pick the even number. - -- (In this context, /even/ means the lowest-order bit is zero.) - | RoundNearestTiesToAway -- ^ Round to nearest representable floating point value. - -- If precisely at half-way, pick the number further away from 0. - -- (That is, for positive values, pick the greater; for negative values, pick the smaller.) - | RoundTowardPositive -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.) - | RoundTowardNegative -- ^ Round towards negative infinity. (Also known as rounding-down or floor.) - | RoundTowardZero -- ^ Round towards zero. (Also known as truncation.) - deriving (Eq, Ord, Show, Read, G.Data, Bounded, Enum) - --- | 'RoundingMode' kind -instance HasKind RoundingMode - -- | Solver configuration. See also 'Data.SBV.z3', 'Data.SBV.yices', 'Data.SBV.cvc4', 'Data.SBV.boolector', 'Data.SBV.mathSAT', etc. -- which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be -- created by varying those values. (Such as @z3{verbose=True}@.) @@ -2001,18 +1986,22 @@ -- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation -- of the real value is not finite, i.e., if it is not rational. -- --- The 'printBase' field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will --- be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis. +-- The 'printBase' field can be used to print numbers in base 2, 10, or 16. +-- +-- The 'crackNum' field can be used to display numbers in detail, all its bits and how they are laid out in memory. Works with all bounded number types +-- (i.e., SWord and SInt), but also with floats. It is particularly useful with floating-point numbers, as it shows you how they are laid out in +-- memory following the IEEE754 rules. data SMTConfig = SMTConfig { verbose :: Bool -- ^ Debug mode , timing :: Timing -- ^ Print timing information on how long different phases took (construction, solving, etc.) , printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.) , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) + , crackNum :: Bool -- ^ For each numeric value, show it in detail in the model with its bits spliced out. Good for floats. , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. , allSatMaxModelCount :: Maybe Int -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all. , allSatPrintAlong :: Bool -- ^ In a 'Data.SBV.allSat' call, print models as they are found. , satTrackUFs :: Bool -- ^ In a 'Data.SBV.sat' call, should we try to extract values of uninterpreted functions? - , isNonModelVar :: T.Text -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything) + , isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything) , validateModel :: Bool -- ^ If set, SBV will attempt to validate the model it gets back from the solver. , optimizeValidateConstraints :: Bool -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints. , transcript :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly) diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -37,7 +37,7 @@ -- *** Integer literals , svInteger, svAsInteger -- *** Float literals - , svFloat, svDouble + , svFloat, svDouble, svFloatingPoint -- *** Algebraic reals (only from rationals) , svReal, svNumerator, svDenominator -- *** Symbolic equality diff --git a/Data/SBV/Float.hs b/Data/SBV/Float.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Float.hs @@ -0,0 +1,25 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Float +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- A collection of arbitrary float operations. +----------------------------------------------------------------------------- + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Data.SBV.Float ( + -- * Type-sized floats + FP(..) + + -- * Constructing values + , fpFromRawRep, fpNaN, fpInf, fpZero + + -- * Operations + , fpFromInteger, fpFromRational, fpFromFloat, fpFromDouble, fpEncodeFloat + ) where + +import Data.SBV.Core.SizedFloats diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -52,7 +52,9 @@ , sendStringToSolver, sendRequestToSolver, retrieveResponseFromSolver -- * Defining new metrics - , addSValOptGoal, sFloatAsComparableSWord32, sDoubleAsComparableSWord64 + , addSValOptGoal + , sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord + , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint ) where import Control.Monad.IO.Class (MonadIO) @@ -61,7 +63,9 @@ import Data.SBV.Core.Model (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod) import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..)) -import Data.SBV.Core.Floating (sFloatAsComparableSWord32, sDoubleAsComparableSWord64) +import Data.SBV.Core.Floating ( sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord + , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint + ) import Data.SBV.Compilers.C (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -130,7 +130,7 @@ -- Q.E.D. -- >>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1) -- Satisfiable. Model: --- s0 = [0,0,16384] :: [Word16] +-- s0 = [0,1] :: [Word16] listToListAt :: SymVal a => SList a -> SInteger -> SList a listToListAt s offset = subList s offset 1 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 @@ -82,6 +82,7 @@ , timing = NoTiming , printBase = 10 , printRealPrec = 16 + , crackNum = False , transcript = Nothing , solver = s , smtLibVersion = smtVersion diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -84,7 +84,7 @@ -- >>> let phone = pre * "-" * post -- >>> sat $ \s -> (s :: SString) `match` phone -- Satisfiable. Model: --- s0 = "388-3826" :: String +-- s0 = "388-3868" :: String class RegExpMatchable a where -- | @`match` s r@ checks whether @s@ is in the language generated by @r@. match :: a -> RegExp -> SBool 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 @@ -15,6 +15,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -50,6 +51,9 @@ import Data.List (intercalate, isPrefixOf, transpose, isInfixOf) import Data.Word (Word8, Word16, Word32, Word64) +import GHC.TypeLits +import Data.Proxy + import Data.IORef (readIORef, writeIORef) import Data.Time (getZonedTime, defaultTimeLocale, formatTime, diffUTCTime, getCurrentTime) @@ -67,8 +71,10 @@ import Data.SBV.Core.Data import Data.SBV.Core.Symbolic (SMTEngine, State(..)) import Data.SBV.Core.Concrete (showCV) -import Data.SBV.Core.Kind (showBaseKind) +import Data.SBV.Core.Kind (showBaseKind, intOfProxy) +import Data.SBV.Core.SizedFloats(FloatingPoint(..)) + import Data.SBV.SMT.Utils (showTimeoutValue, alignPlain, debug, mergeSExpr, SBVException(..)) import Data.SBV.Utils.PrettyNum @@ -80,6 +86,8 @@ import Numeric +import qualified Data.SBV.Utils.CrackNum as CN + -- | Extract the final configuration from a result resultConfig :: SMTResult -> SMTConfig resultConfig (Unsatisfiable c _ ) = c @@ -301,6 +309,12 @@ parseCVs (CV KDouble (CDouble i) : r) = Just (i, r) parseCVs _ = Nothing +-- | A general floating-point extracted from a model +instance (KnownNat eb, KnownNat sb) => SatModel (FloatingPoint eb sb) where + parseCVs (CV (KFP ei si) (CFP fp) : r) + | intOfProxy (Proxy @eb) == ei , intOfProxy (Proxy @sb) == si = Just (FloatingPoint fp, r) + parseCVs _ = Nothing + -- | @CV@ as extracted from a model; trivial definition instance SatModel CV where parseCVs (cv : r) = Just (cv, r) @@ -536,7 +550,7 @@ relevantVars = filter (not . ignore) allVars ignore (T.pack -> s, _) | includeEverything = False - | True = "__internal_sbv_" `T.isPrefixOf` s || isNonModelVar cfg s + | True = "__internal_sbv_" `T.isPrefixOf` s || isNonModelVar cfg (T.unpack s) shM (s, RegularCV v) = let vs = shCV cfg v in ((length s, s), (vlength vs, vs)) shM (s, other) = let vs = show other in ((length s, s), (vlength vs, vs)) @@ -577,6 +591,8 @@ align (xs, r) = unwords $ zipWith left colWidths xs ++ ["=", left resWidth r] where left i x = take i (x ++ repeat ' ') + -- NB. We'll ignore crackNum here. Seems to be overkill while displaying an + -- uninterpreted function. scv = sh (printBase cfg) where sh 2 = binP sh 10 = showCV False @@ -599,11 +615,17 @@ -- | Show a constant value, in the user-specified base shCV :: SMTConfig -> CV -> String -shCV = sh . printBase +shCV SMTConfig{printBase, crackNum} cv = cracked (sh printBase cv) where sh 2 = binS sh 10 = show sh 16 = hexS sh n = \w -> show w ++ " -- Ignoring unsupported printBase " ++ show n ++ ", use 2, 10, or 16." + + cracked def + | not crackNum = def + | True = case CN.crackNum cv of + Nothing -> def + Just cs -> def ++ "\n" ++ cs -- | Helper function to spin off to an SMT solver. pipeProcess :: SMTConfig -> State -> String -> [String] -> String -> (State -> IO a) -> IO a 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 @@ -45,10 +45,11 @@ cvt ctx kindInfo isSat comments (inputs, trackerVars) skolemInps (allConsts, consts) tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out cfg = pgm where hasInteger = KUnbounded `Set.member` kindInfo hasReal = KReal `Set.member` kindInfo - hasFloat = KFloat `Set.member` kindInfo + hasFP = not (null [() | KFP{} <- Set.toList kindInfo]) + || KFloat `Set.member` kindInfo + || KDouble `Set.member` kindInfo hasString = KString `Set.member` kindInfo hasChar = KChar `Set.member` kindInfo - hasDouble = KDouble `Set.member` kindInfo hasRounding = not $ null [s | (s, _) <- usorts, s == "RoundingMode"] hasBVs = not (null [() | KBounded{} <- Set.toList kindInfo]) usorts = [(s, dt) | KUserSort s dt <- Set.toList kindInfo] @@ -124,7 +125,7 @@ | hasArrayInits = setAll "has array initializers" | hasOverflows = setAll "has overflow checks" - | hasDouble || hasFloat || hasRounding + | hasFP || hasRounding = if not (null foralls) then ["(set-logic ALL)"] else if hasBVs @@ -648,8 +649,7 @@ bvOp = all isBounded arguments intOp = any isUnbounded arguments realOp = any isReal arguments - doubleOp = any isDouble arguments - floatOp = any isFloat arguments + fpOp = any (\a -> isDouble a || isFloat a || isFP a) arguments boolOp = all isBoolean arguments charOp = any isChar arguments stringOp = any isString arguments @@ -671,17 +671,17 @@ liftN o _ xs = "(" ++ o ++ " " ++ unwords xs ++ ")" -- lift a binary operation with rounding-mode added; used for floating-point arithmetic - lift2WM o fo | doubleOp || floatOp = lift2 (addRM fo) - | True = lift2 o + lift2WM o fo | fpOp = lift2 (addRM fo) + | True = lift2 o - lift1FP o fo | doubleOp || floatOp = lift1 fo - | True = lift1 o + lift1FP o fo | fpOp = lift1 fo + | True = lift1 o - liftAbs sgned args | doubleOp || floatOp = lift1 "fp.abs" sgned args - | intOp = lift1 "abs" sgned args - | bvOp, sgned = mkAbs (head args) "bvslt" "bvneg" - | bvOp = head args - | True = mkAbs (head args) "<" "-" + liftAbs sgned args | fpOp = lift1 "fp.abs" sgned args + | intOp = lift1 "abs" sgned args + | bvOp, sgned = mkAbs (head args) "bvslt" "bvneg" + | bvOp = head args + | True = mkAbs (head args) "<" "-" where mkAbs x cmp neg = "(ite " ++ ltz ++ " " ++ nx ++ " " ++ x ++ ")" where ltz = "(" ++ cmp ++ " " ++ x ++ " " ++ z ++ ")" nx = "(" ++ neg ++ " " ++ x ++ ")" @@ -699,13 +699,12 @@ neqBV = liftN "distinct" equal sgn sbvs - | doubleOp = lift2 "fp.eq" sgn sbvs - | floatOp = lift2 "fp.eq" sgn sbvs - | True = lift2 "=" sgn sbvs + | fpOp = lift2 "fp.eq" sgn sbvs + | True = lift2 "=" sgn sbvs notEqual sgn sbvs - | doubleOp || floatOp || not hasDistinct = liftP sbvs - | True = liftN "distinct" sgn sbvs + | fpOp || not hasDistinct = liftP sbvs + | True = liftN "distinct" sgn sbvs where liftP [_, _] = "(not " ++ equal sgn sbvs ++ ")" liftP args = "(and " ++ unwords (walk args) ++ ")" @@ -715,8 +714,8 @@ lift2S oU oS sgn = lift2 (if sgn then oS else oU) sgn liftNS oU oS sgn = liftN (if sgn then oS else oU) sgn - lift2Cmp o fo | doubleOp || floatOp = lift2 fo - | True = lift2 o + lift2Cmp o fo | fpOp = lift2 fo + | True = lift2 o unintComp o [a, b] | KUserSort s (Just _) <- kindOf (head arguments) @@ -776,6 +775,7 @@ KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index" KFloat -> error "SBV.SMT.SMTLib2.cvtExp: unexpected float valued index" KDouble -> error "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index" + KFP{} -> error "SBV.SMT.SMTLib2.cvtExp: unexpected arbitrary float valued index" KChar -> error "SBV.SMT.SMTLib2.cvtExp: unexpected char valued index" KString -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" KList k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected list valued: " ++ show k @@ -798,6 +798,7 @@ KReal -> ("<", "<=") KFloat -> ("fp.lt", "fp.leq") KDouble -> ("fp.lt", "fp.geq") + KFP{} -> ("fp.lt", "fp.geq") KChar -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" KString -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" KList k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected sequence valued index: " ++ show k @@ -910,7 +911,7 @@ = f (any hasSign args) (map ssv args) | realOp, Just f <- lookup op smtOpRealTable = f (any hasSign args) (map ssv args) - | floatOp || doubleOp, Just f <- lookup op smtOpFloatDoubleTable + | fpOp, Just f <- lookup op smtOpFloatDoubleTable = f (any hasSign args) (map ssv args) | charOp || stringOp, Just f <- lookup op smtStringTable = f (map ssv args) @@ -1066,6 +1067,7 @@ walk _d _nm _f KUserSort {} = [] walk _d _nm _f KFloat {} = [] walk _d _nm _f KDouble {} = [] + walk _d _nm _f KFP {} = [] walk _d nm f KChar {} = [f nm] walk _d _nm _f KString {} = [] walk d nm _f (KList k) @@ -1116,44 +1118,41 @@ ----------------------------------------------------------------------------------------------- handleFPCast :: Kind -> Kind -> String -> String -> String -handleFPCast kFrom kTo rm input +handleFPCast kFromIn kToIn rm input | kFrom == kTo = input | True = "(" ++ cast kFrom kTo input ++ ")" where addRM a s = s ++ " " ++ rm ++ " " ++ a - -- To go and back from Ints, we detour through reals - cast KUnbounded KFloat a = "(_ to_fp 8 24) " ++ rm ++ " (to_real " ++ a ++ ")" - cast KUnbounded KDouble a = "(_ to_fp 11 53) " ++ rm ++ " (to_real " ++ a ++ ")" - cast KFloat KUnbounded a = "to_int (fp.to_real " ++ a ++ ")" - cast KDouble KUnbounded a = "to_int (fp.to_real " ++ a ++ ")" + kFrom = simplify kFromIn + kTo = simplify kToIn - -- To float/double - cast (KBounded False _) KFloat a = addRM a "(_ to_fp_unsigned 8 24)" - cast (KBounded False _) KDouble a = addRM a "(_ to_fp_unsigned 11 53)" - cast (KBounded True _) KFloat a = addRM a "(_ to_fp 8 24)" - cast (KBounded True _) KDouble a = addRM a "(_ to_fp 11 53)" - cast KReal KFloat a = addRM a "(_ to_fp 8 24)" - cast KReal KDouble a = addRM a "(_ to_fp 11 53)" + simplify KFloat = KFP 8 24 + simplify KDouble = KFP 11 53 + simplify k = k - -- Between floats - cast KFloat KFloat a = addRM a "(_ to_fp 8 24)" - cast KFloat KDouble a = addRM a "(_ to_fp 11 53)" - cast KDouble KFloat a = addRM a "(_ to_fp 8 24)" - cast KDouble KDouble a = addRM a "(_ to_fp 11 53)" + size (eb, sb) = show eb ++ " " ++ 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 ++ ")" + + -- 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) ++ ")" + -- From float/double - cast KFloat (KBounded False m) a = addRM a $ "(_ fp.to_ubv " ++ show m ++ ")" - cast KDouble (KBounded False m) a = addRM a $ "(_ fp.to_ubv " ++ show m ++ ")" - cast KFloat (KBounded True m) a = addRM a $ "(_ fp.to_sbv " ++ show m ++ ")" - cast KDouble (KBounded True m) a = addRM a $ "(_ fp.to_sbv " ++ show m ++ ")" + 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 KFloat KReal a = "fp.to_real" ++ " " ++ a - cast KDouble KReal a = "fp.to_real" ++ " " ++ a + -- To real + 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 + cast f d _ = error $ "SBV.SMTLib2: Unexpected FPCast from: " ++ show f ++ " to " ++ show d rot :: (SV -> String) -> String -> Int -> SV -> String rot ssv o c x = "((_ " ++ o ++ " " ++ show c ++ ") " ++ ssv x ++ ")" diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs --- a/Data/SBV/String.hs +++ b/Data/SBV/String.hs @@ -133,7 +133,7 @@ -- Q.E.D. -- >>> sat $ \s -> length s .>= 2 .&& strToStrAt s 0 ./= strToStrAt s (length s - 1) -- Satisfiable. Model: --- s0 = "ABC" :: String +-- s0 = "AB" :: String strToStrAt :: SString -> SInteger -> SString strToStrAt s offset = subStr s offset 1 diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs --- a/Data/SBV/Tools/GenTest.hs +++ b/Data/SBV/Tools/GenTest.hs @@ -144,6 +144,7 @@ KUnbounded -> let CInteger w = cvVal cv in shexI False True w KFloat -> let CFloat w = cvVal cv in showHFloat w KDouble -> let CDouble w = cvVal cv in showHDouble w + KFP{} -> error "SBV.renderTest: Unsupported arbitrary float" KChar -> error "SBV.renderTest: Unsupported char" KString -> error "SBV.renderTest: Unsupported string" KReal -> let CAlgReal w = cvVal cv in algRealToHaskell w @@ -230,6 +231,7 @@ k@KBounded{} -> error $ "SBV.renderTest: Unsupported kind: " ++ show k KFloat -> "SFloat" KDouble -> "SDouble" + KFP{} -> error "SBV.renderTest: Unsupported arbitrary float" KChar -> error "SBV.renderTest: Unsupported char" KString -> error "SBV.renderTest: Unsupported string" KUnbounded -> error "SBV.renderTest: Unbounded integers are not supported when generating C test-cases." @@ -250,6 +252,7 @@ KUnbounded -> let CInteger w = cvVal cv in shexI False True w KFloat -> let CFloat w = cvVal cv in showCFloat w KDouble -> let CDouble w = cvVal cv in showCDouble w + KFP{} -> error "SBV.renderTest: Unsupported arbitrary float" KChar -> error "SBV.renderTest: Unsupported char" KString -> error "SBV.renderTest: Unsupported string" k@KList{} -> error $ "SBV.renderTest: Unsupported list sort!" ++ show k @@ -330,11 +333,12 @@ _ -> error $ "SBV.renderTest: Unexpected CV: " ++ show cv xlt s (CInteger v) = [toF (testBit v i) | i <- [s-1, s-2 .. 0]] - xlt _ (CFloat r) = error $ "SBV.renderTest.Forte: Unexpected float value: " ++ show r - xlt _ (CDouble r) = error $ "SBV.renderTest.Forte: Unexpected double value: " ++ show r - xlt _ (CChar r) = error $ "SBV.renderTest.Forte: Unexpected char value: " ++ show r - xlt _ (CString r) = error $ "SBV.renderTest.Forte: Unexpected string value: " ++ show r - xlt _ (CAlgReal r) = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r + xlt _ (CFloat r) = error $ "SBV.renderTest.Forte: Unexpected float value: " ++ show r + xlt _ (CDouble r) = error $ "SBV.renderTest.Forte: Unexpected double value: " ++ show r + xlt _ (CFP r) = error $ "SBV.renderTest.Forte: Unexpected arbitrary float value: " ++ show r + xlt _ (CChar r) = error $ "SBV.renderTest.Forte: Unexpected char value: " ++ show r + xlt _ (CString r) = error $ "SBV.renderTest.Forte: Unexpected string value: " ++ show r + xlt _ (CAlgReal r) = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r xlt _ CList{} = error "SBV.renderTest.Forte: Unexpected list value!" xlt _ CSet{} = error "SBV.renderTest.Forte: Unexpected set value!" xlt _ CTuple{} = error "SBV.renderTest.Forte: Unexpected list value!" 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 @@ -31,6 +31,7 @@ ) where import Data.SBV.Core.Data +import Data.SBV.Core.Kind import Data.SBV.Core.Symbolic import Data.SBV.Core.Model import Data.SBV.Core.Operations @@ -99,8 +100,8 @@ instance ArithOverflow SInt32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} instance ArithOverflow SInt64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance (KnownNat n, IsNonZero n) => ArithOverflow (SWord n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance (KnownNat n, IsNonZero n) => ArithOverflow (SInt n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SWord n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SInt n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} instance ArithOverflow SVal where bvAddO = signPick2 bvuaddo bvsaddo @@ -179,14 +180,14 @@ (/!) = checkOp2 ?loc "division" sDiv bvDivO negateChecked = checkOp1 ?loc "unary negation" negate bvNegO -instance (KnownNat n, IsNonZero n) => CheckedArithmetic (WordN n) where +instance (KnownNat n, BVIsNonZero n) => CheckedArithmetic (WordN n) where (+!) = checkOp2 ?loc "addition" (+) bvAddO (-!) = checkOp2 ?loc "subtraction" (-) bvSubO (*!) = checkOp2 ?loc "multiplication" (*) bvMulO (/!) = checkOp2 ?loc "division" sDiv bvDivO negateChecked = checkOp1 ?loc "unary negation" negate bvNegO -instance (KnownNat n, IsNonZero n) => CheckedArithmetic (IntN n) where +instance (KnownNat n, BVIsNonZero n) => CheckedArithmetic (IntN n) where (+!) = checkOp2 ?loc "addition" (+) bvAddO (-!) = checkOp2 ?loc "subtraction" (-) bvSubO (*!) = checkOp2 ?loc "multiplication" (*) bvMulO diff --git a/Data/SBV/Tools/Polynomial.hs b/Data/SBV/Tools/Polynomial.hs --- a/Data/SBV/Tools/Polynomial.hs +++ b/Data/SBV/Tools/Polynomial.hs @@ -29,6 +29,7 @@ import Data.Word (Word8, Word16, Word32, Word64) import Data.SBV.Core.Data +import Data.SBV.Core.Kind import Data.SBV.Core.Sized import Data.SBV.Core.Model @@ -91,7 +92,7 @@ instance Polynomial SWord32 where {showPolynomial b = liftS (sp b); pMult = polyMult; pDivMod = polyDivMod} instance Polynomial SWord64 where {showPolynomial b = liftS (sp b); pMult = polyMult; pDivMod = polyDivMod} -instance (KnownNat n, IsNonZero n) => Polynomial (SWord n) where {showPolynomial b = liftS (sp b); pMult = polyMult; pDivMod = polyDivMod} +instance (KnownNat n, BVIsNonZero n) => Polynomial (SWord n) where {showPolynomial b = liftS (sp b); pMult = polyMult; pDivMod = polyDivMod} lift :: SymVal a => ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a lift f (x, y, z) = fromJust $ unliteral $ f (literal x, literal y, z) diff --git a/Data/SBV/Tools/Range.hs b/Data/SBV/Tools/Range.hs --- a/Data/SBV/Tools/Range.hs +++ b/Data/SBV/Tools/Range.hs @@ -203,4 +203,4 @@ Just xss -> search (xss ++ cs) sofar else search cs sofar -{-# ANN rangesWith ("HLint: ignore Replace case with fromMaybe" :: String) #-} +{-# ANN rangesWith ("HLint: ignore Use fromMaybe" :: String) #-} diff --git a/Data/SBV/Tools/WeakestPreconditions.hs b/Data/SBV/Tools/WeakestPreconditions.hs --- a/Data/SBV/Tools/WeakestPreconditions.hs +++ b/Data/SBV/Tools/WeakestPreconditions.hs @@ -486,4 +486,4 @@ where mCur = currentMeasure is zero = map (const 0) mCur -{-# ANN traceExecution ("HLint: ignore Replace case with fromMaybe" :: String) #-} +{-# ANN traceExecution ("HLint: ignore Use fromMaybe" :: String) #-} diff --git a/Data/SBV/Trans.hs b/Data/SBV/Trans.hs --- a/Data/SBV/Trans.hs +++ b/Data/SBV/Trans.hs @@ -27,11 +27,11 @@ -- *** Signed bit-vectors , SInt8, SInt16, SInt32, SInt64, SInt, IntN -- *** Converting between fixed-size and arbitrary bitvectors - , IsNonZero, FromSized, ToSized, fromSized, toSized + , BVIsNonZero, FromSized, ToSized, fromSized, toSized -- ** Unbounded integers , SInteger -- ** Floating point numbers - , SFloat, SDouble + , SFloat, SDouble, SFloatingPoint -- ** Algebraic reals , SReal, AlgReal, sRealToSInteger -- ** Characters, Strings and Regular Expressions @@ -74,9 +74,17 @@ , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero, sRNE, sRNA, sRTP, sRTN, sRTZ -- ** Conversion to/from floats , IEEEFloatConvertible(..) + -- ** Bit-pattern conversions - , sFloatAsSWord32, sWord32AsSFloat, sDoubleAsSWord64, sWord64AsSDouble, blastSFloat, blastSDouble + , sFloatAsSWord32, sWord32AsSFloat + , sDoubleAsSWord64, sWord64AsSDouble + , sFloatingPointAsSWord, sWordAsSFloatingPoint + -- ** Extracting bit patterns from floats + , blastSFloat + , blastSDouble + , blastSFloatingPoint + -- * Enumerations , mkSymbolicEnumeration @@ -158,6 +166,7 @@ import Data.SBV.Core.AlgReals import Data.SBV.Core.Data +import Data.SBV.Core.Kind import Data.SBV.Core.Model import Data.SBV.Core.Floating import Data.SBV.Core.Sized diff --git a/Data/SBV/Utils/CrackNum.hs b/Data/SBV/Utils/CrackNum.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Utils/CrackNum.hs @@ -0,0 +1,289 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Utils.CrackNum +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Crack internal representation for numeric types +----------------------------------------------------------------------------- + +{-# LANGUAGE NamedFieldPuns #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Data.SBV.Utils.CrackNum ( + crackNum + ) where + +import Data.SBV.Core.Concrete +import Data.SBV.Core.Kind +import Data.SBV.Core.SizedFloats +import Data.SBV.Utils.Numeric +import Data.SBV.Utils.PrettyNum (showFloatAtBase) + +import Data.Char (intToDigit, toUpper, isSpace) + +import Data.Bits +import Data.List + +import LibBF hiding (Zero, bfToString) + +import Numeric + +-- | A class for cracking things deeper, if we know how. +class CrackNum a where + crackNum :: a -> Maybe String + +-- | CVs are easy to crack +instance CrackNum CV where + crackNum cv = case kindOf cv of + -- Maybe one day we'll have a use for these, currently cracking them + -- any further seems overkill + KBool {} -> Nothing + KUnbounded {} -> Nothing + KReal {} -> Nothing + KUserSort {} -> Nothing + KChar {} -> Nothing + KString {} -> Nothing + KList {} -> Nothing + KSet {} -> Nothing + KTuple {} -> Nothing + KMaybe {} -> Nothing + KEither {} -> Nothing + + -- Actual crackables + KFloat{} -> Just $ let CFloat f = cvVal cv in float f + KDouble{} -> Just $ let CDouble d = cvVal cv in float d + KFP{} -> Just $ let CFP f = cvVal cv in float f + KBounded sg sz -> Just $ let CInteger i = cvVal cv in int sg sz i + +-- How far off the screen we want displayed? Somewhat experimentally found. +tab :: String +tab = replicate 18 ' ' + +-- Make splits of 4, top one has the remainder +split4 :: Int -> [Int] +split4 n + | m == 0 = rest + | True = m : rest + where (d, m) = n `divMod` 4 + rest = replicate d 4 + +-- Convert bits to the corresponding integer. +getVal :: [Bool] -> Integer +getVal = foldl (\s b -> 2 * s + if b then 1 else 0) 0 + +-- Show in hex, but pay attention to how wide a field it should be in +mkHex :: [Bool] -> String +mkHex bin = map toUpper $ showHex (getVal bin) "" + +-- | Show a sized word/int in detail +int :: Bool -> Int -> Integer -> String +int signed sz v = intercalate "\n" $ ruler ++ info + where splits = split4 sz + + ruler = map (tab ++) $ mkRuler sz splits + + bitRep :: [[Bool]] + bitRep = split splits [v `testBit` i | i <- reverse [0 .. sz - 1]] + + flatHex = concatMap mkHex bitRep + iprec + | signed = "Signed " ++ show sz ++ "-bit 2's complement integer" + | True = "Unsigned " ++ show sz ++ "-bit word" + + signBit = v `testBit` (sz-1) + s | signBit = "-" + | True = "" + + av = abs v + + info = [ " Binary layout: " ++ unwords [concatMap (\b -> if b then "1" else "0") is | is <- bitRep] + , " Hex layout: " ++ unwords (split (split4 (length flatHex)) flatHex) + , " Type: " ++ iprec + ] + ++ [ " Sign: " ++ if signBit then "Negative" else "Positive" | signed] + ++ [ " Binary Value: " ++ s ++ "0b" ++ showIntAtBase 2 intToDigit av "" + , " Octal Value: " ++ s ++ "0o" ++ showOct av "" + , " Decimal Value: " ++ show v + , " Hex Value: " ++ s ++ "0x" ++ showHex av "" + ] + +-- | What kind of Float is this? +data FPKind = Zero Bool -- with sign + | Infty Bool -- with sign + | NaN + | Subnormal + | Normal + deriving Eq + +-- | Show instance for Kind, not for reading back! +instance Show FPKind where + show Zero{} = "FP_ZERO" + show Infty{} = "FP_INFINITE" + show NaN = "FP_NAN" + show Subnormal = "FP_SUBNORMAL" + show Normal = "FP_NORMAL" + +-- | Find out what kind this float is. We specifically ask +-- the caller to provide if the number is zero, neg-inf, and pos-inf. Why? +-- Because the FP type doesn't have those recognizers that also work with Float/Double. +getKind :: RealFloat a => a -> FPKind +getKind fp + | fp == 0 = Zero (isNegativeZero fp) + | isInfinite fp = Infty (fp < 0) + | isNaN fp = NaN + | isDenormalized fp = Subnormal + | True = Normal + +-- Show the value in different bases +showAtBases :: FPKind -> (String, String, String, String) -> Either String (String, String, String, String) +showAtBases k bvs = case k of + Zero False -> Right ("0b0.0", "0o0.0", "0.0", "0x0.0") + Zero True -> Right ("-0b0.0", "-0o0.0", "-0.0", "-0x0.0") + Infty False -> Left "Infinity" + Infty True -> Left "-Infinity" + NaN -> Left "NaN" + Subnormal -> Right bvs + Normal -> Right bvs + +-- | Float data for display purposes +data FloatData = FloatData { prec :: String + , eb :: Int + , sb :: Int + , bits :: Integer + , fpKind :: FPKind + , fpVals :: Either String (String, String, String, String) + } + +-- | A simple means to organize different bits and pieces of float data +-- for display purposes +class HasFloatData a where + getFloatData :: a -> FloatData + +-- | Float instance +instance HasFloatData Float where + getFloatData f = FloatData { + prec = "Single" + , eb = 8 + , sb = 24 + , bits = fromIntegral (floatToWord f) + , fpKind = k + , fpVals = showAtBases k (showFloatAtBase 2 f "", showFloatAtBase 8 f "", show f, showFloatAtBase 16 f "") + } + where k = getKind f + +-- | Double instance +instance HasFloatData Double where + getFloatData d = FloatData { + prec = "Double" + , eb = 11 + , sb = 53 + , bits = fromIntegral (doubleToWord d) + , fpKind = k + , fpVals = showAtBases k (showFloatAtBase 2 d "", showFloatAtBase 8 d "", show d, showFloatAtBase 16 d "") + } + where k = getKind d + +-- | Find the exponent values, (exponent value, exponent as stored, bias) +getExponentData :: FloatData -> (Integer, Integer, Integer) +getExponentData FloatData{eb, sb, bits, fpKind} = (expValue, expStored, bias) + where -- | Bias is 2^(eb-1) - 1 + bias :: Integer + bias = (2 :: Integer) ^ ((fromIntegral eb :: Integer) - 1) - 1 + + -- | Exponent as stored is simply bit extraction + expStored = getVal [bits `testBit` i | i <- reverse [sb-1 .. sb+eb-2]] + + -- | Exponent value is stored exponent - bias, unless the number is subnormal. In that case it is 1 - bias + expValue = case fpKind of + Subnormal -> 1 - bias + _ -> expStored - bias + +-- | FP instance +instance HasFloatData FP where + getFloatData v@(FP eb sb f) = FloatData { + prec = case (eb, sb) of + ( 5, 11) -> "Half (5 exponent bits, 10 significand bits.)" + ( 8, 24) -> "Single (8 exponent bits, 23 significand bits.)" + (11, 53) -> "Double (11 exponent bits, 52 significand bits.)" + (15, 113) -> "Quad (15 exponent bits, 112 significand bits.)" + ( _, _) -> show eb ++ " exponent bits, " ++ show (sb-1) ++ " significand bit" ++ if sb > 2 then "s" else "" + , eb = eb + , sb = sb + , bits = bfToBits (mkBFOpts eb sb NearEven) f + , fpKind = k + , fpVals = showAtBases k (bfToString 2 True v, bfToString 8 True v, bfToString 10 True v, bfToString 16 True v) + } + where opts = mkBFOpts eb sb NearEven + k | bfIsZero f = Zero (bfIsNeg f) + | bfIsInf f = Infty (bfIsNeg f) + | bfIsNaN f = NaN + | bfIsSubnormal opts f = Subnormal + | True = Normal + +-- | Show a float in detail +float :: HasFloatData a => a -> String +float f = intercalate "\n" $ ruler ++ legend : info + where fd@FloatData{prec, eb, sb, bits, fpKind, fpVals} = getFloatData f + + splits = [1, eb, sb] + ruler = map (tab ++) $ mkRuler (eb + sb) splits + + legend = tab ++ "S " ++ mkTag ('E' : show eb) eb ++ " " ++ mkTag ('S' : show (sb-1)) (sb-1) + + mkTag t len = take len $ replicate ((len - length t) `div` 2) '-' ++ t ++ repeat '-' + + allBits :: [Bool] + allBits = [bits `testBit` i | i <- reverse [0 .. eb + sb - 1]] + + flatHex = concatMap mkHex (split (split4 (eb + sb)) allBits) + sign = bits `testBit` (eb+sb-1) + + (exponentVal, storedExponent, bias) = getExponentData fd + + esInfo = "Stored: " ++ show storedExponent ++ ", Bias: " ++ show bias + + isSubNormal = case fpKind of + Subnormal -> True + _ -> False + + info = [ " Binary layout: " ++ unwords [concatMap (\b -> if b then "1" else "0") is | is <- split splits allBits] + , " Hex layout: " ++ unwords (split (split4 (length flatHex)) flatHex) + , " Precision: " ++ prec + , " Sign: " ++ if sign then "Negative" else "Positive" + ] + ++ [ " Exponent: " ++ show exponentVal ++ " (Subnormal, with fixed exponent value. " ++ esInfo ++ ")" | isSubNormal ] + ++ [ " Exponent: " ++ show exponentVal ++ " (" ++ esInfo ++ ")" | not isSubNormal] + ++ [ " Classification: " ++ show fpKind] + ++ (case fpVals of + Left val -> [ " Value: " ++ val] + Right (bval, oval, dval, hval) -> [ " Binary Value: " ++ bval + , " Octal Value: " ++ oval + , " Decimal Value: " ++ dval + , " Hex Value: " ++ hval + ]) + ++ [ " Note: Representation for NaN's is not unique" | fpKind == NaN] + + +-- | Build a ruler with given split points +mkRuler :: Int -> [Int] -> [String] +mkRuler n splits = map (trimRight . unwords . split splits . trim Nothing) $ transpose $ map pad $ reverse [0 .. n-1] + where len = length (show (n-1)) + pad i = reverse $ take len $ reverse (show i) ++ repeat '0' + + trim _ "" = "" + trim mbPrev (c:cs) + | mbPrev == Just c = ' ' : trim mbPrev cs + | True = c : trim (Just c) cs + + trimRight = reverse . dropWhile isSpace . reverse + +split :: [Int] -> [a] -> [[a]] +split _ [] = [] +split [] xs = [xs] +split (i:is) xs = case splitAt i xs of + (pre, []) -> [pre] + (pre, post) -> pre : split is post diff --git a/Data/SBV/Utils/Numeric.hs b/Data/SBV/Utils/Numeric.hs --- a/Data/SBV/Utils/Numeric.hs +++ b/Data/SBV/Utils/Numeric.hs @@ -9,10 +9,20 @@ -- Various number related utilities ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts #-} + {-# OPTIONS_GHC -Wall -Werror #-} -module Data.SBV.Utils.Numeric where +module Data.SBV.Utils.Numeric ( + fpMaxH, fpMinH, fp2fp, fpRemH, fpRoundToIntegralH, fpIsEqualObjectH, fpCompareObjectH, fpIsNormalizedH + , floatToWord, wordToFloat, doubleToWord, wordToDouble + ) where +import Data.Word +import Data.Array.ST (newArray, readArray, MArray, STUArray) +import Data.Array.Unsafe (castSTUArray) +import GHC.ST (runST, ST) + -- | The SMT-Lib (in particular Z3) implementation for min/max for floats does not agree with -- Haskell's; and also it does not agree with what the hardware does. Sigh.. See: -- @@ -110,3 +120,36 @@ -- and also this is not simply the negation of isDenormalized! fpIsNormalizedH :: RealFloat a => a -> Bool fpIsNormalizedH x = not (isDenormalized x || isInfinite x || isNaN x || x == 0) + +------------------------------------------------------------------------- +-- Reinterpreting float/double as word32/64 and back. Here, we use the +-- definitions from the reinterpret-cast package: +-- +-- http://hackage.haskell.org/package/reinterpret-cast +-- +-- The reason we steal these definitions is to make sure we keep minimal +-- dependencies and no FFI requirements anywhere. +------------------------------------------------------------------------- +-- | Reinterpret-casts a `Float` to a `Word32`. +floatToWord :: Float -> Word32 +floatToWord x = runST (cast x) +{-# INLINEABLE floatToWord #-} + +-- | Reinterpret-casts a `Word32` to a `Float`. +wordToFloat :: Word32 -> Float +wordToFloat x = runST (cast x) +{-# INLINEABLE wordToFloat #-} + +-- | Reinterpret-casts a `Double` to a `Word64`. +doubleToWord :: Double -> Word64 +doubleToWord x = runST (cast x) +{-# INLINEABLE doubleToWord #-} + +-- | Reinterpret-casts a `Word64` to a `Double`. +wordToDouble :: Word64 -> Double +wordToDouble x = runST (cast x) +{-# INLINEABLE wordToDouble #-} + +{-# INLINE cast #-} +cast :: (MArray (STUArray s) a (ST s), MArray (STUArray s) b (ST s)) => a -> ST s b +cast x = newArray (0 :: Int, 0) x >>= castSTUArray >>= flip readArray 0 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 @@ -16,11 +16,11 @@ module Data.SBV.Utils.PrettyNum ( PrettyNum(..), readBin, shex, chex, shexI, sbin, sbinI - , showCFloat, showCDouble, showHFloat, showHDouble + , showCFloat, showCDouble, showHFloat, showHDouble, showBFloat, showFloatAtBase , showSMTFloat, showSMTDouble, smtRoundingMode, cvToSMTLib, mkSkolemZero ) where -import Data.Char (intToDigit, ord) +import Data.Char (intToDigit, ord, chr, toUpper) import Data.Int (Int8, Int16, Int32, Int64) import Data.List (isPrefixOf) import Data.Maybe (fromJust, fromMaybe, listToMaybe) @@ -29,15 +29,15 @@ import qualified Data.Set as Set -import Numeric (showIntAtBase, showHex, readInt) -import qualified Numeric (showHFloat) - -import Data.Numbers.CrackNum (floatToFP, doubleToFP) +import Numeric (showIntAtBase, showHex, readInt, floatToDigits) +import qualified Numeric as N (showHFloat) import Data.SBV.Core.Data -import Data.SBV.Core.Kind (smtType) -import Data.SBV.Core.AlgReals (algRealToSMTLib2) +import Data.SBV.Core.Kind (smtType, smtRoundingMode, showBaseKind) +import Data.SBV.Core.AlgReals (algRealToSMTLib2) +import Data.SBV.Core.SizedFloats (fprToSMTLib2, bfToString) + import Data.SBV.Utils.Lib (stringToQFS) -- | PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers. @@ -162,22 +162,27 @@ hex = shexI False False bin = sbinI False False +shBKind :: HasKind a => a -> String +shBKind a = " :: " ++ showBaseKind (kindOf a) + instance PrettyNum CV where - hexS cv | isUserSort cv = show cv ++ " :: " ++ show (kindOf cv) - | isBoolean cv = hexS (cvToBool cv) ++ " :: Bool" - | isFloat cv = let CFloat f = cvVal cv in show f ++ " :: Float\n" ++ show (floatToFP f) - | isDouble cv = let CDouble d = cvVal cv in show d ++ " :: Double\n" ++ show (doubleToFP d) - | isReal cv = let CAlgReal r = cvVal cv in show r ++ " :: Real" - | isString cv = let CString s = cvVal cv in show s ++ " :: String" + hexS cv | isUserSort 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 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 | 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 | isUserSort cv = show cv ++ " :: " ++ show (kindOf cv) - | isBoolean cv = binS (cvToBool cv) ++ " :: Bool" - | isFloat cv = let CFloat f = cvVal cv in show f ++ " :: Float\n" ++ show (floatToFP f) - | isDouble cv = let CDouble d = cvVal cv in show d ++ " :: Double\n" ++ show (doubleToFP d) - | isReal cv = let CAlgReal r = cvVal cv in show r ++ " :: Real" - | isString cv = let CString s = cvVal cv in show s ++ " :: String" + binS cv | isUserSort 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 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 | 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 @@ -185,6 +190,7 @@ | 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 f | isReal cv = let CAlgReal r = cvVal cv in show r | isString cv = let CString s = cvVal cv in show s | not (isBounded cv) = let CInteger i = cvVal cv in shexI False True i @@ -194,28 +200,31 @@ | 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 f | isReal cv = let CAlgReal r = cvVal cv in show r | isString cv = let CString s = cvVal cv in 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 | isUserSort cv = 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 - | isReal cv = let CAlgReal r = cvVal cv in show r - | isString cv = let CString s = cvVal cv in 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 + hex cv | isUserSort cv = 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 f + | isReal cv = let CAlgReal r = cvVal cv in show r + | isString cv = let CString s = cvVal cv in 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 | isUserSort cv = 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 - | isReal cv = let CAlgReal r = cvVal cv in show r - | isString cv = let CString s = cvVal cv in 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 + bin cv | isUserSort cv = 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 f + | isReal cv = let CAlgReal r = cvVal cv in show r + | isString cv = let CString s = cvVal cv in 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 @@ -337,7 +346,7 @@ | isNaN f = "((float) NAN)" | isInfinite f, f < 0 = "((float) (-INFINITY))" | isInfinite f = "((float) INFINITY)" - | True = Numeric.showHFloat f $ "F /* " ++ show f ++ "F */" + | True = N.showHFloat f $ "F /* " ++ show f ++ "F */" -- | A version of show for doubles that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included. showCDouble :: Double -> String @@ -345,7 +354,7 @@ | isNaN d = "((double) NAN)" | isInfinite d, d < 0 = "((double) (-INFINITY))" | isInfinite d = "((double) INFINITY)" - | True = Numeric.showHFloat d " /* " ++ show d ++ " */" + | True = N.showHFloat d " /* " ++ show d ++ " */" -- | A version of show for floats that generates correct Haskell literals for nan/infinite showHFloat :: Float -> String @@ -374,6 +383,7 @@ | True = "((_ to_fp 8 24) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational f) ++ ")" where as s = "(_ " ++ s ++ " 8 24)" + -- | A version of show for doubles that generates correct SMTLib literals using the rounding mode showSMTDouble :: RoundingMode -> Double -> String showSMTDouble rm d @@ -395,14 +405,6 @@ where n = numerator r d = denominator r --- | Convert a rounding mode to the format SMT-Lib2 understands. -smtRoundingMode :: RoundingMode -> String -smtRoundingMode RoundNearestTiesToEven = "roundNearestTiesToEven" -smtRoundingMode RoundNearestTiesToAway = "roundNearestTiesToAway" -smtRoundingMode RoundTowardPositive = "roundTowardPositive" -smtRoundingMode RoundTowardNegative = "roundTowardNegative" -smtRoundingMode RoundTowardZero = "roundTowardZero" - -- | Convert a CV to an SMTLib2 compliant value cvToSMTLib :: RoundingMode -> CV -> String cvToSMTLib rm x @@ -411,6 +413,7 @@ | isReal x, CAlgReal r <- cvVal x = algRealToSMTLib2 r | isFloat x, CFloat f <- cvVal x = showSMTFloat rm f | isDouble x, CDouble d <- cvVal x = showSMTDouble rm d + | isFP x, CFP f <- cvVal x = fprToSMTLib2 f | not (isBounded x), CInteger w <- cvVal x = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")" | not (hasSign x) , CInteger w <- cvVal x = smtLibHex (intSizeOf x) w -- signed numbers (with 2's complement representation) is problematic @@ -471,7 +474,7 @@ dtConstructor fld args res = "((as " ++ fld ++ " " ++ smtType res ++ ") " ++ unwords args ++ ")" smtLibMaybe :: Kind -> Maybe CVal -> String - smtLibMaybe km@ KMaybe{} Nothing = dtConstructor "nothing_SBVMaybe" [] km + smtLibMaybe km@KMaybe{} Nothing = dtConstructor "nothing_SBVMaybe" [] km smtLibMaybe km@(KMaybe k) (Just c) = dtConstructor "just_SBVMaybe" [cvToSMTLib rm (CV k c)] km smtLibMaybe k _ = error $ "SBV.cvToSMTLib: Impossible case (smtLibMaybe), received kind: " ++ show k @@ -490,3 +493,39 @@ mkSkolemZero _ (KUserSort _ (Just (f:_))) = f mkSkolemZero _ (KUserSort s _) = error $ "SBV.mkSkolemZero: Unexpected user sort: " ++ s mkSkolemZero rm k = cvToSMTLib rm (mkConstCV k (0::Integer)) + +-- | Show a float as a binary +showBFloat :: (Show a, RealFloat a) => a -> ShowS +showBFloat = showFloatAtBase 2 + +-- | Like Haskell's showHFloat, but uses arbitrary base instead. Note that the exponent is always written in decimal. +showFloatAtBase :: (Show a, RealFloat a) => Int -> a -> ShowS +showFloatAtBase base = showString . fmt + where fmt x + | isNaN x = "NaN" + | isInfinite x = (if x < 0 then "-" else "") ++ "Infinity" + | x < 0 || isNegativeZero x = '-' : cvt (-x) + | True = cvt x + + prefix = case base of + 2 -> "0b" + 8 -> "0o" + 10 -> "" + 16 -> "0x" + x -> "0<" ++ show x ++ ">" + + cvt x + | x == 0 = prefix ++ "0p+0" + | True = case floatToDigits (fromIntegral base) x of + r@([], _) -> error $ "Impossible happened: showFloatAtBase: " ++ show (base, show x, r) + (d:ds, e) -> prefix ++ toDigit d ++ frac ds ++ "p" ++ show (e-1) + + -- Given digits, show them except if they're all 0 then drop + frac digits + | all (== 0) digits = "" + | True = "." ++ concatMap toDigit digits + + toDigit v = map toUpper d + where d | v <= 15 = [intToDigit v] + | v < 36 = [chr (ord 'a' + v - 10)] + | True = '<' : show v ++ ">" diff --git a/Data/SBV/Utils/SExpr.hs b/Data/SBV/Utils/SExpr.hs --- a/Data/SBV/Utils/SExpr.hs +++ b/Data/SBV/Utils/SExpr.hs @@ -25,18 +25,18 @@ import Numeric (readInt, readDec, readHex, fromRat) import Data.SBV.Core.AlgReals +import Data.SBV.Core.SizedFloats import Data.SBV.Core.Data (nan, infinity, RoundingMode(..)) -import Data.SBV.Utils.Numeric (fpIsEqualObjectH) - -import Data.Numbers.CrackNum (wordToFloat, wordToDouble) +import Data.SBV.Utils.Numeric (fpIsEqualObjectH, wordToFloat, wordToDouble) -- | ADT S-Expression format, suitable for representing get-model output of SMT-Lib -data SExpr = ECon String - | ENum (Integer, Maybe Int) -- Second argument is how wide the field was in bits, if known. Useful in FP parsing. - | EReal AlgReal - | EFloat Float - | EDouble Double +data SExpr = ECon String + | ENum (Integer, Maybe Int) -- Second argument is how wide the field was in bits, if known. Useful in FP parsing. + | EReal AlgReal + | EFloat Float + | EFloatingPoint FP + | EDouble Double | EApp [SExpr] deriving Show @@ -174,18 +174,30 @@ _ -> die $ "Cannot parse a CVC4 approximate value from: " ++ show x -- NB. Note the lengths on the mantissa for the following two are 23/52; not 24/53! - cvt (EApp [ECon "fp", ENum (s, Just 1), ENum ( e, Just 8), ENum (m, Just 23)]) = return $ EFloat $ getTripleFloat s e m - cvt (EApp [ECon "fp", ENum (s, Just 1), ENum ( e, Just 11), ENum (m, Just 52)]) = return $ EDouble $ getTripleDouble s e m - cvt (EApp [ECon "_", ECon "NaN", ENum ( 8, _), ENum (24, _)]) = return $ EFloat nan - cvt (EApp [ECon "_", ECon "NaN", ENum (11, _), ENum (53, _)]) = return $ EDouble nan - cvt (EApp [ECon "_", ECon "+oo", ENum ( 8, _), ENum (24, _)]) = return $ EFloat infinity - cvt (EApp [ECon "_", ECon "+oo", ENum (11, _), ENum (53, _)]) = return $ EDouble infinity - cvt (EApp [ECon "_", ECon "-oo", ENum ( 8, _), ENum (24, _)]) = return $ EFloat (-infinity) - cvt (EApp [ECon "_", ECon "-oo", ENum (11, _), ENum (53, _)]) = return $ EDouble (-infinity) + cvt (EApp [ECon "fp", ENum (s, Just 1), ENum ( e, Just 8), ENum (m, Just 23)]) = return $ EFloat $ getTripleFloat s e m + cvt (EApp [ECon "fp", ENum (s, Just 1), ENum ( e, Just 11), ENum (m, Just 52)]) = return $ EDouble $ getTripleDouble s e m + cvt (EApp [ECon "fp", ENum (s, Just 1), ENum ( e, Just eb), ENum (m, Just sb)]) = return $ EFloatingPoint $ fpFromRawRep (s == 1) (e, eb) (m, sb+1) + + cvt (EApp [ECon "_", ECon "NaN", ENum ( 8, _), ENum (24, _)]) = return $ EFloat nan + cvt (EApp [ECon "_", ECon "NaN", ENum (11, _), ENum (53, _)]) = return $ EDouble nan + cvt (EApp [ECon "_", ECon "NaN", ENum (eb, _), ENum (sb, _)]) = return $ EFloatingPoint $ fpNaN (fromIntegral eb) (fromIntegral sb) + + cvt (EApp [ECon "_", ECon "+oo", ENum ( 8, _), ENum (24, _)]) = return $ EFloat infinity + cvt (EApp [ECon "_", ECon "+oo", ENum (11, _), ENum (53, _)]) = return $ EDouble infinity + cvt (EApp [ECon "_", ECon "+oo", ENum (eb, _), ENum (sb, _)]) = return $ EFloatingPoint $ fpInf False (fromIntegral eb) (fromIntegral sb) + + cvt (EApp [ECon "_", ECon "-oo", ENum ( 8, _), ENum (24, _)]) = return $ EFloat $ -infinity + cvt (EApp [ECon "_", ECon "-oo", ENum (11, _), ENum (53, _)]) = return $ EDouble $ -infinity + cvt (EApp [ECon "_", ECon "-oo", ENum (eb, _), ENum (sb, _)]) = return $ EFloatingPoint $ fpInf True (fromIntegral eb) (fromIntegral sb) + cvt (EApp [ECon "_", ECon "+zero", ENum ( 8, _), ENum (24, _)]) = return $ EFloat 0 cvt (EApp [ECon "_", ECon "+zero", ENum (11, _), ENum (53, _)]) = return $ EDouble 0 - cvt (EApp [ECon "_", ECon "-zero", ENum ( 8, _), ENum (24, _)]) = return $ EFloat (-0) - cvt (EApp [ECon "_", ECon "-zero", ENum (11, _), ENum (53, _)]) = return $ EDouble (-0) + cvt (EApp [ECon "_", ECon "+zero", ENum (eb, _), ENum (sb, _)]) = return $ EFloatingPoint $ fpZero False (fromIntegral eb) (fromIntegral sb) + + cvt (EApp [ECon "_", ECon "-zero", ENum ( 8, _), ENum (24, _)]) = return $ EFloat $ -0 + cvt (EApp [ECon "_", ECon "-zero", ENum (11, _), ENum (53, _)]) = return $ EDouble $ -0 + cvt (EApp [ECon "_", ECon "-zero", ENum (eb, _), ENum (sb, _)]) = return $ EFloatingPoint $ fpZero True (fromIntegral eb) (fromIntegral sb) + cvt x = return x getCoeff (EApp [ECon "*", ENum k, EApp [ECon "^", ECon "x", ENum p]]) = return (fst k, fst p) -- kx^p @@ -417,11 +429,12 @@ -- you ever get the error line above fire, because you must've disabled the pattern-match -- completion check warning! Shame on you. eRank :: SExpr -> Int - eRank ECon{} = 0 - eRank ENum{} = 1 - eRank EReal{} = 2 - eRank EFloat{} = 3 - eRank EDouble{} = 4 - eRank EApp{} = 5 + eRank ECon{} = 0 + eRank ENum{} = 1 + eRank EReal{} = 2 + eRank EFloat{} = 3 + eRank EFloatingPoint{} = 4 + eRank EDouble{} = 5 + eRank EApp{} = 6 {-# ANN chainAssigns ("HLint: ignore Redundant if" :: String) #-} 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 @@ -7,13 +7,17 @@ -- Stability : experimental -- -- Several examples involving IEEE-754 floating point numbers, i.e., single --- precision 'Float' ('SFloat') and double precision 'Double' ('SDouble') types. +-- precision 'Float' ('SFloat'), double precision 'Double' ('SDouble'), and +-- the generic 'SFloatingPoint' @eb@ @sb@ type where the user can specify the +-- exponent and significand bit-widths. (Note that there is always an extra +-- sign-bit, and the value of @sb@ includes the hidden bit.) -- --- Note that arithmetic with floating point is full of surprises; due to precision +-- Arithmetic with floating point is full of surprises; due to precision -- issues associativity of arithmetic operations typically do not hold. Also, -- the presence of @NaN@ is always something to look out for. ----------------------------------------------------------------------------- +{-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -152,24 +156,19 @@ -- y = -1.10355e-39 :: 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: --- --- >>> -2.240786e-38 + (-1.10355e-39) :: Float --- -2.3511412e-38 --- --- 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: +-- Unfortunately Haskell floats do not allow computation with arbitrary rounding modes, but SBV's +-- 'SFloatingPoint' type does. We have: -- --- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive (-2.240786e-38) (-1.10355e-39 :: SFloat) --- Satisfiable. Model: --- s0 = -2.351141e-38 :: Float +-- >>> fpAdd sRoundNearestTiesToEven (-2.240786e-38) (-1.10355e-39) :: SFPSingle +-- -2.35114116e-38 :: SFloatingPoint 8 24 +-- >>> fpAdd sRoundTowardPositive (-2.240786e-38) (-1.10355e-39) :: SFPSingle +-- -2.35114088e-38 :: SFloatingPoint 8 24 -- -- We can see why these two results are indeed different: The 'RoundTowardPositive' -- (which rounds towards positive infinity from zero) produces a larger result. Indeed, if we treat these numbers -- as 'Double' values, we get: -- --- >> -2.240786e-38 + (-1.10355e-39) :: Double +-- >>> -2.240786e-38 + (-1.10355e-39) :: Double -- -2.351141e-38 -- -- we see that the "more precise" result is larger than what the 'Float' value is, justifying the @@ -187,3 +186,40 @@ constrain $ fpIsPoint lhs constrain $ fpIsPoint rhs return $ lhs ./= rhs + +-- | Arbitrary precision floating-point numbers. SBV can talk about floating point numbers with arbitrary +-- exponent and significand sizes as well. Here is a simple example demonstrating the minimum non-zero positive +-- and maximum floating point values with exponent width 5 and significand width 4, which is actually 3 +-- bits for the significand explicitly stored, includes the hidden bit. We have: +-- +-- >>> fp54Bounds +-- Objective "max": Optimal model: +-- x = 61400 :: FloatingPoint 5 4 +-- max = 503 :: WordN 9 +-- min = 503 :: WordN 9 +-- Objective "min": Optimal model: +-- x = 0.00000763 :: FloatingPoint 5 4 +-- max = 257 :: WordN 9 +-- min = 257 :: WordN 9 +-- +-- The careful reader will notice that the numbers @61400@ and @0.00000763@ are quite suspicious, but the metric +-- space equivalents are correct. The reason for this is due to the sparcity of floats. The "computed" value of +-- the maximum in this bound is actually @61440@, however in @FloatingPoint 5 4@ representation all numbers +-- between @57344@ and @61440@ collapse to the same bit-pattern, and the pretty-printer picks a string +-- representation in decimal that falls within range that it considers is the "simplest." (Printing +-- floats precisely is a thorny subject!) Likewise, the minimum value we're looking for is actually +-- 2^-17, but any number between 2^-16 and 2^-17 will map to this number. It turns out that 0.00000763 +-- in decimal is one such value. Moral of the story is that when reading floating-point numbers in +-- decimal notation one should be very careful about the printed representation and the numeric value; while +-- they will match in vsalue (if there are no bugs!), they can print quite differently! (Also keep in +-- mind the rounding modes that impact how the conversion is done.) +fp54Bounds :: IO OptimizeResult +fp54Bounds = optimize Independent $ do x :: SFloatingPoint 5 4 <- sFloatingPoint "x" + + constrain $ fpIsPoint x + constrain $ x .> 0 + + maximize "max" x + minimize "min" x + + pure sTrue diff --git a/Documentation/SBV/Examples/Puzzles/Garden.hs b/Documentation/SBV/Examples/Puzzles/Garden.hs --- a/Documentation/SBV/Examples/Puzzles/Garden.hs +++ b/Documentation/SBV/Examples/Puzzles/Garden.hs @@ -39,7 +39,7 @@ module Documentation.SBV.Examples.Puzzles.Garden where import Data.SBV -import Data.Text(isSuffixOf) +import Data.List(isSuffixOf) -- | Colors of the flowers data Color = Red | Yellow | Blue diff --git a/Documentation/SBV/Examples/Transformers/SymbolicEval.hs b/Documentation/SBV/Examples/Transformers/SymbolicEval.hs --- a/Documentation/SBV/Examples/Transformers/SymbolicEval.hs +++ b/Documentation/SBV/Examples/Transformers/SymbolicEval.hs @@ -34,6 +34,7 @@ import Control.Monad.IO.Class (MonadIO) import Control.Monad.Reader (MonadReader(reader), asks, ReaderT, runReaderT) import Control.Monad.Trans (lift) +import Data.Kind (Type) import Data.SBV.Dynamic (SVal) import Data.SBV.Internals (SBV(SBV), unSBV) @@ -72,7 +73,7 @@ -- * Symbolic term evaluation -- | The term language we use to express programs and properties. -data Term :: * -> * where +data Term :: Type -> Type where Var :: String -> Term r Lit :: Integer -> Term Integer Plus :: Term Integer -> Term Integer -> Term Integer diff --git a/SBVBenchSuite/BenchSuite/Bench/Bench.hs b/SBVBenchSuite/BenchSuite/Bench/Bench.hs --- a/SBVBenchSuite/BenchSuite/Bench/Bench.hs +++ b/SBVBenchSuite/BenchSuite/Bench/Bench.hs @@ -91,9 +91,9 @@ -- | Set the runner function runner :: (Show c, NFData c) => (forall a. U.Provable a => U.SMTConfig -> a -> IO c) -> Runner -> Runner -runner r' (Runner r@RunnerI{..}) = Runner $ r{runI = toRun r'} -runner r' (RunnerGroup rs) = RunnerGroup $ runner r' <$> rs -runner _ x = x +runner r' (Runner r@RunnerI{}) = Runner $ r{runI = toRun r'} +runner r' (RunnerGroup rs) = RunnerGroup $ runner r' <$> rs +runner _ x = x {-# INLINE runner #-} toRun :: (Show c, NFData c) => @@ -189,10 +189,10 @@ {-# INLINE mkOverheadBenchMark' #-} runOverheadBenchmark :: Runner -> G.Benchmark -runOverheadBenchmark (Runner r@RunnerI{..}) = mkOverheadBenchMark' r -runOverheadBenchmark (RunnerGroup rs) = G.bgroup "" $ -- leave the description close to the benchmark/problem definition - runOverheadBenchmark <$> rs -runOverheadBenchmark (RBenchmark b) = b +runOverheadBenchmark (Runner r@RunnerI{}) = mkOverheadBenchMark' r +runOverheadBenchmark (RunnerGroup rs) = G.bgroup "" $ -- leave the description close to the benchmark/problem definition + runOverheadBenchmark <$> rs +runOverheadBenchmark (RBenchmark b) = b {-# INLINE runOverheadBenchmark #-} -- | make a normal benchmark without the overhead comparison. Notice this is @@ -205,9 +205,9 @@ -- function to convert the runners defined in each file to benchmarks which can -- be run by gauge runBenchmark :: Runner -> G.Benchmark -runBenchmark (Runner r@RunnerI{..}) = mkBenchmark r -runBenchmark (RunnerGroup rs) = G.bgroup "" $ runBenchmark <$> rs -runBenchmark (RBenchmark b) = b +runBenchmark (Runner r@RunnerI{}) = mkBenchmark r +runBenchmark (RunnerGroup rs) = G.bgroup "" $ runBenchmark <$> rs +runBenchmark (RBenchmark b) = b {-# INLINE runBenchmark #-} -- | This is just a wrapper around the RunnerI constructor and serves as the main diff --git a/SBVTestSuite/GoldFiles/arbFp_opt_1.gold b/SBVTestSuite/GoldFiles/arbFp_opt_1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/arbFp_opt_1.gold @@ -0,0 +1,3 @@ +Optimal model: + s0 = 65504 :: FloatingPoint 5 11 + x = 64511 :: Word16 diff --git a/SBVTestSuite/GoldFiles/freshVars.gold b/SBVTestSuite/GoldFiles/freshVars.gold --- a/SBVTestSuite/GoldFiles/freshVars.gold +++ b/SBVTestSuite/GoldFiles/freshVars.gold @@ -41,113 +41,122 @@ (ite (= x Plus) 0 (ite (= x Minus) 1 2)) ) [GOOD] (declare-fun s16 () BinOp) +[GOOD] (declare-fun s17 () (_ FloatingPoint 15 113)) +[GOOD] (declare-fun s18 () (_ FloatingPoint 15 113)) [GOOD] (assert s3) -[GOOD] (define-fun s17 () (_ BitVec 8) #x01) -[GOOD] (define-fun s18 () Bool (= s4 s17)) -[GOOD] (assert s18) -[GOOD] (define-fun s19 () (_ BitVec 16) #x0002) -[GOOD] (define-fun s20 () Bool (= s5 s19)) +[GOOD] (define-fun s19 () (_ BitVec 8) #x01) +[GOOD] (define-fun s20 () Bool (= s4 s19)) [GOOD] (assert s20) -[GOOD] (define-fun s21 () (_ BitVec 32) #x00000003) -[GOOD] (define-fun s22 () Bool (= s6 s21)) +[GOOD] (define-fun s21 () (_ BitVec 16) #x0002) +[GOOD] (define-fun s22 () Bool (= s5 s21)) [GOOD] (assert s22) -[GOOD] (define-fun s23 () (_ BitVec 64) #x0000000000000004) -[GOOD] (define-fun s24 () Bool (= s7 s23)) +[GOOD] (define-fun s23 () (_ BitVec 32) #x00000003) +[GOOD] (define-fun s24 () Bool (= s6 s23)) [GOOD] (assert s24) -[GOOD] (define-fun s25 () (_ BitVec 8) #x05) -[GOOD] (define-fun s26 () Bool (= s8 s25)) +[GOOD] (define-fun s25 () (_ BitVec 64) #x0000000000000004) +[GOOD] (define-fun s26 () Bool (= s7 s25)) [GOOD] (assert s26) -[GOOD] (define-fun s27 () (_ BitVec 16) #x0006) -[GOOD] (define-fun s28 () Bool (= s9 s27)) +[GOOD] (define-fun s27 () (_ BitVec 8) #x05) +[GOOD] (define-fun s28 () Bool (= s8 s27)) [GOOD] (assert s28) -[GOOD] (define-fun s29 () (_ BitVec 32) #x00000007) -[GOOD] (define-fun s30 () Bool (= s10 s29)) +[GOOD] (define-fun s29 () (_ BitVec 16) #x0006) +[GOOD] (define-fun s30 () Bool (= s9 s29)) [GOOD] (assert s30) -[GOOD] (define-fun s31 () (_ BitVec 64) #x0000000000000008) -[GOOD] (define-fun s32 () Bool (= s11 s31)) +[GOOD] (define-fun s31 () (_ BitVec 32) #x00000007) +[GOOD] (define-fun s32 () Bool (= s10 s31)) [GOOD] (assert s32) -[GOOD] (define-fun s33 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0))) -[GOOD] (define-fun s34 () Bool (fp.eq s12 s33)) +[GOOD] (define-fun s33 () (_ BitVec 64) #x0000000000000008) +[GOOD] (define-fun s34 () Bool (= s11 s33)) [GOOD] (assert s34) -[GOOD] (define-fun s35 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) roundNearestTiesToEven (/ 10.0 1.0))) -[GOOD] (define-fun s36 () Bool (fp.eq s13 s35)) +[GOOD] (define-fun s35 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0))) +[GOOD] (define-fun s36 () Bool (fp.eq s12 s35)) [GOOD] (assert s36) -[GOOD] (define-fun s37 () Real (/ 11.0 1.0)) -[GOOD] (define-fun s38 () Bool (= s14 s37)) +[GOOD] (define-fun s37 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) roundNearestTiesToEven (/ 10.0 1.0))) +[GOOD] (define-fun s38 () Bool (fp.eq s13 s37)) [GOOD] (assert s38) -[GOOD] (define-fun s39 () Int 12) -[GOOD] (define-fun s40 () Bool (= s15 s39)) +[GOOD] (define-fun s39 () Real (/ 11.0 1.0)) +[GOOD] (define-fun s40 () Bool (= s14 s39)) [GOOD] (assert s40) -[GOOD] (define-fun s41 () BinOp Plus) -[GOOD] (define-fun s42 () Bool (= s16 s41)) +[GOOD] (define-fun s41 () Int 12) +[GOOD] (define-fun s42 () Bool (= s15 s41)) [GOOD] (assert s42) +[GOOD] (define-fun s43 () BinOp Plus) +[GOOD] (define-fun s44 () Bool (= s16 s43)) +[GOOD] (assert s44) +[GOOD] (define-fun s45 () Bool (fp.eq s17 s18)) +[GOOD] (assert s45) +[GOOD] (define-fun s46 () Bool (= s17 s18)) +[GOOD] (define-fun s47 () Bool (not s46)) +[GOOD] (assert s47) +[GOOD] (define-fun s48 () Bool (fp.isPositive s17)) +[GOOD] (assert s48) [GOOD] (declare-fun array_0 () (Array Int Int)) [GOOD] (define-fun array_0_initializer () Bool true) ; no initializiation needed -[GOOD] (declare-fun s43 () Int) -[GOOD] (declare-fun s44 () Bool) -[GOOD] (define-fun s46 () Int 2) -[GOOD] (define-fun s45 () Int (select array_0 s43)) -[GOOD] (define-fun s47 () Bool (= s45 s46)) -[GOOD] (assert s47) -[GOOD] (define-fun s49 () String (_ char #x61)) +[GOOD] (declare-fun s49 () Int) +[GOOD] (declare-fun s50 () Bool) +[GOOD] (define-fun s52 () Int 2) +[GOOD] (define-fun s51 () Int (select array_0 s49)) +[GOOD] (define-fun s53 () Bool (= s51 s52)) +[GOOD] (assert s53) +[GOOD] (define-fun s55 () String (_ char #x61)) [GOOD] (declare-fun vFArray_uninitializedRead (Bool) String) [GOOD] (assert (forall ((a1 Bool)) (let ((result (vFArray_uninitializedRead a1))) (= 1 (str.len result)) ))) -[GOOD] (define-fun s48 () String (vFArray_uninitializedRead s44)) -[GOOD] (define-fun s50 () Bool (= s48 s49)) -[GOOD] (assert s50) -[GOOD] (define-fun s51 () Int 42) +[GOOD] (define-fun s54 () String (vFArray_uninitializedRead s50)) +[GOOD] (define-fun s56 () Bool (= s54 s55)) +[GOOD] (assert s56) +[GOOD] (define-fun s57 () Int 42) [GOOD] (define-fun array_1 () (Array Int Int) ((as const (Array Int Int)) 42)) [GOOD] (define-fun array_1_initializer () Bool true) ; no initializiation needed -[GOOD] (declare-fun s52 () Int) -[GOOD] (declare-fun s53 () String) -[GOOD] (assert (= 1 (str.len s53))) -[GOOD] (define-fun s54 () Int 96) -[GOOD] (define-fun s55 () Int (select array_1 s54)) -[GOOD] (define-fun s56 () Bool (= s52 s55)) -[GOOD] (assert s56) -[GOOD] (define-fun s57 () String (_ char #x58)) -[GOOD] (define-fun s58 () Bool (= s53 s57)) -[GOOD] (assert s58) -[GOOD] (define-fun s59 () Int 1) -[GOOD] (define-fun s60 () Bool (= s43 s59)) -[GOOD] (assert s60) -[GOOD] (define-fun s61 () Bool (not s44)) -[GOOD] (assert s61) -[GOOD] (declare-fun s62 () String) +[GOOD] (declare-fun s58 () Int) +[GOOD] (declare-fun s59 () String) +[GOOD] (assert (= 1 (str.len s59))) +[GOOD] (define-fun s60 () Int 96) +[GOOD] (define-fun s61 () Int (select array_1 s60)) +[GOOD] (define-fun s62 () Bool (= s58 s61)) +[GOOD] (assert s62) +[GOOD] (define-fun s63 () String (_ char #x58)) +[GOOD] (define-fun s64 () Bool (= s59 s63)) +[GOOD] (assert s64) +[GOOD] (define-fun s65 () Int 1) +[GOOD] (define-fun s66 () Bool (= s49 s65)) +[GOOD] (assert s66) +[GOOD] (define-fun s67 () Bool (not s50)) +[GOOD] (assert s67) +[GOOD] (declare-fun s68 () String) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (declare-fun s63 () (Seq Int)) +[GOOD] (declare-fun s69 () (Seq Int)) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (declare-fun s64 () (Seq (Seq Int))) +[GOOD] (declare-fun s70 () (Seq (Seq Int))) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (declare-fun s65 () (Seq (_ BitVec 8))) +[GOOD] (declare-fun s71 () (Seq (_ BitVec 8))) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (declare-fun s66 () (Seq (Seq (_ BitVec 16)))) -[GOOD] (define-fun s67 () String "hello") -[GOOD] (define-fun s68 () Bool (= s62 s67)) -[GOOD] (assert s68) -[GOOD] (define-fun s69 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4))) -[GOOD] (define-fun s70 () Bool (= s63 s69)) -[GOOD] (assert s70) -[GOOD] (define-fun s71 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7))))) -[GOOD] (define-fun s72 () Bool (= s64 s71)) -[GOOD] (assert s72) -[GOOD] (define-fun s73 () (Seq (_ BitVec 8)) (seq.++ (seq.unit #x01) (seq.unit #x02))) -[GOOD] (define-fun s74 () Bool (= s65 s73)) +[GOOD] (declare-fun s72 () (Seq (Seq (_ BitVec 16)))) +[GOOD] (define-fun s73 () String "hello") +[GOOD] (define-fun s74 () Bool (= s68 s73)) [GOOD] (assert s74) -[GOOD] (define-fun s75 () (Seq (Seq (_ BitVec 16))) (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006))))) -[GOOD] (define-fun s76 () Bool (= s66 s75)) +[GOOD] (define-fun s75 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4))) +[GOOD] (define-fun s76 () Bool (= s69 s75)) [GOOD] (assert s76) +[GOOD] (define-fun s77 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7))))) +[GOOD] (define-fun s78 () Bool (= s70 s77)) +[GOOD] (assert s78) +[GOOD] (define-fun s79 () (Seq (_ BitVec 8)) (seq.++ (seq.unit #x01) (seq.unit #x02))) +[GOOD] (define-fun s80 () Bool (= s71 s79)) +[GOOD] (assert s80) +[GOOD] (define-fun s81 () (Seq (Seq (_ BitVec 16))) (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006))))) +[GOOD] (define-fun s82 () Bool (= s72 s81)) +[GOOD] (assert s82) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -185,27 +194,31 @@ [RECV] ((s15 12)) [SEND] (get-value (s16)) [RECV] ((s16 Plus)) -[SEND] (get-value (s43)) -[RECV] ((s43 1)) -[SEND] (get-value (s44)) -[RECV] ((s44 false)) -[SEND] (get-value (s52)) -[RECV] ((s52 42)) -[SEND] (get-value (s53)) -[RECV] ((s53 "X")) -[SEND] (get-value (s62)) -[RECV] ((s62 "hello")) -[SEND] (get-value (s63)) -[RECV] ((s63 (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4)))) -[SEND] (get-value (s64)) -[RECV] ((s64 (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) +[SEND] (get-value (s49)) +[RECV] ((s49 1)) +[SEND] (get-value (s50)) +[RECV] ((s50 false)) +[SEND] (get-value (s58)) +[RECV] ((s58 42)) +[SEND] (get-value (s59)) +[RECV] ((s59 "X")) +[SEND] (get-value (s68)) +[RECV] ((s68 "hello")) +[SEND] (get-value (s69)) +[RECV] ((s69 (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4)))) +[SEND] (get-value (s70)) +[RECV] ((s70 (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7)))))) -[SEND] (get-value (s65)) -[RECV] ((s65 (seq.++ (seq.unit #x01) (seq.unit #x02)))) -[SEND] (get-value (s66)) -[RECV] ((s66 (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) +[SEND] (get-value (s71)) +[RECV] ((s71 (seq.++ (seq.unit #x01) (seq.unit #x02)))) +[SEND] (get-value (s72)) +[RECV] ((s72 (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006)))))) +[SEND] (get-value (s17)) +[RECV] ((s17 (_ +zero 15 113))) +[SEND] (get-value (s18)) +[RECV] ((s18 (_ -zero 15 113))) *** Solver : Z3 *** Exit code: ExitSuccess @@ -234,4 +247,6 @@ vList2 = [[1,2,3],[4,5,6,7]] :: [[Integer]] vList3 = [1,2] :: [Word8] vList4 = [[1,2,3],[],[4,5,6]] :: [[Word16]] + vQuad = 0.0 :: FloatingPoint 15 113 + wQuad = -0.0 :: FloatingPoint 15 113 DONE! diff --git a/SBVTestSuite/GoldFiles/optFloat1a.gold b/SBVTestSuite/GoldFiles/optFloat1a.gold --- a/SBVTestSuite/GoldFiles/optFloat1a.gold +++ b/SBVTestSuite/GoldFiles/optFloat1a.gold @@ -2,12 +2,24 @@ x = -3.4028235e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 1 11111110 11111111111111111111111 - Hex: FF7F FFFF - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 1 11111110 11111111111111111111111 + Hex layout: FF7F FFFF + Precision: Single Sign: Negative Exponent: 127 (Stored: 254, Bias: 127) - Hex-float: -0x1.fffffep127 - Value: -3.4028235e38 (NORMAL) - min-x = 0x00800000 :: Word32 + Classification: FP_NORMAL + Binary Value: -0b1.11111111111111111111111p127 + Octal Value: -0o3.77777774p42 + Decimal Value: -3.4028235e38 + Hex Value: -0xF.FFFFFp31 + min-x = 8388608 :: Word32 + 3 2 1 0 + 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 0000 0000 1000 0000 0000 0000 0000 0000 + Hex layout: 0080 0000 + Type: Unsigned 32-bit word + Binary Value: 0b100000000000000000000000 + Octal Value: 0o40000000 + Decimal Value: 8388608 + Hex Value: 0x800000 diff --git a/SBVTestSuite/GoldFiles/optFloat1b.gold b/SBVTestSuite/GoldFiles/optFloat1b.gold --- a/SBVTestSuite/GoldFiles/optFloat1b.gold +++ b/SBVTestSuite/GoldFiles/optFloat1b.gold @@ -1,13 +1,22 @@ Optimal model: - x = -Infinity :: Float + x = -Infinity :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 1 11111111 00000000000000000000000 - Hex: FF80 0000 - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 1 11111111 00000000000000000000000 + Hex layout: FF80 0000 + Precision: Single Sign: Negative Exponent: 128 (Stored: 255, Bias: 127) - Hex-float: -Infinity + Classification: FP_INFINITE Value: -Infinity - min-x = 0x007fffff :: Word32 + min-x = 8388607 :: Word32 + 3 2 1 0 + 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 0000 0000 0111 1111 1111 1111 1111 1111 + Hex layout: 007F FFFF + Type: Unsigned 32-bit word + Binary Value: 0b11111111111111111111111 + Octal Value: 0o37777777 + Decimal Value: 8388607 + Hex Value: 0x7fffff diff --git a/SBVTestSuite/GoldFiles/optFloat1c.gold b/SBVTestSuite/GoldFiles/optFloat1c.gold --- a/SBVTestSuite/GoldFiles/optFloat1c.gold +++ b/SBVTestSuite/GoldFiles/optFloat1c.gold @@ -2,12 +2,24 @@ x = 3.4028235e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 11111110 11111111111111111111111 - Hex: 7F7F FFFF - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 0 11111110 11111111111111111111111 + Hex layout: 7F7F FFFF + Precision: Single Sign: Positive Exponent: 127 (Stored: 254, Bias: 127) - Hex-float: +0x1.fffffep127 - Value: +3.4028235e38 (NORMAL) - max-x = 0xff7fffff :: Word32 + Classification: FP_NORMAL + Binary Value: 0b1.11111111111111111111111p127 + Octal Value: 0o3.77777774p42 + Decimal Value: 3.4028235e38 + Hex Value: 0xF.FFFFFp31 + max-x = 4286578687 :: Word32 + 3 2 1 0 + 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 1111 1111 0111 1111 1111 1111 1111 1111 + Hex layout: FF7F FFFF + Type: Unsigned 32-bit word + Binary Value: -0b11111111011111111111111111111111 + Octal Value: -0o37737777777 + Decimal Value: 4286578687 + Hex Value: -0xff7fffff diff --git a/SBVTestSuite/GoldFiles/optFloat1d.gold b/SBVTestSuite/GoldFiles/optFloat1d.gold --- a/SBVTestSuite/GoldFiles/optFloat1d.gold +++ b/SBVTestSuite/GoldFiles/optFloat1d.gold @@ -2,12 +2,21 @@ x = Infinity :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 11111111 00000000000000000000000 - Hex: 7F80 0000 - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 0 11111111 00000000000000000000000 + Hex layout: 7F80 0000 + Precision: Single Sign: Positive Exponent: 128 (Stored: 255, Bias: 127) - Hex-float: +Infinity - Value: +Infinity - max-y = 0xff800000 :: Word32 + Classification: FP_INFINITE + Value: Infinity + max-y = 4286578688 :: Word32 + 3 2 1 0 + 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 1111 1111 1000 0000 0000 0000 0000 0000 + Hex layout: FF80 0000 + Type: Unsigned 32-bit word + Binary Value: -0b11111111100000000000000000000000 + Octal Value: -0o37740000000 + Decimal Value: 4286578688 + Hex Value: -0xff800000 diff --git a/SBVTestSuite/GoldFiles/optFloat2a.gold b/SBVTestSuite/GoldFiles/optFloat2a.gold --- a/SBVTestSuite/GoldFiles/optFloat2a.gold +++ b/SBVTestSuite/GoldFiles/optFloat2a.gold @@ -2,12 +2,24 @@ x = -1.7976931348623157e308 :: Double 6 5 4 3 2 1 0 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 1 11111111110 1111111111111111111111111111111111111111111111111111 - Hex: FFEF FFFF FFFF FFFF - Precision: DP + S ----E11---- ------------------------S52------------------------- + Binary layout: 1 11111111110 1111111111111111111111111111111111111111111111111111 + Hex layout: FFEF FFFF FFFF FFFF + Precision: Double Sign: Negative Exponent: 1023 (Stored: 2046, Bias: 1023) - Hex-float: -0x1.fffffffffffffp1023 - Value: -1.7976931348623157e308 (NORMAL) - min-x = 0x0010000000000000 :: Word64 + Classification: FP_NORMAL + Binary Value: -0b1.1111111111111111111111111111111111111111111111111111p1023 + Octal Value: -0o1.777777777777777774p341 + Decimal Value: -1.7976931348623157e308 + Hex Value: -0xF.FFFFFFFFFFFF8p255 + min-x = 4503599627370496 :: Word64 + 6 5 4 3 2 1 0 + 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 0000 0000 0001 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 + Hex layout: 0010 0000 0000 0000 + Type: Unsigned 64-bit word + Binary Value: 0b10000000000000000000000000000000000000000000000000000 + Octal Value: 0o200000000000000000 + Decimal Value: 4503599627370496 + Hex Value: 0x10000000000000 diff --git a/SBVTestSuite/GoldFiles/optFloat2b.gold b/SBVTestSuite/GoldFiles/optFloat2b.gold --- a/SBVTestSuite/GoldFiles/optFloat2b.gold +++ b/SBVTestSuite/GoldFiles/optFloat2b.gold @@ -1,13 +1,22 @@ Optimal model: - x = -Infinity :: Double + x = -Infinity :: Double 6 5 4 3 2 1 0 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 1 11111111111 0000000000000000000000000000000000000000000000000000 - Hex: FFF0 0000 0000 0000 - Precision: DP + S ----E11---- ------------------------S52------------------------- + Binary layout: 1 11111111111 0000000000000000000000000000000000000000000000000000 + Hex layout: FFF0 0000 0000 0000 + Precision: Double Sign: Negative Exponent: 1024 (Stored: 2047, Bias: 1023) - Hex-float: -Infinity + Classification: FP_INFINITE Value: -Infinity - min-x = 0x000fffffffffffff :: Word64 + min-x = 4503599627370495 :: Word64 + 6 5 4 3 2 1 0 + 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 0000 0000 0000 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 + Hex layout: 000F FFFF FFFF FFFF + Type: Unsigned 64-bit word + Binary Value: 0b1111111111111111111111111111111111111111111111111111 + Octal Value: 0o177777777777777777 + Decimal Value: 4503599627370495 + Hex Value: 0xfffffffffffff diff --git a/SBVTestSuite/GoldFiles/optFloat2c.gold b/SBVTestSuite/GoldFiles/optFloat2c.gold --- a/SBVTestSuite/GoldFiles/optFloat2c.gold +++ b/SBVTestSuite/GoldFiles/optFloat2c.gold @@ -2,12 +2,24 @@ x = 1.7976931348623157e308 :: Double 6 5 4 3 2 1 0 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 0 11111111110 1111111111111111111111111111111111111111111111111111 - Hex: 7FEF FFFF FFFF FFFF - Precision: DP + S ----E11---- ------------------------S52------------------------- + Binary layout: 0 11111111110 1111111111111111111111111111111111111111111111111111 + Hex layout: 7FEF FFFF FFFF FFFF + Precision: Double Sign: Positive Exponent: 1023 (Stored: 2046, Bias: 1023) - Hex-float: +0x1.fffffffffffffp1023 - Value: +1.7976931348623157e308 (NORMAL) - max-x = 0xffefffffffffffff :: Word64 + Classification: FP_NORMAL + Binary Value: 0b1.1111111111111111111111111111111111111111111111111111p1023 + Octal Value: 0o1.777777777777777774p341 + Decimal Value: 1.7976931348623157e308 + Hex Value: 0xF.FFFFFFFFFFFF8p255 + max-x = 18442240474082181119 :: Word64 + 6 5 4 3 2 1 0 + 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 1111 1111 1110 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 + Hex layout: FFEF FFFF FFFF FFFF + Type: Unsigned 64-bit word + Binary Value: -0b1111111111101111111111111111111111111111111111111111111111111111 + Octal Value: -0o1777577777777777777777 + Decimal Value: 18442240474082181119 + Hex Value: -0xffefffffffffffff diff --git a/SBVTestSuite/GoldFiles/optFloat2d.gold b/SBVTestSuite/GoldFiles/optFloat2d.gold --- a/SBVTestSuite/GoldFiles/optFloat2d.gold +++ b/SBVTestSuite/GoldFiles/optFloat2d.gold @@ -1,13 +1,22 @@ Optimal model: - x = Infinity :: Double + x = Infinity :: Double 6 5 4 3 2 1 0 3 21098765432 1098765432109876543210987654321098765432109876543210 - S ----E11---- ------------------------F52------------------------- - Binary: 0 11111111111 0000000000000000000000000000000000000000000000000000 - Hex: 7FF0 0000 0000 0000 - Precision: DP + S ----E11---- ------------------------S52------------------------- + Binary layout: 0 11111111111 0000000000000000000000000000000000000000000000000000 + Hex layout: 7FF0 0000 0000 0000 + Precision: Double Sign: Positive Exponent: 1024 (Stored: 2047, Bias: 1023) - Hex-float: +Infinity - Value: +Infinity - max-y = 0xfff0000000000000 :: Word64 + Classification: FP_INFINITE + Value: Infinity + max-y = 18442240474082181120 :: Word64 + 6 5 4 3 2 1 0 + 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 1111 1111 1111 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 + Hex layout: FFF0 0000 0000 0000 + Type: Unsigned 64-bit word + Binary Value: -0b1111111111110000000000000000000000000000000000000000000000000000 + Octal Value: -0o1777600000000000000000 + Decimal Value: 18442240474082181120 + Hex Value: -0xfff0000000000000 diff --git a/SBVTestSuite/GoldFiles/optFloat3.gold b/SBVTestSuite/GoldFiles/optFloat3.gold --- a/SBVTestSuite/GoldFiles/optFloat3.gold +++ b/SBVTestSuite/GoldFiles/optFloat3.gold @@ -2,34 +2,52 @@ max-x+y = 3.4028235e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 11111110 11111111111111111111111 - Hex: 7F7F FFFF - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 0 11111110 11111111111111111111111 + Hex layout: 7F7F FFFF + Precision: Single Sign: Positive Exponent: 127 (Stored: 254, Bias: 127) - Hex-float: +0x1.fffffep127 - Value: +3.4028235e38 (NORMAL) + Classification: FP_NORMAL + Binary Value: 0b1.11111111111111111111111p127 + Octal Value: 0o3.77777774p42 + Decimal Value: 3.4028235e38 + Hex Value: 0xF.FFFFFp31 x = 1.7014117e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 11111101 11111111111111111111111 - Hex: 7EFF FFFF - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 0 11111101 11111111111111111111111 + Hex layout: 7EFF FFFF + Precision: Single Sign: Positive Exponent: 126 (Stored: 253, Bias: 127) - Hex-float: +0x1.fffffep126 - Value: +1.7014117e38 (NORMAL) + Classification: FP_NORMAL + Binary Value: 0b1.11111111111111111111111p126 + Octal Value: 0o1.77777776p42 + Decimal Value: 1.7014117e38 + Hex Value: 0x7.FFFFF8p31 y = 1.7014117e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 11111101 11111111111111111111111 - Hex: 7EFF FFFF - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 0 11111101 11111111111111111111111 + Hex layout: 7EFF FFFF + Precision: Single Sign: Positive Exponent: 126 (Stored: 253, Bias: 127) - Hex-float: +0x1.fffffep126 - Value: +1.7014117e38 (NORMAL) - metric-max-x+y = 0xff7fffff :: Word32 + Classification: FP_NORMAL + Binary Value: 0b1.11111111111111111111111p126 + Octal Value: 0o1.77777776p42 + Decimal Value: 1.7014117e38 + Hex Value: 0x7.FFFFF8p31 + metric-max-x+y = 4286578687 :: Word32 + 3 2 1 0 + 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 1111 1111 0111 1111 1111 1111 1111 1111 + Hex layout: FF7F FFFF + Type: Unsigned 32-bit word + Binary Value: -0b11111111011111111111111111111111 + Octal Value: -0o37737777777 + Decimal Value: 4286578687 + Hex Value: -0xff7fffff diff --git a/SBVTestSuite/GoldFiles/optFloat4.gold b/SBVTestSuite/GoldFiles/optFloat4.gold --- a/SBVTestSuite/GoldFiles/optFloat4.gold +++ b/SBVTestSuite/GoldFiles/optFloat4.gold @@ -2,34 +2,52 @@ min-x+y = 3.0e-45 :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 00000000 00000000000000000000010 - Hex: 0000 0002 - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 0 00000000 00000000000000000000010 + Hex layout: 0000 0002 + Precision: Single Sign: Positive - Exponent: -126 (Stored: 0, Bias: 126) - Hex-float: +0x1p-148 - Value: +3.0e-45 (DENORMAL) + Exponent: -126 (Subnormal, with fixed exponent value. Stored: 0, Bias: 127) + Classification: FP_SUBNORMAL + Binary Value: 0b1p-148 + Octal Value: 0o4p-50 + Decimal Value: 3.0e-45 + Hex Value: 0x1p-37 x = 1.0e-45 :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 00000000 00000000000000000000001 - Hex: 0000 0001 - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 0 00000000 00000000000000000000001 + Hex layout: 0000 0001 + Precision: Single Sign: Positive - Exponent: -126 (Stored: 0, Bias: 126) - Hex-float: +0x1p-149 - Value: +1.0e-45 (DENORMAL) + Exponent: -126 (Subnormal, with fixed exponent value. Stored: 0, Bias: 127) + Classification: FP_SUBNORMAL + Binary Value: 0b1p-149 + Octal Value: 0o2p-50 + Decimal Value: 1.0e-45 + Hex Value: 0x8p-38 y = 1.0e-45 :: Float 3 2 1 0 1 09876543 21098765432109876543210 - S ---E8--- ----------F23---------- - Binary: 0 00000000 00000000000000000000001 - Hex: 0000 0001 - Precision: SP + S ---E8--- ----------S23---------- + Binary layout: 0 00000000 00000000000000000000001 + Hex layout: 0000 0001 + Precision: Single Sign: Positive - Exponent: -126 (Stored: 0, Bias: 126) - Hex-float: +0x1p-149 - Value: +1.0e-45 (DENORMAL) - metric-min-x+y = 0x80000002 :: Word32 + Exponent: -126 (Subnormal, with fixed exponent value. Stored: 0, Bias: 127) + Classification: FP_SUBNORMAL + Binary Value: 0b1p-149 + Octal Value: 0o2p-50 + Decimal Value: 1.0e-45 + Hex Value: 0x8p-38 + metric-min-x+y = 2147483650 :: Word32 + 3 2 1 0 + 1098 7654 3210 9876 5432 1098 7654 3210 + Binary layout: 1000 0000 0000 0000 0000 0000 0000 0010 + Hex layout: 8000 0002 + Type: Unsigned 32-bit word + Binary Value: -0b10000000000000000000000000000010 + Octal Value: -0o20000000002 + Decimal Value: 2147483650 + Hex Value: -0x80000002 diff --git a/SBVTestSuite/SBVDocTest.hs b/SBVTestSuite/SBVDocTest.hs --- a/SBVTestSuite/SBVDocTest.hs +++ b/SBVTestSuite/SBVDocTest.hs @@ -54,12 +54,12 @@ testFiles = filter (\nm -> not (skipWindows nm || skipRemote nm || skipLocal nm)) allFiles packages = [ "async" - , "crackNum" , "mtl" , "QuickCheck" , "random" , "syb" , "uniplate" + , "libBF" ] pargs = concatMap (\p -> ["-package", p]) packages diff --git a/SBVTestSuite/SBVHLint.hs b/SBVTestSuite/SBVHLint.hs --- a/SBVTestSuite/SBVHLint.hs +++ b/SBVTestSuite/SBVHLint.hs @@ -24,6 +24,7 @@ , "SBVTestSuite" , "-i", "Use otherwise" , "-i", "Parse error" + , "--cpp-simple" ] main :: IO () diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -26,6 +26,7 @@ import qualified TestSuite.Arrays.Query import qualified TestSuite.Arrays.Caching import qualified TestSuite.Basics.AllSat +import qualified TestSuite.Basics.ArbFloats import qualified TestSuite.Basics.ArithNoSolver import qualified TestSuite.Basics.ArithSolver import qualified TestSuite.Basics.Assert @@ -181,6 +182,7 @@ , TestSuite.Arrays.Query.tests , TestSuite.Arrays.Caching.tests , TestSuite.Basics.AllSat.tests + , TestSuite.Basics.ArbFloats.tests , TestSuite.Basics.ArithNoSolver.tests , TestSuite.Basics.Assert.tests , TestSuite.Basics.BasicTests.tests diff --git a/SBVTestSuite/TestSuite/Basics/ArbFloats.hs b/SBVTestSuite/TestSuite/Basics/ArbFloats.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Basics/ArbFloats.hs @@ -0,0 +1,40 @@ +----------------------------------------------------------------------------- +-- | +-- Module : TestSuite.Basics.ArbFloats +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Basic arbitrary float checks +----------------------------------------------------------------------------- + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module TestSuite.Basics.ArbFloats(tests) where + +import Utils.SBVTestFramework + +-- # of inhabitants is 2^sb(2^eb - 1) + 3 +count :: Integer -> Integer -> Integer +count eb sb = 2^sb * (2^eb - 1) + 3 + +tests :: TestTree +tests = testGroup "Basics.ArbFloats" + [ testCase "FP_2_2" (assert $ (== fromIntegral (count 2 2)) <$> numberOfModels (const sTrue :: SFloatingPoint 2 2 -> SBool)) + , testCase "FP_2_3" (assert $ (== fromIntegral (count 2 3)) <$> numberOfModels (const sTrue :: SFloatingPoint 2 3 -> SBool)) + , testCase "FP_2_4" (assert $ (== fromIntegral (count 2 4)) <$> numberOfModels (const sTrue :: SFloatingPoint 2 4 -> SBool)) + + , testCase "FP_3_2" (assert $ (== fromIntegral (count 3 2)) <$> numberOfModels (const sTrue :: SFloatingPoint 3 2 -> SBool)) + , testCase "FP_3_3" (assert $ (== fromIntegral (count 3 3)) <$> numberOfModels (const sTrue :: SFloatingPoint 3 3 -> SBool)) + , testCase "FP_3_4" (assert $ (== fromIntegral (count 3 4)) <$> numberOfModels (const sTrue :: SFloatingPoint 3 4 -> SBool)) + + , testCase "FP_4_2" (assert $ (== fromIntegral (count 4 2)) <$> numberOfModels (const sTrue :: SFloatingPoint 4 2 -> SBool)) + , testCase "FP_4_3" (assert $ (== fromIntegral (count 4 3)) <$> numberOfModels (const sTrue :: SFloatingPoint 4 3 -> SBool)) + , testCase "FP_4_4" (assert $ (== fromIntegral (count 4 4)) <$> numberOfModels (const sTrue :: SFloatingPoint 4 4 -> SBool)) + + , goldenVsStringShow "arbFp_opt_1" (optimize Lexicographic $ \x -> do {constrain (fpIsPoint x); maximize "x" (x::SFPHalf)}) + ] diff --git a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs @@ -18,8 +18,6 @@ module TestSuite.Basics.ArithNoSolver(tests) where -import qualified Data.Numbers.CrackNum as CN (wordToFloat, wordToDouble, floatToWord, doubleToWord) - import Data.SBV.Internals import Utils.SBVTestFramework @@ -400,11 +398,11 @@ -- NB. We don't constant fold float/double conversions, so we skip these -- - ++ [cvtTest ("reinterp_Word32_Float", show x, sWord32AsSFloat (literal x), literal (CN.wordToFloat x)) | x <- w32s] - ++ [cvtTest ("reinterp_Word64_Double", show x, sWord64AsSDouble (literal x), literal (CN.wordToDouble x)) | x <- w64s] + ++ [cvtTest ("reinterp_Word32_Float", show x, sWord32AsSFloat (literal x), literal (wordToFloat x)) | x <- w32s] + ++ [cvtTest ("reinterp_Word64_Double", show x, sWord64AsSDouble (literal x), literal (wordToDouble x)) | x <- w64s] - ++ [cvtTestI ("reinterp_Float_Word32", show x, sFloatAsSWord32 (literal x), CN.floatToWord x) | x <- fs, not (isNaN x)] -- Not unique for NaN - ++ [cvtTestI ("reinterp_Double_Word64", show x, sDoubleAsSWord64 (literal x), CN.doubleToWord x) | x <- ds, not (isNaN x)] -- Not unique for NaN + ++ [cvtTestI ("reinterp_Float_Word32", show x, sFloatAsSWord32 (literal x), floatToWord x) | x <- fs, not (isNaN x)] -- Not unique for NaN + ++ [cvtTestI ("reinterp_Double_Word64", show x, sDoubleAsSWord64 (literal x), doubleToWord x) | x <- ds, not (isNaN x)] -- Not unique for NaN floatRun1 nm f g cmb = [(nm, cmb (x, f x, extract (g (literal x)))) | x <- fs] doubleRun1 nm f g cmb = [(nm, cmb (x, f x, extract (g (literal x)))) | x <- ds] diff --git a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs @@ -19,8 +19,6 @@ module TestSuite.Basics.ArithSolver(tests) where -import qualified Data.Numbers.CrackNum as RC (wordToFloat, wordToDouble, floatToWord, doubleToWord) - import Data.SBV.Internals hiding (free, free_) import Utils.SBVTestFramework @@ -471,11 +469,11 @@ ++ [("fromFP_Double_ToDouble", show x, mkThm1 (m fromSDouble :: SDouble -> SDouble) x x ) | x <- ds] -- Neither Z3 nor MathSAT support Double->Integer/Double->Real conversion for the time being; so we skip those. See GitHub issue: #191 - ++ [("reinterp_Word32_Float", show x, mkThmC sWord32AsSFloat x (RC.wordToFloat x)) | x <- w32s] - ++ [("reinterp_Word64_Double", show x, mkThmC sWord64AsSDouble x (RC.wordToDouble x)) | x <- w64s] + ++ [("reinterp_Word32_Float", show x, mkThmC sWord32AsSFloat x (wordToFloat x)) | x <- w32s] + ++ [("reinterp_Word64_Double", show x, mkThmC sWord64AsSDouble x (wordToDouble x)) | x <- w64s] - ++ [("reinterp_Float_Word32", show x, mkThmP sFloatAsSWord32 x (RC.floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN - ++ [("reinterp_Double_Word64", show x, mkThmP sDoubleAsSWord64 x (RC.doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN + ++ [("reinterp_Float_Word32", show x, mkThmP sFloatAsSWord32 x (floatToWord x)) | x <- fs, not (isNaN x)] -- Not unique for NaN + ++ [("reinterp_Double_Word64", show x, mkThmP sDoubleAsSWord64 x (doubleToWord x)) | x <- ds, not (isNaN x)] -- Not unique for NaN m f = f sRNE diff --git a/SBVTestSuite/TestSuite/Char/Char.hs b/SBVTestSuite/TestSuite/Char/Char.hs --- a/SBVTestSuite/TestSuite/Char/Char.hs +++ b/SBVTestSuite/TestSuite/Char/Char.hs @@ -108,4 +108,5 @@ c <- sChar "c" constrain $ L.length (cf4 x c) .== 1 +{-# ANN module ("HLint: ignore Use ." :: String) #-} {-# ANN module ("HLint: ignore Redundant ^." :: String) #-} diff --git a/SBVTestSuite/TestSuite/Optimization/Floats.hs b/SBVTestSuite/TestSuite/Optimization/Floats.hs --- a/SBVTestSuite/TestSuite/Optimization/Floats.hs +++ b/SBVTestSuite/TestSuite/Optimization/Floats.hs @@ -21,16 +21,16 @@ tests :: TestTree tests = testGroup "Optimization.Floats" - [ goldenVsStringShow "optFloat1a" $ optimizeWith z3{printBase=16} Lexicographic (floatMinMax (minimize "min-x") True) - , goldenVsStringShow "optFloat1b" $ optimizeWith z3{printBase=16} Lexicographic (floatMinMax (minimize "min-x") False) - , goldenVsStringShow "optFloat1c" $ optimizeWith z3{printBase=16} Lexicographic (floatMinMax (maximize "max-x") True) - , goldenVsStringShow "optFloat1d" $ optimizeWith z3{printBase=16} Lexicographic (floatMinMax (maximize "max-y") False) - , goldenVsStringShow "optFloat2a" $ optimizeWith z3{printBase=16} Lexicographic (doubleMinMax (minimize "min-x") True) - , goldenVsStringShow "optFloat2b" $ optimizeWith z3{printBase=16} Lexicographic (doubleMinMax (minimize "min-x") False) - , goldenVsStringShow "optFloat2c" $ optimizeWith z3{printBase=16} Lexicographic (doubleMinMax (maximize "max-x") True) - , goldenVsStringShow "optFloat2d" $ optimizeWith z3{printBase=16} Lexicographic (doubleMinMax (maximize "max-y") False) - , goldenVsStringShow "optFloat3" $ optimizeWith z3{printBase=16} Lexicographic q - , goldenVsStringShow "optFloat4" $ optimizeWith z3{printBase=16} Lexicographic r + [ goldenVsStringShow "optFloat1a" $ optimizeWith z3{crackNum=True} Lexicographic (floatMinMax (minimize "min-x") True) + , goldenVsStringShow "optFloat1b" $ optimizeWith z3{crackNum=True} Lexicographic (floatMinMax (minimize "min-x") False) + , goldenVsStringShow "optFloat1c" $ optimizeWith z3{crackNum=True} Lexicographic (floatMinMax (maximize "max-x") True) + , goldenVsStringShow "optFloat1d" $ optimizeWith z3{crackNum=True} Lexicographic (floatMinMax (maximize "max-y") False) + , goldenVsStringShow "optFloat2a" $ optimizeWith z3{crackNum=True} Lexicographic (doubleMinMax (minimize "min-x") True) + , goldenVsStringShow "optFloat2b" $ optimizeWith z3{crackNum=True} Lexicographic (doubleMinMax (minimize "min-x") False) + , goldenVsStringShow "optFloat2c" $ optimizeWith z3{crackNum=True} Lexicographic (doubleMinMax (maximize "max-x") True) + , goldenVsStringShow "optFloat2d" $ optimizeWith z3{crackNum=True} Lexicographic (doubleMinMax (maximize "max-y") False) + , goldenVsStringShow "optFloat3" $ optimizeWith z3{crackNum=True} Lexicographic q + , goldenVsStringShow "optFloat4" $ optimizeWith z3{crackNum=True} Lexicographic r ] floatMinMax :: (SFloat -> Symbolic ()) -> Bool -> Goal diff --git a/SBVTestSuite/TestSuite/Queries/FreshVars.hs b/SBVTestSuite/TestSuite/Queries/FreshVars.hs --- a/SBVTestSuite/TestSuite/Queries/FreshVars.hs +++ b/SBVTestSuite/TestSuite/Queries/FreshVars.hs @@ -64,6 +64,8 @@ vReal :: SReal <- freshVar_ vInteger :: SInteger <- freshVar "vInteger" vBinOp :: SBinOp <- freshVar "vBinOp" + vQuad :: SFPQuad <- freshVar "vQuad" + wQuad :: SFPQuad <- freshVar "wQuad" constrain vBool constrain $ vWord8 .== 1 @@ -80,6 +82,10 @@ constrain $ vInteger .== 12 constrain $ vBinOp .== sPlus + constrain $ vQuad .== wQuad + constrain $ sNot $ vQuad `fpIsEqualObject` wQuad + constrain $ fpIsPositive vQuad + vSArray :: SArray Integer Integer <- freshArray "vSArray" Nothing vFArray :: SFunArray Bool Char <- freshArray "vFArray" Nothing vi1 <- freshVar "i1" @@ -135,6 +141,8 @@ vList2Val <- getValue vList2 vList3Val <- getValue vList3 vList4Val <- getValue vList4 + vQuadVal <- getValue vQuad + wQuadVal <- getValue wQuad mkSMTResult [ a |-> aVal , vBool |-> vBoolVal @@ -160,5 +168,7 @@ , vList2 |-> vList2Val , vList3 |-> vList3Val , vList4 |-> vList4Val + , vQuad |-> vQuadVal + , wQuad |-> wQuadVal ] _ -> error "didn't expect non-Sat here!" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 8.10 +Version : 8.11 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT @@ -21,19 +21,12 @@ Data-Files : SBVTestSuite/GoldFiles/*.gold Extra-Source-Files : INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With : GHC==8.10.2, GHC==8.8.4 +Tested-With : GHC==9.0.1, GHC==8.10.2, GHC==8.8.4 source-repository head type: git location: git://github.com/LeventErkok/sbv.git --- On build-bots, building HLint takes inordinately long and times out. So --- we use this flag to skip that build. -flag skipHLintTester - description: Do not build the HLint tester - default : False - manual : True - common common-settings default-language: Haskell2010 ghc-options : -Wall -O2 @@ -43,8 +36,8 @@ ghc-options : -Wunused-packages Library - import : common-settings - other-extensions : BangPatterns + import : common-settings + other-extensions: BangPatterns CPP ConstraintKinds DataKinds @@ -80,14 +73,15 @@ TypeSynonymInstances UndecidableInstances ViewPatterns - build-depends : crackNum - , QuickCheck, template-haskell + build-depends : QuickCheck, template-haskell , array, async, containers, deepseq, directory, filepath, time , pretty, process, mtl, random, syb, text, transformers, uniplate + , libBF Exposed-modules : Data.SBV , Data.SBV.Control , Data.SBV.Dynamic , Data.SBV.Either + , Data.SBV.Float , Data.SBV.Internals , Data.SBV.List , Data.SBV.Maybe @@ -201,6 +195,7 @@ , Data.SBV.Core.Operations , Data.SBV.Core.Floating , Data.SBV.Core.Sized + , Data.SBV.Core.SizedFloats , Data.SBV.Core.Symbolic , Data.SBV.Control.BaseIO , Data.SBV.Control.Query @@ -221,6 +216,7 @@ , Data.SBV.Provers.MathSAT , Data.SBV.Provers.Yices , Data.SBV.Provers.Z3 + , Data.SBV.Utils.CrackNum , Data.SBV.Utils.ExtractIO , Data.SBV.Utils.Numeric , Data.SBV.Utils.TDiff @@ -246,8 +242,7 @@ TemplateHaskell TupleSections TypeApplications - build-depends : filepath, crackNum - , sbv, directory, random, mtl, containers + build-depends : filepath, sbv, directory, random, mtl, containers , bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, QuickCheck hs-source-dirs : SBVTestSuite main-is : SBVTest.hs @@ -257,6 +252,7 @@ , TestSuite.Arrays.Query , TestSuite.Arrays.Caching , TestSuite.Basics.AllSat + , TestSuite.Basics.ArbFloats , TestSuite.Basics.ArithNoSolver , TestSuite.Basics.ArithSolver , TestSuite.Basics.Assert @@ -390,9 +386,6 @@ Test-Suite SBVHLint import : common-settings - if flag(skipHLintTester) - buildable: False - build-depends : base, directory, filepath, random , hlint, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck, sbv other-extensions: DataKinds @@ -432,8 +425,7 @@ TemplateHaskell TupleSections TypeApplications - build-depends : filepath, syb, crackNum, text - , sbv, directory, random, mtl, containers, time + build-depends : filepath, syb, text, sbv, directory, random, mtl, containers, time , gauge, process, deepseq, bench-show, silently hs-source-dirs : SBVBenchSuite main-is : SBVBenchmark.hs @@ -537,8 +529,7 @@ TemplateHaskell TupleSections TypeApplications - build-depends : filepath, syb, crackNum - , sbv, directory, random, mtl, containers, time + build-depends : filepath, syb, text, sbv, directory, random, mtl, containers, time , gauge, process, deepseq, silently, bench-show hs-source-dirs : SBVBenchSuite main-is : SBVBench.hs