sbv-5.14: 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 - C

C |
1 (Data Constructor) | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Data Constructor) | Data.SBV.Examples.Misc.Enumerate
c1 | Data.SBV.Examples.Puzzles.Coins
c2 | Data.SBV.Examples.Puzzles.Coins
c3 | Data.SBV.Examples.Puzzles.Coins
c4 | Data.SBV.Examples.Puzzles.Coins
c5 | Data.SBV.Examples.Puzzles.Coins
c6 | Data.SBV.Examples.Puzzles.Coins
cache | Data.SBV.Internals
Cached | Data.SBV.Internals
capabilities | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
capSolverName | Data.SBV.Internals
Cat | Data.SBV.Examples.Puzzles.Fish
cg1 | Data.SBV.Examples.CodeGeneration.CRC_USB5
cg2 | Data.SBV.Examples.CodeGeneration.CRC_USB5
cgAddDecl | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgAddLDFlags | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgAddPrototype | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgAES128BlockEncrypt | Data.SBV.Examples.Crypto.AES
cgAES128Library | Data.SBV.Examples.Crypto.AES
CgArray | Data.SBV.Internals
CgAtomic | Data.SBV.Internals
CgConfig |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
cgDecls | Data.SBV.Internals
CgDouble | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
CgDriver | Data.SBV.Internals
cgDriverVals | Data.SBV.Internals
cgFinalConfig | Data.SBV.Internals
CgFloat | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgGenDriver | Data.SBV.Internals
cgGenerateDriver | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgGenerateMakefile | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgGenMakefile | Data.SBV.Internals
CgHeader | Data.SBV.Internals
cgIgnoreAsserts | Data.SBV.Internals
cgIgnoreSAssert | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgInput | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
cgInputArr | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
cgInputs | Data.SBV.Internals
cgInteger | Data.SBV.Internals
cgIntegerSize | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgLDFlags | Data.SBV.Internals
CgLongDouble | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
CgMakefile | Data.SBV.Internals
cgOutput | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
cgOutputArr | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
cgOutputs | Data.SBV.Internals
cgPerformRTCs | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
CgPgmBundle |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
CgPgmKind | Data.SBV.Internals
cgPrototypes | Data.SBV.Internals
cgReal | Data.SBV.Internals
cgReturn | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
cgReturnArr | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
cgReturns | Data.SBV.Internals
cgRTC | Data.SBV.Internals
cgSBVToSW | Data.SBV.Internals
cgSetDriverValues | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
CgSource | Data.SBV.Internals
CgSRealType | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cgSRealType | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
CgState |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
CgTarget | Data.SBV.Internals
cgUninterpret | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
CgVal | Data.SBV.Internals
check |
1 (Function) | Data.SBV.Examples.Puzzles.MagicSquare
2 (Function) | Data.SBV.Examples.Puzzles.Sudoku
checkAndConvert | Data.SBV.Internals
checkedDiv | Data.SBV.Examples.Misc.NoDiv0
checkOverflow | Data.SBV.Examples.BitPrecise.Legato
checkOverflowCorrect | Data.SBV.Examples.BitPrecise.Legato
cheryl | Data.SBV.Examples.Puzzles.Birthday
chunk | Data.SBV.Examples.Puzzles.MagicSquare
classify | Data.SBV.Examples.Uninterpreted.UISortAllSat
clc | Data.SBV.Examples.BitPrecise.Legato
clearBit | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
CodeGen | Data.SBV.Internals
codeGen |
1 (Function) | Data.SBV.Internals
2 (Function) | Data.SBV.Examples.BitPrecise.MergeSort
Coffee | Data.SBV.Examples.Puzzles.Fish
Coin | Data.SBV.Examples.Puzzles.Coins
Color | Data.SBV.Examples.Puzzles.Fish
combinations | Data.SBV.Examples.Puzzles.Coins
compileToC | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
compileToC' | Data.SBV.Internals
compileToCLib | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
compileToCLib' | Data.SBV.Internals
compileToSMTLib |
1 (Function) | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Function) | Data.SBV.Dynamic
complement | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
complementBit | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
Concrete | Data.SBV.Internals
conditionalSetClearCorrect | Data.SBV.Examples.BitPrecise.BitTricks
Cons | Data.SBV.Examples.Uninterpreted.UISortAllSat
constrain | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
correctness | Data.SBV.Examples.BitPrecise.MergeSort
correctnessTheorem | Data.SBV.Examples.BitPrecise.Legato
Count | Data.SBV.Examples.Puzzles.Counts
count | Data.SBV.Examples.Puzzles.Counts
countLeadingZeros | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
counts | Data.SBV.Examples.Puzzles.Counts
countTrailingZeros | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
crc | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
crcBV | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
crcGood |
1 (Function) | Data.SBV.Examples.CodeGeneration.CRC_USB5
2 (Function) | Data.SBV.Examples.Existentials.CRCPolynomial
crcUSB | Data.SBV.Examples.CodeGeneration.CRC_USB5
crcUSB' | Data.SBV.Examples.CodeGeneration.CRC_USB5
crc_48_16 | Data.SBV.Examples.Existentials.CRCPolynomial
crossTime | Data.SBV.Examples.Puzzles.U2Bridge
CustomLogic | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
CVC4 | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cvc4 | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
cvtModel | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
CW |
1 (Type/Class) | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
CWAlgReal | Data.SBV.Internals, Data.SBV.Dynamic
CWDouble | Data.SBV.Internals, Data.SBV.Dynamic
CWFloat | Data.SBV.Internals, Data.SBV.Dynamic
CWInteger | Data.SBV.Internals, Data.SBV.Dynamic
cwSameType | Data.SBV.Internals
cwToBool | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
CWUserSort | Data.SBV.Internals, Data.SBV.Dynamic
CWVal | Data.SBV.Internals, Data.SBV.Dynamic
cwVal | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic