diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,12 +1,17 @@ * Hackage: * GitHub: -* 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 , which transitively impacted the quick-check as implemented by SBV. * Generalize casts between integral-floats, using the rounding mode round-nearest-ties-to-even. diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -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 diff --git a/Data/SBV/BitVectors/Symbolic.hs b/Data/SBV/BitVectors/Symbolic.hs --- a/Data/SBV/BitVectors/Symbolic.hs +++ b/Data/SBV/BitVectors/Symbolic.hs @@ -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.) diff --git a/Data/SBV/Examples/BitPrecise/Legato.hs b/Data/SBV/Examples/BitPrecise/Legato.hs --- a/Data/SBV/Examples/BitPrecise/Legato.hs +++ b/Data/SBV/Examples/BitPrecise/Legato.hs @@ -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 diff --git a/Data/SBV/Examples/BitPrecise/PrefixSum.hs b/Data/SBV/Examples/BitPrecise/PrefixSum.hs --- a/Data/SBV/Examples/BitPrecise/PrefixSum.hs +++ b/Data/SBV/Examples/BitPrecise/PrefixSum.hs @@ -8,7 +8,7 @@ -- -- The PrefixSum algorithm over power-lists and proof of -- the Ladner-Fischer implementation. --- See +-- See -- and . ----------------------------------------------------------------------------- @@ -25,7 +25,7 @@ ---------------------------------------------------------------------- -- | A poor man's representation of powerlists and --- basic operations on them: . +-- basic operations on them: -- 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 --- or pg. 16 of . +-- or pg. 16 of lf :: (a, a -> a -> a) -> PowerList a -> PowerList a lf _ [] = error "lf: malformed (empty) powerlist" lf _ [x] = [x] diff --git a/Data/SBV/Examples/Misc/Floating.hs b/Data/SBV/Examples/Misc/Floating.hs --- a/Data/SBV/Examples/Misc/Floating.hs +++ b/Data/SBV/Examples/Misc/Floating.hs @@ -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 diff --git a/Data/SBV/Examples/Puzzles/Counts.hs b/Data/SBV/Examples/Puzzles/Counts.hs --- a/Data/SBV/Examples/Puzzles/Counts.hs +++ b/Data/SBV/Examples/Puzzles/Counts.hs @@ -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 diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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) diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -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) diff --git a/Data/SBV/Utils/TDiff.hs b/Data/SBV/Utils/TDiff.hs --- a/Data/SBV/Utils/TDiff.hs +++ b/Data/SBV/Utils/TDiff.hs @@ -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) diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -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" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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