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

Index - C

C 
1 (Data Constructor)Data.SBV.Tools.GenTest
2 (Data Constructor)Data.SBV.Examples.Misc.Enumerate
c1Data.SBV.Examples.Puzzles.Coins
c2Data.SBV.Examples.Puzzles.Coins
c3Data.SBV.Examples.Puzzles.Coins
c4Data.SBV.Examples.Puzzles.Coins
c5Data.SBV.Examples.Puzzles.Coins
c6Data.SBV.Examples.Puzzles.Coins
cacheData.SBV.Internals
CachedData.SBV.Internals
capabilitiesData.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
capSolverNameData.SBV.Internals
CaseCondData.SBV.Internals
CaseCovData.SBV.Internals
CasePathData.SBV.Internals
CaseSplitData.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
CaseVacData.SBV.Internals
CatData.SBV.Examples.Puzzles.Fish
cg1Data.SBV.Examples.CodeGeneration.CRC_USB5
cg2Data.SBV.Examples.CodeGeneration.CRC_USB5
cgAddDeclData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgAddLDFlagsData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgAddPrototypeData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgAES128BlockEncryptData.SBV.Examples.Crypto.AES
cgAES128LibraryData.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.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
CgDriverData.SBV.Internals
cgDriverValsData.SBV.Internals
cgFinalConfigData.SBV.Internals
CgFloatData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgGenDriverData.SBV.Internals
cgGenerateDriverData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgGenerateMakefileData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgGenMakefileData.SBV.Internals
CgHeaderData.SBV.Internals
cgIgnoreAssertsData.SBV.Internals
cgIgnoreSAssertData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgInputData.SBV.Internals, Data.SBV.Tools.CodeGen
cgInputArrData.SBV.Internals, Data.SBV.Tools.CodeGen
cgInputsData.SBV.Internals
cgIntegerData.SBV.Internals
cgIntegerSizeData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgLDFlagsData.SBV.Internals
CgLongDoubleData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
CgMakefileData.SBV.Internals
cgOutputData.SBV.Internals, Data.SBV.Tools.CodeGen
cgOutputArrData.SBV.Internals, Data.SBV.Tools.CodeGen
cgOutputsData.SBV.Internals
cgPerformRTCsData.SBV.Internals, Data.SBV.Tools.CodeGen, 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.Internals, Data.SBV.Tools.CodeGen
cgReturnArrData.SBV.Internals, Data.SBV.Tools.CodeGen
cgReturnsData.SBV.Internals
cgRTCData.SBV.Internals
cgSetDriverValuesData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
CgSourceData.SBV.Internals
CgSRealTypeData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
cgSRealTypeData.SBV.Internals, Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
CgState 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
CgTargetData.SBV.Internals
cgUninterpretData.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
CgValData.SBV.Internals
check 
1 (Function)Data.SBV.Examples.Puzzles.MagicSquare
2 (Function)Data.SBV.Examples.Puzzles.Sudoku
checkAndConvertData.SBV.Internals
CheckCaseVacuityData.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
CheckConstrVacuityData.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
checkedDivData.SBV.Examples.Misc.NoDiv0
checkOverflowData.SBV.Examples.BitPrecise.Legato
checkOverflowCorrectData.SBV.Examples.BitPrecise.Legato
CheckUsingData.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
cherylData.SBV.Examples.Puzzles.Birthday
chunkData.SBV.Examples.Puzzles.MagicSquare
classifyData.SBV.Examples.Uninterpreted.UISortAllSat
clcData.SBV.Examples.BitPrecise.Legato
clearBitData.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
CodeGenData.SBV.Internals
codeGen 
1 (Function)Data.SBV.Internals
2 (Function)Data.SBV.Examples.BitPrecise.MergeSort
CoffeeData.SBV.Examples.Puzzles.Fish
CoinData.SBV.Examples.Puzzles.Coins
ColorData.SBV.Examples.Puzzles.Fish
combinationsData.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
compileToSMTLib 
1 (Function)Data.SBV.Internals
2 (Function)Data.SBV.Dynamic
complementData.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
complementBitData.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
ConcreteData.SBV.Internals
conditionalSetClearCorrectData.SBV.Examples.BitPrecise.BitTricks
ConsData.SBV.Examples.Uninterpreted.UISortAllSat
constrainData.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
correctnessData.SBV.Examples.BitPrecise.MergeSort
correctnessTheoremData.SBV.Examples.BitPrecise.Legato
CountData.SBV.Examples.Puzzles.Counts
countData.SBV.Examples.Puzzles.Counts
countLeadingZerosData.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
countsData.SBV.Examples.Puzzles.Counts
countTrailingZerosData.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
crcData.SBV.Tools.Polynomial
crcBVData.SBV.Tools.Polynomial
crcGood 
1 (Function)Data.SBV.Examples.CodeGeneration.CRC_USB5
2 (Function)Data.SBV.Examples.Existentials.CRCPolynomial
crcUSBData.SBV.Examples.CodeGeneration.CRC_USB5
crcUSB'Data.SBV.Examples.CodeGeneration.CRC_USB5
crc_48_16Data.SBV.Examples.Existentials.CRCPolynomial
crossTimeData.SBV.Examples.Puzzles.U2Bridge
CstrVacData.SBV.Internals
CustomLogicData.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
CVC4Data.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
cvc4Data.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
cvtModelData.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
CWAlgRealData.SBV.Internals, Data.SBV.Dynamic
CWDoubleData.SBV.Internals, Data.SBV.Dynamic
CWFloatData.SBV.Internals, Data.SBV.Dynamic
CWIntegerData.SBV.Internals, Data.SBV.Dynamic
cwSameTypeData.SBV.Internals
cwToBoolData.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
CWUserSortData.SBV.Internals, Data.SBV.Dynamic
CWValData.SBV.Internals, Data.SBV.Dynamic
cwValData.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