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.
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
-
sbv Data.SBV.Dynamic Set. Can be regular or complemented.
-
sbv Data.SBV.Dynamic No documentation available.
cgSetDriverValues :: [Integer] -> SBVCodeGen ()sbv Data.SBV.Dynamic Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.
isSet :: HasKind a => a -> Boolsbv Data.SBV.Dynamic No documentation available.
solverSetOptions :: SMTConfig -> [SMTOption]sbv Data.SBV.Dynamic Options to set as we start the solver
svSetBit :: SVal -> Int -> SValsbv Data.SBV.Dynamic Set a given bit at index
-
sbv Data.SBV.Internals Set. Can be regular or complemented.
ComplementSet :: Set a -> RCSet asbv Data.SBV.Internals No documentation available.