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 |
CAlgReal | Data.SBV.Internals, Data.SBV.Dynamic |
capabilities | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
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 |
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 |
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 |
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 |
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 | |
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 |
constrainWithAttribute | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
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 |
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 |
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 |
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 |