Hoogle Search
Within LTS Haskell 24.52 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
Program :: Symbolic () -> (st -> SBool) -> Stmt st -> (st -> SBool) -> Stable st -> Program stsbv Data.SBV.Tools.WeakestPreconditions No documentation available.
-
sbv Data.SBV.Tools.WeakestPreconditions The result of a weakest-precondition proof.
Proven :: Bool -> ProofResult ressbv Data.SBV.Tools.WeakestPreconditions The property holds. If Bool is True, then total correctness, otherwise partial.
Pareto :: Maybe Int -> OptimizeStylesbv Data.SBV.Trans Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse.
ParetoResult :: (Bool, [SMTResult]) -> OptimizeResultsbv Data.SBV.Trans No documentation available.
-
sbv Data.SBV.Trans 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.
Penalty :: Rational -> Maybe String -> Penaltysbv Data.SBV.Trans Penalty with a weight and an optional group
type
Predicate = Symbolic SBoolsbv Data.SBV.Trans A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The Symbolic monad captures the underlying representation, and can/should be ignored by the users of the library, unless you are building further utilities on top of SBV itself. Instead, simply use the Predicate type when necessary.
-
sbv Data.SBV.Trans No documentation available.
ProofError :: SMTConfig -> [String] -> Maybe SMTResult -> SMTResultsbv Data.SBV.Trans Prover errored out, with possibly a bogus result