sbv 8.10 → 8.11
raw patch · 62 files changed
+2569/−779 lines, 62 filesdep +libBFdep −crackNum
Dependencies added: libBF
Dependencies removed: crackNum
Files
- CHANGES.md +27/−1
- Data/SBV.hs +46/−3
- Data/SBV/Char.hs +8/−6
- Data/SBV/Client/BaseIO.hs +99/−7
- Data/SBV/Compilers/C.hs +3/−0
- Data/SBV/Control/Query.hs +18/−16
- Data/SBV/Control/Utils.hs +44/−34
- Data/SBV/Core/AlgReals.hs +1/−1
- Data/SBV/Core/Concrete.hs +107/−85
- Data/SBV/Core/Data.hs +25/−4
- Data/SBV/Core/Floating.hs +381/−46
- Data/SBV/Core/Kind.hs +130/−8
- Data/SBV/Core/Model.hs +134/−20
- Data/SBV/Core/Operations.hs +60/−46
- Data/SBV/Core/Sized.hs +55/−69
- Data/SBV/Core/SizedFloats.hs +343/−0
- Data/SBV/Core/Symbolic.hs +21/−32
- Data/SBV/Dynamic.hs +1/−1
- Data/SBV/Float.hs +25/−0
- Data/SBV/Internals.hs +6/−2
- Data/SBV/List.hs +1/−1
- Data/SBV/Provers/Prover.hs +1/−0
- Data/SBV/RegExp.hs +1/−1
- Data/SBV/SMT/SMT.hs +25/−3
- Data/SBV/SMT/SMTLib2.hs +46/−47
- Data/SBV/String.hs +1/−1
- Data/SBV/Tools/GenTest.hs +9/−5
- Data/SBV/Tools/Overflow.hs +5/−4
- Data/SBV/Tools/Polynomial.hs +2/−1
- Data/SBV/Tools/Range.hs +1/−1
- Data/SBV/Tools/WeakestPreconditions.hs +1/−1
- Data/SBV/Trans.hs +12/−3
- Data/SBV/Utils/CrackNum.hs +289/−0
- Data/SBV/Utils/Numeric.hs +44/−1
- Data/SBV/Utils/PrettyNum.hs +86/−47
- Data/SBV/Utils/SExpr.hs +37/−24
- Documentation/SBV/Examples/Misc/Floating.hs +50/−14
- Documentation/SBV/Examples/Puzzles/Garden.hs +1/−1
- Documentation/SBV/Examples/Transformers/SymbolicEval.hs +2/−1
- SBVBenchSuite/BenchSuite/Bench/Bench.hs +10/−10
- SBVTestSuite/GoldFiles/arbFp_opt_1.gold +3/−0
- SBVTestSuite/GoldFiles/freshVars.gold +104/−89
- SBVTestSuite/GoldFiles/optFloat1a.gold +19/−7
- SBVTestSuite/GoldFiles/optFloat1b.gold +16/−7
- SBVTestSuite/GoldFiles/optFloat1c.gold +19/−7
- SBVTestSuite/GoldFiles/optFloat1d.gold +16/−7
- SBVTestSuite/GoldFiles/optFloat2a.gold +19/−7
- SBVTestSuite/GoldFiles/optFloat2b.gold +16/−7
- SBVTestSuite/GoldFiles/optFloat2c.gold +19/−7
- SBVTestSuite/GoldFiles/optFloat2d.gold +17/−8
- SBVTestSuite/GoldFiles/optFloat3.gold +37/−19
- SBVTestSuite/GoldFiles/optFloat4.gold +40/−22
- SBVTestSuite/SBVDocTest.hs +1/−1
- SBVTestSuite/SBVHLint.hs +1/−0
- SBVTestSuite/SBVTest.hs +2/−0
- SBVTestSuite/TestSuite/Basics/ArbFloats.hs +40/−0
- SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +4/−6
- SBVTestSuite/TestSuite/Basics/ArithSolver.hs +4/−6
- SBVTestSuite/TestSuite/Char/Char.hs +1/−0
- SBVTestSuite/TestSuite/Optimization/Floats.hs +10/−10
- SBVTestSuite/TestSuite/Queries/FreshVars.hs +10/−0
- sbv.cabal +13/−22
CHANGES.md view
@@ -1,7 +1,33 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* 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
Data/SBV.hs view
@@ -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
Data/SBV/Char.hs view
@@ -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: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>+-- 'SChar' type only covers all unicode characters, following the specification+-- in <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>.+-- 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]
Data/SBV/Client/BaseIO.hs view
@@ -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' --
Data/SBV/Compilers/C.hs view
@@ -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
Data/SBV/Control/Query.hs view
@@ -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
Data/SBV/Control/Utils.hs view
@@ -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
Data/SBV/Core/AlgReals.hs view
@@ -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,
Data/SBV/Core/Concrete.hs view
@@ -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))
Data/SBV/Core/Data.hs view
@@ -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: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml> -- 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
Data/SBV/Core/Floating.hs view
@@ -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) #-}
Data/SBV/Core/Kind.hs view
@@ -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 <https://stackoverflow.com/questions/51900360/making-a-type-constraint-based-on-runtime-value-of-maxbound-int> 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 <https://github.com/malcolmwallace/cpphs/issues/25>.+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"
Data/SBV/Core/Model.hs view
@@ -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.
Data/SBV/Core/Operations.hs view
@@ -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
Data/SBV/Core/Sized.hs view
@@ -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@
+ Data/SBV/Core/SizedFloats.hs view
@@ -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 <https://github.com/GaloisInc/cryptol/issues/1089>+-- 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)
Data/SBV/Core/Symbolic.hs view
@@ -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 _)) = "<symbolic> :: " ++ 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--- <http://github.com/LeventErkok/sbv/issues/301>. 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+-- <http://github.com/LeventErkok/sbv/issues/301>. 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)
Data/SBV/Dynamic.hs view
@@ -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
+ Data/SBV/Float.hs view
@@ -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
Data/SBV/Internals.hs view
@@ -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
Data/SBV/List.hs view
@@ -130,7 +130,7 @@ -- Q.E.D. -- >>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1) -- Satisfiable. Model:--- s0 = [0,0,16384] :: [Word16]+-- s0 = [0,1] :: [Word16] listToListAt :: SymVal a => SList a -> SInteger -> SList a listToListAt s offset = subList s offset 1
Data/SBV/Provers/Prover.hs view
@@ -82,6 +82,7 @@ , timing = NoTiming , printBase = 10 , printRealPrec = 16+ , crackNum = False , transcript = Nothing , solver = s , smtLibVersion = smtVersion
Data/SBV/RegExp.hs view
@@ -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
Data/SBV/SMT/SMT.hs view
@@ -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
Data/SBV/SMT/SMTLib2.hs view
@@ -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 ++ ")"
Data/SBV/String.hs view
@@ -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
Data/SBV/Tools/GenTest.hs view
@@ -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!"
Data/SBV/Tools/Overflow.hs view
@@ -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
Data/SBV/Tools/Polynomial.hs view
@@ -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)
Data/SBV/Tools/Range.hs view
@@ -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) #-}
Data/SBV/Tools/WeakestPreconditions.hs view
@@ -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) #-}
Data/SBV/Trans.hs view
@@ -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
+ Data/SBV/Utils/CrackNum.hs view
@@ -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
Data/SBV/Utils/Numeric.hs view
@@ -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: -- <http://ghc.haskell.org/trac/ghc/ticket/10378>@@ -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
Data/SBV/Utils/PrettyNum.hs view
@@ -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 ++ ">"
Data/SBV/Utils/SExpr.hs view
@@ -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) #-}
Documentation/SBV/Examples/Misc/Floating.hs view
@@ -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
Documentation/SBV/Examples/Puzzles/Garden.hs view
@@ -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
Documentation/SBV/Examples/Transformers/SymbolicEval.hs view
@@ -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
SBVBenchSuite/BenchSuite/Bench/Bench.hs view
@@ -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
+ SBVTestSuite/GoldFiles/arbFp_opt_1.gold view
@@ -0,0 +1,3 @@+Optimal model:+ s0 = 65504 :: FloatingPoint 5 11+ x = 64511 :: Word16
SBVTestSuite/GoldFiles/freshVars.gold view
@@ -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!
SBVTestSuite/GoldFiles/optFloat1a.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat1b.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat1c.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat1d.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat2a.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat2b.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat2c.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat2d.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat3.gold view
@@ -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
SBVTestSuite/GoldFiles/optFloat4.gold view
@@ -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
SBVTestSuite/SBVDocTest.hs view
@@ -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
SBVTestSuite/SBVHLint.hs view
@@ -24,6 +24,7 @@ , "SBVTestSuite" , "-i", "Use otherwise" , "-i", "Parse error"+ , "--cpp-simple" ] main :: IO ()
SBVTestSuite/SBVTest.hs view
@@ -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
+ SBVTestSuite/TestSuite/Basics/ArbFloats.hs view
@@ -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)})+ ]
SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs view
@@ -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]
SBVTestSuite/TestSuite/Basics/ArithSolver.hs view
@@ -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
SBVTestSuite/TestSuite/Char/Char.hs view
@@ -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) #-}
SBVTestSuite/TestSuite/Optimization/Floats.hs view
@@ -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
SBVTestSuite/TestSuite/Queries/FreshVars.hs view
@@ -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!"
sbv.cabal view
@@ -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