Hoogle Search
Within LTS Haskell 24.46 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
newtype
MonadSum (f :: Type -> Type) areducers Data.Semigroup.MonadPlus MonadSum :: f a -> MonadSum (f :: Type -> Type) areducers Data.Semigroup.MonadPlus No documentation available.
getMonadSum :: MonadSum (f :: Type -> Type) a -> f areducers Data.Semigroup.MonadPlus No documentation available.
preludeSummary :: PreludeMacro -> Stringregex Text.RE.TDFA a summary of the macros in the standard environment for this back end in plain text
formatMacroSummary :: RegexType -> MacroEnv -> MacroID -> Stringregex Text.RE.TestBench generate a plain text summary of a macro
preludeMacroSummary :: RegexType -> PreludeMacro -> Stringregex Text.RE.ZeInternals generate a textual summary of the prelude macros
ProduceUnsatAssumptions :: Bool -> SMTOptionsbv Data.SBV.Control No documentation available.
checkSatAssuming :: [SBool] -> Query CheckSatResultsbv Data.SBV.Control Check for satisfiability, under the given conditions. Similar to 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.) NB. For a version which generalizes over the underlying monad, see checkSatAssuming
checkSatAssumingWithUnsatisfiableSet :: [SBool] -> Query (CheckSatResult, Maybe [SBool])sbv Data.SBV.Control Check for satisfiability, under the given conditions. Returns the unsatisfiable set of assumptions. Similar to 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. You must have arranged for the production of unsat assumptions first via
setOption $ ProduceUnsatAssumptions True
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 namedConstraint. If getUnsatCore fills your needs, you should definitely prefer it over checkSatAssumingWithUnsatisfiableSet. NB. For a version which generalizes over the underlying monad, see checkSatAssumingWithUnsatisfiableSetProduceUnsatAssumptions :: Bool -> SMTOptionsbv Data.SBV.Trans.Control No documentation available.