Contents
Index
sbv-0.9.3: 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
<=>
Data.SBV
===
Data.SBV
==>
Data.SBV
A
Data.SBV.Examples.Uninterpreted.AUF
Actions
Data.SBV.Examples.Puzzles.U2Bridge
Adam
Data.SBV.Examples.Puzzles.U2Bridge
adam
Data.SBV.Examples.Puzzles.U2Bridge
adc
Data.SBV.Examples.BitPrecise.Legato
Address
Data.SBV.Examples.BitPrecise.Legato
allDifferent
Data.SBV
allEqual
Data.SBV
allPuzzles
Data.SBV.Examples.Puzzles.Sudoku
allSat
Data.SBV
AllSatResult
1 (Type/Class)
Data.SBV
2 (Data Constructor)
Data.SBV
allSatWith
Data.SBV
assert
Data.SBV.Internals
Assertion
Data.SBV.Internals
bAll
Data.SBV
bAnd
Data.SBV
bAny
Data.SBV
bcc
Data.SBV.Examples.BitPrecise.Legato
bin
Data.SBV
binS
Data.SBV
Bit
Data.SBV.Examples.BitPrecise.Legato
bit
Data.SBV
Bits
Data.SBV
bitSize
Data.SBV
bitValue
Data.SBV
blastBE
Data.SBV
blastLE
Data.SBV
bne
Data.SBV.Examples.BitPrecise.Legato
bnot
Data.SBV
Board
1 (Type/Class)
Data.SBV.Examples.Puzzles.MagicSquare
2 (Type/Class)
Data.SBV.Examples.Puzzles.Sudoku
Bono
Data.SBV.Examples.Puzzles.U2Bridge
bono
Data.SBV.Examples.Puzzles.U2Bridge
Boolean
Data.SBV
bOr
Data.SBV
bumpTime1
Data.SBV.Examples.Puzzles.U2Bridge
bumpTime2
Data.SBV.Examples.Puzzles.U2Bridge
BVDivisible
Data.SBV
bvQuotRem
Data.SBV
check
1 (Function)
Data.SBV.Examples.Puzzles.MagicSquare
2 (Function)
Data.SBV.Examples.Puzzles.Sudoku
chunk
Data.SBV.Examples.Puzzles.MagicSquare
clc
Data.SBV.Examples.BitPrecise.Legato
clearBit
Data.SBV
complement
Data.SBV
complementBit
Data.SBV
conditionalSetClearCorrect
Data.SBV.Examples.BitPrecise.BitTricks
correctnessTheorem
Data.SBV.Examples.BitPrecise.Legato
Count
Data.SBV.Examples.Puzzles.DogCatMouse
crossTime
Data.SBV.Examples.Puzzles.U2Bridge
cvtModel
Data.SBV
defaultSMTCfg
Data.SBV
dex
Data.SBV.Examples.BitPrecise.Legato
diag
Data.SBV.Examples.Puzzles.MagicSquare
displayModels
Data.SBV
dispSolution
Data.SBV.Examples.Puzzles.Sudoku
Edge
Data.SBV.Examples.Puzzles.U2Bridge
edge
Data.SBV.Examples.Puzzles.U2Bridge
Elem
Data.SBV.Examples.Puzzles.MagicSquare
end
Data.SBV.Examples.BitPrecise.Legato
engine
Data.SBV
EqSymbolic
Data.SBV
Equality
Data.SBV
executable
Data.SBV
extend
Data.SBV
Extract
Data.SBV.Examples.BitPrecise.Legato
f
Data.SBV.Examples.Uninterpreted.AUF
false
Data.SBV
fastMaxCorrect
Data.SBV.Examples.BitPrecise.BitTricks
fastMinCorrect
Data.SBV.Examples.BitPrecise.BitTricks
Flag
Data.SBV.Examples.BitPrecise.Legato
FlagC
Data.SBV.Examples.BitPrecise.Legato
Flags
Data.SBV.Examples.BitPrecise.Legato
flags
Data.SBV.Examples.BitPrecise.Legato
FlagZ
Data.SBV.Examples.BitPrecise.Legato
flash
Data.SBV.Examples.Puzzles.U2Bridge
forAll
Data.SBV
forAll_
Data.SBV
free
Data.SBV
free_
Data.SBV
FromBits
Data.SBV
fromBitsBE
Data.SBV
fromBitsLE
Data.SBV
fromBool
Data.SBV
fromCW
Data.SBV
generateGoldCheck
Data.SBV.Internals
getFlag
Data.SBV.Examples.BitPrecise.Legato
getModel
Data.SBV
getReg
Data.SBV.Examples.BitPrecise.Legato
here
Data.SBV.Examples.Puzzles.U2Bridge
hex
Data.SBV
hexS
Data.SBV
initMachine
Data.SBV.Examples.BitPrecise.Legato
InitVals
Data.SBV.Examples.BitPrecise.Legato
Instruction
Data.SBV.Examples.BitPrecise.Legato
Int
Data.SBV
Int16
Data.SBV
Int32
Data.SBV
Int64
Data.SBV
Int8
Data.SBV
ioShowsAs
Data.SBV.Internals
isConcrete
Data.SBV
isMagic
Data.SBV.Examples.Puzzles.MagicSquare
isSatisfiable
Data.SBV
isSatisfiableWithin
Data.SBV
isSigned
Data.SBV
isSymbolic
Data.SBV
isTheorem
Data.SBV
isTheoremWithin
Data.SBV
isU2Member
Data.SBV.Examples.Puzzles.U2Bridge
isValid
1 (Function)
Data.SBV.Examples.Puzzles.NQueens
2 (Function)
Data.SBV.Examples.Puzzles.U2Bridge
ite
Data.SBV
lAdam
Data.SBV.Examples.Puzzles.U2Bridge
Larry
Data.SBV.Examples.Puzzles.U2Bridge
larry
Data.SBV.Examples.Puzzles.U2Bridge
lBono
Data.SBV.Examples.Puzzles.U2Bridge
lda
Data.SBV.Examples.BitPrecise.Legato
ldx
Data.SBV.Examples.BitPrecise.Legato
lEdge
Data.SBV.Examples.Puzzles.U2Bridge
legato
Data.SBV.Examples.BitPrecise.Legato
legatoIsCorrect
Data.SBV.Examples.BitPrecise.Legato
literal
Data.SBV
lLarry
Data.SBV.Examples.Puzzles.U2Bridge
Location
Data.SBV.Examples.Puzzles.U2Bridge
lsb
Data.SBV
magic
Data.SBV.Examples.Puzzles.MagicSquare
Memory
Data.SBV.Examples.BitPrecise.Legato
memory
Data.SBV.Examples.BitPrecise.Legato
Mergeable
Data.SBV
mergeArrays
Data.SBV
mkTestSuite
Data.SBV.Internals
Model
Data.SBV.Examples.BitPrecise.Legato
Mostek
1 (Type/Class)
Data.SBV.Examples.BitPrecise.Legato
2 (Data Constructor)
Data.SBV.Examples.BitPrecise.Legato
Move
Data.SBV.Examples.Puzzles.U2Bridge
move1
Data.SBV.Examples.Puzzles.U2Bridge
move2
Data.SBV.Examples.Puzzles.U2Bridge
msb
Data.SBV
name
Data.SBV
newArray
Data.SBV
newArray_
Data.SBV
nQueens
Data.SBV.Examples.Puzzles.NQueens
numberOfModels
Data.SBV
oneIf
Data.SBV
oppositeSignsCorrect
Data.SBV.Examples.BitPrecise.BitTricks
options
Data.SBV
OrdSymbolic
Data.SBV
output
Data.SBV
pAdd
Data.SBV
parseCWs
Data.SBV
pDiv
Data.SBV
pDivMod
Data.SBV
peek
1 (Function)
Data.SBV.Examples.BitPrecise.Legato
2 (Function)
Data.SBV.Examples.Puzzles.U2Bridge
pMod
Data.SBV
pMult
Data.SBV
poke
Data.SBV.Examples.BitPrecise.Legato
Polynomial
Data.SBV
polynomial
Data.SBV
powerOfTwoCorrect
Data.SBV.Examples.BitPrecise.BitTricks
Predicate
Data.SBV
PrettyNum
Data.SBV
printBase
Data.SBV
Program
Data.SBV.Examples.BitPrecise.Legato
ProofError
Data.SBV
Provable
Data.SBV
prove
Data.SBV
proveThm
Data.SBV.Examples.Uninterpreted.AUF
proveWith
Data.SBV
Puzzle
Data.SBV.Examples.Puzzles.Sudoku
puzzle
Data.SBV.Examples.Puzzles.DogCatMouse
puzzle0
Data.SBV.Examples.Puzzles.Sudoku
puzzle1
Data.SBV.Examples.Puzzles.Sudoku
puzzle2
Data.SBV.Examples.Puzzles.Sudoku
puzzle3
Data.SBV.Examples.Puzzles.Sudoku
puzzle4
Data.SBV.Examples.Puzzles.Sudoku
puzzle5
Data.SBV.Examples.Puzzles.Sudoku
puzzle6
Data.SBV.Examples.Puzzles.Sudoku
queries
Data.SBV.Examples.BitPrecise.BitTricks
readArray
Data.SBV
readBin
Data.SBV
RegA
Data.SBV.Examples.BitPrecise.Legato
Register
Data.SBV.Examples.BitPrecise.Legato
Registers
Data.SBV.Examples.BitPrecise.Legato
registers
Data.SBV.Examples.BitPrecise.Legato
RegX
Data.SBV.Examples.BitPrecise.Legato
resetArray
Data.SBV
Result
Data.SBV.Internals
rorM
Data.SBV.Examples.BitPrecise.Legato
rorR
Data.SBV.Examples.BitPrecise.Legato
rotate
Data.SBV
rotateL
Data.SBV
rotateR
Data.SBV
Row
1 (Type/Class)
Data.SBV.Examples.Puzzles.MagicSquare
2 (Type/Class)
Data.SBV.Examples.Puzzles.Sudoku
run
Data.SBV.Examples.Puzzles.U2Bridge
runLegato
Data.SBV.Examples.BitPrecise.Legato
runSymbolic
Data.SBV.Internals
SArray
Data.SBV
sat
Data.SBV
Satisfiable
Data.SBV
SatModel
Data.SBV
SatResult
1 (Type/Class)
Data.SBV
2 (Data Constructor)
Data.SBV
satWith
Data.SBV
SBool
Data.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
select
Data.SBV
setBit
Data.SBV
setBitTo
Data.SBV
setFlag
Data.SBV.Examples.BitPrecise.Legato
setReg
Data.SBV.Examples.BitPrecise.Legato
SFunArray
Data.SBV
shift
Data.SBV
shiftL
Data.SBV
shiftR
Data.SBV
showPoly
Data.SBV
showsAs
Data.SBV.Internals
SInt16
Data.SBV
SInt32
Data.SBV
SInt64
Data.SBV
SInt8
Data.SBV
smax
Data.SBV
smin
Data.SBV
SMTConfig
1 (Type/Class)
Data.SBV
2 (Data Constructor)
Data.SBV
SMTResult
Data.SBV
SMTSolver
1 (Type/Class)
Data.SBV
2 (Data Constructor)
Data.SBV
Solution
Data.SBV.Examples.Puzzles.NQueens
solve
1 (Function)
Data.SBV.Examples.Puzzles.DogCatMouse
2 (Function)
Data.SBV.Examples.Puzzles.Sudoku
solveAll
Data.SBV.Examples.Puzzles.Sudoku
solveN
Data.SBV.Examples.Puzzles.U2Bridge
solver
Data.SBV
solveU2
Data.SBV.Examples.Puzzles.U2Bridge
split
Data.SBV
Splittable
Data.SBV
start
Data.SBV.Examples.Puzzles.U2Bridge
Status
1 (Type/Class)
Data.SBV.Examples.Puzzles.U2Bridge
2 (Data Constructor)
Data.SBV.Examples.Puzzles.U2Bridge
SU2Member
Data.SBV.Examples.Puzzles.U2Bridge
SWord16
Data.SBV
SWord32
Data.SBV
SWord64
Data.SBV
SWord8
Data.SBV
SymArray
Data.SBV
Symbolic
Data.SBV
symbolicMerge
Data.SBV
SymWord
Data.SBV
Test
Data.SBV.Internals
test
Data.SBV.Internals
testBit
Data.SBV
TestCase
Data.SBV.Internals
TestLabel
Data.SBV.Internals
TestList
Data.SBV.Internals
there
Data.SBV.Examples.Puzzles.U2Bridge
thm
Data.SBV.Examples.Uninterpreted.AUF
ThmResult
1 (Type/Class)
Data.SBV
2 (Data Constructor)
Data.SBV
Time
Data.SBV.Examples.Puzzles.U2Bridge
time
Data.SBV.Examples.Puzzles.U2Bridge
TimeOut
Data.SBV
timeout
Data.SBV
timing
Data.SBV
timingSMTCfg
Data.SBV
true
Data.SBV
U2Member
Data.SBV.Examples.Puzzles.U2Bridge
uninterpret
Data.SBV
Uninterpreted
Data.SBV
Unknown
Data.SBV
unliteral
Data.SBV
Unsatisfiable
Data.SBV
valid
Data.SBV.Examples.Puzzles.Sudoku
Value
Data.SBV.Examples.BitPrecise.Legato
verbose
Data.SBV
verboseSMTCfg
Data.SBV
verboseTimingSMTCfg
Data.SBV
whenS
Data.SBV.Examples.Puzzles.U2Bridge
whereIs
Data.SBV.Examples.Puzzles.U2Bridge
Word
Data.SBV
Word16
Data.SBV
Word32
Data.SBV
Word64
Data.SBV
Word8
Data.SBV
writeArray
Data.SBV
xferFlash
Data.SBV.Examples.Puzzles.U2Bridge
xferPerson
Data.SBV.Examples.Puzzles.U2Bridge
xor
Data.SBV
yices
Data.SBV
|||
Data.SBV
~&
Data.SBV
~:
Data.SBV.Internals
~|
Data.SBV