sbv-8.7: 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 |
1 (Type/Class) | Documentation.SBV.Examples.Crypto.RC4
2 (Type/Class) | Documentation.SBV.Examples.ProofTools.BMC
3 (Data Constructor) | Documentation.SBV.Examples.ProofTools.BMC
4 (Type/Class) | Documentation.SBV.Examples.ProofTools.Fibonacci
5 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Fibonacci
6 (Type/Class) | Documentation.SBV.Examples.ProofTools.Strengthen
7 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Strengthen
8 (Type/Class) | Documentation.SBV.Examples.ProofTools.Sum
9 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Sum
10 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
11 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Length
12 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Sum
s |
1 (Function) | Documentation.SBV.Examples.ProofTools.Sum
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
safe |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
SafeResult |
1 (Type/Class) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
safeWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
3 (Function) | Data.SBV.Dynamic
sailors | Documentation.SBV.Examples.Existentials.Diophantine
sAll | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sAnd | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sAny | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SArr | Data.SBV.Dynamic
SArray |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
sAssert | Data.SBV.Trans, Data.SBV
Sat |
1 (Data Constructor) | Data.SBV.Trans.Control, Data.SBV.Control
2 (Data Constructor) | Documentation.SBV.Examples.Optimization.Enumerate
sat |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
satCmd | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
satConcurrentWithAll |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Dynamic
satConcurrentWithAny |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Dynamic
SatExtField | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Satisfiable | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SatModel | Data.SBV.Trans, Data.SBV
SatResult |
1 (Type/Class) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
satTrackUFs | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Saturday | Documentation.SBV.Examples.Queries.Enums
satWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
3 (Function) | Data.SBV.Dynamic
satWithAll |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Dynamic
satWithAny |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Dynamic
SaveTiming | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SB | Documentation.SBV.Examples.Uninterpreted.Deduce
sBarrelRotateLeft | Data.SBV.Trans, Data.SBV
sBarrelRotateRight | Data.SBV.Trans, Data.SBV
sbin | Data.SBV.Internals
sbinI | Data.SBV.Internals
SBinOp | Documentation.SBV.Examples.Queries.FourFours
SBool | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sBool |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sBools |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sBool_ | 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.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
SBVApp | Data.SBV.Internals
sbvAvailableSolvers | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
sbvCheckSolverInstallation | Data.SBV.Trans, 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.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Trans, Data.SBV
sbvExceptionConfig | Data.SBV.Trans, Data.SBV
sbvExceptionDescription | Data.SBV.Trans, Data.SBV
sbvExceptionExitCode | Data.SBV.Trans, Data.SBV
sbvExceptionExpected | Data.SBV.Trans, Data.SBV
sbvExceptionHint | Data.SBV.Trans, Data.SBV
sbvExceptionReason | Data.SBV.Trans, Data.SBV
sbvExceptionReceived | Data.SBV.Trans, Data.SBV
sbvExceptionSent | Data.SBV.Trans, Data.SBV
sbvExceptionStdErr | Data.SBV.Trans, Data.SBV
sbvExceptionStdOut | Data.SBV.Trans, Data.SBV
SBVExpr | Data.SBV.Internals
SBVPgm |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
sbvQuickCheck | Data.SBV.Trans, Data.SBV
SBVRunMode | Data.SBV.Internals
sbvToSV | Data.SBV.Internals
sbvToSymSV | Data.SBV.Internals
SBVType |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
sbvUninterpret | Data.SBV.Trans, Data.SBV
sCase | Documentation.SBV.Examples.Queries.FourFours
SChar | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sChar |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sChars |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sChar_ | Data.SBV
SColor | Documentation.SBV.Examples.Puzzles.HexPuzzle
sCountLeadingZeros | Data.SBV.Trans, Data.SBV
sCountTrailingZeros | Data.SBV.Trans, Data.SBV
scriptBody | Data.SBV.Internals
scriptModel | Data.SBV.Internals
sCrossTime | Documentation.SBV.Examples.Puzzles.U2Bridge
SDay |
1 (Type/Class) | Documentation.SBV.Examples.Optimization.Enumerate
2 (Type/Class) | Documentation.SBV.Examples.Queries.Enums
sDiv | Data.SBV.Trans, Data.SBV
SDivisible | Data.SBV.Trans, Data.SBV
sDivMod | Data.SBV.Trans, Data.SBV
SDouble | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sDouble |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sDoubleAsComparableSWord64 | Data.SBV.Internals
sDoubleAsSWord64 | Data.SBV.Trans, Data.SBV
sDoubles |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sDouble_ | Data.SBV
SE | Documentation.SBV.Examples.Misc.Enumerate
search | Documentation.SBV.Examples.Puzzles.HexPuzzle
second | Data.SBV.Either
secondQuery | Documentation.SBV.Examples.Queries.Concurrency
SEither | Data.SBV.Internals, Data.SBV
sEither | Data.SBV
sEithers | Data.SBV
sEither_ | Data.SBV
select | Data.SBV.Trans, Data.SBV
selectRe | Documentation.SBV.Examples.Strings.SQLInjection
sElem | Data.SBV.Trans, Data.SBV
sendMoreMoney | Documentation.SBV.Examples.Puzzles.SendMoreMoney
sendRequestToSolver | Data.SBV.Internals
sendStringToSolver | Data.SBV.Internals
Seq | Data.SBV.Tools.WeakestPreconditions
SeqConcat | Data.SBV.Internals
SeqContains | Data.SBV.Internals
SeqIndexOf | Data.SBV.Internals
SeqLen | Data.SBV.Internals
SeqNth | 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.Trans, Data.SBV
setBitTo | Data.SBV.Trans, Data.SBV
setFlag | Documentation.SBV.Examples.BitPrecise.Legato
SetInfo | Data.SBV.Trans.Control, Data.SBV.Control
setInfo | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SetLogic | Data.SBV.Trans.Control, Data.SBV.Control
setLogic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SetOp | Data.SBV.Internals
setOption | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
setReg | Documentation.SBV.Examples.BitPrecise.Legato
setTimeOut | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
setup | Data.SBV.Tools.WeakestPreconditions
SExecutable | Data.SBV.Trans, Data.SBV
sExtractBits | Data.SBV.Trans, Data.SBV
sFalse | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SFiniteBits | Data.SBV.Trans, Data.SBV
sFiniteBitSize | Data.SBV.Trans, Data.SBV
SFloat | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sFloat |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sFloatAsComparableSWord32 | Data.SBV.Internals
sFloatAsSWord32 | Data.SBV.Trans, Data.SBV
sFloats |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sFloat_ | Data.SBV
sFromIntegral | Data.SBV.Trans, 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.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
sgcd | Documentation.SBV.Examples.CodeGeneration.GCD
sgcdIsCorrect | Documentation.SBV.Examples.CodeGeneration.GCD
SHA |
1 (Type/Class) | Documentation.SBV.Examples.Crypto.SHA
2 (Data Constructor) | Documentation.SBV.Examples.Crypto.SHA
sha224 | Documentation.SBV.Examples.Crypto.SHA
sha224P | Documentation.SBV.Examples.Crypto.SHA
sha256 | Documentation.SBV.Examples.Crypto.SHA
sha256P | Documentation.SBV.Examples.Crypto.SHA
sha384 | Documentation.SBV.Examples.Crypto.SHA
sha384P | Documentation.SBV.Examples.Crypto.SHA
sha512 | Documentation.SBV.Examples.Crypto.SHA
sha512P | Documentation.SBV.Examples.Crypto.SHA
sha512_224 | Documentation.SBV.Examples.Crypto.SHA
sha512_224P | Documentation.SBV.Examples.Crypto.SHA
sha512_256 | Documentation.SBV.Examples.Crypto.SHA
sha512_256P | Documentation.SBV.Examples.Crypto.SHA
shaConstants | Documentation.SBV.Examples.Crypto.SHA
shaLoopCount | Documentation.SBV.Examples.Crypto.SHA
shannon | Documentation.SBV.Examples.Uninterpreted.Shannon
shannon2 | Documentation.SBV.Examples.Uninterpreted.Shannon
shaP | Documentation.SBV.Examples.Crypto.SHA
shared | Documentation.SBV.Examples.Queries.Concurrency
sharedDependent | Documentation.SBV.Examples.Queries.Concurrency
shex | Data.SBV.Internals
shexI | Data.SBV.Internals
shift | Data.SBV.Trans, Data.SBV
shiftL | Data.SBV.Trans, Data.SBV
shiftLeft | Documentation.SBV.Examples.CodeGeneration.Uninterpreted
shiftR | Data.SBV.Trans, Data.SBV
Shl | Data.SBV.Internals
showCDouble | Data.SBV.Internals
showCFloat | Data.SBV.Internals
showHash | Documentation.SBV.Examples.Crypto.SHA
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.Trans, Data.SBV, Data.SBV.Dynamic
Shr | Data.SBV.Internals
SHumanHeightInCm | Documentation.SBV.Examples.Misc.Newtypes
SI | Documentation.SBV.Examples.Misc.SetAlgebra
sigma0 | Documentation.SBV.Examples.Crypto.SHA
sigma0Coefficients | Documentation.SBV.Examples.Crypto.SHA
sigma1 | Documentation.SBV.Examples.Crypto.SHA
sigma1Coefficients | Documentation.SBV.Examples.Crypto.SHA
signExtend | Data.SBV.Trans, Data.SBV
sInfinity | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
singleton |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.Set
3 (Function) | Data.SBV.List
SInt | Data.SBV.Trans, Data.SBV
sInt |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
SInt16 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInt16 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt16s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt16_ | Data.SBV
SInt32 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInt32 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt32s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt32_ | Data.SBV
SInt64 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInt64 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt64s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt64_ | Data.SBV
SInt8 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInt8 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt8s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt8_ | Data.SBV
SInteger | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInteger |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sIntegers |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInteger_ | Data.SBV
SIntegral | Data.SBV.Trans, Data.SBV
sIntN | Data.SBV.Dynamic
sIntN_ | Data.SBV.Dynamic
sInts |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt_ | Data.SBV
sJust | Data.SBV.Maybe
Skip | Data.SBV.Tools.WeakestPreconditions
sLeft | Data.SBV.Either
SList | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sList |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sLists |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sList_ | Data.SBV
SLocation | Documentation.SBV.Examples.Puzzles.U2Bridge
smax | Data.SBV.Trans, Data.SBV
SMaybe | Data.SBV.Internals, Data.SBV
sMaybe | Data.SBV
sMaybes | Data.SBV
sMaybe_ | Data.SBV
SMetres | Documentation.SBV.Examples.Misc.Newtypes
smin | Data.SBV.Trans, Data.SBV
sMod | Data.SBV.Trans, Data.SBV
SMTConfig |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SMTErrorBehavior | Data.SBV.Trans.Control, Data.SBV.Control
SMTInfoFlag | Data.SBV.Trans.Control, Data.SBV.Control
SMTInfoResponse | Data.SBV.Trans.Control, Data.SBV.Control
SMTLib2 | Data.SBV.Internals, Data.SBV.Trans, 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.Trans, Data.SBV, Data.SBV.Dynamic
smtLibVersion | Data.SBV.Internals, Data.SBV.Trans, 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.Trans.Control, Data.SBV.Control
SMTProblem |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SMTReasonUnknown | Data.SBV.Trans, Data.SBV
SMTResult | Data.SBV.Internals, Data.SBV.Trans, 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.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SMTVerbosity | Data.SBV.Trans.Control, Data.SBV.Control
sName |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sName_ |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sNaN | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
snoc |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
sNot | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sNotElem | Data.SBV.Trans, Data.SBV
sNothing | Data.SBV.Maybe
sObserve | Data.SBV
softConstrain | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Solution |
1 (Type/Class) | Documentation.SBV.Examples.Existentials.Diophantine
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.NQueens
solve |
1 (Function) | Data.SBV.Trans
2 (Function) | 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.Trans, Data.SBV, Data.SBV.Dynamic
solver | Data.SBV.Internals, Data.SBV.Trans, 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.Trans, Data.SBV, Data.SBV.Dynamic
solveU2 | Documentation.SBV.Examples.Puzzles.U2Bridge
sOr | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sPopCount | Data.SBV.Trans, Data.SBV
Sport | Documentation.SBV.Examples.Puzzles.Fish
SQLExpr | Documentation.SBV.Examples.Strings.SQLInjection
Sqrt | Documentation.SBV.Examples.Queries.FourFours
sqrt | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
SqrtS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
sQuot | Data.SBV.Trans, Data.SBV
sQuotRem | Data.SBV.Trans, Data.SBV
SReal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sReal |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sReals |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sRealToSInteger | Data.SBV.Trans, Data.SBV
sReal_ | Data.SBV
sRem | Data.SBV.Trans, Data.SBV
sRight | Data.SBV.Either
sRNA | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRNE | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRotateLeft | Data.SBV.Trans, Data.SBV
sRotateRight | Data.SBV.Trans, Data.SBV
SRoundingMode | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundNearestTiesToAway | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundNearestTiesToEven | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardNegative | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardPositive | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardZero | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTN | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTP | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTZ | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SSet | Data.SBV.Internals, Data.SBV
sSet | Data.SBV
sSets | Data.SBV
sSet_ | Data.SBV
sShiftLeft | Data.SBV.Trans, Data.SBV
sShiftRight | Data.SBV.Trans, Data.SBV
sSignedShiftArithRight | Data.SBV.Trans, Data.SBV
SState | Documentation.SBV.Examples.Lists.BoundedMutex
SString | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sString |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sStrings |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sString_ | Data.SBV
stability | Data.SBV.Tools.WeakestPreconditions
Stable | Data.SBV.Tools.WeakestPreconditions
stable | Data.SBV.Tools.WeakestPreconditions
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) | Data.SBV.Tools.WeakestPreconditions
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge
3 (Data Constructor) | Documentation.SBV.Examples.Puzzles.U2Bridge
sTestBit | Data.SBV.Trans, Data.SBV
STime | Documentation.SBV.Examples.Puzzles.U2Bridge
Stmt | Data.SBV.Tools.WeakestPreconditions
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
StrNth | 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
sTrue | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
StrUnit | Data.SBV.Internals
Stuck | Data.SBV.Tools.WeakestPreconditions
STuple | Data.SBV.Internals, Data.SBV
sTuple | Data.SBV
STuple2 | Data.SBV.Internals, Data.SBV
STuple3 | Data.SBV.Internals, Data.SBV
STuple4 | Data.SBV.Internals, Data.SBV
STuple5 | Data.SBV.Internals, Data.SBV
STuple6 | Data.SBV.Internals, Data.SBV
STuple7 | Data.SBV.Internals, Data.SBV
STuple8 | Data.SBV.Internals, Data.SBV
sTuples | Data.SBV
sTuple_ | Data.SBV
SU2Member | Documentation.SBV.Examples.Puzzles.U2Bridge
subList | Data.SBV.List
subStr | Data.SBV.String
sudoku | Documentation.SBV.Examples.Puzzles.Sudoku
sum0 | Documentation.SBV.Examples.Crypto.SHA
sum0Coefficients | Documentation.SBV.Examples.Crypto.SHA
sum1 | Documentation.SBV.Examples.Crypto.SHA
sum1Coefficients | Documentation.SBV.Examples.Crypto.SHA
sumCorrect | Documentation.SBV.Examples.ProofTools.Sum
SumS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Sum
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Sum
Sun | Documentation.SBV.Examples.Optimization.Enumerate
Sunday | Documentation.SBV.Examples.Queries.Enums
SUnOp | Documentation.SBV.Examples.Queries.FourFours
supportsApproxReals | Data.SBV.Internals
supportsCustomQueries | Data.SBV.Internals
supportsDataTypes | Data.SBV.Internals
supportsFlattenedModels | 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
supportsSets | Data.SBV.Internals
supportsUnboundedInts | Data.SBV.Internals
supportsUninterpretedSorts | Data.SBV.Internals
SV |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | 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
svBarrelRotateLeft | Data.SBV.Dynamic
svBarrelRotateRight | 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
svStructuralLessThan | 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
swap | Documentation.SBV.Examples.Crypto.RC4
Swede | Documentation.SBV.Examples.Puzzles.Fish
SWord | Data.SBV.Trans, Data.SBV
sWord |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
SWord16 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord16 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord16s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord16_ | Data.SBV
SWord32 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord32 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord32AsSFloat | Data.SBV.Trans, Data.SBV
sWord32s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord32_ | Data.SBV
SWord64 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord64 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord64AsSDouble | Data.SBV.Trans, Data.SBV
sWord64s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord64_ | Data.SBV
SWord8 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord8 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord8s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord8_ | Data.SBV
sWordN | Data.SBV.Dynamic
sWordN_ | Data.SBV.Dynamic
sWords |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord_ | Data.SBV
SymArray | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Symbolic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
symbolic |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
symbolicEnv | Data.SBV.Trans, Data.SBV
symbolicMerge | Data.SBV.Trans, Data.SBV
symbolics |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
SymbolicT | Data.SBV.Trans, Data.SBV
SymTuple | Data.SBV
SymVal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
synthMul22 | Documentation.SBV.Examples.Uninterpreted.Multiply