Hoogle Search

Within LTS Haskell 24.32 (ghc-9.10.3)

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

Exact lookup

1. allSatMaxModelCountReached :: AllSatResult -> Bool

   sbv	Data.SBV

   Did we reach the user given model count limit?

2. allSatPartition :: SymVal a => String -> SBV a -> Symbolic ()

   sbv	Data.SBV

   Create a partitioning constraint, for all-sat calls.

3. allSatPrintAlong :: SMTConfig -> Bool

   sbv	Data.SBV

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

4. allSatResults :: AllSatResult -> [SMTResult]

   sbv	Data.SBV

   All satisfying models

5. allSatSolverReturnedDSat :: AllSatResult -> Bool

   sbv	Data.SBV

   Did the solver report delta-satisfiable at the end?

6. allSatSolverReturnedUnknown :: AllSatResult -> Bool

   sbv	Data.SBV

   Did the solver report unknown at the end?

7. allSatTrackUFs :: SMTConfig -> Bool

   sbv	Data.SBV

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

8. allSatWith :: Satisfiable a => SMTConfig -> a -> IO AllSatResult

   sbv	Data.SBV

   Return all satisfying assignments for a predicate. Note that this call will block until all satisfying assignments are found. If you have a problem with infinitely many satisfying models (consider SInteger) or a very large number of them, you might have to wait for a long time. To avoid such cases, use the allSatMaxModelCount parameter 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 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 NB. For a version which generalizes over the underlying monad, see allSatWith

9. allSatMaxModelCount :: SMTConfig -> Maybe Int

   sbv	Data.SBV.Dynamic

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

10. allSatMaxModelCountReached :: AllSatResult -> Bool

    sbv	Data.SBV.Dynamic

    Did we reach the user given model count limit?

Page 117 of many | Previous | Next