Hoogle Search

Within LTS Haskell 24.42 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

  1. allSatMaxModelCount :: SMTConfig -> Maybe Int

    sbv Data.SBV.Trans

    In a allSat call, return at most this many models. If nothing, return all.

  2. allSatMaxModelCountReached :: AllSatResult -> Bool

    sbv Data.SBV.Trans

    Did we reach the user given model count limit?

  3. allSatPrintAlong :: SMTConfig -> Bool

    sbv Data.SBV.Trans

    In a allSat call, print models as they are found.

  4. allSatResults :: AllSatResult -> [SMTResult]

    sbv Data.SBV.Trans

    All satisfying models

  5. allSatSolverReturnedDSat :: AllSatResult -> Bool

    sbv Data.SBV.Trans

    Did the solver report delta-satisfiable at the end?

  6. allSatSolverReturnedUnknown :: AllSatResult -> Bool

    sbv Data.SBV.Trans

    Did the solver report unknown at the end?

  7. allSatTrackUFs :: SMTConfig -> Bool

    sbv Data.SBV.Trans

    In a allSat call, should we try to extract values of uninterpreted functions?

  8. allSatWith :: SatisfiableM m a => SMTConfig -> a -> m AllSatResult

    sbv Data.SBV.Trans

    Generalization of allSatWith

  9. allAny :: IO Proof

    sbv Documentation.SBV.Examples.KnuckleDragger.Lists 

    not (all id xs) == any not xs
    A list of booleans is not all true, if any of them is false. We have: 
    >>> allAny
Inductive lemma: allAny
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Result:                               Q.E.D.
[Proven] allAny

  10. allModels :: IO AllSatResult

    sbv Documentation.SBV.Examples.Misc.Auxiliary

    Generate all satisfying assignments for our problem. We have: 

    >>> allModels
Solution #1:
x =  1 :: Integer
y = -1 :: Integer
Solution #2:
x = 1 :: Integer
y = 1 :: Integer
Solution #3:
x = 0 :: Integer
y = 0 :: Integer
Found 3 different solutions.
    Note that solutions 2 and 3 share the value x = 1, since there are multiple values of y that make this particular choice of x satisfy our constraint.

Page 119 of many | Previous | Next