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 |
sA | Documentation.SBV.Examples.Misc.Enumerate |
sAdam | Documentation.SBV.Examples.Puzzles.U2Bridge |
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 |
sAlone | Documentation.SBV.Examples.Puzzles.Murder |
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 |
sB | Documentation.SBV.Examples.Misc.Enumerate |
sBar | Documentation.SBV.Examples.Puzzles.Murder |
sBarrelRotateLeft | Data.SBV.Trans, Data.SBV |
sBarrelRotateRight | Data.SBV.Trans, Data.SBV |
sBaseball | Documentation.SBV.Examples.Puzzles.Fish |
sBeach | Documentation.SBV.Examples.Puzzles.Murder |
sBeer | Documentation.SBV.Examples.Puzzles.Fish |
SBeverage | Documentation.SBV.Examples.Puzzles.Fish |
sbin | Data.SBV.Internals |
sbinI | Data.SBV.Internals |
SBinOp | Documentation.SBV.Examples.Queries.FourFours |
sBird | Documentation.SBV.Examples.Puzzles.Fish |
sBlack | Documentation.SBV.Examples.Puzzles.HexPuzzle |
sBlue | |
1 (Function) | Documentation.SBV.Examples.Puzzles.Fish |
2 (Function) | Documentation.SBV.Examples.Puzzles.Garden |
3 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle |
sBono | Documentation.SBV.Examples.Puzzles.U2Bridge |
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 |
sBriton | Documentation.SBV.Examples.Puzzles.Fish |
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 |
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 |
sBystander | Documentation.SBV.Examples.Puzzles.Murder |
sC | Documentation.SBV.Examples.Misc.Enumerate |
sCase | Documentation.SBV.Examples.Queries.FourFours |
sCat | Documentation.SBV.Examples.Puzzles.Fish |
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 |
sCoffee | Documentation.SBV.Examples.Puzzles.Fish |
SColor | |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Fish |
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Garden |
3 (Type/Class) | Documentation.SBV.Examples.Puzzles.HexPuzzle |
sComparableSWord32AsSFloat | Data.SBV.Internals |
sComparableSWord64AsSDouble | Data.SBV.Internals |
sComparableSWordAsSFloatingPoint | Data.SBV.Internals |
sCountLeadingZeros | Data.SBV.Trans, Data.SBV |
sCountTrailingZeros | Data.SBV.Trans, Data.SBV |
scriptBody | Data.SBV.Internals |
scriptModel | Data.SBV.Internals |
sCritical | Documentation.SBV.Examples.Lists.BoundedMutex |
sCrossTime | Documentation.SBV.Examples.Puzzles.U2Bridge |
sDane | Documentation.SBV.Examples.Puzzles.Fish |
SDay | |
1 (Type/Class) | Documentation.SBV.Examples.Optimization.Enumerate |
2 (Type/Class) | Documentation.SBV.Examples.Queries.Enums |
sDiv | Data.SBV.Trans, Data.SBV |
sDivide | Documentation.SBV.Examples.Queries.FourFours |
SDivisible | Data.SBV.Trans, Data.SBV |
sDivMod | Data.SBV.Trans, Data.SBV |
sDog | Documentation.SBV.Examples.Puzzles.Fish |
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 |
sEdge | Documentation.SBV.Examples.Puzzles.U2Bridge |
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 |
Sex | Documentation.SBV.Examples.Puzzles.Murder |
sex | Documentation.SBV.Examples.Puzzles.Murder |
SExecutable | Data.SBV.Trans, Data.SBV |
sExpt | Documentation.SBV.Examples.Queries.FourFours |
sExtractBits | Data.SBV.Trans, Data.SBV |
sFactorial | Documentation.SBV.Examples.Queries.FourFours |
sFalse | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
sFemale | Documentation.SBV.Examples.Puzzles.Murder |
SFiniteBits | Data.SBV.Trans, Data.SBV |
sFiniteBitSize | Data.SBV.Trans, Data.SBV |
sFish | Documentation.SBV.Examples.Puzzles.Fish |
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 |
SFloatingPoint | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
sFloatingPoint | Data.SBV |
sFloatingPointAsComparableSWord | Data.SBV.Internals |
sFloatingPointAsSWord | Data.SBV.Trans, Data.SBV |
sFloatingPoints | Data.SBV |
sFloatingPoint_ | Data.SBV |
sFloats | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
sFloat_ | Data.SBV |
sFootball | Documentation.SBV.Examples.Puzzles.Fish |
SFPDouble | Data.SBV.Internals, Data.SBV |
sFPDouble | Data.SBV |
sFPDoubles | Data.SBV |
sFPDouble_ | Data.SBV |
SFPHalf | Data.SBV.Internals, Data.SBV |
sFPHalf | Data.SBV |
sFPHalfs | Data.SBV |
sFPHalf_ | Data.SBV |
SFPQuad | Data.SBV.Internals, Data.SBV |
sFPQuad | Data.SBV |
sFPQuads | Data.SBV |
sFPQuad_ | Data.SBV |
SFPSingle | Data.SBV.Internals, Data.SBV |
sFPSingle | Data.SBV |
sFPSingles | Data.SBV |
sFPSingle_ | Data.SBV |
sFri | Documentation.SBV.Examples.Optimization.Enumerate |
sFriday | Documentation.SBV.Examples.Queries.Enums |
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 |
sGerman | Documentation.SBV.Examples.Puzzles.Fish |
sGreen | |
1 (Function) | Documentation.SBV.Examples.Puzzles.Fish |
2 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle |
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 |
sHere | Documentation.SBV.Examples.Puzzles.U2Bridge |
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 |
sHockey | Documentation.SBV.Examples.Puzzles.Fish |
sHorse | Documentation.SBV.Examples.Puzzles.Fish |
showBFloat | Data.SBV.Internals |
showCDouble | Data.SBV.Internals |
showCFloat | Data.SBV.Internals |
showFloatAtBase | 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 |
sIdle | Documentation.SBV.Examples.Lists.BoundedMutex |
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 |
sKiller | Documentation.SBV.Examples.Puzzles.Murder |
Skip | Data.SBV.Tools.WeakestPreconditions |
SL | Documentation.SBV.Examples.Uninterpreted.UISortAllSat |
sLarry | Documentation.SBV.Examples.Puzzles.U2Bridge |
sLeft | Data.SBV.Either |
SList | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
sList | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
sListArray | Data.SBV.Internals, Data.SBV |
sLists | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
sList_ | Data.SBV |
SLocation | |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Murder |
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge |
sMale | Documentation.SBV.Examples.Puzzles.Murder |
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 |
sMilk | Documentation.SBV.Examples.Puzzles.Fish |
smin | Data.SBV.Trans, Data.SBV |
sMinus | Documentation.SBV.Examples.Queries.FourFours |
sMod | Data.SBV.Trans, Data.SBV |
sMon | Documentation.SBV.Examples.Optimization.Enumerate |
sMonday | Documentation.SBV.Examples.Queries.Enums |
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 |
SNationality | Documentation.SBV.Examples.Puzzles.Fish |
sNegate | Documentation.SBV.Examples.Queries.FourFours |
snoc | |
1 (Function) | Data.SBV.String |
2 (Function) | Data.SBV.List |
sNorwegian | Documentation.SBV.Examples.Puzzles.Fish |
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 |
SPet | Documentation.SBV.Examples.Puzzles.Fish |
sPlus | Documentation.SBV.Examples.Queries.FourFours |
sPopCount | Data.SBV.Trans, Data.SBV |
Sport | Documentation.SBV.Examples.Puzzles.Fish |
SQ | Documentation.SBV.Examples.Uninterpreted.Sort |
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 |
sReady | Documentation.SBV.Examples.Lists.BoundedMutex |
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 |
sRed | |
1 (Function) | Documentation.SBV.Examples.Puzzles.Fish |
2 (Function) | Documentation.SBV.Examples.Puzzles.Garden |
3 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle |
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 |
SRole | Documentation.SBV.Examples.Puzzles.Murder |
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 |
sSat | Documentation.SBV.Examples.Optimization.Enumerate |
sSaturday | Documentation.SBV.Examples.Queries.Enums |
SSet | Data.SBV.Internals, Data.SBV |
sSet | Data.SBV |
sSets | Data.SBV |
sSet_ | Data.SBV |
SSex | Documentation.SBV.Examples.Puzzles.Murder |
sShiftLeft | Data.SBV.Trans, Data.SBV |
sShiftRight | Data.SBV.Trans, Data.SBV |
sSignedShiftArithRight | Data.SBV.Trans, Data.SBV |
SSport | Documentation.SBV.Examples.Puzzles.Fish |
sSqrt | Documentation.SBV.Examples.Queries.FourFours |
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 |
sSun | Documentation.SBV.Examples.Optimization.Enumerate |
sSunday | Documentation.SBV.Examples.Queries.Enums |
sSwede | Documentation.SBV.Examples.Puzzles.Fish |
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 |
sTea | Documentation.SBV.Examples.Puzzles.Fish |
sTennis | Documentation.SBV.Examples.Puzzles.Fish |
sTestBit | Data.SBV.Trans, Data.SBV |
sThere | Documentation.SBV.Examples.Puzzles.U2Bridge |
sThu | Documentation.SBV.Examples.Optimization.Enumerate |
sThursday | Documentation.SBV.Examples.Queries.Enums |
STime | Documentation.SBV.Examples.Puzzles.U2Bridge |
sTimes | Documentation.SBV.Examples.Queries.FourFours |
Stmt | Data.SBV.Tools.WeakestPreconditions |
StrConcat | Data.SBV.Internals |
StrContains | Data.SBV.Internals |
STree | Data.SBV.Tools.STree |
StrFromCode | Data.SBV.Internals |
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 |
StrToCode | Data.SBV.Internals |
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 |
sTue | Documentation.SBV.Examples.Optimization.Enumerate |
sTuesday | Documentation.SBV.Examples.Queries.Enums |
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 |
supportsBitVectors | Data.SBV.Internals |
supportsCustomQueries | Data.SBV.Internals |
supportsDataTypes | Data.SBV.Internals |
supportsDefineFun | Data.SBV.Internals |
supportsDeltaSat | Data.SBV.Internals |
supportsDirectAccessors | Data.SBV.Internals |
supportsDistinct | Data.SBV.Internals |
supportsFlattenedModels | Data.SBV.Internals |
supportsGlobalDecls | Data.SBV.Internals |
supportsIEEE754 | Data.SBV.Internals |
supportsInt2bv | 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 |
svFloatingPoint | Data.SBV.Dynamic |
svFromIntegral | Data.SBV.Dynamic |
svFromWord1 | Data.SBV.Dynamic |
svGreaterEq | Data.SBV.Dynamic |
svGreaterThan | Data.SBV.Dynamic |
sVictim | Documentation.SBV.Examples.Puzzles.Murder |
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 |
sVolleyball | Documentation.SBV.Examples.Puzzles.Fish |
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 |
sWater | Documentation.SBV.Examples.Puzzles.Fish |
sWed | Documentation.SBV.Examples.Optimization.Enumerate |
Swede | Documentation.SBV.Examples.Puzzles.Fish |
sWednesday | Documentation.SBV.Examples.Queries.Enums |
sWhite | 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 |
sWordAsSFloatingPoint | Data.SBV.Trans, Data.SBV |
sWordN | Data.SBV.Dynamic |
sWordN_ | Data.SBV.Dynamic |
sWords | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
sWord_ | Data.SBV |
sYellow | |
1 (Function) | Documentation.SBV.Examples.Puzzles.Fish |
2 (Function) | Documentation.SBV.Examples.Puzzles.Garden |
sym | Data.SBV.Trans, 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 |