sbv-7.13: 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.Tools.GenTest
2 (Data Constructor) | Documentation.SBV.Examples.Misc.Enumerate
c1 | Documentation.SBV.Examples.Puzzles.Coins
c2 | Documentation.SBV.Examples.Puzzles.Coins
c3 | Documentation.SBV.Examples.Puzzles.Coins
c4 | Documentation.SBV.Examples.Puzzles.Coins
c5 | Documentation.SBV.Examples.Puzzles.Coins
c6 | Documentation.SBV.Examples.Puzzles.Coins
cache | Data.SBV.Internals
Cached | Data.SBV.Internals
capabilities | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
caseSplit | Data.SBV.Control
Cat | Documentation.SBV.Examples.Puzzles.Fish
cg1 | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
cg2 | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
cgAddDecl | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAddLDFlags | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAddPrototype | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAES128BlockEncrypt | Documentation.SBV.Examples.Crypto.AES
cgAES128Library | Documentation.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.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgDriver | Data.SBV.Internals
cgDriverVals | Data.SBV.Internals
cgFinalConfig | Data.SBV.Internals
CgFloat | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenDriver | Data.SBV.Internals
cgGenerateDriver | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenerateMakefile | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenMakefile | Data.SBV.Internals
CgHeader | Data.SBV.Internals
cgIgnoreAsserts | Data.SBV.Internals
cgIgnoreSAssert | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgInput | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgInputArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgInputs | Data.SBV.Internals
cgInteger | Data.SBV.Internals
cgIntegerSize | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgLDFlags | Data.SBV.Internals
CgLongDouble | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgMakefile | Data.SBV.Internals
cgOutput | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgOutputArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgOutputs | Data.SBV.Internals
cgOverwriteFiles | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgOverwriteGenerated | Data.SBV.Internals
cgPerformRTCs | Data.SBV.Tools.CodeGen, Data.SBV.Internals, 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.Tools.CodeGen, Data.SBV.Internals
cgReturnArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgReturns | Data.SBV.Internals
cgRTC | Data.SBV.Internals
cgSetDriverValues | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgSource | Data.SBV.Internals
CgSRealType | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgSRealType | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgState |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
cgSym | Data.SBV.Tools.CodeGen, Data.SBV.Internals
CgTarget | Data.SBV.Internals
cgUninterpret | Data.SBV
CgVal | Data.SBV.Internals
check |
1 (Function) | Documentation.SBV.Examples.Puzzles.MagicSquare
2 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku
checkArithOverflow | Documentation.SBV.Examples.BitPrecise.BrokenSearch
checkCorrectMidValue | Documentation.SBV.Examples.BitPrecise.BrokenSearch
CheckedArithmetic | Data.SBV.Tools.Overflow
checkedDiv | Documentation.SBV.Examples.Misc.NoDiv0
checkMutex | Documentation.SBV.Examples.Lists.BoundedMutex
checkOverflow | Documentation.SBV.Examples.BitPrecise.Legato
checkOverflowCorrect | Documentation.SBV.Examples.BitPrecise.Legato
checkSat | Data.SBV.Control
checkSatAssuming | Data.SBV.Control
checkSatAssumingWithUnsatisfiableSet | Data.SBV.Control
CheckSatResult | Data.SBV.Control
checkSatUsing | Data.SBV.Control
cheryl | Documentation.SBV.Examples.Puzzles.Birthday
chex | Data.SBV.Internals
chr | Data.SBV.Char
chunk | Documentation.SBV.Examples.Puzzles.MagicSquare
classify | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
clc | Documentation.SBV.Examples.BitPrecise.Legato
clearBit | Data.SBV
Closed | Data.SBV.Tools.Range
CodeGen | Data.SBV.Internals
codeGen |
1 (Function) | Data.SBV.Internals
2 (Function) | Documentation.SBV.Examples.BitPrecise.MergeSort
Coffee | Documentation.SBV.Examples.Puzzles.Fish
Coin | Documentation.SBV.Examples.Puzzles.Coins
col | Documentation.SBV.Examples.Puzzles.Garden
Color |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Fish
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Garden
3 (Type/Class) | Documentation.SBV.Examples.Puzzles.HexPuzzle
combinations | Documentation.SBV.Examples.Puzzles.Coins
compileToC | Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
compileToC' | Data.SBV.Internals
compileToCLib | Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
compileToCLib' | Data.SBV.Internals
complement | Data.SBV
complementBit | Data.SBV
Conc | Data.SBV.RegExp, Data.SBV.Internals
Concat | Documentation.SBV.Examples.Strings.SQLInjection
concat |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
Concrete | Data.SBV.Internals
conditionalSetClearCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
Cons | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
Const | Documentation.SBV.Examples.Strings.SQLInjection
constrain | Data.SBV.Internals, Data.SBV
constrainWithAttribute | Data.SBV.Internals, Data.SBV
correctness | Documentation.SBV.Examples.BitPrecise.MergeSort
correctnessTheorem | Documentation.SBV.Examples.BitPrecise.Legato
Count | Documentation.SBV.Examples.Puzzles.Counts
count |
1 (Function) | Documentation.SBV.Examples.Puzzles.Counts
2 (Function) | Documentation.SBV.Examples.Puzzles.Garden
countLeadingZeros | Data.SBV
counts | Documentation.SBV.Examples.Puzzles.Counts
countTrailingZeros | Data.SBV
crc | Data.SBV.Tools.Polynomial
crcBV | Data.SBV.Tools.Polynomial
crcGood |
1 (Function) | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
2 (Function) | Documentation.SBV.Examples.Existentials.CRCPolynomial
crcUSB | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
crcUSB' | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
crc_48_16 | Documentation.SBV.Examples.Existentials.CRCPolynomial
Critical | Documentation.SBV.Examples.Lists.BoundedMutex
critical | Documentation.SBV.Examples.Lists.BoundedMutex
crossTime | Documentation.SBV.Examples.Puzzles.U2Bridge
csDemo1 | Documentation.SBV.Examples.Queries.CaseSplit
csDemo2 | Documentation.SBV.Examples.Queries.CaseSplit
CustomLogic | Data.SBV
CVC4 | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
cvc4 | Data.SBV, Data.SBV.Dynamic
cvtModel | Data.SBV
CW |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Dynamic
CWAlgReal | Data.SBV.Internals, Data.SBV.Dynamic
CWChar | 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
CWList | Data.SBV.Internals, Data.SBV.Dynamic
cwSameType | Data.SBV.Internals
CWString | Data.SBV.Internals, Data.SBV.Dynamic
cwToBool | Data.SBV.Internals, Data.SBV.Dynamic
cwToSMTLib | Data.SBV.Internals
CWUserSort | Data.SBV.Internals, Data.SBV.Dynamic
CWVal | Data.SBV.Internals, Data.SBV.Dynamic
cwVal | Data.SBV.Internals, Data.SBV.Dynamic