sbv 5.14 → 5.15

raw patch · 12 files changed

+98/−48 lines, 12 filesdep ~crackNum

Dependency ranges changed: crackNum

Files

• CHANGES.md +7/−2
• Data/SBV.hs +2/−0
• Data/SBV/BitVectors/Symbolic.hs +2/−1
• Data/SBV/Examples/BitPrecise/Legato.hs +1/−1
• Data/SBV/Examples/BitPrecise/PrefixSum.hs +3/−3
• Data/SBV/Examples/Misc/Floating.hs +23/−23
• Data/SBV/Examples/Puzzles/Counts.hs +2/−2
• Data/SBV/Provers/Prover.hs +3/−3
• Data/SBV/SMT/SMT.hs +1/−1
• Data/SBV/Utils/TDiff.hs +50/−9
• SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
• sbv.cabal +3/−2

@@ -1,12 +1,17 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.14, 2017-01-12+* Latest Hackage released version: 5.15, 2017-01-30 +### Version 5.15, 2017-01-30++  * Bump up dependency on CrackNum >= 1.9, to get access to hexadecimal floats.+  * Improve time/tracking-print code. Thanks to Iavor Diatchki for the patch.+ ### Version 5.14, 2017-01-12      * Bump up QuickCheck dependency to >= 2.9.2 to avoid the following quick-check-    bug http://github.com/nick8325/quickcheck/issues/113, which transitively impacted+    bug <http://github.com/nick8325/quickcheck/issues/113>, which transitively impacted     the quick-check as implemented by SBV.    * Generalize casts between integral-floats, using the rounding mode round-nearest-ties-to-even.

