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

Index - S

 S Data.SBV.Examples.Crypto.RC4 sailors Data.SBV.Examples.Existentials.Diophantine SArray Data.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 satCmd Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 Satisfiable Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SatModel Data.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 satWith Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SB Data.SBV.Examples.Uninterpreted.Deduce SBool Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sBool Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sBools Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sbox Data.SBV.Examples.Crypto.AES sboxInverseCorrect Data.SBV.Examples.Crypto.AES sboxTable Data.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 sbvCheckSolverInstallation Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SBVCodeGen Data.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 sbvPopCount Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SBVRunMode Data.SBV.Internals sbvShiftLeft Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sbvShiftRight Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sbvSignedShiftArithRight Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sbvTestBit Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sbvUninterpret Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 scanlTrace Data.SBV.Examples.BitPrecise.PrefixSum sDiv Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SDivisible Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sDivMod Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 select Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 setBit Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 setBitTo Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 setFlag Data.SBV.Examples.BitPrecise.Legato setReg Data.SBV.Examples.BitPrecise.Legato SFunArray Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sgcd Data.SBV.Examples.CodeGeneration.GCD sgcdIsCorrect Data.SBV.Examples.CodeGeneration.GCD shift Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 shiftL Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 shiftLeft Data.SBV.Examples.CodeGeneration.Uninterpreted shiftR Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 showPoly Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 showPolynomial Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 showType Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SignCast Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 signCast Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SInt16 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInt16 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInt16s Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SInt32 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInt32 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInt32s Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SInt64 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInt64 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInt64s Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SInt8 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInt8 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInt8s Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SInteger Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sInteger Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sIntegers Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SIntegral Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 slet Data.SBV.Internals smax Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 smin Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sMod Data.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 smtFile Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SMTResult Data.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 solve Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 solveAll Data.SBV.Examples.Puzzles.Sudoku solveEuler185 Data.SBV.Examples.Puzzles.Euler185 solveN Data.SBV.Examples.Puzzles.U2Bridge solver Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 solverTweaks Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 solveU2 Data.SBV.Examples.Puzzles.U2Bridge split Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 Splittable Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sQuot Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sQuotRem Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SReal Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sReal Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sReals Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sRem Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 start Data.SBV.Examples.Puzzles.U2Bridge State Data.SBV.Examples.Crypto.AES Status 1 (Type/Class) Data.SBV.Examples.Puzzles.U2Bridge 2 (Data Constructor) Data.SBV.Examples.Puzzles.U2Bridge STree Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SU2Member Data.SBV.Examples.Puzzles.U2Bridge sudoku Data.SBV.Examples.Puzzles.Sudoku swap Data.SBV.Examples.Crypto.RC4 SWord16 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sWord16 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sWord16s Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SWord32 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sWord32 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sWord32s Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SWord48 Data.SBV.Examples.Existentials.CRCPolynomial SWord64 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sWord64 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sWord64s Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SWord8 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sWord8 Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 sWord8s Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SymArray Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 Symbolic Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 symbolic Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 symbolicMerge Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 symbolics Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3 SymWord Data.SBV, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3