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

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
sADocumentation.SBV.Examples.Misc.Enumerate
sAdamDocumentation.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
sailorsDocumentation.SBV.Examples.Existentials.Diophantine
sAllData.SBV.Internals, Data.SBV.Trans, Data.SBV
sAloneDocumentation.SBV.Examples.Puzzles.Murder
sAndData.SBV.Internals, Data.SBV.Trans, Data.SBV
sAnyData.SBV.Internals, Data.SBV.Trans, Data.SBV
SArrData.SBV.Dynamic
SArray 
1 (Type/Class)Data.SBV.Internals, Data.SBV.Trans, Data.SBV
2 (Data Constructor)Data.SBV.Internals
sAssertData.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
satCmdData.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
SatExtFieldData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SatisfiableData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SatModelData.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
satTrackUFsData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SaturdayDocumentation.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
SaveTimingData.SBV.Internals, Data.SBV.Trans, Data.SBV
SBDocumentation.SBV.Examples.Uninterpreted.Deduce
sBDocumentation.SBV.Examples.Misc.Enumerate
sBarDocumentation.SBV.Examples.Puzzles.Murder
sBarrelRotateLeft 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sBarrelRotateRight 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sBaseballDocumentation.SBV.Examples.Puzzles.Fish
sBeachDocumentation.SBV.Examples.Puzzles.Murder
sBeerDocumentation.SBV.Examples.Puzzles.Fish
SBeverageDocumentation.SBV.Examples.Puzzles.Fish
sbinData.SBV.Internals
sbinIData.SBV.Internals
SBinOpDocumentation.SBV.Examples.Queries.FourFours
sBirdDocumentation.SBV.Examples.Puzzles.Fish
sBlackDocumentation.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
sBonoDocumentation.SBV.Examples.Puzzles.U2Bridge
SBoolData.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
sboxDocumentation.SBV.Examples.Crypto.AES
sboxInverseCorrectDocumentation.SBV.Examples.Crypto.AES
sboxTableDocumentation.SBV.Examples.Crypto.AES
sBritonDocumentation.SBV.Examples.Puzzles.Fish
SButtonDocumentation.SBV.Examples.Puzzles.HexPuzzle
SBV 
1 (Type/Class)Data.SBV.Internals, Data.SBV.Trans, Data.SBV
2 (Data Constructor)Data.SBV.Internals
SBVAppData.SBV.Internals
sbvCheckSolverInstallationData.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
sbvExceptionConfigData.SBV.Trans, Data.SBV
sbvExceptionDescriptionData.SBV.Trans, Data.SBV
sbvExceptionExitCodeData.SBV.Trans, Data.SBV
sbvExceptionExpectedData.SBV.Trans, Data.SBV
sbvExceptionHintData.SBV.Trans, Data.SBV
sbvExceptionReasonData.SBV.Trans, Data.SBV
sbvExceptionReceivedData.SBV.Trans, Data.SBV
sbvExceptionSentData.SBV.Trans, Data.SBV
sbvExceptionStdErrData.SBV.Trans, Data.SBV
sbvExceptionStdOutData.SBV.Trans, Data.SBV
sbvExists 
1 (Function)Data.SBV.Internals, Data.SBV.Trans
2 (Function)Data.SBV
sbvExists_ 
1 (Function)Data.SBV.Internals, Data.SBV.Trans
2 (Function)Data.SBV
SBVExprData.SBV.Internals
sbvForall 
1 (Function)Data.SBV.Internals, Data.SBV.Trans
2 (Function)Data.SBV
sbvForall_ 
1 (Function)Data.SBV.Internals, Data.SBV.Trans
2 (Function)Data.SBV
SBVPgm 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
sbvQuickCheckData.SBV.Trans, Data.SBV
SBVReverseData.SBV.Internals
SBVRunModeData.SBV.Internals
sbvToSVData.SBV.Internals
sbvToSymSVData.SBV.Internals
SBVType 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
sbvUninterpretData.SBV.Trans, Data.SBV
sBystanderDocumentation.SBV.Examples.Puzzles.Murder
sCDocumentation.SBV.Examples.Misc.Enumerate
sCaseDocumentation.SBV.Examples.Queries.FourFours
sCatDocumentation.SBV.Examples.Puzzles.Fish
SCharData.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
sCoffeeDocumentation.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
sComparableSWord32AsSFloatData.SBV.Internals
sComparableSWord64AsSDoubleData.SBV.Internals
sComparableSWordAsSFloatingPointData.SBV.Internals
sCountLeadingZerosData.SBV.Trans, Data.SBV
sCountTrailingZerosData.SBV.Trans, Data.SBV
scriptBodyData.SBV.Internals
scriptModelData.SBV.Internals
sCriticalDocumentation.SBV.Examples.Lists.BoundedMutex
sCrossTimeDocumentation.SBV.Examples.Puzzles.U2Bridge
sDaneDocumentation.SBV.Examples.Puzzles.Fish
SDay 
1 (Type/Class)Documentation.SBV.Examples.Optimization.Enumerate
2 (Type/Class)Documentation.SBV.Examples.Queries.Enums
sDivData.SBV.Trans, Data.SBV
sDivideDocumentation.SBV.Examples.Queries.FourFours
SDivisibleData.SBV.Trans, Data.SBV
sDivModData.SBV.Trans, Data.SBV
sDogDocumentation.SBV.Examples.Puzzles.Fish
SDoubleData.SBV.Internals, Data.SBV.Trans, Data.SBV
sDouble 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sDoubleAsComparableSWord64Data.SBV.Internals
sDoubleAsSWord64Data.SBV.Trans, Data.SBV
sDoubles 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sDouble_Data.SBV
SEDocumentation.SBV.Examples.Misc.Enumerate
searchDocumentation.SBV.Examples.Puzzles.HexPuzzle
secondData.SBV.Either
secondQueryDocumentation.SBV.Examples.Queries.Concurrency
sEdgeDocumentation.SBV.Examples.Puzzles.U2Bridge
SEitherData.SBV.Internals, Data.SBV
sEitherData.SBV
sEithersData.SBV
sEither_Data.SBV
selectData.SBV.Trans, Data.SBV
selectReDocumentation.SBV.Examples.Strings.SQLInjection
sElemData.SBV.Trans, Data.SBV
sendMoreMoneyDocumentation.SBV.Examples.Puzzles.SendMoreMoney
sendRequestToSolverData.SBV.Internals
sendStringToSolverData.SBV.Internals
SeqData.SBV.Tools.WeakestPreconditions
SeqConcatData.SBV.Internals
SeqContainsData.SBV.Internals
SeqIndexOfData.SBV.Internals
SeqLenData.SBV.Internals
SeqNthData.SBV.Internals
SeqOp 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
SeqPrefixOfData.SBV.Internals
SeqReplaceData.SBV.Internals
SeqSubseqData.SBV.Internals
SeqSuffixOfData.SBV.Internals
SeqUnitData.SBV.Internals
setBitData.SBV.Trans, Data.SBV
setBitToData.SBV.Trans, Data.SBV
setFlagDocumentation.SBV.Examples.BitPrecise.Legato
SetInfoData.SBV.Trans.Control, Data.SBV.Control
setInfoData.SBV.Internals, Data.SBV.Trans, Data.SBV
SetLogicData.SBV.Trans.Control, Data.SBV.Control
setLogicData.SBV.Internals, Data.SBV.Trans, Data.SBV
SetOpData.SBV.Internals
setOptionData.SBV.Internals, Data.SBV.Trans, Data.SBV
setRegDocumentation.SBV.Examples.BitPrecise.Legato
setTimeOutData.SBV.Internals, Data.SBV.Trans, Data.SBV
setupData.SBV.Tools.WeakestPreconditions
SexDocumentation.SBV.Examples.Puzzles.Murder
sexDocumentation.SBV.Examples.Puzzles.Murder
SExecutableData.SBV.Trans, Data.SBV
sExptDocumentation.SBV.Examples.Queries.FourFours
sExtractBitsData.SBV.Trans, Data.SBV
sFactorialDocumentation.SBV.Examples.Queries.FourFours
sFalseData.SBV.Internals, Data.SBV.Trans, Data.SBV
sFemaleDocumentation.SBV.Examples.Puzzles.Murder
SFiniteBitsData.SBV.Trans, Data.SBV
sFiniteBitSizeData.SBV.Trans, Data.SBV
sFishDocumentation.SBV.Examples.Puzzles.Fish
SFloatData.SBV.Internals, Data.SBV.Trans, Data.SBV
sFloat 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sFloatAsComparableSWord32Data.SBV.Internals
sFloatAsSWord32Data.SBV.Trans, Data.SBV
SFloatingPointData.SBV.Internals, Data.SBV.Trans, Data.SBV
sFloatingPointData.SBV
sFloatingPointAsComparableSWordData.SBV.Internals
sFloatingPointAsSWordData.SBV.Trans, Data.SBV
sFloatingPointsData.SBV
sFloatingPoint_Data.SBV
sFloats 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sFloat_Data.SBV
sFootballDocumentation.SBV.Examples.Puzzles.Fish
SFPBFloatData.SBV.Internals, Data.SBV
sFPBFloatData.SBV
sFPBFloatsData.SBV
sFPBFloat_Data.SBV
SFPDoubleData.SBV.Internals, Data.SBV
sFPDoubleData.SBV
sFPDoublesData.SBV
sFPDouble_Data.SBV
SFPHalfData.SBV.Internals, Data.SBV
sFPHalfData.SBV
sFPHalfsData.SBV
sFPHalf_Data.SBV
SFPQuadData.SBV.Internals, Data.SBV
sFPQuadData.SBV
sFPQuadsData.SBV
sFPQuad_Data.SBV
SFPSingleData.SBV.Internals, Data.SBV
sFPSingleData.SBV
sFPSinglesData.SBV
sFPSingle_Data.SBV
sFriDocumentation.SBV.Examples.Optimization.Enumerate
sFridayDocumentation.SBV.Examples.Queries.Enums
sFromIntegralData.SBV.Trans, Data.SBV
sFromIntegralCheckedData.SBV.Tools.Overflow
sFromIntegralOData.SBV.Tools.Overflow
sgcdDocumentation.SBV.Examples.CodeGeneration.GCD
sgcdIsCorrectDocumentation.SBV.Examples.CodeGeneration.GCD
sGermanDocumentation.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
sha224Documentation.SBV.Examples.Crypto.SHA
sha224PDocumentation.SBV.Examples.Crypto.SHA
sha256Documentation.SBV.Examples.Crypto.SHA
sha256PDocumentation.SBV.Examples.Crypto.SHA
sha384Documentation.SBV.Examples.Crypto.SHA
sha384PDocumentation.SBV.Examples.Crypto.SHA
sha512Documentation.SBV.Examples.Crypto.SHA
sha512PDocumentation.SBV.Examples.Crypto.SHA
sha512_224Documentation.SBV.Examples.Crypto.SHA
sha512_224PDocumentation.SBV.Examples.Crypto.SHA
sha512_256Documentation.SBV.Examples.Crypto.SHA
sha512_256PDocumentation.SBV.Examples.Crypto.SHA
shaConstantsDocumentation.SBV.Examples.Crypto.SHA
shaLoopCountDocumentation.SBV.Examples.Crypto.SHA
shannonDocumentation.SBV.Examples.Uninterpreted.Shannon
shannon2Documentation.SBV.Examples.Uninterpreted.Shannon
shaPDocumentation.SBV.Examples.Crypto.SHA
sharedDocumentation.SBV.Examples.Queries.Concurrency
sharedDependentDocumentation.SBV.Examples.Queries.Concurrency
sHereDocumentation.SBV.Examples.Puzzles.U2Bridge
shexData.SBV.Internals
shexIData.SBV.Internals
shiftData.SBV.Trans, Data.SBV
shiftLData.SBV.Trans, Data.SBV
shiftLeftDocumentation.SBV.Examples.CodeGeneration.Uninterpreted
shiftRData.SBV.Trans, Data.SBV
ShlData.SBV.Internals
sHockeyDocumentation.SBV.Examples.Puzzles.Fish
sHorseDocumentation.SBV.Examples.Puzzles.Fish
showBFloatData.SBV.Internals
showCDoubleData.SBV.Internals
showCFloatData.SBV.Internals
showFloatAtBaseData.SBV.Internals
showHashDocumentation.SBV.Examples.Crypto.SHA
showHDoubleData.SBV.Internals
showHFloatData.SBV.Internals
showModelData.SBV.Internals
showNegativeNumberData.SBV.Internals
showPolyData.SBV.Tools.Polynomial
showPolynomialData.SBV.Tools.Polynomial
showSMTDoubleData.SBV.Internals
showSMTFloatData.SBV.Internals
showTDiffData.SBV.Internals
showTypeData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
ShrData.SBV.Internals
SHumanHeightInCmDocumentation.SBV.Examples.Misc.Newtypes
SIDocumentation.SBV.Examples.Misc.SetAlgebra
sIdleDocumentation.SBV.Examples.Lists.BoundedMutex
sigma0Documentation.SBV.Examples.Crypto.SHA
sigma0CoefficientsDocumentation.SBV.Examples.Crypto.SHA
sigma1Documentation.SBV.Examples.Crypto.SHA
sigma1CoefficientsDocumentation.SBV.Examples.Crypto.SHA
SignExtendData.SBV.Internals
signExtend 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sInfinityData.SBV.Internals, Data.SBV.Trans, Data.SBV
singleton 
1 (Function)Data.SBV.String
2 (Function)Data.SBV.Set
3 (Function)Data.SBV.List
SIntData.SBV.Trans, Data.SBV
sInt 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
SInt16Data.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
SInt32Data.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
SInt64Data.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
SInt8Data.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
SIntegerData.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
SIntegralData.SBV.Trans, Data.SBV
sIntNData.SBV.Dynamic
sIntN_Data.SBV.Dynamic
sInts 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sInt_Data.SBV
sJustData.SBV.Maybe
sKillerDocumentation.SBV.Examples.Puzzles.Murder
SkipData.SBV.Tools.WeakestPreconditions
SLDocumentation.SBV.Examples.Uninterpreted.UISortAllSat
sLarryDocumentation.SBV.Examples.Puzzles.U2Bridge
sLeftData.SBV.Either
SListData.SBV.Internals, Data.SBV.Trans, Data.SBV
sList 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sListArrayData.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
sMaleDocumentation.SBV.Examples.Puzzles.Murder
smaxData.SBV.Trans, Data.SBV
SMaybeData.SBV.Internals, Data.SBV
sMaybeData.SBV
sMaybesData.SBV
sMaybe_Data.SBV
SMetresDocumentation.SBV.Examples.Misc.Newtypes
sMilkDocumentation.SBV.Examples.Puzzles.Fish
sminData.SBV.Trans, Data.SBV
sMinusDocumentation.SBV.Examples.Queries.FourFours
sModData.SBV.Trans, Data.SBV
sMonDocumentation.SBV.Examples.Optimization.Enumerate
sMondayDocumentation.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
SMTErrorBehaviorData.SBV.Trans.Control, Data.SBV.Control
SMTInfoFlagData.SBV.Trans.Control, Data.SBV.Control
SMTInfoResponseData.SBV.Trans.Control, Data.SBV.Control
SMTLib2Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SMTLibPgm 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
smtLibPgmData.SBV.Internals
smtLibReservedNamesData.SBV.Internals
SMTLibVersionData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
smtLibVersionData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
smtLibVersionExtensionData.SBV.Internals
SMTModeData.SBV.Internals
SMTModel 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
SMTOptionData.SBV.Trans.Control, Data.SBV.Control
SMTProblem 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
SMTReasonUnknownData.SBV.Trans, Data.SBV
SMTResultData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
smtRoundingModeData.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
SMTVerbosityData.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
sNaNData.SBV.Internals, Data.SBV.Trans, Data.SBV
SNationalityDocumentation.SBV.Examples.Puzzles.Fish
sNegateDocumentation.SBV.Examples.Queries.FourFours
snoc 
1 (Function)Data.SBV.String
2 (Function)Data.SBV.List
sNorwegianDocumentation.SBV.Examples.Puzzles.Fish
sNotData.SBV.Internals, Data.SBV.Trans, Data.SBV
sNotElemData.SBV.Trans, Data.SBV
sNothingData.SBV.Maybe
sObserveData.SBV
softConstrainData.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
solveAllDocumentation.SBV.Examples.Puzzles.Sudoku
solveCrosswordDocumentation.SBV.Examples.Strings.RegexCrossword
solvedDocumentation.SBV.Examples.Puzzles.Jugs
solveEuler185Documentation.SBV.Examples.Puzzles.Euler185
solveNDocumentation.SBV.Examples.Puzzles.U2Bridge
SolverData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
solverData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SolverCapabilities 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
SolverContextData.SBV.Internals
solverSetOptionsData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
solveU2Documentation.SBV.Examples.Puzzles.U2Bridge
sOrData.SBV.Internals, Data.SBV.Trans, Data.SBV
SPDocumentation.SBV.Examples.Puzzles.Drinker
SPetDocumentation.SBV.Examples.Puzzles.Fish
sPlusDocumentation.SBV.Examples.Queries.FourFours
sPopCountData.SBV.Trans, Data.SBV
SportDocumentation.SBV.Examples.Puzzles.Fish
SQDocumentation.SBV.Examples.Uninterpreted.Sort
SQLExprDocumentation.SBV.Examples.Strings.SQLInjection
SqrtDocumentation.SBV.Examples.Queries.FourFours
sqrtDocumentation.SBV.Examples.WeakestPreconditions.IntSqrt
SqrtS 
1 (Type/Class)Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
2 (Data Constructor)Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
sQuotData.SBV.Trans, Data.SBV
sQuotRemData.SBV.Trans, Data.SBV
SRationalData.SBV.Internals, Data.SBV
sRationalData.SBV
sRationalsData.SBV
sRational_Data.SBV
sReadyDocumentation.SBV.Examples.Lists.BoundedMutex
SRealData.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
sRealToSIntegerData.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
sRemData.SBV.Trans, Data.SBV
sRightData.SBV.Either
sRNAData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRNEData.SBV.Internals, Data.SBV.Trans, Data.SBV
SRoleDocumentation.SBV.Examples.Puzzles.Murder
sRotateLeftData.SBV.Trans, Data.SBV
sRotateRightData.SBV.Trans, Data.SBV
SRoundingModeData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundNearestTiesToAwayData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundNearestTiesToEvenData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardNegativeData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardPositiveData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardZeroData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTNData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTPData.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTZData.SBV.Internals, Data.SBV.Trans, Data.SBV
sSatDocumentation.SBV.Examples.Optimization.Enumerate
sSaturdayDocumentation.SBV.Examples.Queries.Enums
SSetData.SBV.Internals, Data.SBV
sSetData.SBV
sSetsData.SBV
sSet_Data.SBV
SSexDocumentation.SBV.Examples.Puzzles.Murder
sShiftLeftData.SBV.Trans, Data.SBV
sShiftRightData.SBV.Trans, Data.SBV
sSignedShiftArithRightData.SBV.Trans, Data.SBV
SSportDocumentation.SBV.Examples.Puzzles.Fish
sSqrtDocumentation.SBV.Examples.Queries.FourFours
SStateDocumentation.SBV.Examples.Lists.BoundedMutex
SStringData.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
sSunDocumentation.SBV.Examples.Optimization.Enumerate
sSundayDocumentation.SBV.Examples.Queries.Enums
sSwedeDocumentation.SBV.Examples.Puzzles.Fish
stabilityData.SBV.Tools.WeakestPreconditions
StableData.SBV.Tools.WeakestPreconditions
stableData.SBV.Tools.WeakestPreconditions
startDocumentation.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
4 (Type/Class)Documentation.SBV.Examples.Puzzles.AOC_2021_24
5 (Data Constructor)Documentation.SBV.Examples.Puzzles.AOC_2021_24
statementReDocumentation.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
sTeaDocumentation.SBV.Examples.Puzzles.Fish
sTennisDocumentation.SBV.Examples.Puzzles.Fish
sTestBitData.SBV.Trans, Data.SBV
sThereDocumentation.SBV.Examples.Puzzles.U2Bridge
sThuDocumentation.SBV.Examples.Optimization.Enumerate
sThursdayDocumentation.SBV.Examples.Queries.Enums
STimeDocumentation.SBV.Examples.Puzzles.U2Bridge
sTimesDocumentation.SBV.Examples.Queries.FourFours
StmtData.SBV.Tools.WeakestPreconditions
StrConcatData.SBV.Internals
StrContainsData.SBV.Internals
STreeData.SBV.Tools.STree
StrFromCodeData.SBV.Internals
StrIndexOfData.SBV.Internals
StrInReData.SBV.Internals
StrLenData.SBV.Internals
StrNatToStrData.SBV.Internals
StrNthData.SBV.Internals
StrOp 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
StrPrefixOfData.SBV.Internals
strReDocumentation.SBV.Examples.Strings.SQLInjection
StrReplaceData.SBV.Internals
StrStrToNatData.SBV.Internals
StrSubstrData.SBV.Internals
StrSuffixOfData.SBV.Internals
strToCharAtData.SBV.String
StrToCodeData.SBV.Internals
strToNatData.SBV.String
strToStrAtData.SBV.String
sTrueData.SBV.Internals, Data.SBV.Trans, Data.SBV
StrUnitData.SBV.Internals
StuckData.SBV.Tools.WeakestPreconditions
sTueDocumentation.SBV.Examples.Optimization.Enumerate
sTuesdayDocumentation.SBV.Examples.Queries.Enums
STupleData.SBV.Internals, Data.SBV
sTupleData.SBV
STuple2Data.SBV.Internals, Data.SBV
STuple3Data.SBV.Internals, Data.SBV
STuple4Data.SBV.Internals, Data.SBV
STuple5Data.SBV.Internals, Data.SBV
STuple6Data.SBV.Internals, Data.SBV
STuple7Data.SBV.Internals, Data.SBV
STuple8Data.SBV.Internals, Data.SBV
sTuplesData.SBV
sTuple_Data.SBV
SU2MemberDocumentation.SBV.Examples.Puzzles.U2Bridge
subListData.SBV.List
subStrData.SBV.String
sudokuDocumentation.SBV.Examples.Puzzles.Sudoku
sum0Documentation.SBV.Examples.Crypto.SHA
sum0CoefficientsDocumentation.SBV.Examples.Crypto.SHA
sum1Documentation.SBV.Examples.Crypto.SHA
sum1CoefficientsDocumentation.SBV.Examples.Crypto.SHA
sumCorrectDocumentation.SBV.Examples.ProofTools.Sum
SumS 
1 (Type/Class)Documentation.SBV.Examples.WeakestPreconditions.Sum
2 (Data Constructor)Documentation.SBV.Examples.WeakestPreconditions.Sum
sumToNDocumentation.SBV.Examples.Misc.Definitions
SunDocumentation.SBV.Examples.Optimization.Enumerate
SundayDocumentation.SBV.Examples.Queries.Enums
SUnOpDocumentation.SBV.Examples.Queries.FourFours
supportsApproxRealsData.SBV.Internals
supportsBitVectorsData.SBV.Internals
supportsCustomQueriesData.SBV.Internals
supportsDataTypesData.SBV.Internals
supportsDefineFunData.SBV.Internals
supportsDeltaSatData.SBV.Internals
supportsDirectAccessorsData.SBV.Internals
supportsDistinctData.SBV.Internals
supportsFlattenedModelsData.SBV.Internals
supportsGlobalDeclsData.SBV.Internals
supportsIEEE754Data.SBV.Internals
supportsInt2bvData.SBV.Internals
supportsOptimizationData.SBV.Internals
supportsPseudoBooleansData.SBV.Internals
supportsQuantifiersData.SBV.Internals
supportsRealsData.SBV.Internals
supportsSetsData.SBV.Internals
supportsUnboundedIntsData.SBV.Internals
supportsUninterpretedSortsData.SBV.Internals
SV 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
svAbsData.SBV.Dynamic
svAddConstantData.SBV.Dynamic
SVal 
1 (Type/Class)Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor)Data.SBV.Internals
svAndData.SBV.Dynamic
svAsBoolData.SBV.Dynamic
svAsIntegerData.SBV.Dynamic
svBarrelRotateLeftData.SBV.Dynamic
svBarrelRotateRightData.SBV.Dynamic
svBlastBEData.SBV.Dynamic
svBlastLEData.SBV.Dynamic
svBoolData.SBV.Dynamic
svCgInputData.SBV.Internals, Data.SBV.Dynamic
svCgInputArrData.SBV.Internals, Data.SBV.Dynamic
svCgOutputData.SBV.Internals, Data.SBV.Dynamic
svCgOutputArrData.SBV.Internals, Data.SBV.Dynamic
svCgReturnData.SBV.Internals, Data.SBV.Dynamic
svCgReturnArrData.SBV.Internals, Data.SBV.Dynamic
svDecrementData.SBV.Dynamic
svDenominatorData.SBV.Dynamic
svDivideData.SBV.Dynamic
svDoubleData.SBV.Dynamic
svEnumFromThenToData.SBV.Dynamic
svEqualData.SBV.Dynamic
svExpData.SBV.Dynamic
svExtractData.SBV.Dynamic
svFalseData.SBV.Dynamic
svFloatData.SBV.Dynamic
svFloatingPointData.SBV.Dynamic
svFromIntegralData.SBV.Dynamic
svFromWord1Data.SBV.Dynamic
svGreaterEqData.SBV.Dynamic
svGreaterThanData.SBV.Dynamic
sVictimDocumentation.SBV.Examples.Puzzles.Murder
svIncrementData.SBV.Dynamic
svIntegerData.SBV.Dynamic
svIteData.SBV.Dynamic
svJoinData.SBV.Dynamic
svLazyIteData.SBV.Dynamic
svLessEqData.SBV.Dynamic
svLessThanData.SBV.Dynamic
svMinusData.SBV.Dynamic
svMkSymVarData.SBV.Dynamic
svNewVarData.SBV.Dynamic
svNewVar_Data.SBV.Dynamic
svNotData.SBV.Dynamic
svNotEqualData.SBV.Dynamic
svNumeratorData.SBV.Dynamic
sVolleyballDocumentation.SBV.Examples.Puzzles.Fish
svOrData.SBV.Dynamic
svPlusData.SBV.Dynamic
svQuickCheckData.SBV.Dynamic
svQuotData.SBV.Dynamic
svQuotRemData.SBV.Dynamic
svRealData.SBV.Dynamic
svRemData.SBV.Dynamic
svRolData.SBV.Dynamic
svRorData.SBV.Dynamic
svRotateLeftData.SBV.Dynamic
svRotateRightData.SBV.Dynamic
svSelectData.SBV.Dynamic
svSetBitData.SBV.Dynamic
svShiftLeftData.SBV.Dynamic
svShiftRightData.SBV.Dynamic
svShlData.SBV.Dynamic
svShrData.SBV.Dynamic
svSignData.SBV.Dynamic
svSignExtendData.SBV.Dynamic
svStrongEqualData.SBV.Dynamic
svStructuralLessThanData.SBV.Dynamic
svSymbolicMergeData.SBV.Dynamic
svTestBitData.SBV.Dynamic
svTimesData.SBV.Dynamic
svToSVData.SBV.Internals
svToWord1Data.SBV.Dynamic
svTrueData.SBV.Dynamic
svUNegData.SBV.Dynamic
svUninterpretedData.SBV.Dynamic
svUnsignData.SBV.Dynamic
svWordFromBEData.SBV.Dynamic
svWordFromLEData.SBV.Dynamic
svXOrData.SBV.Dynamic
svZeroExtendData.SBV.Dynamic
swapDocumentation.SBV.Examples.Crypto.RC4
sWaterDocumentation.SBV.Examples.Puzzles.Fish
sWedDocumentation.SBV.Examples.Optimization.Enumerate
SwedeDocumentation.SBV.Examples.Puzzles.Fish
sWednesdayDocumentation.SBV.Examples.Queries.Enums
sWhiteDocumentation.SBV.Examples.Puzzles.Fish
SWordData.SBV.Trans, Data.SBV
sWord 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
SWord16Data.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
SWord32Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord32 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sWord32AsSFloatData.SBV.Trans, Data.SBV
sWord32s 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sWord32_Data.SBV
SWord64Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord64 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sWord64AsSDoubleData.SBV.Trans, Data.SBV
sWord64s 
1 (Function)Data.SBV.Trans
2 (Function)Data.SBV
sWord64_Data.SBV
SWord8Data.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
sWordAsSFloatingPointData.SBV.Trans, Data.SBV
sWordNData.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
symData.SBV.Trans, Data.SBV
SymArrayData.SBV.Internals, Data.SBV.Trans, Data.SBV
SymbolicData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
symbolic 
1 (Function)Data.SBV.Internals, Data.SBV.Trans
2 (Function)Data.SBV
symbolicEnvData.SBV.Trans, Data.SBV
symbolicMergeData.SBV.Trans, Data.SBV
symbolics 
1 (Function)Data.SBV.Internals, Data.SBV.Trans
2 (Function)Data.SBV
SymbolicTData.SBV.Trans, Data.SBV
SymTupleData.SBV
SymValData.SBV.Internals, Data.SBV.Trans, Data.SBV
synthMul22Documentation.SBV.Examples.Uninterpreted.Multiply