sbv-10.2: 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
3 (Data Constructor) | Documentation.SBV.Examples.Misc.FirstOrderLogic
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
CAlgReal | Data.SBV.Internals, Data.SBV.Dynamic
capabilities | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
capacity | Documentation.SBV.Examples.Puzzles.Jugs
caseSplit |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Cat | Documentation.SBV.Examples.Puzzles.Fish
CChar | Data.SBV.Internals, Data.SBV.Dynamic
CDouble | Data.SBV.Internals, Data.SBV.Dynamic
ceilingHighEnoughForHuman | Documentation.SBV.Examples.Misc.Newtypes
CEither | Data.SBV.Internals, Data.SBV.Dynamic
CFloat | Data.SBV.Internals, Data.SBV.Dynamic
CFP | Data.SBV.Internals, Data.SBV.Dynamic
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
cgAESLibrary | 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
cgSHA256 | Documentation.SBV.Examples.Crypto.SHA
cgSHA512 | Documentation.SBV.Examples.Crypto.SHA
cgShowU8InHex | Data.SBV.Internals
cgShowU8UsingHex | Data.SBV.Tools.CodeGen, Data.SBV.Internals
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.Trans, Data.SBV
CgVal | Data.SBV.Internals
ch | Documentation.SBV.Examples.Crypto.SHA
check |
1 (Function) | Documentation.SBV.Examples.Puzzles.MagicSquare
2 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku
3 (Function) | Documentation.SBV.Examples.Transformers.SymbolicEval
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
CheckResult | Documentation.SBV.Examples.Transformers.SymbolicEval
checkSat |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
checkSatAssuming |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
checkSatAssumingWithUnsatisfiableSet |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
CheckSatResult | Data.SBV.Trans.Control, Data.SBV.Control
checkSatUsing |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
cheryl | Documentation.SBV.Examples.Puzzles.Birthday
chex | Data.SBV.Internals
chop4 | Documentation.SBV.Examples.Crypto.AES
chr | Data.SBV.Char
chunk | Documentation.SBV.Examples.Puzzles.MagicSquare
chunkBy | Documentation.SBV.Examples.Crypto.SHA
CInteger | Data.SBV.Internals, Data.SBV.Dynamic
classify | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
clc | Documentation.SBV.Examples.BitPrecise.Legato
clearBit | Data.SBV.Trans, Data.SBV
CList | Data.SBV.Internals, Data.SBV.Dynamic
Closed | Data.SBV.Tools.Range
ClosedPoint | Data.SBV
CMaybe | Data.SBV.Internals, Data.SBV.Dynamic
coat | Documentation.SBV.Examples.Lists.CountOutAndTransfer
coatCheck | Documentation.SBV.Examples.Lists.CountOutAndTransfer
CodeGen | Data.SBV.Internals
codeGen |
1 (Function) | Data.SBV.Internals
2 (Function) | Documentation.SBV.Examples.BitPrecise.MergeSort
3 (Function) | Documentation.SBV.Examples.Crypto.Prince
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
commonPT | Documentation.SBV.Examples.Crypto.AES
Comp | Data.SBV.RegExp, Data.SBV.Internals
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 |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Set
complementBit | Data.SBV.Trans, Data.SBV
ComplementSet | Data.SBV.Internals, 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
Consecution | Data.SBV.Tools.Induction
Const |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Murder
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Murder
3 (Data Constructor) | Documentation.SBV.Examples.Strings.SQLInjection
constrain | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Constraint | Data.SBV.Internals
constraint | Data.SBV.Internals
ConstraintSet | Data.SBV.Trans, Data.SBV
constraintStr | Data.SBV.Internals
constrainWithAttribute | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
content | Documentation.SBV.Examples.Puzzles.Jugs
contextState | Data.SBV.Internals
correctness |
1 (Function) | Documentation.SBV.Examples.BitPrecise.MergeSort
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Append
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
8 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
9 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
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
Counterexample | Documentation.SBV.Examples.Transformers.SymbolicEval
countLeadingZeros | Data.SBV.Trans, Data.SBV
counts | Documentation.SBV.Examples.Puzzles.Counts
countTrailingZeros | Data.SBV.Trans, Data.SBV
crack | Data.SBV
crackNum | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
CRational | Data.SBV.Internals, Data.SBV.Dynamic
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
create | Data.SBV.Control
Critical | Documentation.SBV.Examples.Lists.BoundedMutex
crossTime | Documentation.SBV.Examples.Puzzles.U2Bridge
csDemo1 | Documentation.SBV.Examples.Queries.CaseSplit
csDemo2 | Documentation.SBV.Examples.Queries.CaseSplit
CSet | Data.SBV.Internals, Data.SBV.Dynamic
CString | Data.SBV.Internals, Data.SBV.Dynamic
CT | Documentation.SBV.Examples.Crypto.Prince
CTuple | Data.SBV.Internals, Data.SBV.Dynamic
CUserSort | Data.SBV.Internals, Data.SBV.Dynamic
CustomLogic | Data.SBV.Trans, Data.SBV
CV |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Dynamic
CVal | Data.SBV.Internals, Data.SBV.Dynamic
CVC4 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
cvc4 | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
CVC5 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
cvc5 | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
cvSameType | Data.SBV.Internals
cvtModel | Data.SBV.Trans, Data.SBV
cvToBool | Data.SBV.Internals, Data.SBV.Dynamic
cvToSMTLib | Data.SBV.Internals
cvVal | Data.SBV.Internals, Data.SBV.Dynamic