crackNum 3.2 → 3.3

raw patch · 3 files changed

+8/−10 lines, 3 filesdep ~sbv

Dependency ranges changed: sbv

Files

• README.md +1/−3
• crackNum.cabal +3/−3
• src/CrackNum/Main.hs +4/−4

@@ -2,9 +2,7 @@  On Hackage: http://hackage.haskell.org/package/crackNum -[![Build Status](http://img.shields.io/travis/LeventErkok/crackNum.svg?label=Build)](http://travis-ci.org/LeventErkok/crackNum)--### Example: Encode a decimal numer as a single-precision IEEE754 number+### Example: Encode a decimal number as a single-precision IEEE754 number ``` $ crackNum -fsp -- -2.3e6 Satisfiable. Model:

@@ -1,6 +1,6 @@ Cabal-version      : 2.2 Name               : crackNum-Version            : 3.2+Version            : 3.3 Synopsis           : Crack various integer and floating-point data formats Description        : Crack IEEE-754 float formats and arbitrary sized words and integers, showing the layout.                      .@@ -15,7 +15,7 @@ Build-type         : Simple Extra-Source-Files : README.md, COPYRIGHT, CHANGES.md -Tested-With       : GHC==9.0.1+Tested-With       : GHC==9.6.1  source-repository head     type:       git@@ -26,7 +26,7 @@    default-language: Haskell2010    hs-source-dirs  : src    ghc-options     : -Wall -Wunused-packages-   build-depends   : base >= 4.11 && < 5, libBF, sbv >= 8.14+   build-depends   : base >= 4.11 && < 5, libBF, sbv >= 10.0                    , tasty, tasty-golden, filepath, directory, process    other-modules   : Paths_crackNum, CrackNum.TestSuite    autogen-modules : Paths_crackNum

@@ -295,7 +295,7 @@         di :: Bool -> Int -> IO SatResult         di sgn n = do bs <- bitString n                       satWith z3{crackNum=True} $ p bs-             where p :: [Bool] -> Goal+             where p :: [Bool] -> ConstraintSet                    p bs = do x <- (if sgn then sIntN else sWordN) n "DECODED"                              mapM_ constrain $ zipWith (.==) (map SBV (svBlastBE x)) (map literal bs) @@ -316,17 +316,17 @@                      DP     -> print =<< satWith z3{crackNum=True} (dDouble bs)                      FP i j -> print =<< satWith z3{crackNum=True} (dFP i j bs) -        dFloat :: [SBool] -> Goal+        dFloat :: [SBool] -> ConstraintSet         dFloat  bs = do x <- sFloat "DECODED"                         let (s, e, m) = blastSFloat x                         mapM_ constrain $ zipWith (.==) (s : e ++ m) bs -        dDouble :: [SBool] -> Goal+        dDouble :: [SBool] -> ConstraintSet         dDouble bs = do x <- sDouble "DECODED"                         let (s, e, m) = blastSDouble x                         mapM_ constrain $ zipWith (.==) (s : e ++ m) bs -        dFP :: Int -> Int -> [SBool] -> Goal+        dFP :: Int -> Int -> [SBool] -> ConstraintSet         dFP i j bs = do sx <- svNewVar (KFP i j) "DECODED"                         let bits = svBlastBE sx                         mapM_ constrain $ zipWith (.==) (map SBV bits) bs