@@ -236,6 +236,7 @@    -- * SMT Interface: Configurations and solvers   , SMTConfig(..), SMTLibVersion(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers+  , Timing(..), TimedStep(..), TimingInfo, showTDiff    -- * Symbolic computations   , Symbolic, output, SymWord(..)@@ -300,6 +301,7 @@ import Data.SBV.Tools.Optimize import Data.SBV.Tools.Polynomial import Data.SBV.Utils.Boolean+import Data.SBV.Utils.TDiff import Data.Bits import Data.Int import Data.Ratio

@@ -75,6 +75,7 @@ import Data.SBV.BitVectors.Kind import Data.SBV.BitVectors.Concrete import Data.SBV.SMT.SMTLibNames+import Data.SBV.Utils.TDiff(Timing)  import Prelude () import Prelude.Compat@@ -1053,7 +1054,7 @@ -- be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis. data SMTConfig = SMTConfig {          verbose        :: Bool           -- ^ Debug mode-       , timing         :: Bool           -- ^ Print timing information on how long different phases took (construction, solving, etc.)+       , timing         :: Timing         -- ^ Print timing information on how long different phases took (construction, solving, etc.)        , sBranchTimeOut :: Maybe Int      -- ^ How much time to give to the solver for each call of 'sBranch' check. (In seconds. Default: No limit.)        , timeOut        :: Maybe Int      -- ^ How much time to give to the solver. (In seconds. Default: No limit.)        , printBase      :: Int            -- ^ Print integral literals in this base (2, 10, and 16 are supported.)

@@ -286,7 +286,7 @@ --   On a decent MacBook Pro, this proof takes about 3 minutes with the 'SFunArray' memory model --   and about 30 minutes with the 'SArray' model, using yices as the SMT solver correctnessTheorem :: IO ThmResult-correctnessTheorem = proveWith yices{timing = True} $+correctnessTheorem = proveWith yices{timing = PrintTiming} $     forAll ["mem", "addrX", "x", "addrY", "y", "addrLow", "regX", "regA", "memVals", "flagC", "flagZ"]            legatoIsCorrect 

@@ -8,7 +8,7 @@ -- -- The PrefixSum algorithm over power-lists and proof of -- the Ladner-Fischer implementation.--- See <http://www.cs.utexas.edu/users/psp/powerlist.pdf>+-- See <http://dl.acm.org/citation.cfm?id=197356> -- and <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>. ----------------------------------------------------------------------------- @@ -25,7 +25,7 @@ ----------------------------------------------------------------------  -- | A poor man's representation of powerlists and--- basic operations on them: <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.+-- basic operations on them: <http://dl.acm.org/citation.cfm?id=197356> -- We merely represent power-lists by ordinary lists. type PowerList a = [a] @@ -60,7 +60,7 @@ ----------------------------------------------------------------------  -- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>--- or pg. 16 of <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.+-- or pg. 16 of <http://dl.acm.org/citation.cfm?id=197356> lf :: (a, a -> a -> a) -> PowerList a -> PowerList a lf _ []         = error "lf: malformed (empty) powerlist" lf _ [x]        = [x]

@@ -56,16 +56,16 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example:---   x =  5.5511693e-15 :: Float---   y = -2.2204438e-16 :: Float---   z = -3.1763606e-21 :: Float+--   x =  1.9259302e-34 :: Float+--   y = -1.9259117e-34 :: Float+--   z =  -1.814176e-39 :: Float -- -- Indeed, we have: ----- >>> ((5.5511693e-15) + ((-2.2204438e-16) + (-3.1763606e-21))) :: Float--- 5.3291218e-15--- >>> (((5.5511693e-15) + (-2.2204438e-16)) + (-3.1763606e-21)) :: Float--- 5.329122e-15+-- >>> ((1.9259302e-34) + ((-1.9259117e-34) + (-1.814176e-39))) :: Float+-- 3.4438e-41+-- >>> (((1.9259302e-34) + ((-1.9259117e-34))) + (-1.814176e-39)) :: Float+-- 3.4014e-41 -- -- Note the difference between two additions! assocPlusRegular :: IO ThmResult@@ -87,17 +87,17 @@ -- -- >>> nonZeroAddition -- Falsifiable. Counter-example:---   a =  5.1705105e-26 :: Float---   b = -3.8518597e-34 :: Float+--   a = 2.424457e-38 :: Float+--   b =     -1.0e-45 :: Float -- -- Indeed, we have: ----- >>> (5.1705105e-26 + (-3.8518597e-34)) == (5.1705105e-26 :: Float)+-- >>> (2.424457e-38 + (-1.0e-45)) == (2.424457e-38 :: Float) -- True -- -- But: ----- >>> -3.8518597e-34 == (0::Float)+-- >>> -1.0e-45 == (0 :: Float) -- False -- nonZeroAddition :: IO ThmResult@@ -118,13 +118,13 @@ -- -- >>> multInverse -- Falsifiable. Counter-example:---   a = 8.988465674311586e307 :: Double+--   a = 1.119056263978578e-308 :: Double -- -- Indeed, we have: ----- >>> let a = 8.988465674311586e307 :: Double+-- >>> let a = 1.119056263978578e-308 :: Double -- >>> a * (1/a)--- 1.0000000000000002+-- 0.9999999999999999 multInverse :: IO ThmResult multInverse = prove $ do a <- sDouble "a"                          constrain $ fpIsPoint a@@ -146,29 +146,29 @@ -- >>> roundingAdd -- Satisfiable. Model: --   rm = RoundTowardPositive :: RoundingMode---   x  =           1.9531249 :: Float---   y  =        6.2499996e-2 :: Float+--   x  =              -256.0 :: Float+--   y  =       4.6475088e-10 :: 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: ----- >>> (1.9531249 + 6.2499996e-2) :: Float--- 2.0156248+-- >>> (-256.0 + 4.6475088e-10) :: Float+-- -256.0 -- -- While we cannot directly see the result when the mode is 'RoundTowardPositive' in Haskell, we can use -- SBV to provide us with that result thusly: ----- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive 1.9531249 (6.2499996e-2 :: SFloat)+-- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive (-256.0) (4.6475088e-10 :: SFloat) -- Satisfiable. Model:---   s0 = 2.015625 :: Float+--   s0 = -255.99998 :: Float ----- We can see why these two resuls are indeed different. But we can see that the 'RoundTowardsPositive'+-- We can see why these two resuls are indeed different: The 'RoundTowardsPositive' -- (which rounds towards positive-infinity) produces a larger result. Indeed, if we treat these numbers -- as 'Double' values, we get: ----- >>>  (1.9531249 + 6.2499996e-2) :: Double--- 2.015624896+-- >>>  (-256.0 + 4.6475088e-10) :: Double+-- -255.99999999953525 -- -- we see that the "more precise" result is larger than what the 'Float' value is, justifying the -- larger value with 'RoundTowardPositive'. A more detailed study is beyond our current scope, so we'll

@@ -56,9 +56,9 @@ -- -- >>> counts -- Solution #1--- In this sentence, the number of occurrences of 0 is 1, of 1 is 11, of 2 is 2, of 3 is 1, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 1, of 8 is 1, of 9 is 1.--- Solution #2 -- In this sentence, the number of occurrences of 0 is 1, of 1 is 7, of 2 is 3, of 3 is 2, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 2, of 8 is 1, of 9 is 1.+-- Solution #2+-- In this sentence, the number of occurrences of 0 is 1, of 1 is 11, of 2 is 2, of 3 is 1, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 1, of 8 is 1, of 9 is 1. -- Found: 2 solution(s). counts :: IO () counts = do res <- allSat $ puzzle `fmap` mkExistVars 10

@@ -61,7 +61,7 @@  mkConfig :: SMTSolver -> SMTLibVersion -> [String] -> SMTConfig mkConfig s smtVersion tweaks = SMTConfig { verbose        = False-                                         , timing         = False+                                         , timing         = NoTiming                                          , sBranchTimeOut = Nothing                                          , timeOut        = Nothing                                          , printBase      = 10@@ -463,7 +463,7 @@         let msg = when (verbose config) . putStrLn . ("** " ++)             isTiming = timing config         msg "Starting symbolic simulation.."-        res <- timeIf isTiming "problem construction" $ runSymbolic (isSat, config) $ (if isSat then forSome_ else forAll_) predicate >>= output+        res <- timeIf isTiming ProblemConstruction $ runSymbolic (isSat, config) $ (if isSat then forSome_ else forAll_) predicate >>= output         msg $ "Generated symbolic trace:\n" ++ show res         msg "Translating to SMT-Lib.."         runProofOn converter config isSat comments res@@ -474,7 +474,7 @@             solverCaps = capabilities (solver config)         in case res of              Result ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs assertions [o@(SW KBool _)] ->-               timeIf isTiming "translation"+               timeIf isTiming Translation                 $ let skolemMap = skolemize (if isSat then is else map flipQ is)                            where flipQ (ALL, x) = (EX, x)                                  flipQ (EX, x)  = (ALL, x)

@@ -485,7 +485,7 @@       Nothing -> return ()       Just f  -> do msg $ "Saving the generated script in file: " ++ show f                     writeFile f (scriptBody script)-    contents <- timeIf isTiming nmSolver $ pipeProcess config  exec opts script cleanErrs+    contents <- timeIf isTiming (WorkByProver nmSolver) $ pipeProcess config  exec opts script cleanErrs     msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents     case contents of       Left e   -> return $ failure (lines e)

@@ -9,12 +9,42 @@ -- Runs an IO computation printing the time it took to run it ----------------------------------------------------------------------------- -module Data.SBV.Utils.TDiff(timeIf) where+module Data.SBV.Utils.TDiff+  ( timeIf+  , Timing(..)+  , TimedStep(..)+  , TimingInfo+  , showTDiff+  )+  where  import Control.DeepSeq (rnf, NFData(..)) import System.Time     (TimeDiff(..), normalizeTimeDiff, diffClockTimes, getClockTime) import Numeric         (showFFloat) +import           Data.Map (Map)+import qualified Data.Map as Map+import           Data.IORef(IORef, modifyIORef')++-- | Specify how to save timing information, if at all.+data Timing     = NoTiming | PrintTiming | SaveTiming (IORef TimingInfo)++-- | Specify what is being timed.+data TimedStep  = ProblemConstruction | Translation | WorkByProver String+                  deriving (Eq, Ord, Show)++-- | A collection of timed stepd.+type TimingInfo = Map TimedStep TimeDiff++-- | A more helpful show instance for steps+timedStepLabel :: TimedStep -> String+timedStepLabel lbl =+  case lbl of+    ProblemConstruction -> "problem construction"+    Translation         -> "translation"+    WorkByProver x      -> x++-- | Show the time difference in a user-friendly format. showTDiff :: TimeDiff -> String showTDiff itd = et   where td = normalizeTimeDiff itd@@ -26,11 +56,22 @@ -- | If selected, runs the computation @m@, and prints the time it took -- to run it. The return type should be an instance of 'NFData' to ensure -- the correct elapsed time is printed.-timeIf :: NFData a => Bool -> String -> IO a -> IO a-timeIf False _ m = m-timeIf True  w m = do start <- getClockTime-                      r <- m-                      end <- rnf r `seq` getClockTime-                      let elapsed = diffClockTimes end start-                      putStrLn $ "** Elapsed " ++ w ++ " time:" ++ showTDiff elapsed-                      return r+timeIf :: NFData a => Timing -> TimedStep -> IO a -> IO a+timeIf how what m =+  case how of+    NoTiming -> m+    PrintTiming ->+      do (elapsed,a) <- doTime m+         putStrLn $ "** Elapsed " ++ timedStepLabel what ++ " time:" ++ showTDiff elapsed+         return a+    SaveTiming here ->+      do (elapsed,a) <- doTime m+         modifyIORef' here (Map.insert what elapsed)+         return a++doTime :: NFData a => IO a -> IO (TimeDiff,a)+doTime m = do start <- getClockTime+              r <- m+              end <- rnf r `seq` getClockTime+              let elapsed = diffClockTimes end start+              elapsed `seq` return (elapsed, r)

@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Thu Jan 12 09:52:42 PST 2017"+buildTime = "Mon Jan 30 16:59:33 PST 2017"

@@ -1,5 +1,5 @@ Name:          sbv-Version:       5.14+Version:       5.15 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@@ -49,8 +49,9 @@                   , base-compat >= 0.6                   , ghc                   , QuickCheck >= 2.9.2+                  , crackNum >= 1.9                   , array, async, containers, deepseq, directory, filepath, old-time-                  , pretty, process, mtl, random, syb, data-binary-ieee754, crackNum+                  , pretty, process, mtl, random, syb, data-binary-ieee754   Exposed-modules : Data.SBV                   , Data.SBV.Bridge.Boolector                   , Data.SBV.Bridge.CVC4