sbv-0.9.14: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

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
addSubData.SBV.Examples.CodeGeneration.AddSub
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
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
CgPgmBundle 
1 (Type/Class)Data.SBV
2 (Data Constructor)Data.SBV
cg_runLegatoData.SBV.Examples.BitPrecise.Legato
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
compileToSMTLibData.SBV
complementData.SBV
complementBitData.SBV
conditionalSetClearCorrectData.SBV.Examples.BitPrecise.BitTricks
correctnessTheoremData.SBV.Examples.BitPrecise.Legato
CountData.SBV.Examples.Puzzles.DogCatMouse
crossTimeData.SBV.Examples.Puzzles.U2Bridge
cvtModelData.SBV
CWData.SBV.Internals
defaultSMTCfgData.SBV
dexData.SBV.Examples.BitPrecise.Legato
diagData.SBV.Examples.Puzzles.MagicSquare
displayModelsData.SBV
dispSolutionData.SBV.Examples.Puzzles.Sudoku
EdgeData.SBV.Examples.Puzzles.U2Bridge
edgeData.SBV.Examples.Puzzles.U2Bridge
ElemData.SBV.Examples.Puzzles.MagicSquare
endData.SBV.Examples.BitPrecise.Legato
engineData.SBV
EqSymbolicData.SBV
EqualityData.SBV
euler185Data.SBV.Examples.Puzzles.Euler185
executableData.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
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.PrefixSum.PrefixSum
forAllData.SBV
forAll_Data.SBV
freeData.SBV
free_Data.SBV
FromBitsData.SBV
fromBitsBEData.SBV
fromBitsLEData.SBV
fromBoolData.SBV
fromCWData.SBV
genAddSubData.SBV.Examples.CodeGeneration.AddSub
generateGoldCheckData.SBV.Internals
genFib1Data.SBV.Examples.CodeGeneration.Fibonacci
genFib2Data.SBV.Examples.CodeGeneration.Fibonacci
genFreeData.SBV.Internals
genFree_Data.SBV.Internals
genGCDInCData.SBV.Examples.CodeGeneration.GCD
genPopCountInCData.SBV.Examples.CodeGeneration.PopulationCount
genPrefixSumInstanceData.SBV.Examples.PrefixSum.PrefixSum
getFlagData.SBV.Examples.BitPrecise.Legato
getModelData.SBV
getRegData.SBV.Examples.BitPrecise.Legato
GF28Data.SBV.Examples.Polynomials.Polynomials
guessesData.SBV.Examples.Puzzles.Euler185
hereData.SBV.Examples.Puzzles.U2Bridge
hexData.SBV
hexSData.SBV
initMachineData.SBV.Examples.BitPrecise.Legato
InitValsData.SBV.Examples.BitPrecise.Legato
InstructionData.SBV.Examples.BitPrecise.Legato
IntData.SBV
Int16Data.SBV
Int32Data.SBV
Int64Data.SBV
Int8Data.SBV
ioShowsAsData.SBV.Internals
isConcreteData.SBV
isConcretelyData.SBV
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
lAdamData.SBV.Examples.Puzzles.U2Bridge
ladnerFischerTraceData.SBV.Examples.PrefixSum.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.PrefixSum.PrefixSum
literalData.SBV
lLarryData.SBV.Examples.Puzzles.U2Bridge
LocationData.SBV.Examples.Puzzles.U2Bridge
lsbData.SBV
magicData.SBV.Examples.Puzzles.MagicSquare
MemoryData.SBV.Examples.BitPrecise.Legato
memoryData.SBV.Examples.BitPrecise.Legato
MergeableData.SBV
mergeArraysData.SBV
mkConstCWData.SBV.Internals
mkFreeVarsData.SBV
mkSFunArrayData.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
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.PrefixSum.PrefixSum
powerOfTwoCorrectData.SBV.Examples.BitPrecise.BitTricks
PredicateData.SBV
prefixSumData.SBV.Examples.PrefixSum.PrefixSum
PrettyNumData.SBV
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.PrefixSum.PrefixSum
PuzzleData.SBV.Examples.Puzzles.Sudoku
puzzleData.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
readArrayData.SBV
readBinData.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
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
SArrayData.SBV
satData.SBV
SatisfiableData.SBV
SatModelData.SBV
SatResult 
1 (Type/Class)Data.SBV
2 (Data Constructor)Data.SBV
satWithData.SBV
SBoolData.SBV
SBV 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
SBVTestSuite 
1 (Type/Class)Data.SBV.Internals
2 (Data Constructor)Data.SBV.Internals
SBVUFData.SBV
sbvUFNameData.SBV
scanlTraceData.SBV.Examples.PrefixSum.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
shiftRData.SBV
showPolyData.SBV
showsAsData.SBV.Internals
SInt16Data.SBV
SInt32Data.SBV
SInt64Data.SBV
SInt8Data.SBV
smaxData.SBV
sminData.SBV
SMTConfig 
1 (Type/Class)Data.SBV
2 (Data Constructor)Data.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.DogCatMouse
2 (Function)Data.SBV.Examples.Puzzles.Euler185
3 (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
Status 
1 (Type/Class)Data.SBV.Examples.Puzzles.U2Bridge
2 (Data Constructor)Data.SBV.Examples.Puzzles.U2Bridge
SU2MemberData.SBV.Examples.Puzzles.U2Bridge
SWord16Data.SBV
SWord32Data.SBV
SWord64Data.SBV
SWord8Data.SBV
SymArrayData.SBV
SymbolicData.SBV
symbolicMergeData.SBV
SymWordData.SBV
TestData.SBV.Internals
testData.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.PrefixSum.PrefixSum
2 (Function)Data.SBV.Examples.Uninterpreted.AUF
thm2 
1 (Function)Data.SBV.Examples.PrefixSum.PrefixSum
2 (Function)Data.SBV.Examples.Uninterpreted.AUF
thm3Data.SBV.Examples.PrefixSum.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.PrefixSum.PrefixSum
TimeData.SBV.Examples.Puzzles.U2Bridge
timeData.SBV.Examples.Puzzles.U2Bridge
TimeOutData.SBV
timeoutData.SBV
timingData.SBV
timingSMTCfgData.SBV
trueData.SBV
U2MemberData.SBV.Examples.Puzzles.U2Bridge
uninterpretData.SBV
UninterpretedData.SBV
uninterpretWithHandleData.SBV
UnknownData.SBV
unliteralData.SBV
UnsatisfiableData.SBV
unzipPLData.SBV.Examples.PrefixSum.PrefixSum
validData.SBV.Examples.Puzzles.Sudoku
ValueData.SBV.Examples.BitPrecise.Legato
verboseData.SBV
verboseSMTCfgData.SBV
verboseTimingSMTCfgData.SBV
whenSData.SBV.Examples.Puzzles.U2Bridge
whereIsData.SBV.Examples.Puzzles.U2Bridge
WordData.SBV
Word16Data.SBV
Word32Data.SBV
Word64Data.SBV
Word8Data.SBV
writeArrayData.SBV
xferFlashData.SBV.Examples.Puzzles.U2Bridge
xferPersonData.SBV.Examples.Puzzles.U2Bridge
xorData.SBV
yicesData.SBV
zipPLData.SBV.Examples.PrefixSum.PrefixSum
|||Data.SBV
~&Data.SBV
~:Data.SBV.Internals
~|Data.SBV