C | |
1 (Data Constructor) | Data.SBV.Tools.GenTest |
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 |
CaseCond | Data.SBV.Internals |
CaseCov | Data.SBV.Internals |
CasePath | Data.SBV.Internals |
CaseSplit | 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 |
CaseVac | 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.Tools.CodeGen, Data.SBV.Dynamic |
cgAddLDFlags | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
cgAddPrototype | Data.SBV.Internals, Data.SBV.Tools.CodeGen, 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.Tools.CodeGen, Data.SBV.Dynamic |
CgDriver | Data.SBV.Internals |
cgDriverVals | Data.SBV.Internals |
cgFinalConfig | Data.SBV.Internals |
CgFloat | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
cgGenDriver | Data.SBV.Internals |
cgGenerateDriver | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
cgGenerateMakefile | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
cgGenMakefile | Data.SBV.Internals |
CgHeader | Data.SBV.Internals |
cgIgnoreAsserts | Data.SBV.Internals |
cgIgnoreSAssert | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
cgInput | Data.SBV.Internals, Data.SBV.Tools.CodeGen |
cgInputArr | Data.SBV.Internals, Data.SBV.Tools.CodeGen |
cgInputs | Data.SBV.Internals |
cgInteger | Data.SBV.Internals |
cgIntegerSize | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
cgLDFlags | Data.SBV.Internals |
CgLongDouble | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
CgMakefile | Data.SBV.Internals |
cgOutput | Data.SBV.Internals, Data.SBV.Tools.CodeGen |
cgOutputArr | Data.SBV.Internals, Data.SBV.Tools.CodeGen |
cgOutputs | Data.SBV.Internals |
cgPerformRTCs | Data.SBV.Internals, Data.SBV.Tools.CodeGen, 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.Tools.CodeGen |
cgReturnArr | Data.SBV.Internals, Data.SBV.Tools.CodeGen |
cgReturns | Data.SBV.Internals |
cgRTC | Data.SBV.Internals |
cgSetDriverValues | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
CgSource | Data.SBV.Internals |
CgSRealType | Data.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
cgSRealType | Data.SBV.Internals, Data.SBV.Tools.CodeGen, 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 |
CheckCaseVacuity | 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 |
CheckConstrVacuity | 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 |
checkedDiv | Data.SBV.Examples.Misc.NoDiv0 |
checkOverflow | Data.SBV.Examples.BitPrecise.Legato |
checkOverflowCorrect | Data.SBV.Examples.BitPrecise.Legato |
CheckUsing | 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 |
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.Tools.CodeGen, Data.SBV.Dynamic |
compileToC' | Data.SBV.Internals |
compileToCLib | Data.SBV.Tools.CodeGen, Data.SBV.Dynamic |
compileToCLib' | Data.SBV.Internals |
compileToSMTLib | |
1 (Function) | Data.SBV.Internals |
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.Tools.Polynomial |
crcBV | Data.SBV.Tools.Polynomial |
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 |
CstrVac | Data.SBV.Internals |
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 |