sbv-0.9.23: Symbolic bit vectors: Bit-precise verification and automatic C-code generation.

Index

#Data.SBV
&&&Data.SBV
.&.Data.SBV
./=Data.SBV
.<Data.SBV
.<=Data.SBV
.==Data.SBV
.>Data.SBV
.>=Data.SBV
.|.Data.SBV
<*>Data.SBV.Examples.Polynomials.Polynomials
<+>Data.SBV
<=>Data.SBV
===Data.SBV
==>Data.SBV
AData.SBV.Examples.Uninterpreted.AUF
ActionsData.SBV.Examples.Puzzles.U2Bridge
AdamData.SBV.Examples.Puzzles.U2Bridge
adamData.SBV.Examples.Puzzles.U2Bridge
adcData.SBV.Examples.BitPrecise.Legato
addAxiomData.SBV
AddressData.SBV.Examples.BitPrecise.Legato
addRoundKeyData.SBV.Examples.Crypto.AES
addSubData.SBV.Examples.CodeGeneration.AddSub
aes128IsCorrectData.SBV.Examples.Crypto.AES
aes128LibComponentsData.SBV.Examples.Crypto.AES
aesDecryptData.SBV.Examples.Crypto.AES
aesEncryptData.SBV.Examples.Crypto.AES
aesInvRoundData.SBV.Examples.Crypto.AES
aesKeyScheduleData.SBV.Examples.Crypto.AES
aesRoundData.SBV.Examples.Crypto.AES
allDifferentData.SBV
allEqualData.SBV
allPuzzlesData.SBV.Examples.Puzzles.Sudoku
allSatData.SBV
AllSatResult 
1 (Type/Class)Data.SBV
2 (Data Constructor)Data.SBV
allSatWithData.SBV
assertData.SBV.Internals
AssertableData.SBV.Internals
AssertionData.SBV.Internals
BData.SBV.Examples.Uninterpreted.AUF
bAllData.SBV
bAndData.SBV
bAnyData.SBV
bccData.SBV.Examples.BitPrecise.Legato
binData.SBV
binSData.SBV
BitData.SBV.Examples.BitPrecise.Legato
bitData.SBV
BitsData.SBV
bitSizeData.SBV
bitValueData.SBV
blastBEData.SBV
blastLEData.SBV
bneData.SBV.Examples.BitPrecise.Legato
bnotData.SBV
Board 
1 (Type/Class)Data.SBV.Examples.Puzzles.MagicSquare
2 (Type/Class)Data.SBV.Examples.Puzzles.Sudoku
BonoData.SBV.Examples.Puzzles.U2Bridge
bonoData.SBV.Examples.Puzzles.U2Bridge
BooleanData.SBV
bOrData.SBV
bumpTime1Data.SBV.Examples.Puzzles.U2Bridge
bumpTime2Data.SBV.Examples.Puzzles.U2Bridge
BVDivisibleData.SBV
bvQuotRemData.SBV
cg1Data.SBV.Examples.CodeGeneration.CRC_USB5
cg2Data.SBV.Examples.CodeGeneration.CRC_USB5
cgAddDeclData.SBV
cgAddLDFlagsData.SBV
cgAddPrototypeData.SBV
cgAES128BlockEncryptData.SBV.Examples.Crypto.AES
cgAES128LibraryData.SBV.Examples.Crypto.AES
CgDriverData.SBV.Internals
cgGenerateDriverData.SBV
CgHeaderData.SBV.Internals
cgInputData.SBV
cgInputArrData.SBV
cgIntegerSizeData.SBV
CgMakefileData.SBV.Internals
cgOutputData.SBV
cgOutputArrData.SBV
cgPerformRTCsData.SBV
CgPgmBundle 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
CgPgmKindData.SBV.Internals
cgReturnData.SBV
cgReturnArrData.SBV
cgSetDriverValuesData.SBV
CgSourceData.SBV.Internals
cgUninterpretData.SBV
check 
1 (Function)Data.SBV.Examples.Puzzles.MagicSquare
2 (Function)Data.SBV.Examples.Puzzles.Sudoku
checkOverflowData.SBV.Examples.BitPrecise.Legato
checkOverflowCorrectData.SBV.Examples.BitPrecise.Legato
chunkData.SBV.Examples.Puzzles.MagicSquare
clcData.SBV.Examples.BitPrecise.Legato
clearBitData.SBV
compileToCData.SBV
compileToC'Data.SBV.Internals
compileToCLibData.SBV
compileToCLib'Data.SBV.Internals
compileToSMTLibData.SBV
complementData.SBV
complementBitData.SBV
conditionalSetClearCorrectData.SBV.Examples.BitPrecise.BitTricks
correctnessTheoremData.SBV.Examples.BitPrecise.Legato
Count 
1 (Type/Class)Data.SBV.Examples.Puzzles.Counts
2 (Type/Class)Data.SBV.Examples.Puzzles.DogCatMouse
countData.SBV.Examples.Puzzles.Counts
CountsData.SBV.Examples.Puzzles.Counts
crcData.SBV
crcBVData.SBV
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
cvtModelData.SBV
CWData.SBV.Internals
decryptData.SBV.Examples.Crypto.RC4
dexData.SBV.Examples.BitPrecise.Legato
diagData.SBV.Examples.Puzzles.MagicSquare
diffCountData.SBV.Examples.Existentials.CRCPolynomial
displayModelsData.SBV
dispSolutionData.SBV.Examples.Puzzles.Sudoku
doRoundsData.SBV.Examples.Crypto.AES
EdgeData.SBV.Examples.Puzzles.U2Bridge
edgeData.SBV.Examples.Puzzles.U2Bridge
ElemData.SBV.Examples.Puzzles.MagicSquare
encryptData.SBV.Examples.Crypto.RC4
endData.SBV.Examples.BitPrecise.Legato
engineData.SBV
EqSymbolicData.SBV
EqualityData.SBV
euler185Data.SBV.Examples.Puzzles.Euler185
executableData.SBV
existsData.SBV
exists_Data.SBV
extendData.SBV
ExtractData.SBV.Examples.BitPrecise.Legato
f 
1 (Function)Data.SBV.Examples.Uninterpreted.AUF
2 (Function)Data.SBV.Examples.Uninterpreted.Function
falseData.SBV
fastMaxCorrectData.SBV.Examples.BitPrecise.BitTricks
fastMinCorrectData.SBV.Examples.BitPrecise.BitTricks
fastPopCountIsCorrectData.SBV.Examples.CodeGeneration.PopulationCount
fib0Data.SBV.Examples.CodeGeneration.Fibonacci
fib1Data.SBV.Examples.CodeGeneration.Fibonacci
fib2Data.SBV.Examples.CodeGeneration.Fibonacci
findHD4PolynomialsData.SBV.Examples.Existentials.CRCPolynomial
FlagData.SBV.Examples.BitPrecise.Legato
FlagCData.SBV.Examples.BitPrecise.Legato
FlagsData.SBV.Examples.BitPrecise.Legato
flagsData.SBV.Examples.BitPrecise.Legato
FlagZData.SBV.Examples.BitPrecise.Legato
flashData.SBV.Examples.Puzzles.U2Bridge
flIsCorrectData.SBV.Examples.BitPrecise.PrefixSum
forAllData.SBV
forallData.SBV
forAll_Data.SBV
forall_Data.SBV
FromBitsData.SBV
fromBitsBEData.SBV
fromBitsLEData.SBV
fromBoolData.SBV
fromBytesData.SBV.Examples.Crypto.AES
fromCWData.SBV
genAddSubData.SBV.Examples.CodeGeneration.AddSub
genCCodeData.SBV.Examples.CodeGeneration.Uninterpreted
generateGoldCheckData.SBV.Internals
genFib1Data.SBV.Examples.CodeGeneration.Fibonacci
genFib2Data.SBV.Examples.CodeGeneration.Fibonacci
genFinVarData.SBV.Internals
genFinVar_Data.SBV.Internals
genGCDInCData.SBV.Examples.CodeGeneration.GCD
genPolyData.SBV.Examples.Existentials.CRCPolynomial
genPopCountInCData.SBV.Examples.CodeGeneration.PopulationCount
genPrefixSumInstanceData.SBV.Examples.BitPrecise.PrefixSum
getFlagData.SBV.Examples.BitPrecise.Legato
getModelData.SBV
getRegData.SBV.Examples.BitPrecise.Legato
GF28 
1 (Type/Class)Data.SBV.Examples.Crypto.AES
2 (Type/Class)Data.SBV.Examples.Polynomials.Polynomials
gf28InverseData.SBV.Examples.Crypto.AES
gf28MultData.SBV.Examples.Crypto.AES
gf28PowData.SBV.Examples.Crypto.AES
guessesData.SBV.Examples.Puzzles.Euler185
hasSignData.SBV.Internals
HasSignAndSizeData.SBV.Internals
hereData.SBV.Examples.Puzzles.U2Bridge
hexData.SBV
hexSData.SBV
initMachineData.SBV.Examples.BitPrecise.Legato
initRC4Data.SBV.Examples.Crypto.RC4
initSData.SBV.Examples.Crypto.RC4
InitValsData.SBV.Examples.BitPrecise.Legato
InstructionData.SBV.Examples.BitPrecise.Legato
IntData.SBV
Int16Data.SBV
Int32Data.SBV
Int64Data.SBV
Int8Data.SBV
intSizeOfData.SBV.Internals
invMixColumnsData.SBV.Examples.Crypto.AES
ioShowsAsData.SBV.Internals
isConcreteData.SBV
isConcretelyData.SBV
isInfPrecData.SBV.Internals
isMagicData.SBV.Examples.Puzzles.MagicSquare
isSatisfiableData.SBV
isSatisfiableWithinData.SBV
isSignedData.SBV
isSymbolicData.SBV
isTheoremData.SBV
isTheoremWithinData.SBV
isU2MemberData.SBV.Examples.Puzzles.U2Bridge
isValid 
1 (Function)Data.SBV.Examples.Puzzles.NQueens
2 (Function)Data.SBV.Examples.Puzzles.U2Bridge
iteData.SBV
Key 
1 (Type/Class)Data.SBV.Examples.Crypto.AES
2 (Type/Class)Data.SBV.Examples.Crypto.RC4
keyExpansionData.SBV.Examples.Crypto.AES
keyScheduleData.SBV.Examples.Crypto.RC4
keyScheduleStringData.SBV.Examples.Crypto.RC4
KSData.SBV.Examples.Crypto.AES
lAdamData.SBV.Examples.Puzzles.U2Bridge
ladnerFischerTraceData.SBV.Examples.BitPrecise.PrefixSum
LarryData.SBV.Examples.Puzzles.U2Bridge
larryData.SBV.Examples.Puzzles.U2Bridge
lBonoData.SBV.Examples.Puzzles.U2Bridge
ldaData.SBV.Examples.BitPrecise.Legato
ldxData.SBV.Examples.BitPrecise.Legato
lEdgeData.SBV.Examples.Puzzles.U2Bridge
legatoData.SBV.Examples.BitPrecise.Legato
legatoInCData.SBV.Examples.BitPrecise.Legato
legatoIsCorrectData.SBV.Examples.BitPrecise.Legato
lfData.SBV.Examples.BitPrecise.PrefixSum
literalData.SBV
lLarryData.SBV.Examples.Puzzles.U2Bridge
LocationData.SBV.Examples.Puzzles.U2Bridge
lsbData.SBV
magicData.SBV.Examples.Puzzles.MagicSquare
maximizeData.SBV
mbMaxBoundData.SBV
mbMinBoundData.SBV
MemoryData.SBV.Examples.BitPrecise.Legato
memoryData.SBV.Examples.BitPrecise.Legato
MergeableData.SBV
mergeArraysData.SBV
minimizeData.SBV
mkConstCWData.SBV.Internals
mkExistVarsData.SBV
mkForallVarsData.SBV
mkSFunArrayData.SBV
mkSTreeData.SBV
mkTestSuiteData.SBV.Internals
ModelData.SBV.Examples.BitPrecise.Legato
Mostek 
1 (Type/Class)Data.SBV.Examples.BitPrecise.Legato
2 (Data Constructor)Data.SBV.Examples.BitPrecise.Legato
MoveData.SBV.Examples.Puzzles.U2Bridge
move1Data.SBV.Examples.Puzzles.U2Bridge
move2Data.SBV.Examples.Puzzles.U2Bridge
msbData.SBV
multAssocData.SBV.Examples.Polynomials.Polynomials
multCommData.SBV.Examples.Polynomials.Polynomials
multUnitData.SBV.Examples.Polynomials.Polynomials
nameData.SBV
newArrayData.SBV
newArray_Data.SBV
nQueensData.SBV.Examples.Puzzles.NQueens
numberOfModelsData.SBV
oneIfData.SBV
oppositeSignsCorrectData.SBV.Examples.BitPrecise.BitTricks
optimizeData.SBV
optionsData.SBV
OrdSymbolicData.SBV
outputData.SBV
pAddData.SBV
parseCWsData.SBV
pDivData.SBV
pDivModData.SBV
peek 
1 (Function)Data.SBV.Examples.BitPrecise.Legato
2 (Function)Data.SBV.Examples.Puzzles.U2Bridge
pModData.SBV
pMultData.SBV
pokeData.SBV.Examples.BitPrecise.Legato
polyDivModData.SBV.Examples.Polynomials.Polynomials
PolynomialData.SBV
polynomialData.SBV
pop8Data.SBV.Examples.CodeGeneration.PopulationCount
popCountData.SBV.Examples.CodeGeneration.PopulationCount
popCount_SlowData.SBV.Examples.CodeGeneration.PopulationCount
PowerListData.SBV.Examples.BitPrecise.PrefixSum
powerOfTwoCorrectData.SBV.Examples.BitPrecise.BitTricks
PredicateData.SBV
prefixSumData.SBV.Examples.BitPrecise.PrefixSum
PrettyNumData.SBV
prgaData.SBV.Examples.Crypto.RC4
printBaseData.SBV
ProgramData.SBV.Examples.BitPrecise.Legato
ProofErrorData.SBV
ProvableData.SBV
proveData.SBV
proveThm1Data.SBV.Examples.Uninterpreted.AUF
proveThm2Data.SBV.Examples.Uninterpreted.AUF
proveWithData.SBV
psData.SBV.Examples.BitPrecise.PrefixSum
PuzzleData.SBV.Examples.Puzzles.Sudoku
puzzle 
1 (Function)Data.SBV.Examples.Puzzles.Counts
2 (Function)Data.SBV.Examples.Puzzles.DogCatMouse
puzzle0Data.SBV.Examples.Puzzles.Sudoku
puzzle1Data.SBV.Examples.Puzzles.Sudoku
puzzle2Data.SBV.Examples.Puzzles.Sudoku
puzzle3Data.SBV.Examples.Puzzles.Sudoku
puzzle4Data.SBV.Examples.Puzzles.Sudoku
puzzle5Data.SBV.Examples.Puzzles.Sudoku
puzzle6Data.SBV.Examples.Puzzles.Sudoku
queriesData.SBV.Examples.BitPrecise.BitTricks
RC4Data.SBV.Examples.Crypto.RC4
rc4IsCorrectData.SBV.Examples.Crypto.RC4
readArrayData.SBV
readBinData.SBV
readSTreeData.SBV
RegAData.SBV.Examples.BitPrecise.Legato
RegisterData.SBV.Examples.BitPrecise.Legato
RegistersData.SBV.Examples.BitPrecise.Legato
registersData.SBV.Examples.BitPrecise.Legato
RegXData.SBV.Examples.BitPrecise.Legato
resetArrayData.SBV
ResultData.SBV.Internals
rorMData.SBV.Examples.BitPrecise.Legato
rorRData.SBV.Examples.BitPrecise.Legato
rotateData.SBV
rotateLData.SBV
rotateRData.SBV
rotRData.SBV.Examples.Crypto.AES
roundConstantsData.SBV.Examples.Crypto.AES
Row 
1 (Type/Class)Data.SBV.Examples.Puzzles.MagicSquare
2 (Type/Class)Data.SBV.Examples.Puzzles.Sudoku
runData.SBV.Examples.Puzzles.U2Bridge
runLegatoData.SBV.Examples.BitPrecise.Legato
runSymbolicData.SBV.Internals
SData.SBV.Examples.Crypto.RC4
SArrayData.SBV
satData.SBV
SatisfiableData.SBV
SatModelData.SBV
SatResult 
1 (Type/Class)Data.SBV
2 (Data Constructor)Data.SBV
satWithData.SBV
SBoolData.SBV
sboxData.SBV.Examples.Crypto.AES
sboxInverseCorrectData.SBV.Examples.Crypto.AES
sboxTableData.SBV.Examples.Crypto.AES
SBV 
1 (Type/Class)Data.SBV.Internals, Data.SBV
2 (Data Constructor)Data.SBV.Internals
SBVCodeGenData.SBV
SBVTestSuite 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
SBVUFData.SBV
sbvUFNameData.SBV
sbvUninterpretData.SBV
scanlTraceData.SBV.Examples.BitPrecise.PrefixSum
selectData.SBV
setBitData.SBV
setBitToData.SBV
setFlagData.SBV.Examples.BitPrecise.Legato
setRegData.SBV.Examples.BitPrecise.Legato
SFunArrayData.SBV
sgcdData.SBV.Examples.CodeGeneration.GCD
sgcdIsCorrectData.SBV.Examples.CodeGeneration.GCD
shiftData.SBV
shiftLData.SBV
shiftLeftData.SBV.Examples.CodeGeneration.Uninterpreted
shiftRData.SBV
showPolyData.SBV
showPolynomialData.SBV
showsAsData.SBV.Internals
showTypeData.SBV.Internals
SignCastData.SBV
signCastData.SBV
SInt16Data.SBV
SInt32Data.SBV
SInt64Data.SBV
SInt8Data.SBV
SIntegerData.SBV
sizeOfData.SBV.Internals
smaxData.SBV
sminData.SBV
SMTConfig 
1 (Type/Class)Data.SBV
2 (Data Constructor)Data.SBV
smtFileData.SBV
SMTResultData.SBV
SMTSolver 
1 (Type/Class)Data.SBV
2 (Data Constructor)Data.SBV
SolutionData.SBV.Examples.Puzzles.NQueens
solve 
1 (Function)Data.SBV.Examples.Puzzles.Counts
2 (Function)Data.SBV.Examples.Puzzles.DogCatMouse
3 (Function)Data.SBV.Examples.Puzzles.Euler185
4 (Function)Data.SBV.Examples.Puzzles.Sudoku
solveAllData.SBV.Examples.Puzzles.Sudoku
solveNData.SBV.Examples.Puzzles.U2Bridge
solverData.SBV
solveU2Data.SBV.Examples.Puzzles.U2Bridge
splitData.SBV
SplittableData.SBV
startData.SBV.Examples.Puzzles.U2Bridge
StateData.SBV.Examples.Crypto.AES
Status 
1 (Type/Class)Data.SBV.Examples.Puzzles.U2Bridge
2 (Data Constructor)Data.SBV.Examples.Puzzles.U2Bridge
STreeData.SBV
SU2MemberData.SBV.Examples.Puzzles.U2Bridge
swapData.SBV.Examples.Crypto.RC4
SWord16Data.SBV
SWord32Data.SBV
SWord48Data.SBV.Examples.Existentials.CRCPolynomial
SWord64Data.SBV
SWord8Data.SBV
SymArrayData.SBV
SymbolicData.SBV
symbolicMergeData.SBV
SymWordData.SBV
t0Data.SBV.Examples.Crypto.AES
t0FuncData.SBV.Examples.Crypto.AES
t1Data.SBV.Examples.Crypto.AES
t128DecData.SBV.Examples.Crypto.AES
t128EncData.SBV.Examples.Crypto.AES
t192DecData.SBV.Examples.Crypto.AES
t192EncData.SBV.Examples.Crypto.AES
t2Data.SBV.Examples.Crypto.AES
t256DecData.SBV.Examples.Crypto.AES
t256EncData.SBV.Examples.Crypto.AES
t3Data.SBV.Examples.Crypto.AES
TestData.SBV.Internals
testData.SBV.Internals
TestableData.SBV.Internals
testBitData.SBV
TestCaseData.SBV.Internals
testGF28Data.SBV.Examples.Polynomials.Polynomials
TestLabelData.SBV.Internals
TestListData.SBV.Internals
thereData.SBV.Examples.Puzzles.U2Bridge
thm1 
1 (Function)Data.SBV.Examples.BitPrecise.PrefixSum
2 (Function)Data.SBV.Examples.Uninterpreted.AUF
thm2 
1 (Function)Data.SBV.Examples.BitPrecise.PrefixSum
2 (Function)Data.SBV.Examples.Uninterpreted.AUF
thm3Data.SBV.Examples.BitPrecise.PrefixSum
thmBadData.SBV.Examples.Uninterpreted.Function
thmGoodData.SBV.Examples.Uninterpreted.Function
ThmResult 
1 (Type/Class)Data.SBV
2 (Data Constructor)Data.SBV
tiePLData.SBV.Examples.BitPrecise.PrefixSum
TimeData.SBV.Examples.Puzzles.U2Bridge
timeData.SBV.Examples.Puzzles.U2Bridge
TimeOutData.SBV
timeOutData.SBV
timingData.SBV
toBytesData.SBV.Examples.Crypto.AES
trueData.SBV
tstShiftLeftData.SBV.Examples.CodeGeneration.Uninterpreted
u0Data.SBV.Examples.Crypto.AES
u0FuncData.SBV.Examples.Crypto.AES
u1Data.SBV.Examples.Crypto.AES
u2Data.SBV.Examples.Crypto.AES
U2MemberData.SBV.Examples.Puzzles.U2Bridge
u3Data.SBV.Examples.Crypto.AES
uninterpretData.SBV
UninterpretedData.SBV
uninterpretWithHandleData.SBV
UnknownData.SBV
unliteralData.SBV
UnsatisfiableData.SBV
unSBoxData.SBV.Examples.Crypto.AES
unSBoxTableData.SBV.Examples.Crypto.AES
unsignCastData.SBV
unzipPLData.SBV.Examples.BitPrecise.PrefixSum
usb5Data.SBV.Examples.CodeGeneration.CRC_USB5
useSMTLib2Data.SBV
validData.SBV.Examples.Puzzles.Sudoku
ValueData.SBV.Examples.BitPrecise.Legato
verboseData.SBV
whenSData.SBV.Examples.Puzzles.U2Bridge
whereIsData.SBV.Examples.Puzzles.U2Bridge
WordData.SBV
Word16Data.SBV
Word32Data.SBV
Word64Data.SBV
Word8Data.SBV
writeArrayData.SBV
writeSTreeData.SBV
xferFlashData.SBV.Examples.Puzzles.U2Bridge
xferPersonData.SBV.Examples.Puzzles.U2Bridge
xorData.SBV
yicesData.SBV
z3Data.SBV
zipPLData.SBV.Examples.BitPrecise.PrefixSum
|||Data.SBV
~&Data.SBV
~:Data.SBV.Internals
~|Data.SBV