Hoogle Search
Within LTS Haskell 24.60 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
RegularSet :: Set a -> RCSet asbv Data.SBV No documentation available.
-
sbv Data.SBV Symbolic Set. Note that we use RCSet, which supports both regular sets and complements, i.e., those obtained from the universal set (of the right type) by removing elements. Similar to SArray the contents are stored with object equality, which makes a difference if the underlying type contains IEEE Floats.
isSet :: HasKind a => a -> Boolsbv Data.SBV No documentation available.
sSet :: (Ord a, SymVal a) => String -> Symbolic (SSet a)sbv Data.SBV Declare a named SSet. NB. For a version which generalizes over the underlying monad, see sSet
sSetBitTo :: SFiniteBits a => SBV a -> SBV a -> SBool -> SBV asbv Data.SBV Variant of setBitTo when the index is symbolic. If the index it out-of-bounds, then the result is underspecified.
sSet_ :: (Ord a, SymVal a) => Symbolic (SSet a)sbv Data.SBV Declare an unnamed SSet. NB. For a version which generalizes over the underlying monad, see sSet_
sSets :: (Ord a, SymVal a) => [String] -> Symbolic [SSet a]sbv Data.SBV Declare a list of SSet values. NB. For a version which generalizes over the underlying monad, see sSets
solverSetOptions :: SMTConfig -> [SMTOption]sbv Data.SBV Options to set as we start the solver
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-
sbv Data.SBV.Control Reset the solver, by forgetting all the assertions. However, bindings are kept as is, as opposed to a full reset of the solver. Use this variant to clean-up the solver state while leaving the bindings intact. Pops all assertion levels. Declarations and definitions resulting from the setLogic command are unaffected. Note that SBV implicitly uses global-declarations, so bindings will remain intact. NB. For a version which generalizes over the underlying monad, see resetAssertions