sbv 11.2 → 11.3
raw patch · 31 files changed
+146/−119 lines, 31 files
Files
- CHANGES.md +6/−0
- Data/SBV.hs +11/−11
- Data/SBV/Compilers/C.hs +2/−2
- Data/SBV/Control.hs +3/−0
- Data/SBV/Control/BaseIO.hs +1/−1
- Data/SBV/Core/Concrete.hs +8/−8
- Data/SBV/Core/Sized.hs +16/−16
- Data/SBV/Core/Symbolic.hs +8/−8
- Data/SBV/Dynamic.hs +4/−4
- Data/SBV/Provers/Prover.hs +1/−1
- Data/SBV/SMT/SMT.hs +8/−8
- Data/SBV/SMT/Utils.hs +1/−1
- Data/SBV/Tools/KD/KnuckleDragger.hs +3/−3
- Data/SBV/Tools/KD/Utils.hs +1/−1
- Data/SBV/Tools/Range.hs +1/−1
- Data/SBV/Trans.hs +1/−1
- Data/SBV/Trans/Control.hs +2/−2
- Data/SBV/Utils/ExtractIO.hs +4/−4
- Documentation/SBV/Examples/BitPrecise/Legato.hs +1/−1
- Documentation/SBV/Examples/Crypto/SHA.hs +1/−1
- Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs +41/−21
- Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +1/−1
- Documentation/SBV/Examples/Misc/Newtypes.hs +5/−5
- Documentation/SBV/Examples/Transformers/SymbolicEval.hs +8/−10
- Documentation/SBV/Examples/WeakestPreconditions/Basics.hs +1/−1
- Documentation/SBV/Examples/WeakestPreconditions/Fib.hs +1/−1
- Documentation/SBV/Examples/WeakestPreconditions/GCD.hs +1/−1
- Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs +1/−1
- Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs +1/−1
- Documentation/SBV/Examples/WeakestPreconditions/Sum.hs +2/−2
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,6 +1,12 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 11.3, 2025-03-10++ * Fix various haddock documentation links++ * KD: Clean-up proofs using the cases tactic+ ### Version 11.2, 2025-03-08 * Renamed the all-sat partitioning function from 'partition' to 'allSatPartiton'
Data/SBV.hs view
@@ -24,8 +24,8 @@ -- And similarly, 'sat' finds a satisfying instance. The types involved are: -- -- @--- 'prove' :: 'Provable' a => a -> 'IO' 'ThmResult'--- 'sat' :: 'Data.SBV.Provers.Satisfiable' a => a -> 'IO' 'SatResult'+-- 'prove' :: 'Provable' a => a -> 'IO' t'ThmResult'+-- 'sat' :: 'Data.SBV.Provers.Satisfiable' a => a -> 'IO' t'SatResult' -- @ -- -- The classes 'Provable' and 'Data.SBV.Provers.Satisfiable' come with instances for n-ary predicates, for arbitrary n.@@ -385,7 +385,7 @@ -- $softAssertions , assertWithPenalty , Penalty(..) -- ** Field extensions- -- | If an optimization results in an infinity/epsilon value, the returned `CV` value will be in the corresponding extension field.+ -- | If an optimization results in an infinity/epsilon value, the returned t'CV' value will be in the corresponding extension field. , ExtCV(..), GeneralizedCV(..) -- * Model extraction@@ -425,7 +425,7 @@ , some -- * Queriable values- , Queriable(..), freshVar, freshVar_, getValue+ , Queriable(..), freshVar, freshVar_ -- * Module exports -- $moduleExportIntro@@ -727,8 +727,8 @@ @ 'assertWithPenalty' "bounded_x" (x .< 5) 'DefaultPenalty'- 'assertWithPenalty' "bounded_x" (x .< 5) ('Penalty' 2.3 Nothing)- 'assertWithPenalty' "bounded_x" (x .< 5) ('Penalty' 4.7 (Just "group-1")) @+ 'assertWithPenalty' "bounded_x" (x .< 5) $ v'Penalty' 2.3 Nothing+ 'assertWithPenalty' "bounded_x" (x .< 5) $ v'Penalty' 4.7 (Just "group-1") @ In the first form, we are saying that the constraint @x .< 5@ must be satisfied, if possible, but if this constraint can not be satisfied to find a model, it can be violated with the default penalty of 1.@@ -749,7 +749,7 @@ -} {- $resultTypes-'ThmResult', 'SatResult', and 'AllSatResult' are simple newtype wrappers over 'SMTResult'. Their+t'ThmResult', t'SatResult', and t'AllSatResult' are simple newtype wrappers over t'SMTResult'. Their main purpose is so that we can provide custom 'Show' instances to print results accordingly. -} @@ -993,8 +993,8 @@ * "Documentation.SBV.Examples.Puzzles.Rabbits" * "Documentation.SBV.Examples.Misc.FirstOrderLogic" -SBV also supports the constructors 'ExistsUnique' to create unique existentials, in addition to-'ForallN' and 'ExistsN' for creating multiple variables at the same time.+SBV also supports the constructors t'ExistsUnique' to create unique existentials, in addition+to t'ForallN' and t'ExistsN' for creating multiple variables at the same time. In general, SBV will not display the values of quantified variables for a satisfying instance. For a satisfiability problem, you can apply skolemization manually to have these values@@ -1168,7 +1168,7 @@ {- $verbosity -SBV provides various levels of verbosity to aid in debugging, by using the 'SMTConfig' fields:+SBV provides various levels of verbosity to aid in debugging, by using the t'SMTConfig' fields: * ['verbose'] Print on stdout a shortened account of what is sent/received. This is specifically trimmed to reduce noise and is good for quick debugging. The output is not supposed to be machine-readable.@@ -1774,7 +1774,7 @@ project :: a -> QueryT m (QueryResult a) -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other- -- via the 'QueryT' monad transformer.+ -- via the t'QueryT' monad transformer. embed :: QueryResult a -> QueryT m a default project :: (a ~ t e, QueryResult (t e) ~ t (QueryResult e), Traversable t, Monad m, Queriable m e) => a -> QueryT m (QueryResult a)
Data/SBV/Compilers/C.hs view
@@ -62,7 +62,7 @@ renderCgPgmBundle mbDirName (cfg, bundle) return retVal --- | Lower level version of 'compileToC', producing a 'CgPgmBundle'+-- | Lower level version of 'compileToC', producing a t'CgPgmBundle' compileToC' :: String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle) compileToC' nm f = do rands <- randoms `fmap` newStdGen codeGen SBVToC (defaultCgConfig { cgDriverVals = rands }) nm f@@ -82,7 +82,7 @@ renderCgPgmBundle mbDirName (cfg, pgm) return retVal --- | Lower level version of 'compileToCLib', producing a 'CgPgmBundle'+-- | Lower level version of 'compileToCLib', producing a t'CgPgmBundle' compileToCLib' :: String -> [(String, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle) compileToCLib' libName comps = do resCfgBundles <- mapM (uncurry compileToC') comps let (finalCfg, finalPgm) = mergeToLib libName [(c, b) | (_, c, b) <- resCfgBundles]
Data/SBV/Control.hs view
@@ -27,6 +27,9 @@ -- ** Extracting the unsat core , getUnsatCore + -- ** Getting the model value for a symbolic variable+ , getValue+ -- ** Extracting a proof , getProof
Data/SBV/Control/BaseIO.hs view
@@ -192,7 +192,7 @@ -- @ -- -- for this call to not error out! Furthermore, unsat-cores require for the user to name the--- constraints to be considered as part of the set, which is done via 'Data.SBV.Core.namedConstraint'.+-- constraints to be considered as part of the set, which is done via 'Data.SBV.namedConstraint'. -- -- NB. There is no notion of a minimal unsat-core, in case unsatisfiability can be derived -- in multiple ways. Furthermore, Z3 does not guarantee that the generated unsat
Data/SBV/Core/Concrete.hs view
@@ -192,7 +192,7 @@ ] else cvRank a `compare` cvRank b --- | 'CV' represents a concrete word of a fixed size:+-- | A t'CV' represents a concrete word of a fixed size: -- For signed words, the most significant digit is considered to be the sign. data CV = CV { _cvKind :: !Kind , cvVal :: !CVal@@ -300,15 +300,15 @@ normCV c = c {-# INLINE normCV #-} --- | Constant False as a 'CV'. We represent it using the integer value 0.+-- | Constant False as a t'CV'. We represent it using the integer value 0. falseCV :: CV falseCV = CV KBool (CInteger 0) --- | Constant True as a 'CV'. We represent it using the integer value 1.+-- | Constant True as a t'CV'. We represent it using the integer value 1. trueCV :: CV trueCV = CV KBool (CInteger 1) --- | Map a unary function through a 'CV'.+-- | Map a unary function through a t'CV'. mapCV :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float)@@ -333,7 +333,7 @@ CEither{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with either!" CArray{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with arrays!" --- | Map a binary function through a 'CV'.+-- | Map a binary function through a t'CV'. mapCV2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float)@@ -361,11 +361,11 @@ , "*** Please report this as a bug!" ] --- | Show instance for 'CV'.+-- | Show instance for t'CV'. instance Show CV where show = showCV True --- | Show instance for Generalized 'CV'+-- | Show instance for Generalized t'CV' instance Show GeneralizedCV where show (ExtendedCV k) = showExtCV True k show (RegularCV c) = showCV True c@@ -515,7 +515,7 @@ bounds False w = (0, 2^w - 1) bounds True w = (-x, x-1) where x = 2^(w-1) --- | Generate a random constant value ('CV') of the correct kind.+-- | Generate a random constant value (i.e., t'CV') of the correct kind. randomCV :: Kind -> IO CV randomCV k = CV k <$> randomCVal k
Data/SBV/Core/Sized.hs view
@@ -42,22 +42,22 @@ -- | An unsigned bit-vector carrying its size info newtype WordN (n :: Nat) = WordN Integer deriving (Eq, Ord) --- | Show instance for 'WordN'+-- | Show instance for t'WordN' instance Show (WordN n) where show (WordN v) = show v --- | 'WordN' has a kind+-- | t'WordN' has a kind instance (KnownNat n, BVIsNonZero n) => HasKind (WordN n) where kindOf _ = KBounded False (intOfProxy (Proxy @n)) -- | A signed bit-vector carrying its size info newtype IntN (n :: Nat) = IntN Integer deriving (Eq, Ord) --- | Show instance for 'IntN'+-- | Show instance for t'IntN' instance Show (IntN n) where show (IntN v) = show v --- | 'IntN' has a kind+-- | t'IntN' has a kind instance (KnownNat n, BVIsNonZero n) => HasKind (IntN n) where kindOf _ = KBounded True (intOfProxy (Proxy @n)) @@ -93,17 +93,17 @@ uc (SVal _ (Left v)) = cvToBool v uc r = error $ "Impossible happened while lifting " ++ show nm ++ " over " ++ show (k, x, i, r) --- | 'Bounded' instance for 'WordN'+-- | 'Bounded' instance for t'WordN' 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'+-- | 'Bounded' instance for t'IntN' 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'+-- | 'Num' instance for t'WordN' instance (KnownNat n, BVIsNonZero n) => Num (WordN n) where (+) = lift2 "(+)" svPlus (-) = lift2 "(*)" svMinus@@ -113,7 +113,7 @@ signum = WordN . signum . toInteger fromInteger = WordN . fromJust . svAsInteger . svInteger (kindOf (undefined :: WordN n)) --- | 'Num' instance for 'IntN'+-- | 'Num' instance for t'IntN' instance (KnownNat n, BVIsNonZero n) => Num (IntN n) where (+) = lift2 "(+)" svPlus (-) = lift2 "(*)" svMinus@@ -123,35 +123,35 @@ signum = IntN . signum . toInteger fromInteger = IntN . fromJust . svAsInteger . svInteger (kindOf (undefined :: IntN n)) --- | 'Enum' instance for 'WordN'+-- | 'Enum' instance for t'WordN' instance (KnownNat n, BVIsNonZero n) => Enum (WordN n) where toEnum = fromInteger . toInteger fromEnum = fromIntegral . toInteger --- | 'Enum' instance for 'IntN'+-- | 'Enum' instance for t'IntN' instance (KnownNat n, BVIsNonZero n) => Enum (IntN n) where toEnum = fromInteger . toInteger fromEnum = fromIntegral . toInteger --- | 'Real' instance for 'WordN'+-- | 'Real' instance for t'WordN' instance (KnownNat n, BVIsNonZero n) => Real (WordN n) where toRational (WordN x) = toRational x --- | 'Real' instance for 'IntN'+-- | 'Real' instance for t'IntN' instance (KnownNat n, BVIsNonZero n) => Real (IntN n) where toRational (IntN x) = toRational x --- | 'Integral' instance for 'WordN'+-- | 'Integral' instance for t'WordN' 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'+-- | 'Integral' instance for t'IntN' 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'+-- 'Bits' instance for t'WordN' instance (KnownNat n, BVIsNonZero n) => Bits (WordN n) where (.&.) = lift2 "(.&.)" svAnd (.|.) = lift2 "(.|.)" svOr@@ -168,7 +168,7 @@ bit i = 1 `shiftL` i popCount = fromIntegral . popCount . toInteger --- 'Bits' instance for 'IntN'+-- 'Bits' instance for t'IntN' instance (KnownNat n, BVIsNonZero n) => Bits (IntN n) where (.&.) = lift2 "(.&.)" svAnd (.|.) = lift2 "(.|.)" svOr
Data/SBV/Core/Symbolic.hs view
@@ -195,11 +195,11 @@ forceSVArg :: SV -> IO () forceSVArg (SV k n) = k `seq` n `seq` return () --- | Constant False as an 'SV'. Note that this value always occupies slot -2 and level 0.+-- | Constant False as an t'SV'. Note that this value always occupies slot -2 and level 0. falseSV :: SV falseSV = SV KBool $ NodeId (globalSBVContext, Just 0, -2) --- | Constant True as an 'SV'. Note that this value always occupies slot -1 and level 0.+-- | Constant True as an t'SV'. Note that this value always occupies slot -1 and level 0. trueSV :: SV trueSV = SV KBool $ NodeId (globalSBVContext, Just 0, -1) @@ -752,7 +752,7 @@ -- | Helper synonym for text, in case we switch to something else later. type Name = T.Text --- | 'NamedSymVar' pairs symbolic values and user given/automatically generated names+-- | t'NamedSymVar' pairs symbolic values and user given/automatically generated names data NamedSymVar = NamedSymVar !SV !Name deriving (Show, Generic, G.Data) @@ -799,7 +799,7 @@ -- | Penalty for a soft-assertion. The default penalty is @1@, with all soft-assertions belonging -- to the same objective goal. A positive weight and an optional group can be provided by using--- the 'Penalty' constructor.+-- the v'Penalty' constructor. data Penalty = DefaultPenalty -- ^ Default: Penalty of @1@ and no group attached | Penalty Rational (Maybe String) -- ^ Penalty with a weight and an optional group deriving Show@@ -1285,7 +1285,7 @@ instance HasKind SVal where kindOf (SVal k _) = k --- Show instance for 'SVal'. Not particularly "desirable", but will do if needed+-- Show instance for t'SVal'. Not particularly "desirable", but will do if needed -- NB. We do not show the type info on constant KBool values, since there's no -- implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement -- of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!)@@ -1296,7 +1296,7 @@ -- | 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.+-- We really don't want an 'Eq' instance for 'Data.SBV.SBV' or t'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@@ -1706,7 +1706,7 @@ ask = lift ask local f = mapSymbolicT $ mapReaderT $ local f --- | 'Symbolic' is specialization of 'SymbolicT' to the `IO` monad. Unless you are using+-- | 'Symbolic' is specialization of t'SymbolicT' to the `IO` monad. Unless you are using -- transformers explicitly, this is the type you should prefer. type Symbolic = SymbolicT IO @@ -2355,7 +2355,7 @@ isEmptyModel SMTModel{modelAssocs, modelUIFuns} = null modelAssocs && null modelUIFuns -- | The result of an SMT solver call. Each constructor is tagged with--- the 'SMTConfig' that created it so that further tools can inspect it+-- the t'SMTConfig' that created it so that further tools can inspect it -- and build layers of results, if needed. For ordinary uses of the library, -- this type should not be needed, instead use the accessor functions on -- it. (Custom Show instances and model extractors.)
Data/SBV/Dynamic.hs view
@@ -201,14 +201,14 @@ -- | Prove a property with query mode using multiple threads. Each query -- computation will spawn a thread and a unique instance of your solver to run--- asynchronously. The 'Symbolic' 'SVal' is duplicated for each thread. This+-- asynchronously. The 'Symbolic' t'SVal' is duplicated for each thread. This -- function will block until all child threads return. proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)] proveConcurrentWithAll cfg s queries = SBV.proveConcurrentWithAll cfg queries (fmap toSBool s) -- | Prove a property with query mode using multiple threads. Each query -- computation will spawn a thread and a unique instance of your solver to run--- asynchronously. The 'Symbolic' 'SVal' is duplicated for each thread. This+-- asynchronously. The 'Symbolic' t'SVal' is duplicated for each thread. This -- function will return the first query computation that completes, killing the others. proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult) proveConcurrentWithAny cfg s queries = SBV.proveConcurrentWithAny cfg queries (fmap toSBool s)@@ -226,14 +226,14 @@ satWithAny cfgs s = SBV.satWithAny cfgs (fmap toSBool s) -- | Find a satisfying assignment to a property with multiple threads in query--- mode. The 'Symbolic' 'SVal' represents what is known to all child query threads.+-- mode. The 'Symbolic' t'SVal' represents what is known to all child query threads. -- Each query thread will spawn a unique instance of the solver. Only the first -- one to finish will be returned and the other threads will be killed. satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult) satConcurrentWithAny cfg qs s = SBV.satConcurrentWithAny cfg qs (fmap toSBool s) -- | Find a satisfying assignment to a property with multiple threads in query--- mode. The 'Symbolic' 'SVal' represents what is known to all child query threads.+-- mode. The 'Symbolic' t'SVal' represents what is known to all child query threads. -- Each query thread will spawn a unique instance of the solver. This function -- will block until all child threads have completed. satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
Data/SBV/Provers/Prover.hs view
@@ -774,7 +774,7 @@ where comp = do _ <- reducer a >>= output Control.executeQuery QueryInternal q --- | Check if a safe-call was safe or not, turning a 'SafeResult' to a Bool.+-- | Check if a safe-call was safe or not, turning a t'SafeResult' to a Bool. isSafe :: SafeResult -> Bool isSafe (SafeResult (_, _, result)) = case result of Unsatisfiable{} -> True
Data/SBV/SMT/SMT.hs view
@@ -101,24 +101,24 @@ resultConfig (Unknown c _ ) = c resultConfig (ProofError c _ _) = c --- | A 'Data.SBV.prove' call results in a 'ThmResult'+-- | A 'Data.SBV.prove' call results in a t'ThmResult' newtype ThmResult = ThmResult SMTResult deriving NFData --- | A 'Data.SBV.sat' call results in a 'SatResult'--- The reason for having a separate 'SatResult' is to have a more meaningful 'Show' instance.+-- | A 'Data.SBV.sat' call results in a t'SatResult'+-- The reason for having a separate t'SatResult' is to have a more meaningful 'Show' instance. newtype SatResult = SatResult SMTResult deriving NFData --- | An 'Data.SBV.allSat' call results in a 'AllSatResult'+-- | An 'Data.SBV.allSat' call results in a t'AllSatResult' data AllSatResult = AllSatResult { allSatMaxModelCountReached :: Bool -- ^ Did we reach the user given model count limit? , allSatSolverReturnedUnknown :: Bool -- ^ Did the solver report unknown at the end? , allSatSolverReturnedDSat :: Bool -- ^ Did the solver report delta-satisfiable at the end? , allSatResults :: [SMTResult] -- ^ All satisfying models } --- | A 'Data.SBV.safe' call results in a 'SafeResult'-newtype SafeResult = SafeResult (Maybe String, String, SMTResult)+-- | A 'Data.SBV.safe' call results in a t'SafeResult'+newtype SafeResult = SafeResult (Maybe String, String, SMTResult) -- | 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',@@ -449,7 +449,7 @@ getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String] getModelUninterpretedValues s AllSatResult{allSatResults = xs} = map (s `getModelUninterpretedValue`) xs --- | 'ThmResult' as a generic model provider+-- | t'ThmResult' as a generic model provider instance Modelable ThmResult where getModelAssignment (ThmResult r) = getModelAssignment r modelExists (ThmResult r) = modelExists r@@ -457,7 +457,7 @@ getModelObjectives (ThmResult r) = getModelObjectives r getModelUIFuns (ThmResult r) = getModelUIFuns r --- | 'SatResult' as a generic model provider+-- | t'SatResult' as a generic model provider instance Modelable SatResult where getModelAssignment (SatResult r) = getModelAssignment r modelExists (SatResult r) = modelExists r
Data/SBV/SMT/Utils.hs view
@@ -160,7 +160,7 @@ skipBar [] = [] -- Oh dear, line finished, but the string didn't. We're in trouble. Ignore! -- | An exception thrown from SBV. If the solver ever responds with a non-success value for a command,--- SBV will throw an 'SBVException', it so the user can process it as required. The provided 'Show' instance+-- SBV will throw an t'SBVException', it so the user can process it as required. The provided 'Show' instance -- will render the failure nicely. Note that if you ever catch this exception, the solver is no longer alive: -- You should either -- throw the exception up, or do other proper clean-up before continuing. data SBVException = SBVException {
Data/SBV/Tools/KD/KnuckleDragger.hs view
@@ -1184,7 +1184,7 @@ (=:) = chain infixr 1 =: --- | Unicode alternative for `=:`:+-- | Unicode alternative for `=:`. (≡) :: ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a (≡) = (=:) infixr 1 ≡@@ -1213,12 +1213,12 @@ bs |- ps = (sAnd bs, ps) infixl 0 |- --- | Alternative unicode for `|-`:+-- | Alternative unicode for `|-`. (⊢) :: [SBool] -> [ProofStep a] -> (SBool, [ProofStep a]) (⊢) = (|-) infixl 0 ⊢ --- | Alternative unicode for `??`:+-- | Alternative unicode for `??`. (⁇) :: ProofHint a b => a -> b -> ProofStep a (⁇) = (??) infixl 2 ⁇
Data/SBV/Tools/KD/Utils.hs view
@@ -142,7 +142,7 @@ `seq` rnf getProof `seq` rnf proofName --- | Show instance for 'Proof'+-- | Show instance for t'Proof' instance Show Proof where show Proof{rootOfTrust, isUserAxiom, proofName} = '[' : tag ++ "] " ++ proofName where tag | isUserAxiom = "Axiom"
Data/SBV/Tools/Range.hs view
@@ -51,7 +51,7 @@ -- | A range is a pair of boundaries: Lower and upper bounds data Range a = Range (Boundary a) (Boundary a) --- | Show instance for 'Range'+-- | Show instance for t'Range' instance Show a => Show (Range a) where show (Range l u) = sh True l ++ "," ++ sh False u where sh onLeft b = case b of
Data/SBV/Trans.hs view
@@ -124,7 +124,7 @@ -- ** Soft assumptions , assertWithPenalty , Penalty(..) -- ** Field extensions- -- | If an optimization results in an infinity/epsilon value, the returned `CV` value will be in the corresponding extension field.+ -- | If an optimization results in an infinity/epsilon value, the returned t'CV' value will be in the corresponding extension field. , ExtCV(..), GeneralizedCV(..) -- * Model extraction
Data/SBV/Trans/Control.hs view
@@ -22,7 +22,7 @@ -- * Querying the solver -- ** Extracting values- , getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables+ , getValue, getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables -- ** Extracting the unsat core , getUnsatCore@@ -74,7 +74,7 @@ import Data.SBV.Core.Symbolic (MonadQuery(..), QueryT, Query, SymbolicT, QueryContext(..)) import Data.SBV.Control.Query-import Data.SBV.Control.Utils (queryDebug, executeQuery, getFunction)+import Data.SBV.Control.Utils (queryDebug, executeQuery, getFunction, getValue) import Data.SBV.Utils.ExtractIO
Data/SBV/Utils/ExtractIO.hs view
@@ -34,18 +34,18 @@ instance ExtractIO IO where extractIO = fmap pure --- | IO extraction for 'MaybeT'.+-- | IO extraction for t'MaybeT'. instance ExtractIO m => ExtractIO (MaybeT m) where extractIO = fmap MaybeT . extractIO . runMaybeT --- | IO extraction for 'ExceptT'.+-- | IO extraction for t'ExceptT'. instance ExtractIO m => ExtractIO (ExceptT e m) where extractIO = fmap ExceptT . extractIO . runExceptT --- | IO extraction for lazy 'LW.WriterT'.+-- | IO extraction for lazy t'LW.WriterT'. instance (Monoid w, ExtractIO m) => ExtractIO (LW.WriterT w m) where extractIO = fmap LW.WriterT . extractIO . LW.runWriterT --- | IO extraction for strict 'SW.WriterT'.+-- | IO extraction for strict t'SW.WriterT'. instance (Monoid w, ExtractIO m) => ExtractIO (SW.WriterT w m) where extractIO = fmap SW.WriterT . extractIO . SW.runWriterT
Documentation/SBV/Examples/BitPrecise/Legato.hs view
@@ -81,7 +81,7 @@ -- Unlike traditional hardware, we assume the program is stored in some other memory area that -- we need not model. (No self modifying programs!) ----- 'Mostek' is equipped with an automatically derived 'Mergeable' instance+-- t'Mostek' is equipped with an automatically derived 'Mergeable' instance -- because each field is 'Mergeable'. data Mostek = Mostek { memory :: Memory , registers :: Registers
Documentation/SBV/Examples/Crypto/SHA.hs view
@@ -175,7 +175,7 @@ -- * Section 5, Preprocessing ----------------------------------------------------------------------------- --- | 'Block' is a synonym for lists, but makes the intent clear.+-- | t'Block' is a synonym for lists, but makes the intent clear. newtype Block a = Block [a] -- | Prepare the message by turning it into blocks. We also check for the message
Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs view
@@ -71,19 +71,29 @@ -- We have: -- -- >>> oddSequence2--- Inductive lemma (strong): oddSequence--- Base: oddSequence.Base Q.E.D.+-- Lemma: oddSequence_0 Q.E.D.+-- Lemma: oddSequence_1 Q.E.D.+-- Inductive lemma (strong): oddSequence_sNp2+-- Base: oddSequence_sNp2.Base Q.E.D. -- Asms: 1 Q.E.D.--- Step 1: Case split one way:--- Case [1 of 1]: n[1] Q.E.D.--- Completeness: Q.E.D.+-- Step: 1 Q.E.D.+-- Asms: 2 Q.E.D. -- Step: 2 Q.E.D.+-- Asms: 3 Q.E.D. -- Step: 3 Q.E.D. -- Step: 4 Q.E.D. -- Step: 5 Q.E.D. -- Step: 6 Q.E.D. -- Step: 7 Q.E.D.--- Step: oddSequence.Step Q.E.D.+-- Step: oddSequence_sNp2.Step Q.E.D.+-- Lemma: oddSequence+-- Asms : 1 Q.E.D.+-- Step 1: Case split 3 ways:+-- Case [1 of 3]: n[1] Q.E.D.+-- Case [2 of 3]: n[2] Q.E.D.+-- Case [3 of 3]: n[3] Q.E.D.+-- Completeness: Q.E.D.+-- Result: Q.E.D. -- [Proven] oddSequence oddSequence2 :: IO Proof oddSequence2 = runKD $ do@@ -92,21 +102,31 @@ $ ite (n .== 1) 3 $ 2 * s (n-1) - s (n-2) - sInduct "oddSequence"- (\(Forall @"n" n) -> n .>= 0 .=> s n .== 2 * n + 1) $- \ih n -> [n .>= 0] |- s (n+1)- ?? [cases "n" [n+1 .< 2], hyp (n .>= 0)]- =: let focus v = ite (n+1 .<= 0) 1 (ite (n + 1 .== 1) 3 v)- in focus (2 * s n - s (n-1))- ?? ih `at` Inst @"n" n- =: focus (2 * (2 * n + 1) - s (n - 1))- ?? ih `at` Inst @"n" (n-1)- =: focus (2 * (2 * n + 1) - (2 * (n - 1) + 1))- =: focus (4 * n + 2 - (2 * n - 1))- =: focus (4 * n + 2 - 2 * n + 1)- =: focus (2 * n + 2 + 1)- =: focus (2 * (n + 1) + 1)- =: qed+ s0 <- lemma "oddSequence_0" (s 0 .== 1) []+ s1 <- lemma "oddSequence_1" (s 1 .== 3) []++ sNp2 <- sInduct "oddSequence_sNp2"+ (\(Forall @"n" n) -> n .>= 2 .=> s n .== 2 * n + 1) $+ \ih n -> [n .>= 2] |- s (n+1) ?? n .>= 2+ =: 2 * s n - s (n-1) ?? [hyp (n .>= 2), hprf (ih `at` Inst @"n" n) ]+ =: 2*(2*n+1) - s (n-1) ?? [hyp (n .>= 2), hprf (ih `at` Inst @"n" (n-1))]+ =: 2*(2*n+1)-(2*(n-1) + 1)+ =: 4*n+2-(2*n-1)+ =: 4*n+2-2*n+1+ =: 2*n+2+1+ =: 2*(n+1)+1+ =: qed++ calc "oddSequence" (\(Forall @"n" n) -> n .>= 0 .=> s n .== 2 * n + 1) $+ \n -> [n .>= 0] |- s n+ ?? [ cases "n" [n .== 0, n .== 1, n .>= 2]+ , hyp (n .>= 0)+ , hprf s0+ , hprf s1+ , hprf $ sNp2 `at` Inst @"n" n+ ]+ =: 2 * n + 1+ =: qed -- | For strong induction to work, We have to instantiate the proof at a "smaller" value. This -- example demonstrates what happens if we don't. We have:
Documentation/SBV/Examples/Misc/FirstOrderLogic.hs view
@@ -158,7 +158,7 @@ -- * Exists unique {- $existsUnique-We can use the 'ExistsUnique' constructor to indicate a value must exists uniquely. For instance,+We can use the t'ExistsUnique' constructor to indicate a value must exists uniquely. For instance, we can prove that there is an element in 'E' that's less than 'C', but it's not unique. However, there's a unique element that's less than all the elements in 'E':
Documentation/SBV/Examples/Misc/Newtypes.hs view
@@ -29,13 +29,13 @@ -- >>> import Data.SBV #endif --- | A 'Metres' is a newtype wrapper around 'Integer'.+-- | A t'Metres' is a newtype wrapper around 'Integer'. newtype Metres = Metres Integer deriving (Real, Integral, Num, Enum, Eq, Ord) --- | Symbolic version of 'Metres'.+-- | Symbolic version of t'Metres'. type SMetres = SBV Metres --- | To use 'Metres' symbolically, we associate it with the underlying symbolic+-- | To use t'Metres' symbolically, we associate it with the underlying symbolic -- type's kind. instance HasKind Metres where kindOf _ = KUnbounded@@ -53,10 +53,10 @@ -- suits our needs. newtype HumanHeightInCm = HumanHeightInCm Word16 deriving (Real, Integral, Num, Enum, Eq, Ord) --- | Symbolic version of 'HumanHeightInCm'.+-- | Symbolic version of t'HumanHeightInCm'. type SHumanHeightInCm = SBV HumanHeightInCm --- | Symbolic instance simply follows the underlying type, just like 'Metres'.+-- | Symbolic instance simply follows the underlying type, just like t'Metres'. instance HasKind HumanHeightInCm where kindOf _ = KBounded False 16
Documentation/SBV/Examples/Transformers/SymbolicEval.hs view
@@ -6,7 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental ----- A demonstration of the use of the 'SymbolicT' and 'QueryT' transformers in+-- A demonstration of the use of the t'SymbolicT' and t'QueryT' transformers in -- the setting of symbolic program evaluation. -- -- In this example, we perform symbolic evaluation across three steps:@@ -30,8 +30,6 @@ module Documentation.SBV.Examples.Transformers.SymbolicEval where -import Data.SBV (getValue)- import Control.Monad.Except (Except, ExceptT, MonadError, mapExceptT, runExceptT, throwError) import Control.Monad.Identity (Identity(runIdentity)) import Control.Monad.IO.Class (MonadIO)@@ -72,7 +70,7 @@ alloc "" = throwError "tried to allocate unnamed value" alloc nm = free nm --- | Allocate an 'Env' holding all input variables for the program.+-- | Allocate an t'Env' holding all input variables for the program. allocEnv :: Alloc Env allocEnv = do x <- alloc "x"@@ -133,28 +131,28 @@ -- output. newtype Result = Result SVal --- | Makes a 'Result' from a symbolic value.+-- | Makes a t'Result' from a symbolic value. mkResult :: SBV a -> Result mkResult = Result . unSBV --- | Performs symbolic evaluation of a 'Program'.+-- | Performs symbolic evaluation of a t'Program'. runProgramEval :: Env -> Program a -> Except String Result runProgramEval env (Program term) = mkResult <$> runEval env term -- * Property evaluation --- | A property describes a quality of a 'Program'. It is a 'Term' yields a+-- | A property describes a quality of a t'Program'. It is a 'Term' yields a -- boolean value. newtype Property = Property (Term Bool) --- | Performs symbolic evaluation of a 'Property.+-- | Performs symbolic evaluation of a t'Property. runPropertyEval :: Result -> Env -> Property -> Except String (SBV Bool) runPropertyEval (Result res) env (Property term) = runEval (env { result = Just res }) term -- * Checking whether a program satisfies a property --- | The result of 'check'ing the combination of a 'Program' and a 'Property'.+-- | The result of 'check'ing the combination of a t'Program' and a t'Property'. data CheckResult = Proved | Counterexample Integer Integer deriving (Eq, Show) @@ -177,7 +175,7 @@ DSat{} -> throwError "delta-sat" Unk -> throwError "unknown" --- | Checks a 'Property' of a 'Program' (or fails).+-- | Checks a t'Property' of a t'Program' (or fails). check :: Program a -> Property -> IO (Either String CheckResult) check program prop = runExceptT $ runSMTWith z3 $ do env <- runAlloc allocEnv
Documentation/SBV/Examples/WeakestPreconditions/Basics.hs view
@@ -45,7 +45,7 @@ } deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable) --- | Show instance for 'IncS'. The above deriving clause would work just as well,+-- | Show instance for t'IncS'. The above deriving clause would work just as well, -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive. instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (IncS (SBV a)) where show (IncS x y) = "{x = " ++ sh x ++ ", y = " ++ sh y ++ "}"
Documentation/SBV/Examples/WeakestPreconditions/Fib.hs view
@@ -48,7 +48,7 @@ } deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable) --- | Show instance for 'FibS'. The above deriving clause would work just as well,+-- | Show instance for t'FibS'. The above deriving clause would work just as well, -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive. instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (FibS (SBV a)) where show (FibS n i k m) = "{n = " ++ sh n ++ ", i = " ++ sh i ++ ", k = " ++ sh k ++ ", m = " ++ sh m ++ "}"
Documentation/SBV/Examples/WeakestPreconditions/GCD.hs view
@@ -54,7 +54,7 @@ } deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable) --- | Show instance for 'GCDS'. The above deriving clause would work just as well,+-- | Show instance for t'GCDS'. The above deriving clause would work just as well, -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive. instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (GCDS (SBV a)) where show (GCDS x y i j) = "{x = " ++ sh x ++ ", y = " ++ sh y ++ ", i = " ++ sh i ++ ", j = " ++ sh j ++ "}"
Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs view
@@ -38,7 +38,7 @@ } deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable) --- | Show instance for 'DivS'. The above deriving clause would work just as well,+-- | Show instance for t'DivS'. The above deriving clause would work just as well, -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive. instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (DivS (SBV a)) where show (DivS x y q r) = "{x = " ++ sh x ++ ", y = " ++ sh y ++ ", q = " ++ sh q ++ ", r = " ++ sh r ++ "}"
Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs view
@@ -42,7 +42,7 @@ } deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable) --- | Show instance for 'SqrtS'. The above deriving clause would work just as well,+-- | Show instance for t'SqrtS'. The above deriving clause would work just as well, -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive. instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (SqrtS (SBV a)) where show (SqrtS x sqrt i j) = "{x = " ++ sh x ++ ", sqrt = " ++ sh sqrt ++ ", i = " ++ sh i ++ ", j = " ++ sh j ++ "}"
Documentation/SBV/Examples/WeakestPreconditions/Sum.hs view
@@ -44,13 +44,13 @@ } deriving (Show, Generic, Mergeable, Traversable, Functor, Foldable) --- | Show instance for 'SumS'. The above deriving clause would work just as well,+-- | Show instance for t'SumS'. The above deriving clause would work just as well, -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive. instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (SumS (SBV a)) where show (SumS n i s) = "{n = " ++ sh n ++ ", i = " ++ sh i ++ ", s = " ++ sh s ++ "}" where sh v = maybe "<symbolic>" show (unliteral v) --- | 'Queriable instance for our state+-- | 'Queriable' instance for our state instance Queriable IO (SumS SInteger) where type QueryResult (SumS SInteger) = SumS Integer create = SumS <$> freshVar_ <*> freshVar_ <*> freshVar_
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 11.2+Version : 11.3 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