sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- #
- %
- &
- *
- +
- .
- /
- <
- =
- |
- -
- ~
- _
- All

Index - S

S | Documentation.SBV.Examples.Crypto.RC4
safe | Data.SBV
SafeResult |
1 (Type/Class) | Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV, Data.SBV.Dynamic
safeWith |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
sailors | Documentation.SBV.Examples.Existentials.Diophantine
SArr | Data.SBV.Dynamic
SArray |
1 (Type/Class) | Data.SBV.Internals, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
sAssert | Data.SBV
Sat | Data.SBV.Control
sat | Data.SBV
satCmd | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SatExtField | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
Satisfiable | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SatModel | Data.SBV
SatResult |
1 (Type/Class) | Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV, Data.SBV.Dynamic
Saturday | Documentation.SBV.Examples.Queries.Enums
satWith |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
satWithAll |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
satWithAny |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
SaveTiming | Data.SBV.Internals, Data.SBV
SB | Documentation.SBV.Examples.Uninterpreted.Deduce
sbin | Data.SBV.Internals
sbinI | Data.SBV.Internals
SBinOp | Documentation.SBV.Examples.Queries.FourFours
SBool | Data.SBV.Internals, Data.SBV
sBool | Data.SBV
sBools | Data.SBV
sbox | Documentation.SBV.Examples.Crypto.AES
sboxInverseCorrect | Documentation.SBV.Examples.Crypto.AES
sboxTable | Documentation.SBV.Examples.Crypto.AES
SButton | Documentation.SBV.Examples.Puzzles.HexPuzzle
SBV |
1 (Type/Class) | Data.SBV.Internals, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
SBVApp | Data.SBV.Internals
sbvAvailableSolvers | Data.SBV, Data.SBV.Dynamic
sbvCheckSolverInstallation | Data.SBV, Data.SBV.Dynamic
SBVCodeGen |
1 (Type/Class) | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals
SBVException |
1 (Type/Class) | Data.SBV
2 (Data Constructor) | Data.SBV
sbvExceptionConfig | Data.SBV
sbvExceptionDescription | Data.SBV
sbvExceptionExitCode | Data.SBV
sbvExceptionExpected | Data.SBV
sbvExceptionHint | Data.SBV
sbvExceptionReason | Data.SBV
sbvExceptionReceived | Data.SBV
sbvExceptionSent | Data.SBV
sbvExceptionStdErr | Data.SBV
sbvExceptionStdOut | Data.SBV
SBVExpr | Data.SBV.Internals
SBVPgm |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
sbvQuickCheck | Data.SBV
SBVRunMode | Data.SBV.Internals
sbvToSW | Data.SBV.Internals
sbvToSymSW | Data.SBV.Internals
SBVType |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
sbvUninterpret | Data.SBV
sCase | Documentation.SBV.Examples.Queries.FourFours
SChar | Data.SBV.Internals, Data.SBV
sChar | Data.SBV
sChars | Data.SBV
SColor | Documentation.SBV.Examples.Puzzles.HexPuzzle
sCountLeadingZeros | Data.SBV
sCountTrailingZeros | Data.SBV
scriptBody | Data.SBV.Internals
scriptModel | Data.SBV.Internals
sCrossTime | Documentation.SBV.Examples.Puzzles.U2Bridge
SDay | Documentation.SBV.Examples.Queries.Enums
sDiv | Data.SBV
SDivisible | Data.SBV
sDivMod | Data.SBV
SDouble | Data.SBV.Internals, Data.SBV
sDouble | Data.SBV
sDoubleAsSWord64 | Data.SBV
sDoubles | Data.SBV
SE | Documentation.SBV.Examples.Misc.Enumerate
search | Documentation.SBV.Examples.Puzzles.HexPuzzle
select | Data.SBV
selectRe | Documentation.SBV.Examples.Strings.SQLInjection
sElem | Data.SBV
sendMoreMoney | Documentation.SBV.Examples.Puzzles.SendMoreMoney
sendRequestToSolver | Data.SBV.Internals
sendStringToSolver | Data.SBV.Internals
SeqConcat | Data.SBV.Internals
SeqContains | Data.SBV.Internals
SeqIndexOf | Data.SBV.Internals
SeqLen | Data.SBV.Internals
SeqOp |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SeqPrefixOf | Data.SBV.Internals
SeqReplace | Data.SBV.Internals
SeqSubseq | Data.SBV.Internals
SeqSuffixOf | Data.SBV.Internals
SeqUnit | Data.SBV.Internals
setBit | Data.SBV
setBitTo | Data.SBV
setFlag | Documentation.SBV.Examples.BitPrecise.Legato
SetInfo | Data.SBV.Control
setInfo | Data.SBV.Internals, Data.SBV
SetLogic | Data.SBV.Control
setLogic | Data.SBV.Internals, Data.SBV
setOption | Data.SBV.Internals, Data.SBV
setReg | Documentation.SBV.Examples.BitPrecise.Legato
setTimeOut | Data.SBV.Internals, Data.SBV
SExecutable | Data.SBV
sexprToVal | Data.SBV.Control
sExtractBits | Data.SBV
SFiniteBits | Data.SBV
sFiniteBitSize | Data.SBV
SFloat | Data.SBV.Internals, Data.SBV
sFloat | Data.SBV
sFloatAsSWord32 | Data.SBV
sFloats | Data.SBV
sFromIntegral | Data.SBV
sFromIntegralChecked | Data.SBV.Tools.Overflow
sFromIntegralO | Data.SBV.Tools.Overflow
SFunArr | Data.SBV.Dynamic
SFunArray |
1 (Type/Class) | Data.SBV.Internals, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
sgcd | Documentation.SBV.Examples.CodeGeneration.GCD
sgcdIsCorrect | Documentation.SBV.Examples.CodeGeneration.GCD
shannon | Documentation.SBV.Examples.Uninterpreted.Shannon
shannon2 | Documentation.SBV.Examples.Uninterpreted.Shannon
shex | Data.SBV.Internals
shexI | Data.SBV.Internals
shift | Data.SBV
shiftL | Data.SBV
shiftLeft | Documentation.SBV.Examples.CodeGeneration.Uninterpreted
shiftR | Data.SBV
Shl | Data.SBV.Internals
showCDouble | Data.SBV.Internals
showCFloat | Data.SBV.Internals
showHDouble | Data.SBV.Internals
showHFloat | Data.SBV.Internals
showModel | Data.SBV.Internals
showPoly | Data.SBV.Tools.Polynomial
showPolynomial | Data.SBV.Tools.Polynomial
showSMTDouble | Data.SBV.Internals
showSMTFloat | Data.SBV.Internals
showTDiff | Data.SBV.Internals
showType | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
Shr | Data.SBV.Internals
sInfinity | Data.SBV.Internals, Data.SBV
singleton |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
SInt16 | Data.SBV.Internals, Data.SBV
sInt16 | Data.SBV
sInt16s | Data.SBV
SInt32 | Data.SBV.Internals, Data.SBV
sInt32 | Data.SBV
sInt32s | Data.SBV
SInt64 | Data.SBV.Internals, Data.SBV
sInt64 | Data.SBV
sInt64s | Data.SBV
SInt8 | Data.SBV.Internals, Data.SBV
sInt8 | Data.SBV
sInt8s | Data.SBV
SInteger | Data.SBV.Internals, Data.SBV
sInteger | Data.SBV
sIntegers | Data.SBV
SIntegral | Data.SBV
sIntN | Data.SBV.Dynamic
sIntN_ | Data.SBV.Dynamic
SList | Data.SBV.Internals, Data.SBV
sList | Data.SBV
sLists | Data.SBV
SLocation | Documentation.SBV.Examples.Puzzles.U2Bridge
smax | Data.SBV
smin | Data.SBV
sMod | Data.SBV
SMTConfig |
1 (Type/Class) | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SMTErrorBehavior | Data.SBV.Control
SMTInfoFlag | Data.SBV.Control
SMTInfoResponse | Data.SBV.Control
SMTLib2 | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SMTLibPgm |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
smtLibPgm | Data.SBV.Internals
smtLibReservedNames | Data.SBV.Internals
SMTLibVersion | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
smtLibVersion | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
smtLibVersionExtension | Data.SBV.Internals
SMTMode | Data.SBV.Internals
SMTModel |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SMTOption | Data.SBV.Control
SMTProblem |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SMTReasonUnknown | Data.SBV
SMTResult | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
smtRoundingMode | Data.SBV.Internals
SMTScript |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SMTSolver |
1 (Type/Class) | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SMTValue | Data.SBV.Control
SMTVerbosity | Data.SBV.Control
sName | Data.SBV
sName_ | Data.SBV
sNaN | Data.SBV.Internals, Data.SBV
softConstrain | Data.SBV.Internals, Data.SBV
Solution |
1 (Type/Class) | Documentation.SBV.Examples.Existentials.Diophantine
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.NQueens
solve | Data.SBV
solveAll | Documentation.SBV.Examples.Puzzles.Sudoku
solveCrossword | Documentation.SBV.Examples.Strings.RegexCrossword
solveEuler185 | Documentation.SBV.Examples.Puzzles.Euler185
solveN | Documentation.SBV.Examples.Puzzles.U2Bridge
Solver | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
solver | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SolverCapabilities |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SolverContext | Data.SBV.Internals
solverSetOptions | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
solveU2 | Documentation.SBV.Examples.Puzzles.U2Bridge
split | Data.SBV
Splittable | Data.SBV
sPopCount | Data.SBV
Sport | Documentation.SBV.Examples.Puzzles.Fish
SQLExpr | Documentation.SBV.Examples.Strings.SQLInjection
Sqrt | Documentation.SBV.Examples.Queries.FourFours
sQuot | Data.SBV
sQuotRem | Data.SBV
SReal | Data.SBV.Internals, Data.SBV
sReal | Data.SBV
sReals | Data.SBV
sRealToSInteger | Data.SBV
sRem | Data.SBV
sRNA | Data.SBV.Internals, Data.SBV
sRNE | Data.SBV.Internals, Data.SBV
sRotateLeft | Data.SBV
sRotateRight | Data.SBV
SRoundingMode | Data.SBV.Internals, Data.SBV
sRoundNearestTiesToAway | Data.SBV.Internals, Data.SBV
sRoundNearestTiesToEven | Data.SBV.Internals, Data.SBV
sRoundTowardNegative | Data.SBV.Internals, Data.SBV
sRoundTowardPositive | Data.SBV.Internals, Data.SBV
sRoundTowardZero | Data.SBV.Internals, Data.SBV
sRTN | Data.SBV.Internals, Data.SBV
sRTP | Data.SBV.Internals, Data.SBV
sRTZ | Data.SBV.Internals, Data.SBV
sShiftLeft | Data.SBV
sShiftRight | Data.SBV
sSignedShiftArithRight | Data.SBV
SState | Documentation.SBV.Examples.Lists.BoundedMutex
SString | Data.SBV.Internals, Data.SBV
sString | Data.SBV
sStrings | Data.SBV
start | Documentation.SBV.Examples.Puzzles.U2Bridge
State |
1 (Type/Class) | Data.SBV.Internals
2 (Type/Class) | Documentation.SBV.Examples.Crypto.AES
3 (Type/Class) | Documentation.SBV.Examples.Lists.BoundedMutex
statementRe | Documentation.SBV.Examples.Strings.SQLInjection
Status |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.U2Bridge
sTestBit | Data.SBV
STime | Documentation.SBV.Examples.Puzzles.U2Bridge
StrConcat | Data.SBV.Internals
StrContains | Data.SBV.Internals
STree | Data.SBV.Tools.STree
StrIndexOf | Data.SBV.Internals
StrInRe | Data.SBV.Internals
StrLen | Data.SBV.Internals
StrNatToStr | Data.SBV.Internals
StrOp |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
StrPrefixOf | Data.SBV.Internals
strRe | Documentation.SBV.Examples.Strings.SQLInjection
StrReplace | Data.SBV.Internals
StrStrToNat | Data.SBV.Internals
StrSubstr | Data.SBV.Internals
StrSuffixOf | Data.SBV.Internals
strToCharAt | Data.SBV.String
strToNat | Data.SBV.String
strToStrAt | Data.SBV.String
StrUnit | Data.SBV.Internals
SU2Member | Documentation.SBV.Examples.Puzzles.U2Bridge
subList | Data.SBV.List
subStr | Data.SBV.String
sudoku | Documentation.SBV.Examples.Puzzles.Sudoku
Sunday | Documentation.SBV.Examples.Queries.Enums
SUnOp | Documentation.SBV.Examples.Queries.FourFours
supportsApproxReals | Data.SBV.Internals
supportsCustomQueries | Data.SBV.Internals
supportsFlattenedSequences | Data.SBV.Internals
supportsGlobalDecls | Data.SBV.Internals
supportsIEEE754 | Data.SBV.Internals
supportsOptimization | Data.SBV.Internals
supportsPseudoBooleans | Data.SBV.Internals
supportsQuantifiers | Data.SBV.Internals
supportsReals | Data.SBV.Internals
supportsUnboundedInts | Data.SBV.Internals
supportsUninterpretedSorts | Data.SBV.Internals
svAbs | Data.SBV.Dynamic
svAddConstant | Data.SBV.Dynamic
SVal |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals
svAnd | Data.SBV.Dynamic
svAsBool | Data.SBV.Dynamic
svAsInteger | Data.SBV.Dynamic
svBlastBE | Data.SBV.Dynamic
svBlastLE | Data.SBV.Dynamic
svBool | Data.SBV.Dynamic
svCgInput | Data.SBV.Internals, Data.SBV.Dynamic
svCgInputArr | Data.SBV.Internals, Data.SBV.Dynamic
svCgOutput | Data.SBV.Internals, Data.SBV.Dynamic
svCgOutputArr | Data.SBV.Internals, Data.SBV.Dynamic
svCgReturn | Data.SBV.Internals, Data.SBV.Dynamic
svCgReturnArr | Data.SBV.Internals, Data.SBV.Dynamic
svDecrement | Data.SBV.Dynamic
svDenominator | Data.SBV.Dynamic
svDivide | Data.SBV.Dynamic
svDouble | Data.SBV.Dynamic
svEnumFromThenTo | Data.SBV.Dynamic
svEqual | Data.SBV.Dynamic
svExp | Data.SBV.Dynamic
svExtract | Data.SBV.Dynamic
svFalse | Data.SBV.Dynamic
svFloat | Data.SBV.Dynamic
svFromIntegral | Data.SBV.Dynamic
svFromWord1 | Data.SBV.Dynamic
svGreaterEq | Data.SBV.Dynamic
svGreaterThan | Data.SBV.Dynamic
svIncrement | Data.SBV.Dynamic
svInteger | Data.SBV.Dynamic
svIte | Data.SBV.Dynamic
svJoin | Data.SBV.Dynamic
svLazyIte | Data.SBV.Dynamic
svLessEq | Data.SBV.Dynamic
svLessThan | Data.SBV.Dynamic
svMinus | Data.SBV.Dynamic
svMkSymVar | Data.SBV.Dynamic
svNot | Data.SBV.Dynamic
svNotEqual | Data.SBV.Dynamic
svNumerator | Data.SBV.Dynamic
svOr | Data.SBV.Dynamic
svPlus | Data.SBV.Dynamic
svQuickCheck | Data.SBV.Dynamic
svQuot | Data.SBV.Dynamic
svQuotRem | Data.SBV.Dynamic
svReal | Data.SBV.Dynamic
svRem | Data.SBV.Dynamic
svRol | Data.SBV.Dynamic
svRor | Data.SBV.Dynamic
svRotateLeft | Data.SBV.Dynamic
svRotateRight | Data.SBV.Dynamic
svSelect | Data.SBV.Dynamic
svSetBit | Data.SBV.Dynamic
svShiftLeft | Data.SBV.Dynamic
svShiftRight | Data.SBV.Dynamic
svShl | Data.SBV.Dynamic
svShr | Data.SBV.Dynamic
svSign | Data.SBV.Dynamic
svSymbolicMerge | Data.SBV.Dynamic
svTestBit | Data.SBV.Dynamic
svTimes | Data.SBV.Dynamic
svToWord1 | Data.SBV.Dynamic
svTrue | Data.SBV.Dynamic
svUNeg | Data.SBV.Dynamic
svUninterpreted | Data.SBV.Dynamic
svUnsign | Data.SBV.Dynamic
svWordFromBE | Data.SBV.Dynamic
svWordFromLE | Data.SBV.Dynamic
svXOr | Data.SBV.Dynamic
SW |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
swap | Documentation.SBV.Examples.Crypto.RC4
Swede | Documentation.SBV.Examples.Puzzles.Fish
SWord16 | Data.SBV.Internals, Data.SBV
sWord16 | Data.SBV
sWord16s | Data.SBV
SWord32 | Data.SBV.Internals, Data.SBV
sWord32 | Data.SBV
sWord32AsSFloat | Data.SBV
sWord32s | Data.SBV
SWord4 | Documentation.SBV.Examples.Misc.Word4
SWord48 | Documentation.SBV.Examples.Existentials.CRCPolynomial
SWord64 | Data.SBV.Internals, Data.SBV
sWord64 | Data.SBV
sWord64AsSDouble | Data.SBV
sWord64s | Data.SBV
SWord8 | Data.SBV.Internals, Data.SBV
sWord8 | Data.SBV
sWord8s | Data.SBV
sWordN | Data.SBV.Dynamic
sWordN_ | Data.SBV.Dynamic
SymArray | Data.SBV.Internals, Data.SBV
Symbolic | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
symbolic | Data.SBV.Internals, Data.SBV
symbolicMerge | Data.SBV
symbolics | Data.SBV.Internals, Data.SBV
SymWord | Data.SBV.Internals, Data.SBV