packages feed

sbv 7.11 → 7.12

raw patch · 33 files changed

+217/−135 lines, 33 files

Files

CHANGES.md view
@@ -1,7 +1,19 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 7.11, 2018-09-20+* Latest Hackage released version: 7.12, 2018-09-23++### Version 7.12, 2018-09-23+  +  * Modifications to make SBV compile with GHC 8.6.1. (SBV should+    now compile fine with all versions of GHC since 8.0.1; and+    possibly earlier. Please report if you are using a version+    in this range and have issues.)++  * Improve the BoundedMutex example to show a non-fair trace.+    See "Documentation/SBV/Examples/Lists/BoundedMutex.hs".++  * Improve Haddock documentation links throughout.  ### Version 7.11, 2018-09-20
Data/SBV.hs view
@@ -48,8 +48,10 @@ -- --   * 'SDouble': IEEE-754 double-precision floating point values -----   * 'SString', 'RegExp': Strings and regular expressions+--   * 'SChar', 'SString', 'RegExp': Characters, strings and regular expressions --+--   * 'SList': Symbolic lists (which can be nested)+-- --   * 'SArray', 'SFunArray': Flat arrays of symbolic values. -- --   * Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.@@ -506,15 +508,15 @@  >>> let safeSub x y = ite (x .>= y) (sub x y) 0 -Clearly, 'safeSub' must be safe. And indeed, SBV can prove that:+Clearly, @safeSub@ must be safe. And indeed, SBV can prove that:  >>> safe (safeSub :: SInt8 -> SInt8 -> SInt8) [sub: x >= y must hold!: No violations detected] -Note how we used 'sub' and 'safeSub' polymorphically. We only need to monomorphise our types when a proof+Note how we used @sub@ and @safeSub@ polymorphically. We only need to monomorphise our types when a proof attempt is done, as we did in the 'safe' calls. -If required, the user can pass a 'CallStack' through the first argument to 'sAssert', which will be used+If required, the user can pass a @CallStack@ through the first argument to 'sAssert', which will be used by SBV to print a diagnostic info to pinpoint the failure.  Also see "Documentation.SBV.Examples.Misc.NoDiv0" for the classic div-by-zero example.@@ -522,7 +524,7 @@   {- $optiIntro-  SBV can optimize metric functions, i.e., those that generate both bounded 'SIntN', 'SWordN', and unbounded 'SInteger'+  SBV can optimize metric functions, i.e., those that generate both bounded @SIntN@, @SWordN@, and unbounded 'SInteger'   types, along with those produce 'SReal's. That is, it can find models satisfying all the constraints while minimizing   or maximizing user given metrics. Currently, optimization requires the use of the z3 SMT solver as the backend,   and a good review of these features is given@@ -764,14 +766,14 @@     holds. In other words, the constraint says that we only care about     the input space that satisfies the constraint. -  * In a 'quickCheck' call: The constraint acts as a filter for 'quickCheck';+  * In a @quickCheck@ call: The constraint acts as a filter for @quickCheck@;     if the constraint does not hold, then the input value is considered to be irrelevant     and is skipped. Note that this is similar to 'prove', but is stronger: We do not     accept a test case to be valid just because the constraints fail on them, although     semantically the implication does hold. We simply skip that test case as a /bad/     test vector. -  * In a 'genTest' call: Similar to 'quickCheck' and 'prove': If a constraint+  * In a 'Data.SBV.Tools.GenTest.genTest' call: Similar to @quickCheck@ and 'prove': If a constraint     does not hold, the input value is ignored and is not included in the test     set. -}@@ -796,8 +798,8 @@ trivial. Hence, this predicate is provable, but is not satisfiable. To make sure the given constraints are not vacuous, the functions 'isVacuous' (and 'isVacuousWith') can be used. -Also note that this semantics imply that test case generation ('genTest') and quick-check-can take arbitrarily long in the presence of constraints, if the random input values generated+Also note that this semantics imply that test case generation ('Data.SBV.Tools.GenTest.genTest') and+quick-check can take arbitrarily long in the presence of constraints, if the random input values generated rarely satisfy the constraints. (As an extreme case, consider @'constrain' 'false'@.) -} @@ -852,7 +854,7 @@ -}  {- $unsatCores-Named constraints are useful when used in conjunction with 'getUnsatCore' function+Named constraints are useful when used in conjunction with 'Data.SBV.Control.getUnsatCore' function where the backend solver can be queried to obtain an unsat core in case the constraints are unsatisfiable. See 'Data.SBV.Control.getUnsatCore' for details and "Documentation.SBV.Examples.Queries.UnsatCore" for an example use case. -}@@ -867,13 +869,13 @@  (Note that you'll also need to use the language pragmas @DeriveDataTypeable@, @DeriveAnyClass@, and import @Data.Generics@ for the above to work.) -This is all it takes to introduce 'B' as an uninterpreted sort in SBV, which makes the type @SBV B@ automagically become available as the type-of symbolic values that ranges over 'B' values. Note that the @()@ argument is important to distinguish it from enumerations, which will be+This is all it takes to introduce @B@ as an uninterpreted sort in SBV, which makes the type @SBV B@ automagically become available as the type+of symbolic values that ranges over @B@ values. Note that the @()@ argument is important to distinguish it from enumerations, which will be translated to proper SMT data-types.   Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by-the 'Uninterpreted' class.+the 'Data.SBV.Core.Model.Uninterpreted' class. -}  {- $enumerations@@ -983,7 +985,7 @@ {- $observeInternal  The 'observe' command can be used to trace values of arbitrary expressions during a 'sat', 'prove', or perhaps more-importantly, in a 'quickCheck' call. This is useful for, for instance, recording expected/obtained expressions as a symbolic program is executing.+importantly, in a @quickCheck@ call. This is useful for, for instance, recording expected/obtained expressions as a symbolic program is executing.  >>> :{ prove $ do a1 <- free "i1"
Data/SBV/Compilers/CodeGen.hs view
@@ -9,6 +9,7 @@ -- Code generation utilities ----------------------------------------------------------------------------- +{-# LANGUAGE CPP                        #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} @@ -55,6 +56,10 @@ import Data.SBV.Core.Data import Data.SBV.Core.Symbolic (svToSymSW, svMkSymVar, outputSVal) +#if MIN_VERSION_base(4,11,0)+import Control.Monad.Fail as Fail+#endif+ -- | Abstract over code generation for different languages class CgTarget a where   targetName :: a -> String@@ -68,7 +73,7 @@         , cgDriverVals         :: [Integer]          -- ^ Values to use for the driver program generated, useful for generating non-random drivers.         , cgGenDriver          :: Bool               -- ^ If 'True', will generate a driver program         , cgGenMakefile        :: Bool               -- ^ If 'True', will generate a makefile-        , cgIgnoreAsserts      :: Bool               -- ^ If 'True', will ignore 'sAssert' calls+        , cgIgnoreAsserts      :: Bool               -- ^ If 'True', will ignore 'Data.SBV.sAssert' calls         , cgOverwriteGenerated :: Bool               -- ^ If 'True', will overwrite the generated files without prompting.         } @@ -115,7 +120,11 @@ -- reference parameters (for returning composite values in languages such as C), -- and return values. newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)-                   deriving (Applicative, Functor, Monad, MonadIO, MonadState CgState)+                   deriving ( Applicative, Functor, Monad, MonadIO, MonadState CgState+#if MIN_VERSION_base(4,11,0)+                            , Fail.MonadFail+#endif+                            )  -- | Reach into symbolic monad from code-generation cgSym :: Symbolic a -> SBVCodeGen a@@ -164,7 +173,7 @@ cgSRealType rt = modify' (\s -> s {cgFinalConfig = (cgFinalConfig s) { cgReal = Just rt }})  -- | Should we generate a driver program? Default: 'True'. When a library is generated, it will have--- a driver if any of the contituent functions has a driver. (See 'compileToCLib'.)+-- a driver if any of the contituent functions has a driver. (See 'Data.SBV.Tools.CodeGen.compileToCLib'.) cgGenerateDriver :: Bool -> SBVCodeGen () cgGenerateDriver b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenDriver = b } }) @@ -176,7 +185,7 @@ cgSetDriverValues :: [Integer] -> SBVCodeGen () cgSetDriverValues vs = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } }) --- | Ignore assertions (those generated by 'sAssert' calls) in the generated C code+-- | Ignore assertions (those generated by 'Data.SBV.sAssert' calls) in the generated C code cgIgnoreSAssert :: Bool -> SBVCodeGen () cgIgnoreSAssert b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgIgnoreAsserts = b } }) @@ -364,7 +373,7 @@                                      unless overWrite $ putStrLn $ "Generating: " ++ show fn ++ ".."                                      writeFile fn (render' (vcat ds)) --- | An alternative to Pretty's 'render', which might have "leading" white-space in empty lines. This version+-- | An alternative to Pretty's @render@, which might have "leading" white-space in empty lines. This version -- eliminates such whitespace. render' :: Doc -> String render' = unlines . map clean . lines . P.render
Data/SBV/Control.hs view
@@ -131,8 +131,8 @@                                                 return $ Just (xv2, yv2) @ -Note the type of 'test', it returns an optional pair of integers in the 'Symbolic' monad. We turn-it into an IO value with the 'runSMT' function: (There's also 'runSMTWith' that uses a user specified+Note the type of @test@: it returns an optional pair of integers in the 'Symbolic' monad. We turn+it into an IO value with the 'Data.SBV.Control.runSMT' function: (There's also 'Data.SBV.Control.runSMTWith' that uses a user specified solver instead of the default.)  @@@ -153,7 +153,7 @@  For other examples see: -  - "Documentation.SBV.Examples.Queries.AllSat": Simulating SBV's 'allSat' using queries.+  - "Documentation.SBV.Examples.Queries.AllSat": Simulating SBV's 'Data.SBV.allSat' using queries.   - "Documentation.SBV.Examples.Queries.CaseSplit": Performing a case-split during a query.   - "Documentation.SBV.Examples.Queries.Enums": Using enumerations in queries.   - "Documentation.SBV.Examples.Queries.FourFours": Solution to a fun arithmetic puzzle, coded using queries.
Data/SBV/Control/Query.hs view
@@ -375,14 +375,14 @@                         simplify (EApp xs)                  = EApp (map simplify xs)                         simplify e                          = e --- | Check for satisfiability, under the given conditions. Similar to 'checkSat' except it allows making+-- | Check for satisfiability, under the given conditions. Similar to 'Data.SBV.Control.checkSat' except it allows making -- further assumptions as captured by the first argument of booleans. (Also see 'checkSatAssumingWithUnsatisfiableSet' -- for a variant that returns the subset of the given assumptions that led to the 'Unsat' conclusion.) checkSatAssuming :: [SBool] -> Query CheckSatResult checkSatAssuming sBools = fst <$> checkSatAssumingHelper False sBools  -- | Check for satisfiability, under the given conditions. Returns the unsatisfiable--- set of assumptions. Similar to 'checkSat' except it allows making further assumptions+-- set of assumptions. Similar to 'Data.SBV.Control.checkSat' except it allows making further assumptions -- as captured by the first argument of booleans. If the result is 'Unsat', the user will -- also receive a subset of the given assumptions that led to the 'Unsat' conclusion. Note -- that while this set will be a subset of the inputs, it is not necessarily guaranteed to be minimal.@@ -397,7 +397,7 @@ -- for this call to not error out! -- -- Usage note: 'getUnsatCore' is usually easier to use than 'checkSatAssumingWithUnsatisfiableSet', as it--- allows the use of named assertions, as obtained by 'namedAssert'. If 'getUnsatCore'+-- allows the use of named assertions, as obtained by 'namedConstraint'. If 'getUnsatCore' -- fills your needs, you should definitely prefer it over 'checkSatAssumingWithUnsatisfiableSet'. checkSatAssumingWithUnsatisfiableSet :: [SBool] -> Query (CheckSatResult, Maybe [SBool]) checkSatAssumingWithUnsatisfiableSet = checkSatAssumingHelper True@@ -554,9 +554,10 @@                                               return $ Just (n, res)  -- | Reset the solver, by forgetting all the assertions. However, bindings are kept as is,--- as opposed to 'reset'. Use this variant to clean-up the solver state while leaving the bindings--- intact. Pops all assertion levels. Declarations and definitions resulting from the 'setLogic'--- command are unaffected. Note that SBV implicitly uses global-declarations, so bindings will remain intact.+-- as opposed to a full reset of the solver. Use this variant to clean-up the solver+-- state while leaving the bindings intact. Pops all assertion levels. Declarations and+-- definitions resulting from the 'Data.SBV.setLogic' command are unaffected. Note that SBV+-- implicitly uses global-declarations, so bindings will remain intact. resetAssertions :: Query () resetAssertions = do send True "(reset-assertions)"                      modifyQueryState $ \s -> s{queryAssertionStackDepth = 0}
Data/SBV/Control/Types.hs view
@@ -27,7 +27,7 @@  import Control.DeepSeq (NFData(..)) --- | Result of a 'checkSat' or 'checkSatAssuming' call.+-- | Result of a 'Data.SBV.Control.checkSat' or 'Data.SBV.Control.checkSatAssuming' call. data CheckSatResult = Sat           -- ^ Satisfiable: A model is available, which can be queried with 'Data.SBV.Control.getValue'.                     | Unsat         -- ^ Unsatisfiable: No model is available. Unsat cores might be obtained via 'Data.SBV.Control.getUnsatCore'.                     | Unk           -- ^ Unknown: Use 'Data.SBV.Control.getUnknownReason' to obtain an explanation why this might be the case.@@ -161,7 +161,7 @@         logic l          = "(set-logic " ++ show l ++ ")"  -- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the--- user can override this choice using a call to 'setLogic' This is especially handy if one is experimenting with custom+-- user can override this choice using a call to 'Data.SBV.setLogic' This is especially handy if one is experimenting with custom -- logics that might be supported on new solvers. See <http://smtlib.cs.uiowa.edu/logics.shtml> for the official list. data Logic   = AUFLIA             -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.
Data/SBV/Control/Utils.hs view
@@ -132,7 +132,7 @@ getSBVPgm = do State{spgm} <- get                io $ readIORef spgm --- | Get the assertions put in via 'sAssert'+-- | Get the assertions put in via 'Data.SBV.sAssert' getSBVAssertions :: Query [(String, Maybe CallStack, SW)] getSBVAssertions = do State{rAsserts} <- get                       io $ reverse <$> readIORef rAsserts@@ -198,7 +198,7 @@   where k = kindOf (undefined :: a)  -- | Create a fresh variable in query mode. You should prefer--- creating input variables using 'sBool', 'sInt32', etc., which act+-- creating input variables using 'Data.SBV.sBool', 'Data.SBV.sInt32', etc., which act -- as primary inputs to the model and can be existential or universal. -- Use 'freshVar' only in query mode for anonymous temporary variables. -- Such variables are always existential. Note that 'freshVar' should hardly be@@ -557,7 +557,7 @@                           return $ preQs ++ trackers ++ postQs --- | Get observables, i.e., those explicitly labeled by the user with a call to 'observe'.+-- | Get observables, i.e., those explicitly labeled by the user with a call to 'Data.SBV.observe'. getObservables :: Query [(String, SW)] getObservables = do State{rObservables} <- get @@ -664,8 +664,8 @@                                         Just d  -> do constrain d                                                       go (cnt+1) resultsSoFar --- | Retrieve the set of unsatisfiable assumptions, following a call to 'checkSatAssumingWithUnsatisfiableSet'. Note that--- this function isn't exported to the user, but rather used internally. The user simple calls 'checkSatAssumingWithUnsatisfiableSet'.+-- | Retrieve the set of unsatisfiable assumptions, following a call to 'Data.SBV.Control.checkSatAssumingWithUnsatisfiableSet'. Note that+-- this function isn't exported to the user, but rather used internally. The user simple calls 'Data.SBV.Control.checkSatAssumingWithUnsatisfiableSet'. getUnsatAssumptions :: [String] -> [(String, a)] -> Query [a] getUnsatAssumptions originals proxyMap = do         let cmd = "(get-unsat-assumptions)"
Data/SBV/Core/Data.hs view
@@ -91,7 +91,7 @@ extendPathCondition :: State -> (SBool -> SBool) -> State extendPathCondition st f = extendSValPathCondition st (unSBV . f . SBV) --- | The "Symbolic" value. The parameter 'a' is phantom, but is+-- | The "Symbolic" value. The parameter @a@ is phantom, but is -- extremely important in keeping the user interface strongly typed. newtype SBV a = SBV { unSBV :: SVal }               deriving (Generic, NFData)@@ -210,7 +210,7 @@ sRoundNearestTiesToAway :: SRoundingMode sRoundNearestTiesToAway = literal RoundNearestTiesToAway --- | Symbolic variant of 'RoundNearestPositive'+-- | Symbolic variant of 'RoundTowardPositive' sRoundTowardPositive :: SRoundingMode sRoundTowardPositive = literal RoundTowardPositive @@ -298,7 +298,7 @@    -- | Set a solver time-out value, in milli-seconds. This function    -- essentially translates to the SMTLib call @(set-info :timeout val)@,    -- and your backend solver may or may not support it! The amount given-   -- is in milliseconds. Also see the function 'timeOut' for finer level+   -- is in milliseconds. Also see the function 'Data.SBV.Control.timeOut' for finer level    -- control of time-outs, directly from SBV.    setTimeOut :: Integer -> m () @@ -350,8 +350,8 @@ ------------------------------------------------------------------------------- -- | A 'SymWord' is a potential symbolic bitvector that can be created instances of -- to be fed to a symbolic program. Note that these methods are typically not needed--- in casual uses with 'prove', 'sat', 'allSat' etc, as default instances automatically--- provide the necessary bits.+-- in casual uses with 'Data.SBV.prove', 'Data.SBV.sat', 'Data.SBV.allSat' etc, as+-- default instances automatically provide the necessary bits. class (HasKind a, Ord a, Typeable a) => SymWord a where   -- | Create a user named input (universal)   forall :: String -> Symbolic (SBV a)@@ -453,7 +453,7 @@ -- --    * 'SArray' produces SMTLib arrays, and requires a solver that understands the --      array theory. 'SFunArray' is internally handled, and thus can be used with---      any solver. (Note that all solvers except 'abc' support arrays, so this isn't+--      any solver. (Note that all solvers except 'Data.SBV.abc' support arrays, so this isn't --      a big decision factor.) -- --    * For both arrays, if a default value is supplied, then reading from uninitialized
Data/SBV/Core/Kind.hs view
@@ -45,7 +45,7 @@  -- | The interesting about the show instance is that it can tell apart two kinds nicely; since it conveniently -- ignores the enumeration constructors. Also, when we construct a 'KUserSort', we make sure we don't use any of--- the reserved names; see 'constructUIKind' for details.+-- the reserved names; see 'constructUKind' for details. instance Show Kind where   show KBool              = "SBool"   show (KBounded False n) = "SWord" ++ show n@@ -122,7 +122,7 @@ -- | A class for capturing values that have a sign and a size (finite or infinite) -- minimal complete definition: kindOf, unless you can take advantage of the default -- signature: This class can be automatically derived for data-types that have--- a 'Data' instance; this is useful for creating uninterpreted sorts. So, in+-- a 'G.Data' instance; this is useful for creating uninterpreted sorts. So, in -- reality, end users should almost never need to define any methods. class HasKind a where   kindOf          :: a -> Kind
Data/SBV/Core/Model.hs view
@@ -605,7 +605,7 @@ instance SIntegral Integer  -- | Finite bit-length symbolic values. Essentially the same as 'SIntegral', but further leaves out 'Integer'. Loosely--- based on Haskell's 'FiniteBits' class, but with more methods defined and structured differently to fit into the+-- based on Haskell's @FiniteBits@ class, but with more methods defined and structured differently to fit into the -- symbolic world view. Minimal complete definition: 'sFiniteBitSize'. class (SymWord a, Num a, Bits a) => SFiniteBits a where     -- | Bit size.@@ -760,42 +760,42 @@                     registerKind st KUnbounded                     newExpr st KBool (SBVApp (PseudoBoolean o) xsw) --- | 'true' if at most `k` of the input arguments are 'true'+-- | 'true' if at most @k@ of the input arguments are 'true' pbAtMost :: [SBool] -> Int -> SBool pbAtMost xs k  | k < 0             = error $ "SBV.pbAtMost: Non-negative value required, received: " ++ show k  | all isConcrete xs = literal $ sum (map (pbToInteger "pbAtMost" 1) xs) <= fromIntegral k  | True              = liftPB "pbAtMost" (PB_AtMost k) xs --- | 'true' if at least `k` of the input arguments are 'true'+-- | 'true' if at least @k@ of the input arguments are 'true' pbAtLeast :: [SBool] -> Int -> SBool pbAtLeast xs k  | k < 0             = error $ "SBV.pbAtLeast: Non-negative value required, received: " ++ show k  | all isConcrete xs = literal $ sum (map (pbToInteger "pbAtLeast" 1) xs) >= fromIntegral k  | True              = liftPB "pbAtLeast" (PB_AtLeast k) xs --- | 'true' if exactly `k` of the input arguments are 'true'+-- | 'true' if exactly @k@ of the input arguments are 'true' pbExactly :: [SBool] -> Int -> SBool pbExactly xs k  | k < 0             = error $ "SBV.pbExactly: Non-negative value required, received: " ++ show k  | all isConcrete xs = literal $ sum (map (pbToInteger "pbExactly" 1) xs) == fromIntegral k  | True              = liftPB "pbExactly" (PB_Exactly k) xs --- | 'true' if the sum of coefficients for 'true' elements is at most 'k'. Generalizes 'pbAtMost'.+-- | 'true' if the sum of coefficients for 'true' elements is at most @k@. Generalizes 'pbAtMost'. pbLe :: [(Int, SBool)] -> Int -> SBool pbLe xs k  | k < 0                       = error $ "SBV.pbLe: Non-negative value required, received: " ++ show k  | all isConcrete (map snd xs) = literal $ sum [pbToInteger "pbLe" c b | (c, b) <- xs] <= fromIntegral k  | True                        = liftPB "pbLe" (PB_Le (map fst xs) k) (map snd xs) --- | 'true' if the sum of coefficients for 'true' elements is at least 'k'. Generalizes 'pbAtLeast'.+-- | 'true' if the sum of coefficients for 'true' elements is at least @k@. Generalizes 'pbAtLeast'. pbGe :: [(Int, SBool)] -> Int -> SBool pbGe xs k  | k < 0                       = error $ "SBV.pbGe: Non-negative value required, received: " ++ show k  | all isConcrete (map snd xs) = literal $ sum [pbToInteger "pbGe" c b | (c, b) <- xs] >= fromIntegral k  | True                        = liftPB "pbGe" (PB_Ge (map fst xs) k) (map snd xs) --- | 'true' if the sum of coefficients for 'true' elements is exactly least 'k'. Useful for coding+-- | 'true' if the sum of coefficients for 'true' elements is exactly least @k@. Useful for coding -- /exactly K-of-N/ constraints, and in particular mutex constraints. pbEq :: [(Int, SBool)] -> Int -> SBool pbEq xs k@@ -1216,7 +1216,7 @@   sQuotRem = liftQRem   sDivMod  = liftDMod --- | Lift 'QRem' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which+-- | Lift 'quotRem' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which -- holds even when @x@ is @0@ itself. liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a) liftQRem x y@@ -1239,7 +1239,7 @@                                    mkSymOp o st sgnsz sw1 sw2         z = genLiteral (kindOf x) (0::Integer) --- | Lift 'DMod' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which+-- | Lift 'divMod' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which -- holds even when @x@ is @0@ itself. Essentially, this is conversion from quotRem -- (truncate to 0) to divMod (truncate towards negative infinity) liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)@@ -1295,9 +1295,9 @@ -- with a default value, simulating array/list indexing. It's an n-way generalization -- of the 'ite' function. ----- Minimal complete definition: None, if the type is instance of 'Generic'. Otherwise+-- Minimal complete definition: None, if the type is instance of @Generic@. Otherwise -- 'symbolicMerge'. Note that most types subject to merging are likely to be--- trivial instances of 'Generic'.+-- trivial instances of @Generic@. class Mergeable a where    -- | Merge two values based on the condition. The first argument states    -- whether we force the then-and-else branches before the merging, at the@@ -1870,7 +1870,7 @@             noQC us         = error $ "Cannot quick-check in the presence of uninterpreted constants: " ++ intercalate ", " us --- | Quick check an SBV property. Note that a regular 'quickCheck' call will work just as+-- | Quick check an SBV property. Note that a regular @quickCheck@ call will work just as -- well. Use this variant if you want to receive the boolean result. sbvQuickCheck :: Symbolic SBool -> IO Bool sbvQuickCheck prop = QC.isSuccess `fmap` QC.quickCheckResult prop
Data/SBV/Core/Operations.hs view
@@ -498,20 +498,20 @@                                      where k = ite (y .== 0) x (x+1)                                  When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd-                                like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else'-                                branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value-                                is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound.+                                like to share @k@, which would evaluate (correctly) to @x@ under the given assumption. When we backtrack and evaluate the 'else'+                                branch of the first ite, we'd see @k@ is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value+                                is @x@, which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound.                                  A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is,-                                in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this+                                in the above example, we should record that the value of @k@ was cached under the assumption that @y@ is 0. While sound, this                                 approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself.                                 To wit, consider:                                     foo x y = ite (y .== 0) k (k+1)                                      where k = x+5 -                                If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to-                                re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing,+                                If we tracked the assumptions, we would recompute @k@ twice, since the branch assumptions would differ. Clearly, there is no need to+                                re-compute @k@ in this case since its value is independent of @y@. Note that the whole SBV performance story is based on agressive sharing,                                 and losing that would have other significant ramifications.                                  The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather
Data/SBV/Core/Symbolic.hs view
@@ -88,6 +88,10 @@  import Data.SBV.Control.Types +#if MIN_VERSION_base(4,11,0)+import Control.Monad.Fail as Fail+#endif+ -- | A symbolic node id newtype NodeId = NodeId Int deriving (Eq, Ord) @@ -234,7 +238,7 @@   show Overflow_SMul_UDFL = "bvsmul_noudfl"   show Overflow_UMul_OVFL = "bvumul_noovfl" --- | String operations. Note that we do not define `StrAt` as it translates to `StrSubStr` trivially.+-- | String operations. Note that we do not define @StrAt@ as it translates to 'StrSubstr' trivially. data StrOp = StrConcat       -- ^ Concatenation of one or more strings            | StrLen          -- ^ String length            | StrUnit         -- ^ Unit string@@ -250,7 +254,7 @@            deriving (Eq, Ord)  -- | Regular expressions. Note that regular expressions themselves are--- concrete, but the `match` function from the 'RegExpMatchable' class+-- concrete, but the 'Data.SBV.RegExp.match' function from the 'Data.SBV.RegExp.RegExpMatchable' class -- can check membership against a symbolic string/character. Also, we -- are preferring a datatype approach here, as opposed to coming up with -- some string-representation; there are way too many alternatives@@ -317,7 +321,7 @@   show (Union [x])       = show x   show (Union xs)        = "(re.union " ++ unwords (map show xs) ++ ")" --- | Show instance for `StrOp`. Note that the mapping here is+-- | Show instance for @StrOp@. Note that the mapping here is -- important to match the SMTLib equivalents, see here: <http://rise4fun.com/z3/tutorialcontent/sequences> instance Show StrOp where   show StrConcat   = "str.++"@@ -346,7 +350,7 @@            | SeqReplace   -- ^ See StrReplace   deriving (Eq, Ord) --- | Show instance for `SeqOp`. Again, mapping is important.+-- | Show instance for @SeqOp@. Again, mapping is important. instance Show SeqOp where   show SeqConcat   = "seq.++"   show SeqLen      = "seq.len"@@ -913,9 +917,9 @@ -- the new kind might introduce a constraint that effects the logic. For -- instance, if we're seeing 'Double' for the first time and using a BV -- logic, then things would fall apart. But this should be rare, and hopefully--- the 'success' checking mechanism will catch the rare cases where this+-- the success-response checking mechanism will catch the rare cases where this -- is an issue. In either case, the user can always arrange for the right--- logic by calling 'setLogic' appropriately, so it seems safe to just+-- logic by calling 'Data.SBV.setLogic' appropriately, so it seems safe to just -- allow for this. registerKind :: State -> Kind -> IO () registerKind st k@@ -999,13 +1003,17 @@ -- state of the computation, layered on top of IO for creating unique -- references to hold onto intermediate results. newtype Symbolic a = Symbolic (ReaderT State IO a)-                   deriving (Applicative, Functor, Monad, MonadIO, MonadReader State)+                   deriving ( Applicative, Functor, Monad, MonadIO, MonadReader State+#if MIN_VERSION_base(4,11,0)+                            , Fail.MonadFail+#endif+                            )  -- | Create a symbolic value, based on the quantifier we have. If an -- explicit quantifier is given, we just use that. If not, then we -- pick the quantifier appropriately based on the run-mode. -- @randomCW@ is used for generating random values for this variable--- when used for 'quickCheck' or 'genTest' purposes.+-- when used for @quickCheck@ or 'Data.SBV.Tools.GenTest.genTest' purposes. svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal svMkSymVar = svMkSymVarGen False @@ -1033,7 +1041,7 @@ -- explicit quantifier is given, we just use that. If not, then we -- pick the quantifier appropriately based on the run-mode. -- @randomCW@ is used for generating random values for this variable--- when used for 'quickCheck' or 'genTest' purposes.+-- when used for @quickCheck@ or 'Data.SBV.Tools.GenTest.genTest' purposes. svMkSymVarGen :: Bool -> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal svMkSymVarGen isTracker mbQ k mbNm st = do         rm <- readIORef (runMode st)@@ -1420,8 +1428,9 @@ -- | 'RoundingMode' kind instance HasKind RoundingMode --- | Solver configuration. See also 'z3', 'yices', 'cvc4', 'boolector', '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}@.)+-- | 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}@.) -- -- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does -- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
Data/SBV/Dynamic.hs view
@@ -112,7 +112,7 @@   -- ** Code generation with uninterpreted functions   , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert -  -- ** Code generation with 'SInteger' and 'SReal' types+  -- ** Code generation with 'Data.SBV.SInteger' and 'Data.SBV.SReal' types   , cgIntegerSize, cgSRealType, CgSRealType(..)    -- ** Compilation to C@@ -209,6 +209,6 @@ getModelAssignment = SBV.getModelAssignment  -- | Extract a model dictionary. Extract a dictionary mapping the variables to--- their respective values as returned by the SMT solver. Also see `getModelDictionaries`.+-- their respective values as returned by the SMT solver. Also see `Data.SBV.SMT.getModelDictionaries`. getModelDictionary :: SMTResult -> Map String CW getModelDictionary = SBV.getModelDictionary
Data/SBV/Internals.hs view
@@ -87,7 +87,7 @@ {- $coordinateSolverInfo In rare cases it might be necessary to send an arbitrary string down to the solver. Needless to say, this should be avoided if at all possible. Users should prefer the provided API. If you do find yourself-needing 'send' and 'ask' directly, please get in touch to see if SBV can support a typed API for your use case.+needing 'Data.SBV.Control.Utils.send' and 'Data.SBV.Control.Utils.ask' directly, please get in touch to see if SBV can support a typed API for your use case. Similarly, the function 'retrieveResponseFromSolver' might occasionally be necessary to clean-up the communication buffer. We would like to hear if you do need these functions regularly so we can provide better support. -}
Data/SBV/List.hs view
@@ -109,7 +109,7 @@  | True  = subList l 0 (length l - 1) --- | @`singleton` x@ is the list of length 1 that contains the only value `x`.+-- | @`singleton` x@ is the list of length 1 that contains the only value @x@. -- -- >>> prove $ \(x :: SInteger) -> head (singleton x) .== x -- Q.E.D.@@ -251,10 +251,9 @@          $ subList s i (ls - i)   where ls = length s --- | @`subList` s offset len@ is the sublist of @s@ at offset `offset` with length `len`.+-- | @`subList` s offset len@ is the sublist of @s@ at offset @offset@ with length @len@. -- This function is under-specified when the offset is outside the range of positions in @s@ or @len@--- is negative or @offset+len@ exceeds the length of @s@. For a friendlier version of this function--- that acts like Haskell's `take`\/`drop`, see `strTake`\/`strDrop`.+-- is negative or @offset+len@ exceeds the length of @s@. -- -- >>> prove $ \(l :: SList Integer) i -> i .>= 0 &&& i .< length l ==> subList l 0 i .++ subList l i (length l - i) .== l -- Q.E.D.
Data/SBV/List/Bounded.hs view
@@ -19,8 +19,8 @@ module Data.SBV.List.Bounded (      -- * General folds      bfoldr, bfoldl-     -- * Map, filter, zipWith-   , bmap, bfilter, bzipWith+     -- * Map, filter, zipWith, elem+   , bmap, bfilter, bzipWith, belem      -- * Aggregates    , bsum, bprod, band, bor, bany, ball, bmaximum, bminimum    )@@ -36,13 +36,13 @@  -- | Bounded fold from the right. bfoldr :: (SymWord a, SymWord b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b-bfoldr cnt f b = go cnt+bfoldr cnt f b = go (cnt `max` 0)   where go 0 _ = b         go i s = lcase s b (\h t -> h `f` go (i-1) t)  -- | Bounded fold from the left. bfoldl :: (SymWord a, SymWord b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b-bfoldl cnt f = go cnt+bfoldl cnt f = go (cnt `max` 0)   where go 0 b _ = b         go i b s = lcase s b (\h t -> go (i-1) (b `f` h) t) @@ -66,7 +66,7 @@ band :: Int -> SList Bool -> SBool band i = bfoldr i (&&&) (true  :: SBool) --- | Bounded logical and+-- | Bounded logical or bor :: Int -> SList Bool -> SBool bor i = bfoldr i (|||) (false :: SBool) @@ -88,8 +88,12 @@  -- | Bounded zipWith bzipWith :: (SymWord a, SymWord b, SymWord c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c-bzipWith cnt f = go cnt+bzipWith cnt f = go (cnt `max` 0)    where go 0 _  _  = []          go i xs ys = ite (L.null xs ||| L.null ys)                           []                           (f (L.head xs) (L.head ys) .: go (i-1) (L.tail xs) (L.tail ys))++-- | Bounded element check+belem :: SymWord a => Int -> SBV a -> SList a -> SBool+belem i e = bany i (e .==)
Data/SBV/Provers/Prover.hs view
@@ -187,7 +187,7 @@   -- in the configuration.   --   -- NB. Uninterpreted constant/function values and counter-examples for array values are ignored for-  -- the purposes of @'allSat'@. That is, only the satisfying assignments modulo uninterpreted functions and+  -- the purposes of 'allSat'. That is, only the satisfying assignments modulo uninterpreted functions and   -- array inputs will be returned. This is due to the limitation of not having a robust means of getting a   -- function counter-example back from the SMT solver.   --  Find all satisfying assignments using the given SMT-solver@@ -562,7 +562,7 @@    safe :: a -> IO [SafeResult]    safe = safeWith defaultSMTCfg -   -- | Check if any of the 'sAssert' calls can be violated.+   -- | Check if any of the 'Data.SBV.sAssert' calls can be violated.    safeWith :: SMTConfig -> a -> IO [SafeResult]    safeWith cfg a = do cwd <- (++ "/") <$> getCurrentDirectory                        let mkRelative path@@ -572,7 +572,7 @@      where check mkRelative = Control.query $ Control.getSBVAssertions >>= mapM (verify mkRelative)             -- check that the cond is unsatisfiable. If satisfiable, that would-           -- indicate the assignment under which the 'sAssert' would fail+           -- indicate the assignment under which the 'Data.SBV.sAssert' would fail            verify :: (FilePath -> FilePath) -> (String, Maybe CallStack, SW) -> Query SafeResult            verify mkRelative (msg, cs, cond) = do                    let locInfo ps = let loc (f, sl) = concat [mkRelative (srcLocFile sl), ":", show (srcLocStartLine sl), ":", show (srcLocStartCol sl), ":", f]
Data/SBV/RegExp.hs view
@@ -99,7 +99,7 @@            opt = Nothing  -- | A literal regular-expression, matching the given string exactly. Note that--- with 'OverloadedStrings' extension, you can simply use a Haskell+-- with @OverloadedStrings@ extension, you can simply use a Haskell -- string to mean the same thing, so this function is rarely needed. -- -- >>> prove $ \(s :: SString) -> s `match` exactly "LITERAL" <=> s .== "LITERAL"@@ -295,7 +295,7 @@ {- $matching A symbolic string or a character ('SString' or 'SChar') can be matched against a regular-expression. Note that the regular-expression itself is not a symbolic object: It's a fully concrete representation, as-captured by the 'RegExp' class. The 'RegExp' class is an instance of 'IsString', which makes writing+captured by the 'RegExp' class. The 'RegExp' class is an instance of the @IsString@ class, which makes writing literal matches easier. The 'RegExp' type also has a (somewhat degenerate) 'Num' instance: Concatenation corresponds to multiplication, union corresponds to addition, and @0@ corresponds to the empty language.
Data/SBV/SMT/SMT.hs view
@@ -79,24 +79,24 @@ resultConfig (Unknown       c _) = c resultConfig (ProofError    c _) = c --- | A 'prove' call results in a 'ThmResult'+-- | A 'Data.SBV.prove' call results in a 'ThmResult' newtype ThmResult = ThmResult SMTResult                   deriving NFData --- | A 'sat' call results in a 'SatResult'+-- | A 'Data.SBV.sat' call results in a 'SatResult' -- The reason for having a separate 'SatResult' is to have a more meaningful 'Show' instance. newtype SatResult = SatResult SMTResult                   deriving NFData --- | An 'allSat' call results in a 'AllSatResult'. The first boolean says whether we+-- | An 'Data.SBV.allSat' call results in a 'AllSatResult'. The first boolean says whether we -- hit the max-model limit as we searched. The second boolean says whether -- there were prefix-existentials. newtype AllSatResult = AllSatResult (Bool, Bool, [SMTResult]) --- | A 'safe' call results in a 'SafeResult'+-- | A 'Data.SBV.safe' call results in a 'SafeResult' newtype SafeResult   = SafeResult   (Maybe String, String, SMTResult) --- | An 'optimize' call results in a 'OptimizeResult'. In the 'ParetoResult' case, the boolean is 'True'+-- | An 'Data.SBV.optimize' call results in a 'OptimizeResult'. In the 'ParetoResult' case, the boolean is 'True' -- if we reached pareto-query limit and so there might be more unqueried results remaining. If 'False', -- it means that we have all the pareto fronts returned. See the 'Pareto' 'OptimizeStyle' for details. data OptimizeResult = LexicographicResult SMTResult@@ -172,7 +172,7 @@                                     (tag "Optimal in an extension field:" ++ "\n")  -- | Instances of 'SatModel' can be automatically extracted from models returned by the--- solvers. The idea is that the sbv infrastructure provides a stream of 'CW''s (constant-words)+-- solvers. The idea is that the sbv infrastructure provides a stream of CW's (constant-words) -- coming from the solver, and the type @a@ is interpreted based on these constants. Many typical -- instances are already provided, so new instances can be declared with relative ease. --@@ -256,7 +256,7 @@   parseCWs (CW KDouble (CWDouble i) : r) = Just (i, r)   parseCWs _                             = Nothing --- | 'CW' as extracted from a model; trivial definition+-- | @CW@ as extracted from a model; trivial definition instance SatModel CW where   parseCWs (cw : r) = Just (cw, r)   parseCWs []       = Nothing@@ -349,7 +349,7 @@   getModelObjectiveValue :: String -> a -> Maybe GeneralizedCW   getModelObjectiveValue v r = v `M.lookup` getModelObjectives r --- | Return all the models from an 'allSat' call, similar to 'extractModel' but+-- | Return all the models from an 'Data.SBV.allSat' call, similar to 'extractModel' but -- is suitable for the case of multiple results. extractModels :: SatModel a => AllSatResult -> [a] extractModels (AllSatResult (_, _, xs)) = [ms | Right (_, ms) <- map getModelAssignment xs]@@ -411,9 +411,9 @@                    Just (_, ys) -> error $ "SBV.parseModelOut: Partially constructed model; remaining elements: " ++ show ys                    Nothing      -> error $ "SBV.parseModelOut: Cannot construct a model from: " ++ show m --- | Given an 'allSat' call, we typically want to iterate over it and print the results in sequence. The--- 'displayModels' function automates this task by calling 'disp' on each result, consecutively. The first--- 'Int' argument to 'disp' 'is the current model number. The second argument is a tuple, where the first+-- | Given an 'Data.SBV.allSat' call, we typically want to iterate over it and print the results in sequence. The+-- 'displayModels' function automates this task by calling @disp@ on each result, consecutively. The first+-- 'Int' argument to @disp@ 'is the current model number. The second argument is a tuple, where the first -- element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown) displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int displayModels disp (AllSatResult (_, _, ms)) = do@@ -532,7 +532,7 @@                 | SolverTimeout   String  -- ^ Timeout expired                 | SolverException String  -- ^ Something else went wrong --- | A variant of 'readProcessWithExitCode'; except it deals with SBV continuations+-- | A variant of @readProcessWithExitCode@; except it deals with SBV continuations runSolver :: SMTConfig -> State -> FilePath -> [String] -> String -> (State -> IO a) -> IO a runSolver cfg ctx execPath opts pgm continuation  = do let nm  = show (name (solver cfg))
Data/SBV/String.hs view
@@ -249,10 +249,9 @@          $ subStr s i (ls - i)   where ls = length s --- | @`subStr` s offset len@ is the substring of @s@ at offset `offset` with length `len`.+-- | @`subStr` s offset len@ is the substring of @s@ at offset @offset@ with length @len@. -- This function is under-specified when the offset is outside the range of positions in @s@ or @len@--- is negative or @offset+len@ exceeds the length of @s@. For a friendlier version of this function--- that acts like Haskell's `take`\/`drop`, see `strTake`\/`strDrop`.+-- is negative or @offset+len@ exceeds the length of @s@. -- -- >>> prove $ \s i -> i .>= 0 &&& i .< length s ==> subStr s 0 i .++ subStr s i (length s - i) .== s -- Q.E.D.@@ -334,7 +333,7 @@   = lift3 StrIndexOf Nothing s sub offset  -- | @`strToNat` s@. Retrieve integer encoded by string @s@ (ground rewriting only).--- Note that by definition this function only works when 's' only contains digits,+-- Note that by definition this function only works when @s@ only contains digits, -- that is, if it encodes a natural number. Otherwise, it returns '-1'. -- See <http://cvc4.cs.stanford.edu/wiki/Strings> for details. --
Data/SBV/Tools/CodeGen.hs view
@@ -30,7 +30,7 @@         -- ** Code generation with uninterpreted functions         , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert -        -- ** Code generation with 'SInteger' and 'SReal' types+        -- ** Code generation with 'Data.SBV.SInteger' and 'Data.SBV.SReal' types         -- $unboundedCGen         , cgIntegerSize, cgSRealType, CgSRealType(..) @@ -51,11 +51,11 @@ -}  {- $unboundedCGen-The types 'SInteger' and 'SReal' are unbounded quantities that have no direct counterparts in the C language. Therefore,+The types 'Data.SBV.SInteger' and 'Data.SBV.SReal' are unbounded quantities that have no direct counterparts in the C language. Therefore, it is not possible to generate standard C code for SBV programs using these types, unless custom libraries are available. To overcome this, SBV allows the user to explicitly set what the corresponding types should be for these two cases, using the functions below. Note that while these mappings will produce valid C code, the resulting code will be subject to-overflow/underflows for 'SInteger', and rounding for 'SReal', so there is an implicit loss of precision.+overflow/underflows for 'Data.SBV.SInteger', and rounding for 'Data.SBV.SReal', so there is an implicit loss of precision.  If the user does /not/ specify these mappings, then SBV will refuse to compile programs that involve these types.
Data/SBV/Tools/Overflow.hs view
@@ -103,8 +103,8 @@   bvNegO     = signPick1 bvunego     bvsnego  -- | A class of checked-arithmetic operations. These follow the usual arithmetic,--- except make calls to 'sAssert' to ensure no overflow/underflow can occur.--- Use them in conjunction with 'safe' to ensure no overflow can happen.+-- except make calls to 'Data.SBV.sAssert' to ensure no overflow/underflow can occur.+-- Use them in conjunction with 'Data.SBV.safe' to ensure no overflow can happen. class (ArithOverflow (SBV a), Num a, SymWord a) => CheckedArithmetic a where   (+!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a   (-!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a@@ -455,7 +455,7 @@                   | m > n = false                   | True  = SBV $ svAll [(unSBV x `svTestBit` (n-1)) `svEqual` svFalse, svNot $ allZero (n-1) (m-1) x] --- | Version of 'sFromIntegral' that has calls to 'sAssert' for checking no overflow/underflow can happen. Use it with a 'safe' call.+-- | Version of 'sFromIntegral' that has calls to 'Data.SBV.sAssert' for checking no overflow/underflow can happen. Use it with a 'Data.SBV.safe' call. sFromIntegralChecked :: forall a b. (?loc :: CallStack, Integral a, HasKind a, HasKind b, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> SBV b sFromIntegralChecked x = sAssert (Just ?loc) (msg "underflows") (bnot u)                        $ sAssert (Just ?loc) (msg "overflows")  (bnot o)
Data/SBV/Tools/Polynomial.hs view
@@ -211,7 +211,7 @@ -- polynomial division, but this routine is much faster in practice.) -- -- NB. The @n@th bit of the polynomial @p@ /must/ be set for the CRC--- to be computed correctly. Note that the polynomial argument 'p' will+-- to be computed correctly. Note that the polynomial argument @p@ will -- not even have this bit present most of the time, as it will typically -- contain bits @0@ through @n-1@ as usual in the CRC literature. The higher -- order @n@th bit is simply assumed to be set, as it does not make@@ -221,9 +221,9 @@ -- NB. The literature on CRC's has many variants on how CRC's are computed. -- We follow the following simple procedure: -----     * Extend the message 'm' by adding 'n' 0 bits on the right+--     * Extend the message @m@ by adding @n@ 0 bits on the right -----     * Divide the polynomial thus obtained by the 'p'+--     * Divide the polynomial thus obtained by the @p@ -- --     * The remainder is the CRC value. --
Data/SBV/Utils/Boolean.hs view
@@ -18,7 +18,7 @@ infixr 1 ==>, <=>  -- implies, iff  -- | The 'Boolean' class: a generalization of Haskell's 'Bool' type--- Haskell 'Bool' and SBV's 'SBool' are instances of this class, unifying the treatment of boolean values.+-- Haskell 'Bool' and SBV's 'Data.SBV.SBool' are instances of this class, unifying the treatment of boolean values. -- -- Minimal complete definition: 'true', 'bnot', '&&&' -- However, it's advisable to define 'false', and '|||' as well (typically), for clarity.
Data/SBV/Utils/Numeric.hs view
@@ -40,7 +40,7 @@    where isN0   = isNegativeZero          isP0 a = a == 0 && not (isN0 a) --- | SMTLib compliant definition for 'fpMin'. See the comments for 'fpMax'.+-- | SMTLib compliant definition for 'Data.SBV.fpMin'. See the comments for 'Data.SBV.fpMax'. fpMinH :: RealFloat a => a -> a -> a fpMinH x y    | isNaN x                                  = y
Documentation/SBV/Examples/BitPrecise/MergeSort.hs view
@@ -71,8 +71,8 @@  -- | Asserting correctness of merge-sort for a list of the given size. Note that we can -- only check correctness for fixed-size lists. Also, the proof will get more and more--- complicated for the backend SMT solver as 'n' increases. A value around 5 or 6 should--- be fairly easy to prove. For instance, we have:+-- complicated for the backend SMT solver as the list size increases. A value around+-- 5 or 6 should be fairly easy to prove. For instance, we have: -- -- >>> correctness 5 -- Q.E.D.@@ -85,7 +85,7 @@ -- * Generating C code ----------------------------------------------------------------------------- --- | Generate C code for merge-sorting an array of size 'n'. Again, we're restricted+-- | Generate C code for merge-sorting an array of size @n@. Again, we're restricted -- to fixed size inputs. While the output is not how one would code merge sort in C -- by hand, it's a faithful rendering of all the operations merge-sort would do as -- described by its Haskell counterpart.
Documentation/SBV/Examples/Lists/BoundedMutex.hs view
@@ -22,6 +22,7 @@ import Data.SBV import Data.SBV.Control +import Data.SBV.List ((.!!)) import qualified Data.SBV.List         as L import qualified Data.SBV.List.Bounded as L @@ -124,3 +125,52 @@                                               io . putStrLn $ "P1: " ++ show p1V                                               io . putStrLn $ "P2: " ++ show p2V                                               io . putStrLn $ "Ts: " ++ show ts++-- | Our algorithm is correct, but it is not fair. It does not guarantee that a process that+-- wants to enter its critical-section will always do so eventually. Demonstrate this by+-- trying to show a bounded trace of length 10, such that the second process is ready but+-- never transitions to critical. We have:+--+-- >>> notFair 10+-- Fairness is violated at bound: 10+-- P1: [Idle,Idle,Ready,Critical,Idle,Idle,Ready,Critical,Idle,Idle]+-- P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready]+-- Ts: [1,2,1,1,1,1,1,1,1,1]+--+-- As expected, P2 gets ready but never goes critical since the arbiter keeps picking+-- P1 unfairly.+--+-- Exercise for the reader: Change the 'validTurns' function so that it alternates the turns+-- from the previous value if neither process is in critical. Show that this makes the 'notFair'+-- function below no longer exhibits the issue. Is this sufficient? Concurrent programming is tricky!+notFair :: Int -> IO ()+notFair b = runSMT $ do p1    :: SList State   <- sList "p1"+                        p2    :: SList State   <- sList "p2"+                        turns :: SList Integer <- sList "turns"++                        -- Ensure that both sequences and the turns are valid+                        constrain $ validSequence b 1 turns p1+                        constrain $ validSequence b 2 turns p2+                        constrain $ validTurns    b turns p1 p2++                        -- Ensure that the second process becomes ready in the second cycle:+                        constrain $ p2 .!! 1 .== ready++                        -- Find a trace where p2 never goes critical+                        -- counter example, we would've found a violation!+                        constrain $ bnot $ L.belem b critical p2++                        query $ do cs <- checkSat+                                   case cs of+                                     Unk   -> error "Solver said Unknown!"+                                     Unsat -> error "Solver couldn't find a violating trace!"+                                     Sat   -> do io . putStrLn $ "Fairness is violated at bound: " ++ show b+                                                 do p1V <- getValue p1+                                                    p2V <- getValue p2+                                                    ts  <- getValue turns++                                                    io . putStrLn $ "P1: " ++ show p1V+                                                    io . putStrLn $ "P2: " ++ show p2V+                                                    io . putStrLn $ "Ts: " ++ show ts++{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
Documentation/SBV/Examples/Misc/Floating.hs view
@@ -142,9 +142,8 @@ -- can effect the results of a computation if the exact result cannot be precisely -- represented. SBV exports the functions 'fpAdd', 'fpSub', 'fpMul', 'fpDiv', 'fpFMA' -- and 'fpSqrt' which allows users to specify the IEEE supported 'RoundingMode' for--- the operation. (Also see the class 'RoundingFloat'.) This example illustrates how SBV--- can be used to find rounding-modes where, for instance, addition can produce different--- results. We have:+-- the operation. This example illustrates how SBV can be used to find rounding-modes+-- where, for instance, addition can produce different results. We have: -- -- >>> roundingAdd -- Satisfiable. Model:@@ -166,7 +165,7 @@ -- Satisfiable. Model: --   s0 = 0.999939 :: Float ----- We can see why these two resuls are indeed different: The 'RoundTowardsPositive'+-- We can see why these two resuls are indeed different: The 'RoundTowardPositive' -- (which rounds towards positive-infinity) produces a larger result. Indeed, if we treat these numbers -- as 'Double' values, we get: --
Documentation/SBV/Examples/Puzzles/Birthday.hs view
@@ -91,7 +91,7 @@ -- | Encode the conversation as given in the puzzle. -- -- NB. Lee Pike pointed out that not all the constraints are actually necessary! (Private--- communication.) The puzzle still has a unique solution if the statements 'a1' and 'b1'+-- communication.) The puzzle still has a unique solution if the statements @a1@ and @b1@ -- (i.e., Albert and Bernard saying they themselves do not know the answer) are removed. -- To experiment you can simply comment out those statements and observe that there still -- is a unique solution. Thanks to Lee for pointing this out! In fact, it is instructive to
Documentation/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -83,7 +83,7 @@ -- -- This type is equipped with an automatically derived 'Mergeable' instance -- because each field is 'Mergeable'. A 'Generic' instance must also be derived--- for this to work, and the 'DeriveAnyClass' language extension must be+-- for this to work, and the @DeriveAnyClass@ language extension must be -- enabled. The derived 'Mergeable' instance simply walks down the structure -- field by field and merges each one. An equivalent hand-written 'Mergeable' -- instance is provided in a comment below.@@ -146,7 +146,7 @@  -- | Transferring a person to the other side xferPerson :: SU2Member -> Move ()-xferPerson p =  do [lb, le, la, ll] <- mapM peek [lBono, lEdge, lAdam, lLarry]+xferPerson p =  do ~[lb, le, la, ll] <- mapM peek [lBono, lEdge, lAdam, lLarry]                    let move l = ite (l .== here) there here                        lb' = ite (p .== bono)  (move lb) lb                        le' = ite (p .== edge)  (move le) le@@ -162,7 +162,7 @@ bumpTime2 :: SU2Member -> SU2Member -> Move () bumpTime2 p1 p2 = modify $ \s -> s{time = time s + sCrossTime p1 `smax` sCrossTime p2} --- | Symbolic version of 'when'+-- | Symbolic version of 'Control.Monad.when' whenS :: SBool -> Move () -> Move () whenS t a = ite t a (return ())
Documentation/SBV/Examples/Queries/AllSat.hs view
@@ -8,7 +8,7 @@ -- -- When we would like to find all solutions to a problem, we can query the -- solver repeatedly, telling it to give us a new model each time. SBV already--- provides 'allSat' that precisely does this. However, this example demonstrates+-- provides 'Data.SBV.allSat' that precisely does this. However, this example demonstrates -- how the query mode can be used to achieve the same, and can also incorporate -- extra conditions with easy as we walk through solutions. -----------------------------------------------------------------------------
Documentation/SBV/Examples/Strings/SQLInjection.hs view
@@ -116,11 +116,9 @@ -- -- Indeed, if we substitute the suggested string, we get the program: ----- @---   query ("SELECT msg FROM msgs where topicid='h'; DROP TABLE 'users'")--- @+-- > query ("SELECT msg FROM msgs where topicid='h'; DROP TABLE 'users'") ----- which would query for topic 'h' and then delete the users table!+-- which would query for topic @h@ and then delete the users table! findInjection :: SQLExpr -> IO String findInjection expr = runSMT $ do     badTopic <- sString "badTopic"
sbv.cabal view
@@ -1,5 +1,5 @@ Name:          sbv-Version:       7.11+Version:       7.12 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