Hoogle Search

Within LTS Haskell 24.34 (ghc-9.10.3)

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

Exact lookup

1. 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 checkSatAssumingWithUnsatisfiableSet

2. ProduceUnsatAssumptions :: Bool -> SMTOption

   sbv	Data.SBV.Trans.Control

   No documentation available.

3. checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult

   sbv	Data.SBV.Trans.Control

   Generalization of checkSatAssuming

4. checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])

   sbv	Data.SBV.Trans.Control

   Generalization of checkSatAssumingWithUnsatisfiableSet

5. module Documentation.SBV.Examples.BitPrecise.PrefixSum

   The PrefixSum algorithm over power-lists and proof of the Ladner-Fischer implementation. See https://www.cs.utexas.edu/~misra/psp.dir/powerlist.pdf and http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf.

6. goodSum :: Symbolic [(Integer, Integer)]

   sbv	Documentation.SBV.Examples.Queries.AllSat

   Find all solutions to x + y .== 10 for positive x and y. This is rather silly to do in the query mode as allSat can do this automatically, but it demonstrates how we can dynamically query the result and put in new constraints based on those.

7. imperativeSum :: Invariant S -> Maybe (Measure S) -> Program S

   sbv	Documentation.SBV.Examples.WeakestPreconditions.Sum

   A program is the algorithm, together with its pre- and post-conditions.

8. module SequenceFormats.FreqSum

   Module to parse and write freqSum files. The freqsum format is defined here: https://rarecoal-docs.readthedocs.io/en/latest/rarecoal-tools.html#vcf2freqsum

9. data FreqSumEntry

   sequence-formats	SequenceFormats.FreqSum

   A Datatype to denote a single freqSum line

10. FreqSumEntry :: Chrom -> Int -> Maybe ByteString -> Maybe Double -> Char -> Char -> [Maybe (Int, Int)] -> FreqSumEntry

    sequence-formats	SequenceFormats.FreqSum

    No documentation available.

Page 177 of many | Previous | Next