sbv-8.10: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Index - C

C 
1 (Data Constructor)Data.SBV.Tools.GenTest
2 (Data Constructor)Documentation.SBV.Examples.Misc.Enumerate
c1Documentation.SBV.Examples.Puzzles.Coins
c2Documentation.SBV.Examples.Puzzles.Coins
c3Documentation.SBV.Examples.Puzzles.Coins
c4Documentation.SBV.Examples.Puzzles.Coins
c5Documentation.SBV.Examples.Puzzles.Coins
c6Documentation.SBV.Examples.Puzzles.Coins
cacheData.SBV.Internals
CachedData.SBV.Internals
CAlgRealData.SBV.Internals, Data.SBV.Dynamic
capabilitiesData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
caseSplit 
1 (Function)Data.SBV.Trans.Control
2 (Function)Data.SBV.Control
CatDocumentation.SBV.Examples.Puzzles.Fish
CCharData.SBV.Internals, Data.SBV.Dynamic
CDoubleData.SBV.Internals, Data.SBV.Dynamic
ceilingHighEnoughForHumanDocumentation.SBV.Examples.Misc.Newtypes
CEitherData.SBV.Internals, Data.SBV.Dynamic
CFloatData.SBV.Internals, Data.SBV.Dynamic
cg1Documentation.SBV.Examples.CodeGeneration.CRC_USB5
cg2Documentation.SBV.Examples.CodeGeneration.CRC_USB5
cgAddDeclData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAddLDFlagsData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAddPrototypeData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAES128BlockEncryptDocumentation.SBV.Examples.Crypto.AES
cgAES128LibraryDocumentation.SBV.Examples.Crypto.AES
cgAESLibraryDocumentation.SBV.Examples.Crypto.AES
CgArrayData.SBV.Internals
CgAtomicData.SBV.Internals
CgConfig 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
cgDeclsData.SBV.Internals
CgDoubleData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgDriverData.SBV.Internals
cgDriverValsData.SBV.Internals
cgFinalConfigData.SBV.Internals
CgFloatData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenDriverData.SBV.Internals
cgGenerateDriverData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenerateMakefileData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenMakefileData.SBV.Internals
CgHeaderData.SBV.Internals
cgIgnoreAssertsData.SBV.Internals
cgIgnoreSAssertData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgInputData.SBV.Tools.CodeGen, Data.SBV.Internals
cgInputArrData.SBV.Tools.CodeGen, Data.SBV.Internals
cgInputsData.SBV.Internals
cgIntegerData.SBV.Internals
cgIntegerSizeData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgLDFlagsData.SBV.Internals
CgLongDoubleData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgMakefileData.SBV.Internals
cgOutputData.SBV.Tools.CodeGen, Data.SBV.Internals
cgOutputArrData.SBV.Tools.CodeGen, Data.SBV.Internals
cgOutputsData.SBV.Internals
cgOverwriteFilesData.SBV.Tools.CodeGen, Data.SBV.Internals
cgOverwriteGeneratedData.SBV.Internals
cgPerformRTCsData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgPgmBundle 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
CgPgmKindData.SBV.Internals
cgPrototypesData.SBV.Internals
cgRealData.SBV.Internals
cgReturnData.SBV.Tools.CodeGen, Data.SBV.Internals
cgReturnArrData.SBV.Tools.CodeGen, Data.SBV.Internals
cgReturnsData.SBV.Internals
cgRTCData.SBV.Internals
cgSetDriverValuesData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgSHA256Documentation.SBV.Examples.Crypto.SHA
cgShowU8InHexData.SBV.Internals
cgShowU8UsingHexData.SBV.Tools.CodeGen, Data.SBV.Internals
CgSourceData.SBV.Internals
CgSRealTypeData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgSRealTypeData.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgState 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
cgSymData.SBV.Tools.CodeGen, Data.SBV.Internals
CgTargetData.SBV.Internals
cgUninterpretData.SBV.Trans, Data.SBV
CgValData.SBV.Internals
chDocumentation.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
checkArithOverflowDocumentation.SBV.Examples.BitPrecise.BrokenSearch
checkCorrectMidValueDocumentation.SBV.Examples.BitPrecise.BrokenSearch
CheckedArithmeticData.SBV.Tools.Overflow
checkedDivDocumentation.SBV.Examples.Misc.NoDiv0
checkMutexDocumentation.SBV.Examples.Lists.BoundedMutex
checkOverflowDocumentation.SBV.Examples.BitPrecise.Legato
checkOverflowCorrectDocumentation.SBV.Examples.BitPrecise.Legato
CheckResultDocumentation.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
CheckSatResultData.SBV.Trans.Control, Data.SBV.Control
checkSatUsing 
1 (Function)Data.SBV.Trans.Control
2 (Function)Data.SBV.Control
cherylDocumentation.SBV.Examples.Puzzles.Birthday
chexData.SBV.Internals
chrData.SBV.Char
chunkDocumentation.SBV.Examples.Puzzles.MagicSquare
chunkByDocumentation.SBV.Examples.Crypto.SHA
CIntegerData.SBV.Internals, Data.SBV.Dynamic
classifyDocumentation.SBV.Examples.Uninterpreted.UISortAllSat
clcDocumentation.SBV.Examples.BitPrecise.Legato
clearBitData.SBV.Trans, Data.SBV
CListData.SBV.Internals, Data.SBV.Dynamic
ClosedData.SBV.Tools.Range
ClosedPointData.SBV
CMaybeData.SBV.Internals, Data.SBV.Dynamic
CodeGenData.SBV.Internals
codeGen 
1 (Function)Data.SBV.Internals
2 (Function)Documentation.SBV.Examples.BitPrecise.MergeSort
CoffeeDocumentation.SBV.Examples.Puzzles.Fish
CoinDocumentation.SBV.Examples.Puzzles.Coins
colDocumentation.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
combinationsDocumentation.SBV.Examples.Puzzles.Coins
compileToCData.SBV.Tools.CodeGen, Data.SBV.Dynamic
compileToC'Data.SBV.Internals
compileToCLibData.SBV.Tools.CodeGen, Data.SBV.Dynamic
compileToCLib'Data.SBV.Internals
complement 
1 (Function)Data.SBV.Trans, Data.SBV
2 (Function)Data.SBV.Set
complementBitData.SBV.Trans, Data.SBV
ComplementSetData.SBV.Internals, Data.SBV
ConcData.SBV.RegExp, Data.SBV.Internals
ConcatDocumentation.SBV.Examples.Strings.SQLInjection
concat 
1 (Function)Data.SBV.String
2 (Function)Data.SBV.List
ConcreteData.SBV.Internals
conditionalSetClearCorrectDocumentation.SBV.Examples.BitPrecise.BitTricks
ConsecutionData.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
constrainData.SBV.Internals, Data.SBV.Trans, Data.SBV
constrainWithAttributeData.SBV.Internals, Data.SBV.Trans, Data.SBV
contextStateData.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
correctnessTheoremDocumentation.SBV.Examples.BitPrecise.Legato
CountDocumentation.SBV.Examples.Puzzles.Counts
count 
1 (Function)Documentation.SBV.Examples.Puzzles.Counts
2 (Function)Documentation.SBV.Examples.Puzzles.Garden
CounterexampleDocumentation.SBV.Examples.Transformers.SymbolicEval
countLeadingZerosData.SBV.Trans, Data.SBV
countsDocumentation.SBV.Examples.Puzzles.Counts
countTrailingZerosData.SBV.Trans, Data.SBV
crcData.SBV.Tools.Polynomial
crcBVData.SBV.Tools.Polynomial
crcGood 
1 (Function)Documentation.SBV.Examples.CodeGeneration.CRC_USB5
2 (Function)Documentation.SBV.Examples.Existentials.CRCPolynomial
crcUSBDocumentation.SBV.Examples.CodeGeneration.CRC_USB5
crcUSB'Documentation.SBV.Examples.CodeGeneration.CRC_USB5
crc_48_16Documentation.SBV.Examples.Existentials.CRCPolynomial
createData.SBV.Control
CriticalDocumentation.SBV.Examples.Lists.BoundedMutex
crossTimeDocumentation.SBV.Examples.Puzzles.U2Bridge
csDemo1Documentation.SBV.Examples.Queries.CaseSplit
csDemo2Documentation.SBV.Examples.Queries.CaseSplit
CSetData.SBV.Internals, Data.SBV.Dynamic
CStringData.SBV.Internals, Data.SBV.Dynamic
CTupleData.SBV.Internals, Data.SBV.Dynamic
CUserSortData.SBV.Internals, Data.SBV.Dynamic
CustomLogicData.SBV.Trans, Data.SBV
CV 
1 (Type/Class)Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor)Data.SBV.Internals, Data.SBV.Dynamic
CValData.SBV.Internals, Data.SBV.Dynamic
CVC4Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
cvc4Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
cvSameTypeData.SBV.Internals
cvtModelData.SBV.Trans, Data.SBV
cvToBoolData.SBV.Internals, Data.SBV.Dynamic
cvToSMTLibData.SBV.Internals
cvValData.SBV.Internals, Data.SBV.Dynamic