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

Index - S

SData.SBV.Examples.Crypto.RC4
sailorsData.SBV.Examples.Existentials.Diophantine
SArrayData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sat 
1 (Function)Data.SBV
2 (Function)Data.SBV.Bridge.CVC4
3 (Function)Data.SBV.Bridge.Yices
4 (Function)Data.SBV.Bridge.Z3
satCmdData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SatisfiableData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SatModelData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SatResult 
1 (Type/Class)Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Data Constructor)Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
satWithData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SBData.SBV.Examples.Uninterpreted.Deduce
SBoolData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sBoolData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sBoolsData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sboxData.SBV.Examples.Crypto.AES
sboxInverseCorrectData.SBV.Examples.Crypto.AES
sboxTableData.SBV.Examples.Crypto.AES
SBV 
1 (Type/Class)Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Data Constructor)Data.SBV.Internals
sbvCheckSolverInstallationData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SBVCodeGenData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sbvCurrentSolver 
1 (Function)Data.SBV
2 (Function)Data.SBV.Bridge.CVC4
3 (Function)Data.SBV.Bridge.Yices
4 (Function)Data.SBV.Bridge.Z3
sbvPopCountData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SBVRunModeData.SBV.Internals
sbvShiftLeftData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sbvShiftRightData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sbvSignedShiftArithRightData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sbvTestBitData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sbvUninterpretData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
scanlTraceData.SBV.Examples.BitPrecise.PrefixSum
sDivData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SDivisibleData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sDivModData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
selectData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
setBitData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
setBitToData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
setFlagData.SBV.Examples.BitPrecise.Legato
setRegData.SBV.Examples.BitPrecise.Legato
SFunArrayData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sgcdData.SBV.Examples.CodeGeneration.GCD
sgcdIsCorrectData.SBV.Examples.CodeGeneration.GCD
shiftData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
shiftLData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
shiftLeftData.SBV.Examples.CodeGeneration.Uninterpreted
shiftRData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
showPolyData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
showPolynomialData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
showTypeData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SignCastData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
signCastData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SInt16Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sInt16Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sInt16sData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SInt32Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sInt32Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sInt32sData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SInt64Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sInt64Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sInt64sData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SInt8Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sInt8Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sInt8sData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SIntegerData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sIntegerData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sIntegersData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SIntegralData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sletData.SBV.Internals
smaxData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sminData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sModData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SMTConfig 
1 (Type/Class)Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Data Constructor)Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
smtFileData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SMTResultData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SMTSolver 
1 (Type/Class)Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Data Constructor)Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
Solution 
1 (Type/Class)Data.SBV.Examples.Existentials.Diophantine
2 (Type/Class)Data.SBV.Examples.Puzzles.NQueens
solveData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
solveAllData.SBV.Examples.Puzzles.Sudoku
solveEuler185Data.SBV.Examples.Puzzles.Euler185
solveNData.SBV.Examples.Puzzles.U2Bridge
solverData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
solverTweaksData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
solveU2Data.SBV.Examples.Puzzles.U2Bridge
splitData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SplittableData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sQuotData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sQuotRemData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SRealData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sRealData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sRealsData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sRemData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
startData.SBV.Examples.Puzzles.U2Bridge
StateData.SBV.Examples.Crypto.AES
Status 
1 (Type/Class)Data.SBV.Examples.Puzzles.U2Bridge
2 (Data Constructor)Data.SBV.Examples.Puzzles.U2Bridge
STreeData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SU2MemberData.SBV.Examples.Puzzles.U2Bridge
sudokuData.SBV.Examples.Puzzles.Sudoku
swapData.SBV.Examples.Crypto.RC4
SWord16Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sWord16Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sWord16sData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SWord32Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sWord32Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sWord32sData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SWord48Data.SBV.Examples.Existentials.CRCPolynomial
SWord64Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sWord64Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sWord64sData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SWord8Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sWord8Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
sWord8sData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SymArrayData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SymbolicData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
symbolicData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
symbolicMergeData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
symbolicsData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
SymWordData.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3