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

Index

!! |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
!<<. | Data.SBV.Trans, Data.SBV
!>>. | Data.SBV.Trans, Data.SBV
# |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
% | Data.SBV.Trans, Data.SBV
*! | Data.SBV.Tools.Overflow
+! | Data.SBV.Tools.Overflow
++ |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
-! | Data.SBV.Tools.Overflow
.% | Data.SBV.Rational
.&& | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.&. | Data.SBV.Trans, Data.SBV
./= | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
./== | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.: |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
.< | Data.SBV.Trans, Data.SBV
.<+> | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.<<. | Data.SBV.Trans, Data.SBV
.<= | Data.SBV.Trans, Data.SBV
.<=> | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.== | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.=== | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.=> | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.> | Data.SBV.Trans, Data.SBV
.>= | Data.SBV.Trans, Data.SBV
.>>. | Data.SBV.Trans, Data.SBV
.^ | Data.SBV.Trans, Data.SBV
.^. | Data.SBV.Trans, Data.SBV
.|. | Data.SBV.Trans, Data.SBV
.|| | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.~& | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
.~| | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
/! | Data.SBV.Tools.Overflow
=== | Data.SBV.Trans, Data.SBV
A |
1 (Data Constructor) | Documentation.SBV.Examples.Misc.Enumerate
2 (Data Constructor) | Documentation.SBV.Examples.Misc.FirstOrderLogic
3 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Append
ABC | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
abc | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Abort | Data.SBV.Tools.WeakestPreconditions
AbortReachable | Data.SBV.Tools.WeakestPreconditions
Abs | Data.SBV.Internals
ack | Documentation.SBV.Examples.Misc.Definitions
ack1y | Documentation.SBV.Examples.Misc.Definitions
Actions | Documentation.SBV.Examples.Puzzles.U2Bridge
Adam | Documentation.SBV.Examples.Puzzles.U2Bridge
adc | Documentation.SBV.Examples.BitPrecise.Legato
add | Documentation.SBV.Examples.Puzzles.AOC_2021_24
add1 | Documentation.SBV.Examples.Misc.Definitions
add1Example | Documentation.SBV.Examples.Misc.Definitions
AddExtCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
addPoly | Data.SBV.Tools.Polynomial
addRoundKey | Documentation.SBV.Examples.Crypto.AES
addSub | Documentation.SBV.Examples.CodeGeneration.AddSub
addSValOptGoal | Data.SBV.Internals
aes128CT | Documentation.SBV.Examples.Crypto.AES
aes128InvKey | Documentation.SBV.Examples.Crypto.AES
aes128IsCorrect | Documentation.SBV.Examples.Crypto.AES
aes128Key | Documentation.SBV.Examples.Crypto.AES
aes192CT | Documentation.SBV.Examples.Crypto.AES
aes192InvKey | Documentation.SBV.Examples.Crypto.AES
aes192InvKeyExtended | Documentation.SBV.Examples.Crypto.AES
aes192Key | Documentation.SBV.Examples.Crypto.AES
aes256CT | Documentation.SBV.Examples.Crypto.AES
aes256InvKey | Documentation.SBV.Examples.Crypto.AES
aes256Key | Documentation.SBV.Examples.Crypto.AES
aesDecrypt | Documentation.SBV.Examples.Crypto.AES
aesDecryptUnwoundKey | Documentation.SBV.Examples.Crypto.AES
aesEncrypt | Documentation.SBV.Examples.Crypto.AES
aesInvKeySchedule | Documentation.SBV.Examples.Crypto.AES
aesInvRound | Documentation.SBV.Examples.Crypto.AES
aesKeySchedule | Documentation.SBV.Examples.Crypto.AES
aesLibComponents | Documentation.SBV.Examples.Crypto.AES
aesRound | Documentation.SBV.Examples.Crypto.AES
age |
1 (Function) | Documentation.SBV.Examples.Puzzles.Murder
2 (Function) | Documentation.SBV.Examples.Puzzles.Orangutans
AlgInterval | Data.SBV.Internals, Data.SBV
algorithm |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Append
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
8 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
AlgPolyRoot | Data.SBV.Internals, Data.SBV
AlgRational | Data.SBV.Internals, Data.SBV
AlgReal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
AlgRealPoly |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
algRealToRational | Data.SBV
ALL | Data.SBV.Internals, Data.SBV.Dynamic
All | Data.SBV.RegExp, Data.SBV.Internals
all | Data.SBV.List
AllChar | Data.SBV.RegExp, Data.SBV.Internals
allEqual | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
allModels | Documentation.SBV.Examples.Misc.Auxiliary
Alloc |
1 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
alloc | Documentation.SBV.Examples.Transformers.SymbolicEval
allocate | Documentation.SBV.Examples.Optimization.VM
allocEnv | Documentation.SBV.Examples.Transformers.SymbolicEval
allPossibleTrees | Documentation.SBV.Examples.Queries.FourFours
allPuzzles | Documentation.SBV.Examples.Puzzles.Sudoku
allSat |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
allSatMaxModelCount | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatMaxModelCountReached | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatPrintAlong | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
AllSatResult |
1 (Type/Class) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatResults | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatSolverReturnedDSat | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatSolverReturnedUnknown | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatTrackUFs | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
allSatWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
3 (Function) | Data.SBV.Dynamic
AllStatistics | Data.SBV.Trans.Control, Data.SBV.Control
almostWeekend | Documentation.SBV.Examples.Optimization.Enumerate
Alone | Documentation.SBV.Examples.Puzzles.Murder
ALU | Documentation.SBV.Examples.Puzzles.AOC_2021_24
Ambalat | Documentation.SBV.Examples.Puzzles.Orangutans
And |
1 (Type/Class) | Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Trans, Data.SBV
3 (Data Constructor) | Data.SBV.Internals
4 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
and |
1 (Function) | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
2 (Function) | Documentation.SBV.Examples.Uninterpreted.Deduce
any | Data.SBV.List
anyChar | Data.SBV.RegExp
AppC |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Append
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Append
approxRational | Data.SBV.Trans, Data.SBV
AppS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Append
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Append
ArithOverflow | Data.SBV.Tools.Overflow
ArrayContext | Data.SBV.Internals
ArrayFree | Data.SBV.Internals
ArrayInfo | Data.SBV.Internals
ArrayMerge | Data.SBV.Internals
ArrayMutate | Data.SBV.Internals
ArrEq | Data.SBV.Internals
ArrRead | Data.SBV.Internals
asciiLetter | Data.SBV.RegExp
asciiLower | Data.SBV.RegExp
asciiUpper | Data.SBV.RegExp
assert | Data.SBV.Tools.WeakestPreconditions
AssertionStackLevels | Data.SBV.Trans.Control, Data.SBV.Control
AssertWithPenalty | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
assertWithPenalty |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
Assign | Data.SBV.Tools.WeakestPreconditions
Assignment | Documentation.SBV.Examples.Puzzles.Orangutans
assocPlus | Documentation.SBV.Examples.Misc.Floating
assocPlusRegular | Documentation.SBV.Examples.Misc.Floating
AUFLIA | Data.SBV.Trans, Data.SBV
AUFLIRA | Data.SBV.Trans, Data.SBV
AUFNIRA | Data.SBV.Trans, Data.SBV
Aug | Documentation.SBV.Examples.Puzzles.Birthday
Authors | Data.SBV.Trans.Control, Data.SBV.Control
axiomatizeFib | Documentation.SBV.Examples.WeakestPreconditions.Fib
axiomatizeGCD | Documentation.SBV.Examples.WeakestPreconditions.GCD
B |
1 (Data Constructor) | Documentation.SBV.Examples.Misc.Enumerate
2 (Data Constructor) | Documentation.SBV.Examples.Misc.FirstOrderLogic
3 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
4 (Type/Class) | Documentation.SBV.Examples.Uninterpreted.Deduce
BadPostcondition | Data.SBV.Tools.WeakestPreconditions
BadPrecondition | Data.SBV.Tools.WeakestPreconditions
ball | Data.SBV.Tools.BoundedList
band | Data.SBV.Tools.BoundedList
bany | Data.SBV.Tools.BoundedList
Bar | Documentation.SBV.Examples.Puzzles.Murder
Basahan | Documentation.SBV.Examples.Puzzles.Orangutans
Baseball | Documentation.SBV.Examples.Puzzles.Fish
basis | Documentation.SBV.Examples.Existentials.Diophantine
bcc | Documentation.SBV.Examples.BitPrecise.Legato
BD | Documentation.SBV.Examples.Puzzles.Birthday
Beach | Documentation.SBV.Examples.Puzzles.Murder
Beer | Documentation.SBV.Examples.Puzzles.Fish
belem | Data.SBV.Tools.BoundedList
Beverage | Documentation.SBV.Examples.Puzzles.Fish
bfilter | Data.SBV.Tools.BoundedList
bfix | Data.SBV.Tools.BoundedFix
bfoldl | Data.SBV.Tools.BoundedList
bfoldlM | Data.SBV.Tools.BoundedList
bfoldr | Data.SBV.Tools.BoundedList
bfoldrM | Data.SBV.Tools.BoundedList
bill | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
bimap | Data.SBV.Either
bin | Data.SBV.Internals
Binary | Documentation.SBV.Examples.Uninterpreted.Shannon
BinOp | Documentation.SBV.Examples.Queries.FourFours
binP | Data.SBV.Internals
binS | Data.SBV.Internals
Bird | Documentation.SBV.Examples.Puzzles.Fish
Birthday | Documentation.SBV.Examples.Puzzles.Birthday
Bit | Documentation.SBV.Examples.BitPrecise.Legato
bit | Data.SBV.Trans, Data.SBV
bitDefault | Data.SBV.Trans, Data.SBV
bitReverse16 | Data.SBV.Trans, Data.SBV
bitReverse32 | Data.SBV.Trans, Data.SBV
bitReverse64 | Data.SBV.Trans, Data.SBV
bitReverse8 | Data.SBV.Trans, Data.SBV
Bits | Data.SBV.Trans, Data.SBV
bitSize | Data.SBV.Trans, Data.SBV
bitSizeMaybe | Data.SBV.Trans, Data.SBV
Bitwuzla | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
bitwuzla | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Black | Documentation.SBV.Examples.Puzzles.HexPuzzle
black | Documentation.SBV.Examples.Puzzles.Rabbits
blastBE | Data.SBV.Trans, Data.SBV
blastLE | Data.SBV.Trans, Data.SBV
blastSDouble | Data.SBV.Trans, Data.SBV
blastSFloat | Data.SBV.Trans, Data.SBV
blastSFloatingPoint | Data.SBV.Trans, Data.SBV
Block |
1 (Type/Class) | Documentation.SBV.Examples.Crypto.Prince
2 (Type/Class) | Documentation.SBV.Examples.Crypto.SHA
3 (Data Constructor) | Documentation.SBV.Examples.Crypto.SHA
blockSize | Documentation.SBV.Examples.Crypto.SHA
Blue |
1 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Fish
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Garden
3 (Data Constructor) | Documentation.SBV.Examples.Puzzles.HexPuzzle
bmap | Data.SBV.Tools.BoundedList
bmapM | Data.SBV.Tools.BoundedList
bmaximum | Data.SBV.Tools.BoundedList
bmc | Data.SBV.Tools.BMC
bmcWith | Data.SBV.Tools.BMC
bminimum | Data.SBV.Tools.BoundedList
bne | Documentation.SBV.Examples.BitPrecise.Legato
Board |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.MagicSquare
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Sudoku
Bono | Documentation.SBV.Examples.Puzzles.U2Bridge
Boolector | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
boolector | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
bor | Data.SBV.Tools.BoundedList
Boundary | Data.SBV.Tools.Range
BoundedCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
bprod | Data.SBV.Tools.BoundedList
breverse | Data.SBV.Tools.BoundedList
Briton | Documentation.SBV.Examples.Puzzles.Fish
bsort | Data.SBV.Tools.BoundedList
bsum | Data.SBV.Tools.BoundedList
bumpTime1 | Documentation.SBV.Examples.Puzzles.U2Bridge
bumpTime2 | Documentation.SBV.Examples.Puzzles.U2Bridge
Button | Documentation.SBV.Examples.Puzzles.HexPuzzle
bvAddO | Data.SBV.Tools.Overflow
bvDivO | Data.SBV.Tools.Overflow
bvDrop |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
bvExtract |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
BVIsNonZero | Data.SBV.Trans, Data.SBV
bvMulO | Data.SBV.Tools.Overflow
bvMulOFast | Data.SBV.Tools.Overflow
bvNegO | Data.SBV.Tools.Overflow
bvSubO | Data.SBV.Tools.Overflow
bvTake |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
Bystander | Documentation.SBV.Examples.Puzzles.Murder
ByteConverter | Data.SBV
byteSwap16 | Data.SBV.Trans, Data.SBV
byteSwap32 | Data.SBV.Trans, Data.SBV
byteSwap64 | Data.SBV.Trans, Data.SBV
bzipWith | Data.SBV.Tools.BoundedList
C |
1 (Data Constructor) | Data.SBV.Tools.GenTest
2 (Data Constructor) | Documentation.SBV.Examples.Misc.Enumerate
3 (Data Constructor) | Documentation.SBV.Examples.Misc.FirstOrderLogic
c1 | Documentation.SBV.Examples.Puzzles.Coins
c2 | Documentation.SBV.Examples.Puzzles.Coins
c3 | Documentation.SBV.Examples.Puzzles.Coins
c4 | Documentation.SBV.Examples.Puzzles.Coins
c5 | Documentation.SBV.Examples.Puzzles.Coins
c6 | Documentation.SBV.Examples.Puzzles.Coins
cache | Data.SBV.Internals
Cached | Data.SBV.Internals
CAlgReal | Data.SBV.Internals, Data.SBV.Dynamic
capabilities | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
capacity | Documentation.SBV.Examples.Puzzles.Jugs
caseSplit |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Cat | Documentation.SBV.Examples.Puzzles.Fish
CChar | Data.SBV.Internals, Data.SBV.Dynamic
CDouble | Data.SBV.Internals, Data.SBV.Dynamic
ceilingHighEnoughForHuman | Documentation.SBV.Examples.Misc.Newtypes
CEither | Data.SBV.Internals, Data.SBV.Dynamic
CFloat | Data.SBV.Internals, Data.SBV.Dynamic
CFP | Data.SBV.Internals, Data.SBV.Dynamic
cg1 | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
cg2 | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
cgAddDecl | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAddLDFlags | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAddPrototype | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgAES128BlockEncrypt | Documentation.SBV.Examples.Crypto.AES
cgAES128Library | Documentation.SBV.Examples.Crypto.AES
cgAESLibrary | Documentation.SBV.Examples.Crypto.AES
CgArray | Data.SBV.Internals
CgAtomic | Data.SBV.Internals
CgConfig |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
cgDecls | Data.SBV.Internals
CgDouble | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgDriver | Data.SBV.Internals
cgDriverVals | Data.SBV.Internals
cgFinalConfig | Data.SBV.Internals
CgFloat | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenDriver | Data.SBV.Internals
cgGenerateDriver | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenerateMakefile | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgGenMakefile | Data.SBV.Internals
CgHeader | Data.SBV.Internals
cgIgnoreAsserts | Data.SBV.Internals
cgIgnoreSAssert | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgInput | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgInputArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgInputs | Data.SBV.Internals
cgInteger | Data.SBV.Internals
cgIntegerSize | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgLDFlags | Data.SBV.Internals
CgLongDouble | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgMakefile | Data.SBV.Internals
cgOutput | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgOutputArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgOutputs | Data.SBV.Internals
cgOverwriteFiles | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgOverwriteGenerated | Data.SBV.Internals
cgPerformRTCs | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgPgmBundle |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
CgPgmKind | Data.SBV.Internals
cgPrototypes | Data.SBV.Internals
cgReal | Data.SBV.Internals
cgReturn | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgReturnArr | Data.SBV.Tools.CodeGen, Data.SBV.Internals
cgReturns | Data.SBV.Internals
cgRTC | Data.SBV.Internals
cgSetDriverValues | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgSHA256 | Documentation.SBV.Examples.Crypto.SHA
cgSHA512 | Documentation.SBV.Examples.Crypto.SHA
cgShowU8InHex | Data.SBV.Internals
cgShowU8UsingHex | Data.SBV.Tools.CodeGen, Data.SBV.Internals
CgSource | Data.SBV.Internals
CgSRealType | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
cgSRealType | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
CgState |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
cgSym | Data.SBV.Tools.CodeGen, Data.SBV.Internals
CgTarget | Data.SBV.Internals
cgUninterpret | Data.SBV.Trans, Data.SBV
CgVal | Data.SBV.Internals
ch | Documentation.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
checkArithOverflow | Documentation.SBV.Examples.BitPrecise.BrokenSearch
checkCorrectMidValue | Documentation.SBV.Examples.BitPrecise.BrokenSearch
CheckedArithmetic | Data.SBV.Tools.Overflow
checkedDiv | Documentation.SBV.Examples.Misc.NoDiv0
checkMutex | Documentation.SBV.Examples.Lists.BoundedMutex
checkOverflow | Documentation.SBV.Examples.BitPrecise.Legato
checkOverflowCorrect | Documentation.SBV.Examples.BitPrecise.Legato
CheckResult | Documentation.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
CheckSatResult | Data.SBV.Trans.Control, Data.SBV.Control
checkSatUsing |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
cheryl | Documentation.SBV.Examples.Puzzles.Birthday
chex | Data.SBV.Internals
chop4 | Documentation.SBV.Examples.Crypto.AES
chr | Data.SBV.Char
chunk | Documentation.SBV.Examples.Puzzles.MagicSquare
chunkBy | Documentation.SBV.Examples.Crypto.SHA
CInteger | Data.SBV.Internals, Data.SBV.Dynamic
classify | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
clc | Documentation.SBV.Examples.BitPrecise.Legato
clearBit | Data.SBV.Trans, Data.SBV
CList | Data.SBV.Internals, Data.SBV.Dynamic
Closed | Data.SBV.Tools.Range
ClosedPoint | Data.SBV
CMaybe | Data.SBV.Internals, Data.SBV.Dynamic
coat | Documentation.SBV.Examples.Lists.CountOutAndTransfer
coatCheck | Documentation.SBV.Examples.Lists.CountOutAndTransfer
CodeGen | Data.SBV.Internals
codeGen |
1 (Function) | Data.SBV.Internals
2 (Function) | Documentation.SBV.Examples.BitPrecise.MergeSort
3 (Function) | Documentation.SBV.Examples.Crypto.Prince
Coffee | Documentation.SBV.Examples.Puzzles.Fish
Coin | Documentation.SBV.Examples.Puzzles.Coins
col | Documentation.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
combinations | Documentation.SBV.Examples.Puzzles.Coins
commonPT | Documentation.SBV.Examples.Crypto.AES
Comp | Data.SBV.RegExp, Data.SBV.Internals
compileToC | Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
compileToC' | Data.SBV.Internals
compileToCLib | Data.SBV.Tools.CodeGen, Data.SBV.Dynamic
compileToCLib' | Data.SBV.Internals
complement |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Set
complementBit | Data.SBV.Trans, Data.SBV
ComplementSet | Data.SBV.Internals, Data.SBV
Conc | Data.SBV.RegExp, Data.SBV.Internals
Concat | Documentation.SBV.Examples.Strings.SQLInjection
concat |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
Concrete | Data.SBV.Internals
conditionalSetClearCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
Consecution | Data.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
constrain | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Constraint | Data.SBV.Internals
constraint | Data.SBV.Internals
ConstraintSet | Data.SBV.Trans, Data.SBV
constraintStr | Data.SBV.Internals
constrainWithAttribute | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
content | Documentation.SBV.Examples.Puzzles.Jugs
contextState | Data.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
correctnessTheorem | Documentation.SBV.Examples.BitPrecise.Legato
Count | Documentation.SBV.Examples.Puzzles.Counts
count |
1 (Function) | Documentation.SBV.Examples.Puzzles.Counts
2 (Function) | Documentation.SBV.Examples.Puzzles.Garden
Counterexample | Documentation.SBV.Examples.Transformers.SymbolicEval
countLeadingZeros | Data.SBV.Trans, Data.SBV
counts | Documentation.SBV.Examples.Puzzles.Counts
countTrailingZeros | Data.SBV.Trans, Data.SBV
crack | Data.SBV
crackNum | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
CRational | Data.SBV.Internals, Data.SBV.Dynamic
crc | Data.SBV.Tools.Polynomial
crcBV | Data.SBV.Tools.Polynomial
crcGood |
1 (Function) | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
2 (Function) | Documentation.SBV.Examples.Existentials.CRCPolynomial
crcUSB | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
crcUSB' | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
crc_48_16 | Documentation.SBV.Examples.Existentials.CRCPolynomial
create | Data.SBV.Control
Critical | Documentation.SBV.Examples.Lists.BoundedMutex
crossTime | Documentation.SBV.Examples.Puzzles.U2Bridge
csDemo1 | Documentation.SBV.Examples.Queries.CaseSplit
csDemo2 | Documentation.SBV.Examples.Queries.CaseSplit
CSet | Data.SBV.Internals, Data.SBV.Dynamic
CString | Data.SBV.Internals, Data.SBV.Dynamic
CT | Documentation.SBV.Examples.Crypto.Prince
CTuple | Data.SBV.Internals, Data.SBV.Dynamic
CUserSort | Data.SBV.Internals, Data.SBV.Dynamic
CustomLogic | Data.SBV.Trans, Data.SBV
CV |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Dynamic
CVal | Data.SBV.Internals, Data.SBV.Dynamic
CVC4 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
cvc4 | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
CVC5 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
cvc5 | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
cvSameType | Data.SBV.Internals
cvtModel | Data.SBV.Trans, Data.SBV
cvToBool | Data.SBV.Internals, Data.SBV.Dynamic
cvToSMTLib | Data.SBV.Internals
cvVal | Data.SBV.Internals, Data.SBV.Dynamic
D | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
d | Documentation.SBV.Examples.Puzzles.Drinker
D14 | Documentation.SBV.Examples.Puzzles.Birthday
D15 | Documentation.SBV.Examples.Puzzles.Birthday
D16 | Documentation.SBV.Examples.Puzzles.Birthday
D17 | Documentation.SBV.Examples.Puzzles.Birthday
D18 | Documentation.SBV.Examples.Puzzles.Birthday
D19 | Documentation.SBV.Examples.Puzzles.Birthday
Dane | Documentation.SBV.Examples.Puzzles.Fish
Data | Documentation.SBV.Examples.Puzzles.AOC_2021_24
Day |
1 (Type/Class) | Documentation.SBV.Examples.Optimization.Enumerate
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Birthday
3 (Type/Class) | Documentation.SBV.Examples.Queries.Enums
decimal | Data.SBV.RegExp
Deck | Documentation.SBV.Examples.Lists.CountOutAndTransfer
decrypt |
1 (Function) | Documentation.SBV.Examples.Crypto.Prince
2 (Function) | Documentation.SBV.Examples.Crypto.RC4
defaultCgConfig | Data.SBV.Internals
defaultDeltaSMTCfg | Data.SBV
DefaultPenalty | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
defaultSMTCfg | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
defaultSolverConfig | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
defaultWPCfg | Data.SBV.Tools.WeakestPreconditions
delete | Data.SBV.Set
DeltaSat | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
demo |
1 (Function) | Documentation.SBV.Examples.Queries.AllSat
2 (Function) | Documentation.SBV.Examples.Queries.Concurrency
demoDependent | Documentation.SBV.Examples.Queries.Concurrency
denominator | Data.SBV.Trans, Data.SBV
derivative | Documentation.SBV.Examples.Uninterpreted.Shannon
dex | Documentation.SBV.Examples.BitPrecise.Legato
diag | Documentation.SBV.Examples.Puzzles.MagicSquare
DiagnosticOutputChannel | Data.SBV.Trans.Control, Data.SBV.Control
Dict | Documentation.SBV.Examples.Misc.Tuple
Diff | Data.SBV.RegExp, Data.SBV.Internals
diffCount | Documentation.SBV.Examples.Existentials.CRCPolynomial
difference | Data.SBV.Set
digit | Data.SBV.RegExp
digitToInt | Data.SBV.Char
disjoint | Data.SBV.Set
displayModels | Data.SBV.Trans, Data.SBV
distinct | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
distinctExcept | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
div | Documentation.SBV.Examples.Puzzles.AOC_2021_24
Divide | Documentation.SBV.Examples.Queries.FourFours
DivS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
Dog | Documentation.SBV.Examples.Puzzles.Fish
Dolly | Documentation.SBV.Examples.Puzzles.Orangutans
doRounds | Documentation.SBV.Examples.Crypto.AES
doubleToWord | Data.SBV.Internals
dprove |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
dproveWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
DReal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
dReal | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
drinker | Documentation.SBV.Examples.Puzzles.Drinker
drop |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
dropRe | Documentation.SBV.Examples.Strings.SQLInjection
DSat | Data.SBV.Trans.Control, Data.SBV.Control
dsat |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
dsatPrecision | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
dsatWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
E |
1 (Type/Class) | Documentation.SBV.Examples.BitPrecise.MergeSort
2 (Type/Class) | Documentation.SBV.Examples.Misc.Enumerate
3 (Type/Class) | Documentation.SBV.Examples.Misc.FirstOrderLogic
echo |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Edge | Documentation.SBV.Examples.Puzzles.U2Bridge
either | Data.SBV.Either
EitherAccess | Data.SBV.Internals
EitherConstructor | Data.SBV.Internals
EitherIs | Data.SBV.Internals
Elem | Documentation.SBV.Examples.Puzzles.MagicSquare
elem |
1 (Function) | Data.SBV.List
2 (Function) | Data.SBV.Char
elemAt | Data.SBV.List
elts | Documentation.SBV.Examples.Misc.Enumerate
embed | Data.SBV.Control
empty | Data.SBV.Set
encrypt |
1 (Function) | Documentation.SBV.Examples.Crypto.Prince
2 (Function) | Documentation.SBV.Examples.Crypto.RC4
end | Documentation.SBV.Examples.BitPrecise.Legato
engine | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
ensureSat |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Env |
1 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
env | Documentation.SBV.Examples.Puzzles.AOC_2021_24
envX | Documentation.SBV.Examples.Transformers.SymbolicEval
envY | Documentation.SBV.Examples.Transformers.SymbolicEval
Epsilon | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
eql | Documentation.SBV.Examples.Puzzles.AOC_2021_24
eqSArr | Data.SBV.Dynamic
EqSymbolic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Equal | Data.SBV.Internals
Equality | Data.SBV.Trans, Data.SBV
Equals | Documentation.SBV.Examples.Transformers.SymbolicEval
ErrorBehavior | Data.SBV.Trans.Control, Data.SBV.Control
ErrorContinuedExecution | Data.SBV.Trans.Control, Data.SBV.Control
ErrorImmediateExit | Data.SBV.Trans.Control, Data.SBV.Control
euler185 | Documentation.SBV.Examples.Puzzles.Euler185
Eva | Documentation.SBV.Examples.Puzzles.Orangutans
Eval |
1 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
eval |
1 (Function) | Documentation.SBV.Examples.Queries.FourFours
2 (Function) | Documentation.SBV.Examples.Strings.SQLInjection
3 (Function) | Documentation.SBV.Examples.Transformers.SymbolicEval
evenOdd |
1 (Function) | Documentation.SBV.Examples.Misc.Definitions
2 (Function) | Documentation.SBV.Examples.Queries.Interpolants
evenOdd2 | Documentation.SBV.Examples.Misc.Definitions
everything | Data.SBV.RegExp
EX | Data.SBV.Internals, Data.SBV.Dynamic
ex1 |
1 (Function) | Documentation.SBV.Examples.ProofTools.BMC
2 (Function) | Documentation.SBV.Examples.ProofTools.Strengthen
3 (Function) | Documentation.SBV.Examples.Transformers.SymbolicEval
ex2 |
1 (Function) | Documentation.SBV.Examples.ProofTools.BMC
2 (Function) | Documentation.SBV.Examples.ProofTools.Strengthen
3 (Function) | Documentation.SBV.Examples.Transformers.SymbolicEval
ex3 |
1 (Function) | Documentation.SBV.Examples.ProofTools.Strengthen
2 (Function) | Documentation.SBV.Examples.Transformers.SymbolicEval
ex4 | Documentation.SBV.Examples.ProofTools.Strengthen
ex5 | Documentation.SBV.Examples.ProofTools.Strengthen
ex6 | Documentation.SBV.Examples.ProofTools.Strengthen
exactly | Data.SBV.RegExp
example |
1 (Function) | Documentation.SBV.Examples.Misc.SoftConstrain
2 (Function) | Documentation.SBV.Examples.Misc.Tuple
3 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle
4 (Function) | Documentation.SBV.Examples.Queries.Abducts
exampleMathSAT | Documentation.SBV.Examples.Queries.Interpolants
exampleProgram | Documentation.SBV.Examples.Strings.SQLInjection
executable | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
existential | Documentation.SBV.Examples.Uninterpreted.Shannon
Exists |
1 (Type/Class) | Data.SBV
2 (Data Constructor) | Data.SBV
ExistsN |
1 (Type/Class) | Data.SBV
2 (Data Constructor) | Data.SBV
existsOK | Documentation.SBV.Examples.Uninterpreted.Shannon
ExistsUnique |
1 (Type/Class) | Data.SBV
2 (Data Constructor) | Data.SBV
exit |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
expandKey | Documentation.SBV.Examples.Crypto.Prince
exploitRe | Documentation.SBV.Examples.Strings.SQLInjection
Expt | Documentation.SBV.Examples.Queries.FourFours
ExtCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
ExtendedCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
extendPathCondition | Data.SBV.Internals
extraArgs | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Extract |
1 (Data Constructor) | Data.SBV.Internals
2 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato
extractFinalKey | Documentation.SBV.Examples.Crypto.AES
extractFinalKeyExtended | Documentation.SBV.Examples.Crypto.AES
ExtractIO | Data.SBV.Trans.Control, Data.SBV.Control
extractIO | Data.SBV.Trans.Control, Data.SBV.Control
extractModel | Data.SBV.Trans, Data.SBV
extractModels | Data.SBV.Trans, Data.SBV
extractSymbolicSimulationState | Data.SBV.Internals
F |
1 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
2 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Fib
f |
1 (Function) | Documentation.SBV.Examples.Uninterpreted.AUF
2 (Function) | Documentation.SBV.Examples.Uninterpreted.Function
3 (Function) | Documentation.SBV.Examples.Uninterpreted.Sort
F1 | Documentation.SBV.Examples.BitPrecise.Legato
F2 | Documentation.SBV.Examples.BitPrecise.Legato
Factorial | Documentation.SBV.Examples.Queries.FourFours
Failed |
1 (Data Constructor) | Data.SBV.Tools.WeakestPreconditions
2 (Data Constructor) | Data.SBV.Tools.Induction
falseCV | Data.SBV.Internals
falseSV | Data.SBV.Internals
Falsity | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
fastMaxCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
fastMinCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
fastPopCountIsCorrect | Documentation.SBV.Examples.CodeGeneration.PopulationCount
Female | Documentation.SBV.Examples.Puzzles.Murder
fib | Documentation.SBV.Examples.WeakestPreconditions.Fib
fib0 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
fib1 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
fib2 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
fibCorrect | Documentation.SBV.Examples.ProofTools.Fibonacci
FibS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Fib
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Fib
fill | Documentation.SBV.Examples.Queries.FourFours
fillBoard | Documentation.SBV.Examples.Puzzles.Sudoku
filter | Data.SBV.List
find | Documentation.SBV.Examples.Queries.FourFours
findDays | Documentation.SBV.Examples.Queries.Enums
findHD4Polynomials | Documentation.SBV.Examples.Existentials.CRCPolynomial
findInjection | Documentation.SBV.Examples.Strings.SQLInjection
FiniteBits | Data.SBV.Trans, Data.SBV
finiteBitSize | Data.SBV.Trans, Data.SBV
first | Data.SBV.Either
firstQuery | Documentation.SBV.Examples.Queries.Concurrency
firstWeekend | Documentation.SBV.Examples.Optimization.Enumerate
Fish | Documentation.SBV.Examples.Puzzles.Fish
fishOwner | Documentation.SBV.Examples.Puzzles.Fish
Flag | Documentation.SBV.Examples.BitPrecise.Legato
FlagC | Documentation.SBV.Examples.BitPrecise.Legato
Flags | Documentation.SBV.Examples.BitPrecise.Legato
flags | Documentation.SBV.Examples.BitPrecise.Legato
FlagZ | Documentation.SBV.Examples.BitPrecise.Legato
flash | Documentation.SBV.Examples.Puzzles.U2Bridge
flIsCorrect | Documentation.SBV.Examples.BitPrecise.PrefixSum
floating | Data.SBV.RegExp
FloatingPoint | Data.SBV
floatToWord | Data.SBV.Internals
Flower | Documentation.SBV.Examples.Puzzles.Garden
flowerCount | Documentation.SBV.Examples.Puzzles.Garden
flyspeck | Documentation.SBV.Examples.DeltaSat.DeltaSat
foldl | Data.SBV.List
foldli | Data.SBV.List
foldr | Data.SBV.List
foldri | Data.SBV.List
Football | Documentation.SBV.Examples.Puzzles.Fish
Forall |
1 (Type/Class) | Data.SBV
2 (Data Constructor) | Data.SBV
ForallN |
1 (Type/Class) | Data.SBV
2 (Data Constructor) | Data.SBV
forceSVArg | Data.SBV.Internals
Forte | Data.SBV.Tools.GenTest
four | Documentation.SBV.Examples.Misc.Enumerate
fourCoat | Documentation.SBV.Examples.Lists.CountOutAndTransfer
FP |
1 (Type/Class) | Data.SBV.Float
2 (Data Constructor) | Data.SBV.Float
fp2fp | Data.SBV.Internals
fp54Bounds | Documentation.SBV.Examples.Misc.Floating
fpAbs | Data.SBV.Trans, Data.SBV
fpAdd | Data.SBV.Trans, Data.SBV
FPBFloat | Data.SBV
fpCompareObjectH | Data.SBV.Internals
fpDiv | Data.SBV.Trans, Data.SBV
FPDouble | Data.SBV
fpEncodeFloat | Data.SBV.Float
fpExponentSize | Data.SBV.Float
fpFMA | Data.SBV.Trans, Data.SBV
fpFromBigFloat | Data.SBV.Float
fpFromDouble | Data.SBV.Float
fpFromFloat | Data.SBV.Float
fpFromInteger | Data.SBV.Float
fpFromRational | Data.SBV.Float
fpFromRawRep | Data.SBV.Float
FPHalf | Data.SBV
fpInf | Data.SBV.Float
fpIsEqualObject | Data.SBV.Trans, Data.SBV
fpIsEqualObjectH | Data.SBV.Internals
fpIsInfinite | Data.SBV.Trans, Data.SBV
fpIsNaN | Data.SBV.Trans, Data.SBV
fpIsNegative | Data.SBV.Trans, Data.SBV
fpIsNegativeZero | Data.SBV.Trans, Data.SBV
fpIsNormal | Data.SBV.Trans, Data.SBV
fpIsNormalizedH | Data.SBV.Internals
fpIsPoint | Data.SBV.Trans, Data.SBV
fpIsPositive | Data.SBV.Trans, Data.SBV
fpIsPositiveZero | Data.SBV.Trans, Data.SBV
fpIsSubnormal | Data.SBV.Trans, Data.SBV
fpIsZero | Data.SBV.Trans, Data.SBV
fpMax | Data.SBV.Trans, Data.SBV
fpMaxH | Data.SBV.Internals
fpMin | Data.SBV.Trans, Data.SBV
fpMinH | Data.SBV.Internals
fpMul | Data.SBV.Trans, Data.SBV
fpNaN | Data.SBV.Float
fpNeg | Data.SBV.Trans, Data.SBV
FPOp | Data.SBV.Internals
FPQuad | Data.SBV
fpRem | Data.SBV.Trans, Data.SBV
fpRemH | Data.SBV.Internals
fpRoundToIntegral | Data.SBV.Trans, Data.SBV
fpRoundToIntegralH | Data.SBV.Internals
fpSignificandSize | Data.SBV.Float
FPSingle | Data.SBV
fpSqrt | Data.SBV.Trans, Data.SBV
fpSub | Data.SBV.Trans, Data.SBV
fpValue | Data.SBV.Float
fpZero | Data.SBV.Float
FP_Abs | Data.SBV.Internals
FP_Add | Data.SBV.Internals
FP_Cast | Data.SBV.Internals
FP_Div | Data.SBV.Internals
FP_FMA | Data.SBV.Internals
FP_IsInfinite | Data.SBV.Internals
FP_IsNaN | Data.SBV.Internals
FP_IsNegative | Data.SBV.Internals
FP_IsNormal | Data.SBV.Internals
FP_IsPositive | Data.SBV.Internals
FP_IsSubnormal | Data.SBV.Internals
FP_IsZero | Data.SBV.Internals
FP_Max | Data.SBV.Internals
FP_Min | Data.SBV.Internals
FP_Mul | Data.SBV.Internals
FP_Neg | Data.SBV.Internals
FP_ObjEqual | Data.SBV.Internals
FP_Reinterpret | Data.SBV.Internals
FP_Rem | Data.SBV.Internals
FP_RoundToIntegral | Data.SBV.Internals
FP_Sqrt | Data.SBV.Internals
FP_Sub | Data.SBV.Internals
Francine | Documentation.SBV.Examples.Puzzles.Orangutans
free |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
free_ |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
Fresh | Data.SBV.Control
fresh | Data.SBV.Control
freshArray |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
freshArray_ |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
freshLambdaArray | Data.SBV.Trans.Control
freshLambdaArray_ | Data.SBV.Trans.Control
freshVar |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
freshVar_ |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Fri | Documentation.SBV.Examples.Optimization.Enumerate
Friday | Documentation.SBV.Examples.Queries.Enums
fromBitsBE | Data.SBV.Trans, Data.SBV
fromBitsLE | Data.SBV.Trans, Data.SBV
fromBool | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
fromBytes | Data.SBV
fromCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
fromJust | Data.SBV.Maybe
fromLeft | Data.SBV.Either
fromList | Data.SBV.Set
fromMaybe | Data.SBV.Maybe
fromMetricSpace | Data.SBV
fromNibbles | Documentation.SBV.Examples.Crypto.Prince
fromRight | Data.SBV.Either
fromSDouble | Data.SBV.Trans, Data.SBV
fromSFloat | Data.SBV.Trans, Data.SBV
fromSFloatingPoint | Data.SBV.Trans, Data.SBV
FromSized | Data.SBV.Trans, Data.SBV
fromSized | Data.SBV.Trans, Data.SBV
full | Data.SBV.Set
fullAdder | Data.SBV.Trans, Data.SBV
fullMultiplier | Data.SBV.Trans, Data.SBV
G | Documentation.SBV.Examples.WeakestPreconditions.GCD
gcd | Documentation.SBV.Examples.WeakestPreconditions.GCD
GCDS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.GCD
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.GCD
genAddSub | Documentation.SBV.Examples.CodeGeneration.AddSub
genCCode | Documentation.SBV.Examples.CodeGeneration.Uninterpreted
generalize | Documentation.SBV.Examples.Transformers.SymbolicEval
GeneralizedCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
generate | Documentation.SBV.Examples.Queries.FourFours
generateSMTBenchmarkProof |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Dynamic
generateSMTBenchmarkSat |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Dynamic
genFib1 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
genFib2 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
genFibs | Documentation.SBV.Examples.Lists.Fibonacci
genFromCV | Data.SBV.Internals
genGCDInC | Documentation.SBV.Examples.CodeGeneration.GCD
genLiteral | Data.SBV.Internals
genLs | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
genMkSymVar | Data.SBV.Internals
genParse | Data.SBV.Internals, Data.SBV.Dynamic
genPoly | Documentation.SBV.Examples.Existentials.CRCPolynomial
genPopCountInC | Documentation.SBV.Examples.CodeGeneration.PopulationCount
genTest | Data.SBV.Tools.GenTest
genVals | Documentation.SBV.Examples.Misc.ModelExtract
German | Documentation.SBV.Examples.Puzzles.Fish
getAbduct |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getAbductNext |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getAnd | Data.SBV.Trans, Data.SBV
getAssertions |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getAssertionStackDepth |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getAssignment |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getAvailableSolvers | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
getConst | Documentation.SBV.Examples.Puzzles.Murder
getFlag | Documentation.SBV.Examples.BitPrecise.Legato
getFunction |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getId | Data.SBV.Internals
getIff | Data.SBV.Trans, Data.SBV
getInfo |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getInterpolantMathSAT |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getInterpolantZ3 |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getIor | Data.SBV.Trans, Data.SBV
getModel |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getModelAssignment |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Dynamic
getModelDictionaries | Data.SBV.Trans, Data.SBV
getModelDictionary |
1 (Function) | Data.SBV.Trans, Data.SBV
2 (Function) | Data.SBV.Dynamic
getModelObjectives | Data.SBV.Trans, Data.SBV
getModelObjectiveValue | Data.SBV.Trans, Data.SBV
getModelUIFuns | Data.SBV.Trans, Data.SBV
getModelUIFunValue | Data.SBV.Trans, Data.SBV
getModelUninterpretedValue | Data.SBV.Trans, Data.SBV
getModelUninterpretedValues | Data.SBV.Trans, Data.SBV
getModelValue | Data.SBV.Trans, Data.SBV
getModelValues | Data.SBV.Trans, Data.SBV
getObservables |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getOption |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getPathCondition | Data.SBV.Internals
getPerson | Documentation.SBV.Examples.Puzzles.Murder
getProof |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getReg | Documentation.SBV.Examples.BitPrecise.Legato
getSMTResult |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getTableIndex | Data.SBV.Internals
getTestValues | Data.SBV.Tools.GenTest
getUninterpretedValue |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getUnknownReason |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getUnsatCore |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getValue |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
getXor | Data.SBV.Trans, Data.SBV
GF28 |
1 (Type/Class) | Documentation.SBV.Examples.Crypto.AES
2 (Type/Class) | Documentation.SBV.Examples.Misc.Polynomials
gf28Inverse | Documentation.SBV.Examples.Crypto.AES
gf28Mult | Documentation.SBV.Examples.Crypto.AES
gf28Pow | Documentation.SBV.Examples.Crypto.AES
gfMult | Documentation.SBV.Examples.Misc.Polynomials
Good | Data.SBV.Tools.WeakestPreconditions
goodSum | Documentation.SBV.Examples.Queries.AllSat
Gracie | Documentation.SBV.Examples.Puzzles.Orangutans
GreaterEq | Data.SBV.Internals
GreaterThan |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
greedy | Documentation.SBV.Examples.Puzzles.Rabbits
Green |
1 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Fish
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.HexPuzzle
Grid | Documentation.SBV.Examples.Puzzles.HexPuzzle
guess | Documentation.SBV.Examples.Queries.GuessNumber
guesses | Documentation.SBV.Examples.Puzzles.Euler185
h0 | Documentation.SBV.Examples.Crypto.SHA
Handler | Documentation.SBV.Examples.Puzzles.Orangutans
handler | Documentation.SBV.Examples.Puzzles.Orangutans
hashBlock | Documentation.SBV.Examples.Crypto.SHA
Haskell | Data.SBV.Tools.GenTest
HasKind | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
hasSign | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
hasSize | Data.SBV.Set
head |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
Here | Documentation.SBV.Examples.Puzzles.U2Bridge
hex | Data.SBV.Internals
hex2 | Documentation.SBV.Examples.Crypto.RC4
hex8 | Documentation.SBV.Examples.Crypto.AES
hexadecimal | Data.SBV.RegExp
hexDigit | Data.SBV.RegExp
hexP | Data.SBV.Internals
hexS | Data.SBV.Internals
Hockey | Documentation.SBV.Examples.Puzzles.Fish
holds | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
Homogeneous | Documentation.SBV.Examples.Existentials.Diophantine
Horse | Documentation.SBV.Examples.Puzzles.Fish
HumanHeightInCm |
1 (Type/Class) | Documentation.SBV.Examples.Misc.Newtypes
2 (Data Constructor) | Documentation.SBV.Examples.Misc.Newtypes
I | Documentation.SBV.Examples.WeakestPreconditions.Basics
i |
1 (Function) | Documentation.SBV.Examples.ProofTools.Fibonacci
2 (Function) | Documentation.SBV.Examples.ProofTools.Sum
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
identifier | Data.SBV.RegExp
Identity | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
Idle | Documentation.SBV.Examples.Lists.BoundedMutex
IEEEFloatConvertible | Data.SBV.Trans, Data.SBV
IEEEFloating | Data.SBV.Trans, Data.SBV
IEEEFP | Data.SBV.Internals
If | Data.SBV.Tools.WeakestPreconditions
Iff |
1 (Type/Class) | Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Trans, Data.SBV
iff | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
ignoreExitCode | Data.SBV.Trans.Control, Data.SBV.Control, Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Imm | Documentation.SBV.Examples.Puzzles.AOC_2021_24
imperativeAppend | Documentation.SBV.Examples.WeakestPreconditions.Append
imperativeDiv | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
imperativeFib | Documentation.SBV.Examples.WeakestPreconditions.Fib
imperativeGCD | Documentation.SBV.Examples.WeakestPreconditions.GCD
imperativeInc | Documentation.SBV.Examples.WeakestPreconditions.Basics
imperativeLength | Documentation.SBV.Examples.WeakestPreconditions.Length
imperativeSqrt | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
imperativeSum | Documentation.SBV.Examples.WeakestPreconditions.Sum
Implies |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
implode |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
IncS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Basics
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Basics
Independent | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
IndependentResult | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Indeterminate | Data.SBV.Tools.WeakestPreconditions
indexOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
induct | Data.SBV.Tools.Induction
InductionResult | Data.SBV.Tools.Induction
InductionStep | Data.SBV.Tools.Induction
inductNat | Data.SBV.Tools.NaturalInduction
inductNatWith | Data.SBV.Tools.NaturalInduction
inductWith | Data.SBV.Tools.Induction
Infinite | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
infinity | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
InfoKeyword | Data.SBV.Trans.Control, Data.SBV.Control
Inhabitant | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
init |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
initCgState | Data.SBV.Internals
Initiation | Data.SBV.Tools.Induction
initJugs | Documentation.SBV.Examples.Puzzles.Jugs
initMachine | Documentation.SBV.Examples.BitPrecise.Legato
initRC4 | Documentation.SBV.Examples.Crypto.RC4
initS | Documentation.SBV.Examples.Crypto.RC4
InitVals | Documentation.SBV.Examples.BitPrecise.Legato
inNewAssertionStack |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
inp | Documentation.SBV.Examples.Puzzles.AOC_2021_24
inputs | Documentation.SBV.Examples.Puzzles.AOC_2021_24
inRange | Data.SBV.Trans, Data.SBV
insert | Data.SBV.Set
inSMTMode | Data.SBV.Internals
Instruction | Documentation.SBV.Examples.BitPrecise.Legato
Int | Data.SBV.Trans, Data.SBV
Int16 | Data.SBV.Trans, Data.SBV
Int32 | Data.SBV.Trans, Data.SBV
Int64 | Data.SBV.Trans, Data.SBV
Int8 | Data.SBV.Trans, Data.SBV
Inter | Data.SBV.RegExp, Data.SBV.Internals
internalConstraint | Data.SBV.Internals
internalVariable | Data.SBV.Internals
intersection | Data.SBV.Set
intersections | Data.SBV.Set
Interval | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
IntN | Data.SBV.Trans, Data.SBV
intSizeOf | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
intToDigit | Data.SBV.Char
Invariant | Data.SBV.Tools.WeakestPreconditions
invariant |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
InvariantMaintain | Data.SBV.Tools.WeakestPreconditions
InvariantPre | Data.SBV.Tools.WeakestPreconditions
invKeyExpansion | Documentation.SBV.Examples.Crypto.AES
invMixColumns | Documentation.SBV.Examples.Crypto.AES
invRound | Documentation.SBV.Examples.Crypto.Prince
io |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Ior |
1 (Type/Class) | Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Trans, Data.SBV
IRun | Data.SBV.Internals
is | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
ISafe | Data.SBV.Internals
isAlphaL1 | Data.SBV.Char
isAlphaNumL1 | Data.SBV.Char
isAscii | Data.SBV.Char
isAsciiLower | Data.SBV.Char
isAsciiUpper | Data.SBV.Char
isBoolean | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isBounded | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isCgDriver | Data.SBV.Internals
isCgMakefile | Data.SBV.Internals
isChar | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isCodeGenMode | Data.SBV.Internals
isConcrete | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
isConcretely | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
isControlL1 | Data.SBV.Char
isDigit | Data.SBV.Char
isDouble | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isEither | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isEmpty | Data.SBV.Set
ISetup | Data.SBV.Internals
isEven | Documentation.SBV.Examples.Misc.Definitions
isEvenOdd | Documentation.SBV.Examples.Misc.Definitions
isFloat | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isFP | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isFull | Data.SBV.Set
isHexDigit | Data.SBV.Char
isInfixOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
isJust | Data.SBV.Maybe
isLatin1 | Data.SBV.Char
isLeft | Data.SBV.Either
isLetterL1 | Data.SBV.Char
isLinearOrder | Data.SBV
isList | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isLowerL1 | Data.SBV.Char
isMagic | Documentation.SBV.Examples.Puzzles.MagicSquare
isMarkL1 | Data.SBV.Char
isMaybe | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isNonModelVar | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isNothing | Data.SBV.Maybe
isNumberL1 | Data.SBV.Char
isOctDigit | Data.SBV.Char
isOdd | Documentation.SBV.Examples.Misc.Definitions
isPartialOrder | Data.SBV
isPermutationOf | Documentation.SBV.Examples.BitPrecise.MergeSort
isPiecewiseLinearOrder | Data.SBV
isPrefixOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
isPrintL1 | Data.SBV.Char
isProperSubsetOf | Data.SBV.Set
isPunctuationL1 | Data.SBV.Char
isRational | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isReal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isRegularCV | Data.SBV.Internals
isRight | Data.SBV.Either
isSafe | Data.SBV.Trans, Data.SBV
isSatisfiable |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
isSatisfiableWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
isSeparatorL1 | Data.SBV.Char
isSet | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isSigned | Data.SBV.Trans, Data.SBV
isSpaceL1 | Data.SBV.Char
isString | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isSubsetOf | Data.SBV.Set
isSuffixOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
isSymbolic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
isSymbolL1 | Data.SBV.Char
IStage | Data.SBV.Internals
isTheorem |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
isTheoremWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
isTreeOrder | Data.SBV
isTuple | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isUnbounded | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isUniversal | Data.SBV.Set
isUpperL1 | Data.SBV.Char
isUserSort | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
isVacuousProof |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
isVacuousProofWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
isValid |
1 (Function) | Documentation.SBV.Examples.Puzzles.NQueens
2 (Function) | Documentation.SBV.Examples.Puzzles.U2Bridge
isWeekend | Documentation.SBV.Examples.Optimization.Enumerate
Ite | Data.SBV.Internals
ite | Data.SBV.Trans, Data.SBV
iteLazy | Data.SBV.Trans, Data.SBV
ites | Data.SBV.Tools.Polynomial
j |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
john | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
Join | Data.SBV.Internals
Jug |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Jugs
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Jugs
Jul | Documentation.SBV.Examples.Puzzles.Birthday
Jun | Documentation.SBV.Examples.Puzzles.Birthday
k |
1 (Function) | Documentation.SBV.Examples.ProofTools.Fibonacci
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
KBool | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KBounded | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KChar | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KDouble | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KEither | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Kendisi | Documentation.SBV.Examples.Puzzles.Orangutans
Key |
1 (Type/Class) | Documentation.SBV.Examples.Crypto.AES
2 (Type/Class) | Documentation.SBV.Examples.Crypto.Prince
3 (Type/Class) | Documentation.SBV.Examples.Crypto.RC4
keyExpansion | Documentation.SBV.Examples.Crypto.AES
keySchedule | Documentation.SBV.Examples.Crypto.RC4
keyScheduleString | Documentation.SBV.Examples.Crypto.RC4
KFloat | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KFP | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Killer | Documentation.SBV.Examples.Puzzles.Murder
killer | Documentation.SBV.Examples.Puzzles.Murder
Kind | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KindCast | Data.SBV.Internals
kindOf | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KList | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KMaybe | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Knave | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
Knight | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
knownAnswerTests | Documentation.SBV.Examples.Crypto.SHA
KPlus | Data.SBV.RegExp, Data.SBV.Internals
KRational | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KReal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KS | Documentation.SBV.Examples.Crypto.AES
KSet | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KStar | Data.SBV.RegExp, Data.SBV.Internals
KString | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KTuple | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KUnbounded | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
KUserSort | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
L | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
l | Documentation.SBV.Examples.WeakestPreconditions.Length
Label | Data.SBV.Internals
label | Data.SBV.Trans, Data.SBV
lAdam | Documentation.SBV.Examples.Puzzles.U2Bridge
ladyAndTigers | Documentation.SBV.Examples.Puzzles.LadyAndTigers
Lambda | Data.SBV.Internals
lambda | Data.SBV.Internals
lambdaAsArray | Data.SBV
LambdaGen | Data.SBV.Internals
lambdaStr | Data.SBV.Internals
Larry | Documentation.SBV.Examples.Puzzles.U2Bridge
lBono | Documentation.SBV.Examples.Puzzles.U2Bridge
lda | Documentation.SBV.Examples.BitPrecise.Legato
ldn | Documentation.SBV.Examples.Existentials.Diophantine
ldx | Documentation.SBV.Examples.BitPrecise.Legato
lEdge | Documentation.SBV.Examples.Puzzles.U2Bridge
legato | Documentation.SBV.Examples.BitPrecise.Legato
legatoInC | Documentation.SBV.Examples.BitPrecise.Legato
legatoIsCorrect | Documentation.SBV.Examples.BitPrecise.Legato
len | Documentation.SBV.Examples.Misc.Definitions
LenC |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Length
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Length
lenExample | Documentation.SBV.Examples.Misc.Definitions
length |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
LenS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Length
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Length
LessEq | Data.SBV.Internals
LessThan |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
Lexicographic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
LexicographicResult | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
lf | Documentation.SBV.Examples.BitPrecise.PrefixSum
liftCV2 | Data.SBV.Internals
liftDMod | Data.SBV.Internals
liftEither | Data.SBV.Either
liftMaybe | Data.SBV.Maybe
liftQRem | Data.SBV.Internals
listToListAt | Data.SBV.List
Lit | Documentation.SBV.Examples.Transformers.SymbolicEval
Literal | Data.SBV.RegExp, Data.SBV.Internals
literal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
LkUp | Data.SBV.Internals
lLarry | Documentation.SBV.Examples.Puzzles.U2Bridge
LO | Documentation.SBV.Examples.BitPrecise.Legato
Location |
1 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Murder
3 (Type/Class) | Documentation.SBV.Examples.Puzzles.Orangutans
4 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge
location |
1 (Function) | Documentation.SBV.Examples.Puzzles.Murder
2 (Function) | Documentation.SBV.Examples.Puzzles.Orangutans
Logic | Data.SBV.Trans, Data.SBV
Logic_ALL | Data.SBV.Trans, Data.SBV
Logic_NONE | Data.SBV.Trans, Data.SBV
Loop | Data.SBV.RegExp, Data.SBV.Internals
LRA | Data.SBV.Trans, Data.SBV
lsb | Data.SBV.Trans, Data.SBV
M | Documentation.SBV.Examples.Strings.SQLInjection
m |
1 (Function) | Documentation.SBV.Examples.Crypto.Prince
2 (Function) | Documentation.SBV.Examples.ProofTools.Fibonacci
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
m' | Documentation.SBV.Examples.Crypto.Prince
magic | Documentation.SBV.Examples.Puzzles.MagicSquare
maj | Documentation.SBV.Examples.Crypto.SHA
Male | Documentation.SBV.Examples.Puzzles.Murder
map |
1 (Function) | Data.SBV.Maybe
2 (Function) | Data.SBV.List
map2 | Data.SBV.Maybe
mapCV | Data.SBV.Internals
mapCV2 | Data.SBV.Internals
mapi | Data.SBV.List
maskAndMult | Documentation.SBV.Examples.BitPrecise.MultMask
mat | Documentation.SBV.Examples.Crypto.Prince
match | Data.SBV.RegExp
MathSAT | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
mathSAT | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
maxE | Documentation.SBV.Examples.Misc.Enumerate
Maximize | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
maximize | Data.SBV
May | Documentation.SBV.Examples.Puzzles.Birthday
maybe | Data.SBV.Maybe
MaybeAccess | Data.SBV.Internals
MaybeConstructor | Data.SBV.Internals
MaybeIs | Data.SBV.Internals
mdp | Data.SBV.Tools.Polynomial
Measure | Data.SBV.Tools.WeakestPreconditions
measure |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
MeasureBound | Data.SBV.Tools.WeakestPreconditions
MeasureDecrease | Data.SBV.Tools.WeakestPreconditions
member | Data.SBV.Set
Memory | Documentation.SBV.Examples.BitPrecise.Legato
memory | Documentation.SBV.Examples.BitPrecise.Legato
memset | Documentation.SBV.Examples.Misc.LambdaArray
memsetExample | Documentation.SBV.Examples.Misc.LambdaArray
Merah | Documentation.SBV.Examples.Puzzles.Orangutans
merge | Documentation.SBV.Examples.BitPrecise.MergeSort
Mergeable | Data.SBV.Trans, Data.SBV
mergeArrays | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
mergeSArr | Data.SBV.Dynamic
mergeSort | Documentation.SBV.Examples.BitPrecise.MergeSort
Metres |
1 (Type/Class) | Documentation.SBV.Examples.Misc.Newtypes
2 (Data Constructor) | Documentation.SBV.Examples.Misc.Newtypes
Metric | Data.SBV
MetricSpace | Data.SBV
midPointAlternative | Documentation.SBV.Examples.BitPrecise.BrokenSearch
midPointBroken | Documentation.SBV.Examples.BitPrecise.BrokenSearch
midPointFixed | Documentation.SBV.Examples.BitPrecise.BrokenSearch
Milk | Documentation.SBV.Examples.Puzzles.Fish
minE | Documentation.SBV.Examples.Misc.Enumerate
Minimize | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
minimize | Data.SBV
Minus |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
mInv | Documentation.SBV.Examples.Crypto.Prince
MkAssignment | Documentation.SBV.Examples.Puzzles.Orangutans
mkBirthday | Documentation.SBV.Examples.Puzzles.Birthday
mkCoin | Documentation.SBV.Examples.Puzzles.Coins
mkConstCV | Data.SBV.Internals
mkConstraint | Data.SBV.Internals
mkFibs | Documentation.SBV.Examples.Lists.Fibonacci
mkFreeVars |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
mkLambda | Data.SBV.Internals
mkNewState | Data.SBV.Internals
mkQuery | Documentation.SBV.Examples.Transformers.SymbolicEval
mkResult | Documentation.SBV.Examples.Transformers.SymbolicEval
mkSMTResult |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
mkSTree | Data.SBV.Tools.STree
mkSym | Documentation.SBV.Examples.Puzzles.Orangutans
mkSymbolicEnumeration | Data.SBV.Trans, Data.SBV
mkSymSBV | Data.SBV.Internals
mkSymVal |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
mkTransitiveClosure | Data.SBV
mkUninterpretedSort | Data.SBV.Trans, Data.SBV
mMult | Documentation.SBV.Examples.Crypto.Prince
mod | Documentation.SBV.Examples.Puzzles.AOC_2021_24
Modelable | Data.SBV.Trans, Data.SBV
modelAssocs | Data.SBV.Internals
modelBindings | Data.SBV.Internals
modelExists | Data.SBV.Trans, Data.SBV
modelObjectives | Data.SBV.Internals
modelsWithYAux | Documentation.SBV.Examples.Misc.Auxiliary
modelUIFuns | Data.SBV.Internals
Mon | Documentation.SBV.Examples.Optimization.Enumerate
monad | Documentation.SBV.Examples.Puzzles.AOC_2021_24
MonadQuery | Data.SBV.Trans.Control, Data.SBV.Control
MonadSymbolic | Data.SBV.Trans, Data.SBV
Monday | Documentation.SBV.Examples.Queries.Enums
Month | Documentation.SBV.Examples.Puzzles.Birthday
Mostek |
1 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato
2 (Data Constructor) | Documentation.SBV.Examples.BitPrecise.Legato
Move | Documentation.SBV.Examples.Puzzles.U2Bridge
move1 | Documentation.SBV.Examples.Puzzles.U2Bridge
move2 | Documentation.SBV.Examples.Puzzles.U2Bridge
moves | Documentation.SBV.Examples.Puzzles.Jugs
msb | Data.SBV.Trans, Data.SBV
msMaximize | Data.SBV
msMinimize | Data.SBV
mul | Documentation.SBV.Examples.Puzzles.AOC_2021_24
mul22 | Documentation.SBV.Examples.Uninterpreted.Multiply
MulExtCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
multAssoc | Documentation.SBV.Examples.Misc.Polynomials
multComm | Documentation.SBV.Examples.Misc.Polynomials
multInverse | Documentation.SBV.Examples.Misc.Floating
multUnit | Documentation.SBV.Examples.Misc.Polynomials
mutex | Documentation.SBV.Examples.Lists.BoundedMutex
n |
1 (Function) | Documentation.SBV.Examples.ProofTools.Fibonacci
2 (Function) | Documentation.SBV.Examples.ProofTools.Sum
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
Name | Data.SBV.Trans.Control, Data.SBV.Control
name | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
namedConstraint | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
namedLambda | Data.SBV.Internals
namedLambdaStr | Data.SBV.Internals
NamedSymVar |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
nameRe | Documentation.SBV.Examples.Strings.SQLInjection
nan | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Nationality | Documentation.SBV.Examples.Puzzles.Fish
natToStr | Data.SBV.String
needsExistentials | Data.SBV.Internals
neg | Documentation.SBV.Examples.Uninterpreted.Shannon
Negate | Documentation.SBV.Examples.Queries.FourFours
negateChecked | Data.SBV.Tools.Overflow
NegatesTo | Data.SBV
nestedArray | Documentation.SBV.Examples.Misc.NestedArray
nestedExample | Documentation.SBV.Examples.Lists.Nested
newArray |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
newArrayInState | Data.SBV.Internals
newArray_ |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
newExpr | Data.SBV.Internals
newline | Data.SBV.RegExp
newPerson | Documentation.SBV.Examples.Puzzles.Murder
newSArr | Data.SBV.Dynamic
newUninterpreted | Data.SBV.Internals
next | Documentation.SBV.Examples.Puzzles.HexPuzzle
Nibble | Documentation.SBV.Examples.Crypto.Prince
nil |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
nm | Documentation.SBV.Examples.Puzzles.Murder
noChange |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
NodeId |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
nonDecreasing | Documentation.SBV.Examples.BitPrecise.MergeSort
None | Data.SBV.RegExp, Data.SBV.Internals
NonHomogeneous | Documentation.SBV.Examples.Existentials.Diophantine
NonLinear | Data.SBV.Internals
nonLinear | Documentation.SBV.Examples.Crypto.Prince
NonQueryVar | Data.SBV.Internals
nonZeroAddition | Documentation.SBV.Examples.Misc.Floating
normCV | Data.SBV.Internals
Norwegian | Documentation.SBV.Examples.Puzzles.Fish
Not |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
not |
1 (Function) | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
2 (Function) | Documentation.SBV.Examples.Uninterpreted.Deduce
notElem |
1 (Function) | Data.SBV.List
2 (Function) | Data.SBV.Char
NotEqual | Data.SBV.Internals
notFair | Documentation.SBV.Examples.Lists.BoundedMutex
nothing | Data.SBV.RegExp
NoTiming | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
notMember | Data.SBV.Set
noWiggle | Documentation.SBV.Examples.Uninterpreted.Shannon
nQueens | Documentation.SBV.Examples.Puzzles.NQueens
null |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.Set
3 (Function) | Data.SBV.List
numerator | Data.SBV.Trans, Data.SBV
Objective | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
observe | Data.SBV.Trans, Data.SBV
observeIf | Data.SBV
octal | Data.SBV.RegExp
octDigit | Data.SBV.RegExp
Ofallo | Documentation.SBV.Examples.Puzzles.Orangutans
offsetIndexOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
old | Documentation.SBV.Examples.Puzzles.Rabbits
oneBits | Data.SBV.Trans, Data.SBV
oneIf | Data.SBV.Trans, Data.SBV
oneOf | Data.SBV.RegExp
Op | Data.SBV.Internals
Open | Data.SBV.Tools.Range
OpenPoint | Data.SBV
oppositeSignsCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
Opt | Data.SBV.RegExp, Data.SBV.Internals
optimize |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
OptimizeResult | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
OptimizeStyle | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
optimizeValidateConstraints | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
optimizeWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
OptionKeyword | Data.SBV.Trans.Control, Data.SBV.Control
options | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Or |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
or | Documentation.SBV.Examples.Uninterpreted.Deduce
Orangutan | Documentation.SBV.Examples.Puzzles.Orangutans
orangutan | Documentation.SBV.Examples.Puzzles.Orangutans
ord | Data.SBV.Char
OrdSymbolic | Data.SBV.Trans, Data.SBV
outOfInit | Documentation.SBV.Examples.Misc.LambdaArray
output |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
outputSVal | Data.SBV.Dynamic
Outputtable | Data.SBV.Internals
outside | Documentation.SBV.Examples.Misc.ModelExtract
OverflowOp | Data.SBV.Internals
Overflow_SMul_OVFL | Data.SBV.Internals
Overflow_SMul_UDFL | Data.SBV.Internals
Overflow_UMul_OVFL | Data.SBV.Internals
OvOp | Data.SBV.Internals
P | Documentation.SBV.Examples.Puzzles.Drinker
p | Documentation.SBV.Examples.Queries.UnsatCore
pAdd | Data.SBV.Tools.Polynomial
Pareto | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
ParetoResult | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
parseCVs | Data.SBV.Trans, Data.SBV
PartialCorrectness | Data.SBV.Tools.Induction
pbAtLeast | Data.SBV.Trans, Data.SBV
pbAtMost | Data.SBV.Trans, Data.SBV
pbEq | Data.SBV.Trans, Data.SBV
pbExactly | Data.SBV.Trans, Data.SBV
pbGe | Data.SBV.Trans, Data.SBV
pbLe | Data.SBV.Trans, Data.SBV
pbMutexed | Data.SBV.Trans, Data.SBV
PBOp | Data.SBV.Internals
pbStronglyMutexed | Data.SBV.Trans, Data.SBV
PB_AtLeast | Data.SBV.Internals
PB_AtMost | Data.SBV.Internals
PB_Eq | Data.SBV.Internals
PB_Exactly | Data.SBV.Internals
PB_Ge | Data.SBV.Internals
PB_Le | Data.SBV.Internals
pDiv | Data.SBV.Tools.Polynomial
pDivMod | Data.SBV.Tools.Polynomial
peek |
1 (Function) | Documentation.SBV.Examples.BitPrecise.Legato
2 (Function) | Documentation.SBV.Examples.Puzzles.U2Bridge
Penalty |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Person |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Murder
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Murder
Pet | Documentation.SBV.Examples.Puzzles.Fish
pgm1 | Documentation.SBV.Examples.ProofTools.Strengthen
pgm2 | Documentation.SBV.Examples.ProofTools.Strengthen
pgmAssignments | Data.SBV.Internals
pingPong | Documentation.SBV.Examples.Misc.Definitions
play | Documentation.SBV.Examples.Queries.GuessNumber
Plus |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
3 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
pMod | Data.SBV.Tools.Polynomial
pMult | Data.SBV.Tools.Polynomial
poExample | Documentation.SBV.Examples.Misc.FirstOrderLogic
poke | Documentation.SBV.Examples.BitPrecise.Legato
polyDivMod | Documentation.SBV.Examples.Misc.Polynomials
Polynomial | Data.SBV.Tools.Polynomial
polynomial | Data.SBV.Tools.Polynomial
pop |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
pop8 | Documentation.SBV.Examples.CodeGeneration.PopulationCount
popCount | Data.SBV.Trans, Data.SBV
popCountDefault | Data.SBV.Trans, Data.SBV
popCountFast | Documentation.SBV.Examples.CodeGeneration.PopulationCount
popCountSlow | Documentation.SBV.Examples.CodeGeneration.PopulationCount
pos | Documentation.SBV.Examples.Uninterpreted.Shannon
post |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
postcondition | Data.SBV.Tools.WeakestPreconditions
Power | Data.SBV.RegExp, Data.SBV.Internals
PowerList | Documentation.SBV.Examples.BitPrecise.PrefixSum
powerOfTwoCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
pre |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib
3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
precondition | Data.SBV.Tools.WeakestPreconditions
Predicate | Data.SBV.Trans, Data.SBV
prepareMessage | Documentation.SBV.Examples.Crypto.SHA
preprocess | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
PrettyNum | Data.SBV.Internals
prga | Documentation.SBV.Examples.Crypto.RC4
prince | Documentation.SBV.Examples.Crypto.Prince
princeCore | Documentation.SBV.Examples.Crypto.Prince
printBase | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
printRealPrec | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
PrintTiming | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
problem |
1 (Function) | Documentation.SBV.Examples.Misc.Auxiliary
2 (Function) | Documentation.SBV.Examples.Misc.Newtypes
3 (Function) | Documentation.SBV.Examples.Optimization.ExtField
4 (Function) | Documentation.SBV.Examples.Optimization.LinearOpt
5 (Function) | Documentation.SBV.Examples.ProofTools.BMC
6 (Function) | Documentation.SBV.Examples.ProofTools.Strengthen
ProduceAbducts | Data.SBV.Trans.Control, Data.SBV.Control
ProduceAssertions | Data.SBV.Trans.Control, Data.SBV.Control
ProduceAssignments | Data.SBV.Trans.Control, Data.SBV.Control
ProduceInterpolants | Data.SBV.Trans.Control, Data.SBV.Control
ProduceProofs | Data.SBV.Trans.Control, Data.SBV.Control
ProduceUnsatAssumptions | Data.SBV.Trans.Control, Data.SBV.Control
ProduceUnsatCores | Data.SBV.Trans.Control, Data.SBV.Control
production | Documentation.SBV.Examples.Optimization.Production
progInfo | Data.SBV.Internals
Program |
1 (Type/Class) | Data.SBV.Tools.WeakestPreconditions
2 (Data Constructor) | Data.SBV.Tools.WeakestPreconditions
3 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato
4 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval
5 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
program | Data.SBV.Tools.WeakestPreconditions
project | Data.SBV.Control
proofArgReduce | Data.SBV.Trans
ProofError | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
ProofResult | Data.SBV.Tools.WeakestPreconditions
Property |
1 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
prop_ExpandKey | Documentation.SBV.Examples.Crypto.Prince
prop_RoundKeys | Documentation.SBV.Examples.Crypto.Prince
prop_SBox | Documentation.SBV.Examples.Crypto.Prince
prop_sr | Documentation.SBV.Examples.Crypto.Prince
Provable | Data.SBV.Trans, Data.SBV
ProvableM | Data.SBV.Internals, Data.SBV.Trans
prove |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
proveConcurrentWithAll |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
proveConcurrentWithAny |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
Proved | Documentation.SBV.Examples.Transformers.SymbolicEval
Proven |
1 (Data Constructor) | Data.SBV.Tools.WeakestPreconditions
2 (Data Constructor) | Data.SBV.Tools.Induction
proveSArray | Documentation.SBV.Examples.Uninterpreted.AUF
proveWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
3 (Function) | Data.SBV.Dynamic
proveWithAll |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
proveWithAny |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
ps | Documentation.SBV.Examples.BitPrecise.PrefixSum
PseudoBoolean | Data.SBV.Internals
PT | Documentation.SBV.Examples.Crypto.Prince
punctuation | Data.SBV.RegExp
push |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Puzzle | Documentation.SBV.Examples.Puzzles.Sudoku
puzzle |
1 (Function) | Documentation.SBV.Examples.Puzzles.AOC_2021_24
2 (Function) | Documentation.SBV.Examples.Puzzles.Birthday
3 (Function) | Documentation.SBV.Examples.Puzzles.Coins
4 (Function) | Documentation.SBV.Examples.Puzzles.Counts
5 (Function) | Documentation.SBV.Examples.Puzzles.DogCatMouse
6 (Function) | Documentation.SBV.Examples.Puzzles.Garden
7 (Function) | Documentation.SBV.Examples.Puzzles.Jugs
8 (Function) | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
9 (Function) | Documentation.SBV.Examples.Puzzles.Murder
10 (Function) | Documentation.SBV.Examples.Puzzles.Orangutans
11 (Function) | Documentation.SBV.Examples.Queries.FourFours
puzzle1 |
1 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku
2 (Function) | Documentation.SBV.Examples.Strings.RegexCrossword
puzzle2 |
1 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku
2 (Function) | Documentation.SBV.Examples.Strings.RegexCrossword
puzzle3 |
1 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku
2 (Function) | Documentation.SBV.Examples.Strings.RegexCrossword
puzzle4 | Documentation.SBV.Examples.Puzzles.Sudoku
puzzle5 | Documentation.SBV.Examples.Puzzles.Sudoku
puzzle6 | Documentation.SBV.Examples.Puzzles.Sudoku
Q |
1 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
3 (Type/Class) | Documentation.SBV.Examples.Uninterpreted.Sort
q | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
qe | Documentation.SBV.Examples.Misc.FirstOrderLogic
QF_ABV | Data.SBV.Trans, Data.SBV
QF_AUFBV | Data.SBV.Trans, Data.SBV
QF_AUFLIA | Data.SBV.Trans, Data.SBV
QF_AX | Data.SBV.Trans, Data.SBV
QF_BV | Data.SBV.Trans, Data.SBV
QF_FD | Data.SBV.Trans, Data.SBV
QF_FP | Data.SBV.Trans, Data.SBV
QF_FPBV | Data.SBV.Trans, Data.SBV
QF_IDL | Data.SBV.Trans, Data.SBV
QF_LIA | Data.SBV.Trans, Data.SBV
QF_LRA | Data.SBV.Trans, Data.SBV
QF_NIA | Data.SBV.Trans, Data.SBV
QF_NRA | Data.SBV.Trans, Data.SBV
QF_RDL | Data.SBV.Trans, Data.SBV
QF_S | Data.SBV.Trans, Data.SBV
QF_UF | Data.SBV.Trans, Data.SBV
QF_UFBV | Data.SBV.Trans, Data.SBV
QF_UFIDL | Data.SBV.Trans, Data.SBV
QF_UFLIA | Data.SBV.Trans, Data.SBV
QF_UFLRA | Data.SBV.Trans, Data.SBV
QF_UFNIRA | Data.SBV.Trans, Data.SBV
QF_UFNRA | Data.SBV.Trans, Data.SBV
QNot | Data.SBV
qNot | Data.SBV
QuantifiedBool |
1 (Data Constructor) | Data.SBV.Internals
2 (Type/Class) | Data.SBV.Internals, Data.SBV
quantifiedBool | Data.SBV.Internals, Data.SBV
Quantifier | Data.SBV.Internals, Data.SBV.Dynamic
Queriable | Data.SBV.Control
queries | Documentation.SBV.Examples.BitPrecise.BitTricks
Query |
1 (Type/Class) | Data.SBV.Trans.Control, Data.SBV.Control
2 (Data Constructor) | Documentation.SBV.Examples.Strings.SQLInjection
query |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
queryAsk | Data.SBV.Internals
queryAssertionStackDepth | Data.SBV.Internals
queryConfig | Data.SBV.Internals
QueryContext | Data.SBV.Internals
queryDebug |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
QueryExternal | Data.SBV.Internals
QueryInternal | Data.SBV.Internals
queryOne | Documentation.SBV.Examples.Queries.Concurrency
QueryResult | Data.SBV.Control
queryRetrieveResponse | Data.SBV.Internals
querySend | Data.SBV.Internals
QueryState |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
queryState | Data.SBV.Trans.Control, Data.SBV.Control
QueryT |
1 (Type/Class) | Data.SBV.Trans.Control, Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
queryTerminate | Data.SBV.Internals
queryTimeOutValue | Data.SBV.Internals
queryTwo | Documentation.SBV.Examples.Queries.Concurrency
QueryVar | Data.SBV.Internals
Quirrel | Documentation.SBV.Examples.Puzzles.Orangutans
Quot | Data.SBV.Internals
r | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
Rabbit | Documentation.SBV.Examples.Puzzles.Rabbits
rabbits | Documentation.SBV.Examples.Puzzles.Rabbits
rabbitsAreOK | Documentation.SBV.Examples.Puzzles.Rabbits
RandomSeed | Data.SBV.Trans.Control, Data.SBV.Control
Range |
1 (Data Constructor) | Data.SBV.RegExp, Data.SBV.Internals
2 (Type/Class) | Data.SBV.Tools.Range
3 (Data Constructor) | Data.SBV.Tools.Range
ranges | Data.SBV.Tools.Range
rangesWith | Data.SBV.Tools.Range
RatApprox | Data.SBV
RatExact | Data.SBV
RatInterval | Data.SBV
Ratio | Data.SBV.Trans, Data.SBV
Rational | Data.SBV.Trans, Data.SBV
RationalConstructor | Data.SBV.Internals
RationalCV | Data.SBV
RatIrreducible | Data.SBV
RC4 | Documentation.SBV.Examples.Crypto.RC4
rc4IsCorrect | Documentation.SBV.Examples.Crypto.RC4
rConstants | Documentation.SBV.Examples.Crypto.Prince
RCSet | Data.SBV.Internals, Data.SBV
read | Documentation.SBV.Examples.Puzzles.AOC_2021_24
readArray | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
readBin | Data.SBV.Internals
readSArr | Data.SBV.Dynamic
readSTree | Data.SBV.Tools.STree
ReadVar | Documentation.SBV.Examples.Strings.SQLInjection
Ready | Documentation.SBV.Examples.Lists.BoundedMutex
RealPoint | Data.SBV
realPoint | Data.SBV
ReasonUnknown | Data.SBV.Trans.Control, Data.SBV.Control
Red |
1 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Fish
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Garden
3 (Data Constructor) | Documentation.SBV.Examples.Puzzles.HexPuzzle
redirectVerbose | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Reg | Documentation.SBV.Examples.Puzzles.AOC_2021_24
RegA | Documentation.SBV.Examples.BitPrecise.Legato
RegExEq | Data.SBV.Internals
RegExNEq | Data.SBV.Internals
RegExOp |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
RegExp | Data.SBV.RegExp, Data.SBV.Internals
RegExpMatchable | Data.SBV.RegExp
Register |
1 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.AOC_2021_24
register | Documentation.SBV.Examples.Puzzles.AOC_2021_24
registerKind | Data.SBV.Internals
Registers | Documentation.SBV.Examples.BitPrecise.Legato
registers | Documentation.SBV.Examples.BitPrecise.Legato
registerUISMTFunction | Data.SBV.Control
RegularCV | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
RegularSet | Data.SBV.Internals, Data.SBV
RegX | Documentation.SBV.Examples.BitPrecise.Legato
Relation | Data.SBV
Rem | Data.SBV.Internals
renderCgPgmBundle | Data.SBV.Internals
renderTest | Data.SBV.Tools.GenTest
replace |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
ReproducibleResourceLimit | Data.SBV.Trans.Control, Data.SBV.Control
resArrays | Data.SBV.Internals
resAsgns | Data.SBV.Internals
resAssertions | Data.SBV.Internals
resConstraints | Data.SBV.Internals
resConsts | Data.SBV.Internals
resDefinitions | Data.SBV.Internals
resetAssertions |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
reskinds | Data.SBV.Internals
resObservables | Data.SBV.Internals
resOutputs | Data.SBV.Internals
resParams | Data.SBV.Internals
Resp_AllStatistics | Data.SBV.Trans.Control, Data.SBV.Control
Resp_AssertionStackLevels | Data.SBV.Trans.Control, Data.SBV.Control
Resp_Authors | Data.SBV.Trans.Control, Data.SBV.Control
Resp_Error | Data.SBV.Trans.Control, Data.SBV.Control
Resp_InfoKeyword | Data.SBV.Trans.Control, Data.SBV.Control
Resp_Name | Data.SBV.Trans.Control, Data.SBV.Control
Resp_ReasonUnknown | Data.SBV.Trans.Control, Data.SBV.Control
Resp_Unsupported | Data.SBV.Trans.Control, Data.SBV.Control
Resp_Version | Data.SBV.Trans.Control, Data.SBV.Control
resTables | Data.SBV.Internals
resTraces | Data.SBV.Internals
resUIConsts | Data.SBV.Internals
resUISegs | Data.SBV.Internals
Result |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
3 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval
4 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval
result | Documentation.SBV.Examples.Transformers.SymbolicEval
retrieveResponseFromSolver | Data.SBV.Internals
reverse |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
Rol | Data.SBV.Internals
Role | Documentation.SBV.Examples.Puzzles.Murder
role | Documentation.SBV.Examples.Puzzles.Murder
Ror | Data.SBV.Internals
rorM | Documentation.SBV.Examples.BitPrecise.Legato
rorR | Documentation.SBV.Examples.BitPrecise.Legato
rotate | Data.SBV.Trans, Data.SBV
rotateL | Data.SBV.Trans, Data.SBV
rotateR | Data.SBV.Trans, Data.SBV
rotR | Documentation.SBV.Examples.Crypto.AES
round | Documentation.SBV.Examples.Crypto.Prince
roundConstants | Documentation.SBV.Examples.Crypto.AES
roundingAdd | Documentation.SBV.Examples.Misc.Floating
RoundingMode | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
roundingMode | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
RoundNearestTiesToAway | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
RoundNearestTiesToEven | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
RoundTowardNegative | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
RoundTowardPositive | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
RoundTowardZero | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Row |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.MagicSquare
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Sudoku
run |
1 (Function) | Documentation.SBV.Examples.Puzzles.AOC_2021_24
2 (Function) | Documentation.SBV.Examples.Puzzles.U2Bridge
runAESTests | Documentation.SBV.Examples.Crypto.AES
runAlloc | Documentation.SBV.Examples.Transformers.SymbolicEval
runEval | Documentation.SBV.Examples.Transformers.SymbolicEval
runLegato | Documentation.SBV.Examples.BitPrecise.Legato
runProgramEval | Documentation.SBV.Examples.Transformers.SymbolicEval
runPropertyEval | Documentation.SBV.Examples.Transformers.SymbolicEval
runQ | Documentation.SBV.Examples.Transformers.SymbolicEval
runQueryT | Data.SBV.Internals
runSMT |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
runSMTWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
runSymbolic | Data.SBV.Internals
S |
1 (Type/Class) | Documentation.SBV.Examples.Crypto.RC4
2 (Type/Class) | Documentation.SBV.Examples.ProofTools.BMC
3 (Data Constructor) | Documentation.SBV.Examples.ProofTools.BMC
4 (Type/Class) | Documentation.SBV.Examples.ProofTools.Fibonacci
5 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Fibonacci
6 (Type/Class) | Documentation.SBV.Examples.ProofTools.Strengthen
7 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Strengthen
8 (Type/Class) | Documentation.SBV.Examples.ProofTools.Sum
9 (Data Constructor) | Documentation.SBV.Examples.ProofTools.Sum
10 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
11 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Length
12 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Sum
s |
1 (Function) | Documentation.SBV.Examples.ProofTools.Sum
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum
sA |
1 (Function) | Documentation.SBV.Examples.Misc.Enumerate
2 (Function) | Documentation.SBV.Examples.Misc.FirstOrderLogic
sAdam | Documentation.SBV.Examples.Puzzles.U2Bridge
safe |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
SafeResult |
1 (Type/Class) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
safeWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
3 (Function) | Data.SBV.Dynamic
sailors | Documentation.SBV.Examples.Existentials.Diophantine
sAll | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sAlone | Documentation.SBV.Examples.Puzzles.Murder
sAmbalat | Documentation.SBV.Examples.Puzzles.Orangutans
sAnd | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sAny | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SArr | Data.SBV.Dynamic
SArray |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
sAssert | Data.SBV.Trans, Data.SBV
Sat |
1 (Data Constructor) | Data.SBV.Trans.Control, Data.SBV.Control
2 (Data Constructor) | Documentation.SBV.Examples.Optimization.Enumerate
sat |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
satArgReduce | Data.SBV.Trans
satCmd | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
satConcurrentWithAll |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
satConcurrentWithAny |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
SatExtField | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Satisfiable |
1 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Type/Class) | Data.SBV.Trans, Data.SBV
SatisfiableM | Data.SBV.Internals, Data.SBV.Trans
SatModel | Data.SBV.Trans, Data.SBV
SatResult |
1 (Type/Class) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Saturday | Documentation.SBV.Examples.Queries.Enums
satWith |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
3 (Function) | Data.SBV.Dynamic
satWithAll |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
satWithAny |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
sAug | Documentation.SBV.Examples.Puzzles.Birthday
SaveTiming | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
says | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
SB | Documentation.SBV.Examples.Uninterpreted.Deduce
sB |
1 (Function) | Documentation.SBV.Examples.Misc.Enumerate
2 (Function) | Documentation.SBV.Examples.Misc.FirstOrderLogic
sBar | Documentation.SBV.Examples.Puzzles.Murder
sBarrelRotateLeft |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sBarrelRotateRight |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sBasahan | Documentation.SBV.Examples.Puzzles.Orangutans
sBaseball | Documentation.SBV.Examples.Puzzles.Fish
sBeach | Documentation.SBV.Examples.Puzzles.Murder
sBeer | Documentation.SBV.Examples.Puzzles.Fish
SBeverage | Documentation.SBV.Examples.Puzzles.Fish
sbin | Data.SBV.Internals
sbinI | Data.SBV.Internals
SBinOp | Documentation.SBV.Examples.Queries.FourFours
sBird | Documentation.SBV.Examples.Puzzles.Fish
sBlack | Documentation.SBV.Examples.Puzzles.HexPuzzle
sBlue |
1 (Function) | Documentation.SBV.Examples.Puzzles.Fish
2 (Function) | Documentation.SBV.Examples.Puzzles.Garden
3 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle
sBono | Documentation.SBV.Examples.Puzzles.U2Bridge
SBool | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sBool |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sBools |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sBool_ | Data.SBV
sBox | Documentation.SBV.Examples.Crypto.Prince
sbox | Documentation.SBV.Examples.Crypto.AES
sBoxInv | Documentation.SBV.Examples.Crypto.Prince
sboxInverseCorrect | Documentation.SBV.Examples.Crypto.AES
sboxTable | Documentation.SBV.Examples.Crypto.AES
sBriton | Documentation.SBV.Examples.Puzzles.Fish
SButton | Documentation.SBV.Examples.Puzzles.HexPuzzle
SBV |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
SBVApp | Data.SBV.Internals
sbvCheckSolverInstallation | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SBVCodeGen |
1 (Type/Class) | Data.SBV.Tools.CodeGen, Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals
sbvDefineValue | Data.SBV.Trans, Data.SBV
SBVException |
1 (Type/Class) | Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Trans, Data.SBV
sbvExceptionConfig | Data.SBV.Trans, Data.SBV
sbvExceptionDescription | Data.SBV.Trans, Data.SBV
sbvExceptionExitCode | Data.SBV.Trans, Data.SBV
sbvExceptionExpected | Data.SBV.Trans, Data.SBV
sbvExceptionHint | Data.SBV.Trans, Data.SBV
sbvExceptionReason | Data.SBV.Trans, Data.SBV
sbvExceptionReceived | Data.SBV.Trans, Data.SBV
sbvExceptionSent | Data.SBV.Trans, Data.SBV
sbvExceptionStdErr | Data.SBV.Trans, Data.SBV
sbvExceptionStdOut | Data.SBV.Trans, Data.SBV
SBVExpr | Data.SBV.Internals
SBVPgm |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
sbvQuickCheck | Data.SBV.Trans, Data.SBV
SBVReverse | Data.SBV.Internals
SBVRunMode | Data.SBV.Internals
sbvToSV | Data.SBV.Internals
sbvToSymSV | Data.SBV.Internals
SBVType |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
sBystander | Documentation.SBV.Examples.Puzzles.Murder
sC |
1 (Function) | Documentation.SBV.Examples.Misc.Enumerate
2 (Function) | Documentation.SBV.Examples.Misc.FirstOrderLogic
sCase | Documentation.SBV.Examples.Queries.FourFours
sCat | Documentation.SBV.Examples.Puzzles.Fish
SChar | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sChar |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sChars |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sChar_ | Data.SBV
sCoffee | Documentation.SBV.Examples.Puzzles.Fish
SColor |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Fish
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Garden
3 (Type/Class) | Documentation.SBV.Examples.Puzzles.HexPuzzle
sComparableSWord32AsSFloat | Data.SBV.Internals
sComparableSWord64AsSDouble | Data.SBV.Internals
sComparableSWordAsSFloatingPoint | Data.SBV.Internals
sCountLeadingZeros | Data.SBV.Trans, Data.SBV
sCountTrailingZeros | Data.SBV.Trans, Data.SBV
scriptBody | Data.SBV.Internals
scriptModel | Data.SBV.Internals
sCritical | Documentation.SBV.Examples.Lists.BoundedMutex
sCrossTime | Documentation.SBV.Examples.Puzzles.U2Bridge
sD14 | Documentation.SBV.Examples.Puzzles.Birthday
sD15 | Documentation.SBV.Examples.Puzzles.Birthday
sD16 | Documentation.SBV.Examples.Puzzles.Birthday
sD17 | Documentation.SBV.Examples.Puzzles.Birthday
sD18 | Documentation.SBV.Examples.Puzzles.Birthday
sD19 | Documentation.SBV.Examples.Puzzles.Birthday
sDane | Documentation.SBV.Examples.Puzzles.Fish
SDay |
1 (Type/Class) | Documentation.SBV.Examples.Optimization.Enumerate
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Birthday
3 (Type/Class) | Documentation.SBV.Examples.Queries.Enums
sDiv | Data.SBV.Trans, Data.SBV
sDivide | Documentation.SBV.Examples.Queries.FourFours
SDivisible | Data.SBV.Trans, Data.SBV
sDivMod | Data.SBV.Trans, Data.SBV
sDog | Documentation.SBV.Examples.Puzzles.Fish
sDolly | Documentation.SBV.Examples.Puzzles.Orangutans
SDouble | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sDouble |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sDoubleAsComparableSWord64 | Data.SBV.Internals
sDoubleAsSWord64 | Data.SBV.Trans, Data.SBV
sDoubles |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sDouble_ | Data.SBV
SE |
1 (Type/Class) | Documentation.SBV.Examples.Misc.Enumerate
2 (Type/Class) | Documentation.SBV.Examples.Misc.FirstOrderLogic
search | Documentation.SBV.Examples.Puzzles.HexPuzzle
second | Data.SBV.Either
secondQuery | Documentation.SBV.Examples.Queries.Concurrency
sEdge | Documentation.SBV.Examples.Puzzles.U2Bridge
sEDiv | Data.SBV
sEDivMod | Data.SBV
SEither | Data.SBV.Internals, Data.SBV
sEither | Data.SBV
sEithers | Data.SBV
sEither_ | Data.SBV
select | Data.SBV.Trans, Data.SBV
selectRe | Documentation.SBV.Examples.Strings.SQLInjection
sElem | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sEMod | Data.SBV
sendMoreMoney | Documentation.SBV.Examples.Puzzles.SendMoreMoney
sendRequestToSolver | Data.SBV.Internals
sendStringToSolver | Data.SBV.Internals
Seq | Data.SBV.Tools.WeakestPreconditions
SeqConcat | Data.SBV.Internals
SeqContains | Data.SBV.Internals
SeqFoldLeft | Data.SBV.Internals
SeqFoldLeftI | Data.SBV.Internals
SeqIndexOf | Data.SBV.Internals
SeqLen | Data.SBV.Internals
SeqMap | Data.SBV.Internals
SeqMapI | Data.SBV.Internals
SeqNth | Data.SBV.Internals
SeqOp |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SeqPrefixOf | Data.SBV.Internals
SeqReplace | Data.SBV.Internals
SeqSubseq | Data.SBV.Internals
SeqSuffixOf | Data.SBV.Internals
SeqUnit | Data.SBV.Internals
setBit | Data.SBV.Trans, Data.SBV
setBitTo | Data.SBV.Trans, Data.SBV
setFlag | Documentation.SBV.Examples.BitPrecise.Legato
SetInfo | Data.SBV.Trans.Control, Data.SBV.Control
setInfo | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SetLogic | Data.SBV.Trans.Control, Data.SBV.Control
setLogic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SetOp | Data.SBV.Internals
setOption | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
setReg | Documentation.SBV.Examples.BitPrecise.Legato
setTimeOut | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
setup | Data.SBV.Tools.WeakestPreconditions
sEva | Documentation.SBV.Examples.Puzzles.Orangutans
Sex | Documentation.SBV.Examples.Puzzles.Murder
sex | Documentation.SBV.Examples.Puzzles.Murder
SExecutable | Data.SBV.Trans, Data.SBV
sExpt | Documentation.SBV.Examples.Queries.FourFours
sExtractBits | Data.SBV.Trans, Data.SBV
sFactorial | Documentation.SBV.Examples.Queries.FourFours
sFalse | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sFalsity | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
sFemale | Documentation.SBV.Examples.Puzzles.Murder
SFiniteBits | Data.SBV.Trans, Data.SBV
sFiniteBitSize | Data.SBV.Trans, Data.SBV
sFish | Documentation.SBV.Examples.Puzzles.Fish
SFloat | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sFloat |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sFloatAsComparableSWord32 | Data.SBV.Internals
sFloatAsSWord32 | Data.SBV.Trans, Data.SBV
SFloatingPoint | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sFloatingPoint | Data.SBV
sFloatingPointAsComparableSWord | Data.SBV.Internals
sFloatingPointAsSWord | Data.SBV.Trans, Data.SBV
sFloatingPoints | Data.SBV
sFloatingPoint_ | Data.SBV
sFloats |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sFloat_ | Data.SBV
sFootball | Documentation.SBV.Examples.Puzzles.Fish
SFPBFloat | Data.SBV.Internals, Data.SBV
sFPBFloat | Data.SBV
sFPBFloats | Data.SBV
sFPBFloat_ | Data.SBV
SFPDouble | Data.SBV.Internals, Data.SBV
sFPDouble | Data.SBV
sFPDoubles | Data.SBV
sFPDouble_ | Data.SBV
SFPHalf | Data.SBV.Internals, Data.SBV
sFPHalf | Data.SBV
sFPHalfs | Data.SBV
sFPHalf_ | Data.SBV
SFPQuad | Data.SBV.Internals, Data.SBV
sFPQuad | Data.SBV
sFPQuads | Data.SBV
sFPQuad_ | Data.SBV
SFPSingle | Data.SBV.Internals, Data.SBV
sFPSingle | Data.SBV
sFPSingles | Data.SBV
sFPSingle_ | Data.SBV
sFrancine | Documentation.SBV.Examples.Puzzles.Orangutans
sFri | Documentation.SBV.Examples.Optimization.Enumerate
sFriday | Documentation.SBV.Examples.Queries.Enums
sFromIntegral | Data.SBV.Trans, Data.SBV
sFromIntegralChecked | Data.SBV.Tools.Overflow
sFromIntegralO | Data.SBV.Tools.Overflow
sgcd | Documentation.SBV.Examples.CodeGeneration.GCD
sgcdIsCorrect | Documentation.SBV.Examples.CodeGeneration.GCD
sGerman | Documentation.SBV.Examples.Puzzles.Fish
sGracie | Documentation.SBV.Examples.Puzzles.Orangutans
sGreen |
1 (Function) | Documentation.SBV.Examples.Puzzles.Fish
2 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle
SHA |
1 (Type/Class) | Documentation.SBV.Examples.Crypto.SHA
2 (Data Constructor) | Documentation.SBV.Examples.Crypto.SHA
sha224 | Documentation.SBV.Examples.Crypto.SHA
sha224P | Documentation.SBV.Examples.Crypto.SHA
sha256 | Documentation.SBV.Examples.Crypto.SHA
sha256P | Documentation.SBV.Examples.Crypto.SHA
sha384 | Documentation.SBV.Examples.Crypto.SHA
sha384P | Documentation.SBV.Examples.Crypto.SHA
sha512 | Documentation.SBV.Examples.Crypto.SHA
sha512P | Documentation.SBV.Examples.Crypto.SHA
sha512_224 | Documentation.SBV.Examples.Crypto.SHA
sha512_224P | Documentation.SBV.Examples.Crypto.SHA
sha512_256 | Documentation.SBV.Examples.Crypto.SHA
sha512_256P | Documentation.SBV.Examples.Crypto.SHA
shaConstants | Documentation.SBV.Examples.Crypto.SHA
shaLoopCount | Documentation.SBV.Examples.Crypto.SHA
Shamir | Documentation.SBV.Examples.Puzzles.Orangutans
SHandler | Documentation.SBV.Examples.Puzzles.Orangutans
shannon | Documentation.SBV.Examples.Uninterpreted.Shannon
shannon2 | Documentation.SBV.Examples.Uninterpreted.Shannon
shaP | Documentation.SBV.Examples.Crypto.SHA
shared | Documentation.SBV.Examples.Queries.Concurrency
sharedDependent | Documentation.SBV.Examples.Queries.Concurrency
sHere | Documentation.SBV.Examples.Puzzles.U2Bridge
shex | Data.SBV.Internals
shexI | Data.SBV.Internals
shift | Data.SBV.Trans, Data.SBV
shiftL | Data.SBV.Trans, Data.SBV
shiftLeft | Documentation.SBV.Examples.CodeGeneration.Uninterpreted
shiftR | Data.SBV.Trans, Data.SBV
Shl | Data.SBV.Internals
sHockey | Documentation.SBV.Examples.Puzzles.Fish
sHorse | Documentation.SBV.Examples.Puzzles.Fish
showBFloat | Data.SBV.Internals
showBlock | Documentation.SBV.Examples.Crypto.Prince
showCDouble | Data.SBV.Internals
showCFloat | Data.SBV.Internals
showFloatAtBase | Data.SBV.Internals
showHash | Documentation.SBV.Examples.Crypto.SHA
showHDouble | Data.SBV.Internals
showHFloat | Data.SBV.Internals
showModel | Data.SBV.Internals
showNegativeNumber | Data.SBV.Internals
showPoly | Data.SBV.Tools.Polynomial
showPolynomial | Data.SBV.Tools.Polynomial
showSMTDouble | Data.SBV.Internals
showSMTFloat | Data.SBV.Internals
showTDiff | Data.SBV.Internals
showType | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Shr | Data.SBV.Internals
SHumanHeightInCm | Documentation.SBV.Examples.Misc.Newtypes
SI | Documentation.SBV.Examples.Misc.SetAlgebra
SIdentity | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
sIdle | Documentation.SBV.Examples.Lists.BoundedMutex
sigma0 | Documentation.SBV.Examples.Crypto.SHA
sigma0Coefficients | Documentation.SBV.Examples.Crypto.SHA
sigma1 | Documentation.SBV.Examples.Crypto.SHA
sigma1Coefficients | Documentation.SBV.Examples.Crypto.SHA
SignExtend | Data.SBV.Internals
signExtend |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInfinity | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
singleton |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.Set
3 (Function) | Data.SBV.List
SInhabitant | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
SInt | Data.SBV.Trans, Data.SBV
sInt |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
SInt16 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInt16 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt16s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt16_ | Data.SBV
SInt32 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInt32 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt32s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt32_ | Data.SBV
SInt64 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInt64 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt64s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt64_ | Data.SBV
SInt8 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInt8 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt8s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt8_ | Data.SBV
SInteger | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sInteger |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sIntegers |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInteger_ | Data.SBV
SIntegral | Data.SBV.Trans, Data.SBV
sIntN | Data.SBV.Dynamic
sIntN_ | Data.SBV.Dynamic
sInts |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sInt_ | Data.SBV
sJul | Documentation.SBV.Examples.Puzzles.Birthday
sJun | Documentation.SBV.Examples.Puzzles.Birthday
sJust | Data.SBV.Maybe
sKendisi | Documentation.SBV.Examples.Puzzles.Orangutans
sKiller | Documentation.SBV.Examples.Puzzles.Murder
Skip | Data.SBV.Tools.WeakestPreconditions
sKnave | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
sKnight | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
skolemEx1 | Documentation.SBV.Examples.Misc.FirstOrderLogic
skolemEx2 | Documentation.SBV.Examples.Misc.FirstOrderLogic
skolemEx3 | Documentation.SBV.Examples.Misc.FirstOrderLogic
skolemEx4 | Documentation.SBV.Examples.Misc.FirstOrderLogic
Skolemize | Data.SBV
skolemize | Data.SBV
SL | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
sLarry | Documentation.SBV.Examples.Puzzles.U2Bridge
sLeft | Data.SBV.Either
SList | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sList |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sListArray | Data.SBV.Internals, Data.SBV
sLists |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sList_ | Data.SBV
SLocation |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Murder
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Orangutans
3 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge
sMale | Documentation.SBV.Examples.Puzzles.Murder
smax | Data.SBV.Trans, Data.SBV
sMay | Documentation.SBV.Examples.Puzzles.Birthday
SMaybe | Data.SBV.Internals, Data.SBV
sMaybe | Data.SBV
sMaybes | Data.SBV
sMaybe_ | Data.SBV
sMerah | Documentation.SBV.Examples.Puzzles.Orangutans
SMetres | Documentation.SBV.Examples.Misc.Newtypes
sMilk | Documentation.SBV.Examples.Puzzles.Fish
smin | Data.SBV.Trans, Data.SBV
sMinus | Documentation.SBV.Examples.Queries.FourFours
sMod | Data.SBV.Trans, Data.SBV
sMon | Documentation.SBV.Examples.Optimization.Enumerate
sMonday | Documentation.SBV.Examples.Queries.Enums
SMonth | Documentation.SBV.Examples.Puzzles.Birthday
SMTConfig |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SMTDefinable | Data.SBV.Trans, Data.SBV
SMTErrorBehavior | Data.SBV.Trans.Control, Data.SBV.Control
smtFunction | Data.SBV.Trans, Data.SBV
SMTInfoFlag | Data.SBV.Trans.Control, Data.SBV.Control
SMTInfoResponse | Data.SBV.Trans.Control, Data.SBV.Control
SMTLib2 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SMTLibPgm |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
smtLibPgm | Data.SBV.Internals
smtLibReservedNames | Data.SBV.Internals
SMTLibVersion | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
smtLibVersion | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
smtLibVersionExtension | Data.SBV.Internals
SMTMode | Data.SBV.Internals
SMTModel |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SMTOption | Data.SBV.Trans.Control, Data.SBV.Control
SMTProblem |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SMTReasonUnknown | Data.SBV.Trans, Data.SBV
SMTResult | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
smtRoundingMode | Data.SBV.Internals
SMTScript |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SMTSolver |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SMTVerbosity | Data.SBV.Trans.Control, Data.SBV.Control
sName |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sNaN | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SNationality | Documentation.SBV.Examples.Puzzles.Fish
sNegate | Documentation.SBV.Examples.Queries.FourFours
snoc |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
sNorwegian | Documentation.SBV.Examples.Puzzles.Fish
sNot | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sNotElem | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sNothing | Data.SBV.Maybe
sObserve | Data.SBV
sOfallo | Documentation.SBV.Examples.Puzzles.Orangutans
softConstrain | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Solution |
1 (Type/Class) | Documentation.SBV.Examples.Existentials.Diophantine
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.NQueens
solve |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
solveCrossword | Documentation.SBV.Examples.Strings.RegexCrossword
solved | Documentation.SBV.Examples.Puzzles.Jugs
solveEuler185 | Documentation.SBV.Examples.Puzzles.Euler185
solveN | Documentation.SBV.Examples.Puzzles.U2Bridge
Solver | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
solver | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
SolverCapabilities |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SolverContext | Data.SBV.Internals
solverSetOptions | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
solveU2 | Documentation.SBV.Examples.Puzzles.U2Bridge
sOr | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SOrangutan | Documentation.SBV.Examples.Puzzles.Orangutans
SP | Documentation.SBV.Examples.Puzzles.Drinker
SpecialRelOp | Data.SBV.Internals
SPet | Documentation.SBV.Examples.Puzzles.Fish
sPlus | Documentation.SBV.Examples.Queries.FourFours
sPopCount | Data.SBV.Trans, Data.SBV
Sport | Documentation.SBV.Examples.Puzzles.Fish
SQ | Documentation.SBV.Examples.Uninterpreted.Sort
SQLExpr | Documentation.SBV.Examples.Strings.SQLInjection
Sqrt | Documentation.SBV.Examples.Queries.FourFours
sqrt | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
SqrtS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
sQuirrel | Documentation.SBV.Examples.Puzzles.Orangutans
sQuot | Data.SBV.Trans, Data.SBV
sQuotRem | Data.SBV.Trans, Data.SBV
sr | Documentation.SBV.Examples.Crypto.Prince
SRabbit | Documentation.SBV.Examples.Puzzles.Rabbits
SRational | Data.SBV.Internals, Data.SBV
sRational | Data.SBV
sRationals | Data.SBV
sRational_ | Data.SBV
sReady | Documentation.SBV.Examples.Lists.BoundedMutex
SReal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sReal |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sReals |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sRealToSInteger | Data.SBV.Trans, Data.SBV
sReal_ | Data.SBV
sRed |
1 (Function) | Documentation.SBV.Examples.Puzzles.Fish
2 (Function) | Documentation.SBV.Examples.Puzzles.Garden
3 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle
sRem | Data.SBV.Trans, Data.SBV
sRight | Data.SBV.Either
srInv | Documentation.SBV.Examples.Crypto.Prince
sRNA | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRNE | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
SRole | Documentation.SBV.Examples.Puzzles.Murder
sRotateLeft | Data.SBV.Trans, Data.SBV
sRotateRight | Data.SBV.Trans, Data.SBV
SRoundingMode | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundNearestTiesToAway | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundNearestTiesToEven | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardNegative | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardPositive | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRoundTowardZero | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTN | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTP | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sRTZ | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sSat | Documentation.SBV.Examples.Optimization.Enumerate
sSaturday | Documentation.SBV.Examples.Queries.Enums
SSet | Data.SBV.Internals, Data.SBV
sSet | Data.SBV
sSets | Data.SBV
sSet_ | Data.SBV
SSex | Documentation.SBV.Examples.Puzzles.Murder
sShamir | Documentation.SBV.Examples.Puzzles.Orangutans
sShiftLeft | Data.SBV.Trans, Data.SBV
sShiftRight | Data.SBV.Trans, Data.SBV
sSignedShiftArithRight | Data.SBV.Trans, Data.SBV
SSport | Documentation.SBV.Examples.Puzzles.Fish
sSqrt | Documentation.SBV.Examples.Queries.FourFours
SState | Documentation.SBV.Examples.Lists.BoundedMutex
SStatement | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
SString | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sString |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sStrings |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sString_ | Data.SBV
sSun | Documentation.SBV.Examples.Optimization.Enumerate
sSunday | Documentation.SBV.Examples.Queries.Enums
sSwede | Documentation.SBV.Examples.Puzzles.Fish
stability | Data.SBV.Tools.WeakestPreconditions
Stable | Data.SBV.Tools.WeakestPreconditions
stable | Data.SBV.Tools.WeakestPreconditions
sTarakan | Documentation.SBV.Examples.Puzzles.Orangutans
start | Documentation.SBV.Examples.Puzzles.U2Bridge
State |
1 (Type/Class) | Data.SBV.Internals
2 (Type/Class) | Documentation.SBV.Examples.Crypto.AES
3 (Type/Class) | Documentation.SBV.Examples.Lists.BoundedMutex
4 (Type/Class) | Documentation.SBV.Examples.Puzzles.AOC_2021_24
5 (Data Constructor) | Documentation.SBV.Examples.Puzzles.AOC_2021_24
Statement | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
statementRe | Documentation.SBV.Examples.Strings.SQLInjection
Status |
1 (Type/Class) | Data.SBV.Tools.WeakestPreconditions
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.U2Bridge
3 (Data Constructor) | Documentation.SBV.Examples.Puzzles.U2Bridge
sTea | Documentation.SBV.Examples.Puzzles.Fish
sTennis | Documentation.SBV.Examples.Puzzles.Fish
sTestBit | Data.SBV.Trans, Data.SBV
sThere | Documentation.SBV.Examples.Puzzles.U2Bridge
sThu | Documentation.SBV.Examples.Optimization.Enumerate
sThursday | Documentation.SBV.Examples.Queries.Enums
STime | Documentation.SBV.Examples.Puzzles.U2Bridge
sTimes | Documentation.SBV.Examples.Queries.FourFours
Stmt | Data.SBV.Tools.WeakestPreconditions
StrConcat | Data.SBV.Internals
StrContains | Data.SBV.Internals
STree | Data.SBV.Tools.STree
StrFromCode | Data.SBV.Internals
StrIndexOf | Data.SBV.Internals
StrInRe | Data.SBV.Internals
StrLen | Data.SBV.Internals
StrNatToStr | Data.SBV.Internals
StrNth | Data.SBV.Internals
StrOp |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
StrPrefixOf | Data.SBV.Internals
strRe | Documentation.SBV.Examples.Strings.SQLInjection
StrReplace | Data.SBV.Internals
StrStrToNat | Data.SBV.Internals
StrSubstr | Data.SBV.Internals
StrSuffixOf | Data.SBV.Internals
strToCharAt | Data.SBV.String
StrToCode | Data.SBV.Internals
strToNat | Data.SBV.String
strToStrAt | Data.SBV.String
sTrue | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
StrUnit | Data.SBV.Internals
sTruth | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
Stuck | Data.SBV.Tools.WeakestPreconditions
sTue | Documentation.SBV.Examples.Optimization.Enumerate
sTuesday | Documentation.SBV.Examples.Queries.Enums
STuple | Data.SBV.Internals, Data.SBV
sTuple | Data.SBV
STuple2 | Data.SBV.Internals, Data.SBV
STuple3 | Data.SBV.Internals, Data.SBV
STuple4 | Data.SBV.Internals, Data.SBV
STuple5 | Data.SBV.Internals, Data.SBV
STuple6 | Data.SBV.Internals, Data.SBV
STuple7 | Data.SBV.Internals, Data.SBV
STuple8 | Data.SBV.Internals, Data.SBV
sTuples | Data.SBV
sTuple_ | Data.SBV
SU | Documentation.SBV.Examples.Misc.FirstOrderLogic
SU2Member | Documentation.SBV.Examples.Puzzles.U2Bridge
subList | Data.SBV.List
subStr | Data.SBV.String
sudoku | Documentation.SBV.Examples.Puzzles.Sudoku
sum0 | Documentation.SBV.Examples.Crypto.SHA
sum0Coefficients | Documentation.SBV.Examples.Crypto.SHA
sum1 | Documentation.SBV.Examples.Crypto.SHA
sum1Coefficients | Documentation.SBV.Examples.Crypto.SHA
sumCorrect | Documentation.SBV.Examples.ProofTools.Sum
SumS |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Sum
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Sum
sumToN | Documentation.SBV.Examples.Misc.Definitions
sumToNExample | Documentation.SBV.Examples.Misc.Definitions
Sun | Documentation.SBV.Examples.Optimization.Enumerate
Sunday | Documentation.SBV.Examples.Queries.Enums
SUnOp | Documentation.SBV.Examples.Queries.FourFours
supportsApproxReals | Data.SBV.Internals
supportsBitVectors | Data.SBV.Internals
supportsCustomQueries | Data.SBV.Internals
supportsDataTypes | Data.SBV.Internals
supportsDefineFun | Data.SBV.Internals
supportsDeltaSat | Data.SBV.Internals
supportsDirectAccessors | Data.SBV.Internals
supportsDistinct | Data.SBV.Internals
supportsFlattenedModels | Data.SBV.Internals
supportsFoldAndMap | Data.SBV.Internals
supportsGlobalDecls | Data.SBV.Internals
supportsIEEE754 | Data.SBV.Internals
supportsInt2bv | Data.SBV.Internals
supportsOptimization | Data.SBV.Internals
supportsPseudoBooleans | Data.SBV.Internals
supportsQuantifiers | Data.SBV.Internals
supportsReals | Data.SBV.Internals
supportsSets | Data.SBV.Internals
supportsSpecialRels | Data.SBV.Internals
supportsUnboundedInts | Data.SBV.Internals
supportsUninterpretedSorts | Data.SBV.Internals
SV |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
3 (Type/Class) | Documentation.SBV.Examples.Misc.FirstOrderLogic
svAbs | Data.SBV.Dynamic
svAddConstant | Data.SBV.Dynamic
SVal |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals
svAnd | Data.SBV.Dynamic
svAsBool | Data.SBV.Dynamic
svAsInteger | Data.SBV.Dynamic
svBarrelRotateLeft | Data.SBV.Dynamic
svBarrelRotateRight | Data.SBV.Dynamic
svBlastBE | Data.SBV.Dynamic
svBlastLE | Data.SBV.Dynamic
svBool | Data.SBV.Dynamic
svCgInput | Data.SBV.Internals, Data.SBV.Dynamic
svCgInputArr | Data.SBV.Internals, Data.SBV.Dynamic
svCgOutput | Data.SBV.Internals, Data.SBV.Dynamic
svCgOutputArr | Data.SBV.Internals, Data.SBV.Dynamic
svCgReturn | Data.SBV.Internals, Data.SBV.Dynamic
svCgReturnArr | Data.SBV.Internals, Data.SBV.Dynamic
svDecrement | Data.SBV.Dynamic
svDenominator | Data.SBV.Dynamic
svDivide | Data.SBV.Dynamic
svDouble | Data.SBV.Dynamic
svEnumFromThenTo | Data.SBV.Dynamic
svEqual | Data.SBV.Dynamic
svExp | Data.SBV.Dynamic
svExtract | Data.SBV.Dynamic
svFalse | Data.SBV.Dynamic
svFloat | Data.SBV.Dynamic
svFloatingPoint | Data.SBV.Dynamic
svFromIntegral | Data.SBV.Dynamic
svFromWord1 | Data.SBV.Dynamic
svGreaterEq | Data.SBV.Dynamic
svGreaterThan | Data.SBV.Dynamic
sVictim | Documentation.SBV.Examples.Puzzles.Murder
svIncrement | Data.SBV.Dynamic
svInteger | Data.SBV.Dynamic
svIte | Data.SBV.Dynamic
svJoin | Data.SBV.Dynamic
svLazyIte | Data.SBV.Dynamic
svLessEq | Data.SBV.Dynamic
svLessThan | Data.SBV.Dynamic
svMinus | Data.SBV.Dynamic
svMkSymVar | Data.SBV.Dynamic
svNewVar | Data.SBV.Dynamic
svNewVar_ | Data.SBV.Dynamic
svNot | Data.SBV.Dynamic
svNotEqual | Data.SBV.Dynamic
svNumerator | Data.SBV.Dynamic
sVolleyball | Documentation.SBV.Examples.Puzzles.Fish
svOr | Data.SBV.Dynamic
svPlus | Data.SBV.Dynamic
svQuickCheck | Data.SBV.Dynamic
svQuot | Data.SBV.Dynamic
svQuotRem | Data.SBV.Dynamic
svReal | Data.SBV.Dynamic
svRem | Data.SBV.Dynamic
svRol | Data.SBV.Dynamic
svRor | Data.SBV.Dynamic
svRotateLeft | Data.SBV.Dynamic
svRotateRight | Data.SBV.Dynamic
svSelect | Data.SBV.Dynamic
svSetBit | Data.SBV.Dynamic
svShiftLeft | Data.SBV.Dynamic
svShiftRight | Data.SBV.Dynamic
svShl | Data.SBV.Dynamic
svShr | Data.SBV.Dynamic
svSign | Data.SBV.Dynamic
svSignExtend | Data.SBV.Dynamic
svStrongEqual | Data.SBV.Dynamic
svStructuralLessThan | Data.SBV.Dynamic
svSymbolicMerge | Data.SBV.Dynamic
svTestBit | Data.SBV.Dynamic
svTimes | Data.SBV.Dynamic
svToSV | Data.SBV.Internals
svToWord1 | Data.SBV.Dynamic
svTrue | Data.SBV.Dynamic
svUNeg | Data.SBV.Dynamic
svUninterpreted | Data.SBV.Dynamic
svUnsign | Data.SBV.Dynamic
svWordFromBE | Data.SBV.Dynamic
svWordFromLE | Data.SBV.Dynamic
svXOr | Data.SBV.Dynamic
svZeroExtend | Data.SBV.Dynamic
swap |
1 (Function) | Data.SBV.Tuple
2 (Function) | Documentation.SBV.Examples.Crypto.RC4
sWater | Documentation.SBV.Examples.Puzzles.Fish
sWed | Documentation.SBV.Examples.Optimization.Enumerate
Swede | Documentation.SBV.Examples.Puzzles.Fish
sWednesday | Documentation.SBV.Examples.Queries.Enums
sWhite | Documentation.SBV.Examples.Puzzles.Fish
SWord | Data.SBV.Trans, Data.SBV
sWord |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
SWord16 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord16 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord16s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord16_ | Data.SBV
SWord32 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord32 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord32AsSFloat | Data.SBV.Trans, Data.SBV
sWord32s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord32_ | Data.SBV
SWord64 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord64 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord64AsSDouble | Data.SBV.Trans, Data.SBV
sWord64s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord64_ | Data.SBV
SWord8 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
sWord8 |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord8s |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord8_ | Data.SBV
sWordAsSFloatingPoint | Data.SBV.Trans, Data.SBV
sWordN | Data.SBV.Dynamic
sWordN_ | Data.SBV.Dynamic
sWords |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
sWord_ | Data.SBV
sYellow |
1 (Function) | Documentation.SBV.Examples.Puzzles.Fish
2 (Function) | Documentation.SBV.Examples.Puzzles.Garden
sym | Data.SBV.Trans, Data.SBV
SymArray | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
Symbolic | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
symbolic |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
symbolicEnv | Data.SBV.Trans, Data.SBV
symbolicMerge | Data.SBV.Trans, Data.SBV
symbolics |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans
2 (Function) | Data.SBV
SymbolicT | Data.SBV.Trans, Data.SBV
SymTuple | Data.SBV
SymVal | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
synthMul22 | Documentation.SBV.Examples.Uninterpreted.Multiply
T | Documentation.SBV.Examples.Queries.FourFours
t0 | Documentation.SBV.Examples.Crypto.AES
t0Func | Documentation.SBV.Examples.Crypto.AES
t1 |
1 (Function) | Documentation.SBV.Examples.Crypto.AES
2 (Function) | Documentation.SBV.Examples.Uninterpreted.Sort
t128Dec | Documentation.SBV.Examples.Crypto.AES
t128Enc | Documentation.SBV.Examples.Crypto.AES
t192Dec | Documentation.SBV.Examples.Crypto.AES
t192Enc | Documentation.SBV.Examples.Crypto.AES
t2 |
1 (Function) | Documentation.SBV.Examples.Crypto.AES
2 (Function) | Documentation.SBV.Examples.Uninterpreted.Sort
t256Dec | Documentation.SBV.Examples.Crypto.AES
t256Enc | Documentation.SBV.Examples.Crypto.AES
t3 | Documentation.SBV.Examples.Crypto.AES
tab | Data.SBV.RegExp
taggedSkolemize | Data.SBV
tail |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
take |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
tallestHumanEver | Documentation.SBV.Examples.Misc.Newtypes
Tarakan | Documentation.SBV.Examples.Puzzles.Orangutans
targetName | Data.SBV.Internals
tcExample1 | Documentation.SBV.Examples.Misc.FirstOrderLogic
tcExample2 | Documentation.SBV.Examples.Misc.FirstOrderLogic
tcExample3 | Documentation.SBV.Examples.Misc.FirstOrderLogic
Tea | Documentation.SBV.Examples.Puzzles.Fish
Tennis | Documentation.SBV.Examples.Puzzles.Fish
Term | Documentation.SBV.Examples.Transformers.SymbolicEval
Ternary | Documentation.SBV.Examples.Uninterpreted.Shannon
test |
1 (Function) | Documentation.SBV.Examples.Existentials.Diophantine
2 (Function) | Documentation.SBV.Examples.Uninterpreted.Deduce
test1 | Documentation.SBV.Examples.Misc.NoDiv0
test2 | Documentation.SBV.Examples.Misc.NoDiv0
testBit | Data.SBV.Trans, Data.SBV
testBitDefault | Data.SBV.Trans, Data.SBV
testGF28 | Documentation.SBV.Examples.Misc.Polynomials
TestStyle | Data.SBV.Tools.GenTest
TestVectors | Data.SBV.Tools.GenTest
testVectors | Documentation.SBV.Examples.Crypto.Prince
There | Documentation.SBV.Examples.Puzzles.U2Bridge
thm | Documentation.SBV.Examples.Uninterpreted.AUF
thm1 | Documentation.SBV.Examples.BitPrecise.PrefixSum
thm2 | Documentation.SBV.Examples.BitPrecise.PrefixSum
thmGood | Documentation.SBV.Examples.Uninterpreted.Function
ThmResult |
1 (Type/Class) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Thu | Documentation.SBV.Examples.Optimization.Enumerate
Thursday | Documentation.SBV.Examples.Queries.Enums
tiePL | Documentation.SBV.Examples.BitPrecise.PrefixSum
Time | Documentation.SBV.Examples.Puzzles.U2Bridge
time | Documentation.SBV.Examples.Puzzles.U2Bridge
timeout |
1 (Function) | Data.SBV.Trans.Control
2 (Function) | Data.SBV.Control
Times |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
Timing | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
timing | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
toBytes | Data.SBV
toIntegralSized | Data.SBV.Trans, Data.SBV
toLowerL1 | Data.SBV.Char
toMetricSpace | Data.SBV
toNibbles | Documentation.SBV.Examples.Crypto.Prince
toSDouble | Data.SBV.Trans, Data.SBV
toSFloat | Data.SBV.Trans, Data.SBV
toSFloatingPoint | Data.SBV.Trans, Data.SBV
ToSized | Data.SBV.Trans, Data.SBV
toSized | Data.SBV.Trans, Data.SBV
toUpperL1 | Data.SBV.Char
traceExecution | Data.SBV.Tools.WeakestPreconditions
transcript | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
transfer | Documentation.SBV.Examples.Puzzles.Jugs
translate | Data.SBV.Internals
trueCV | Data.SBV.Internals
trueSV | Data.SBV.Internals
Truth | Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
ts | Documentation.SBV.Examples.WeakestPreconditions.Append
tstShiftLeft | Documentation.SBV.Examples.CodeGeneration.Uninterpreted
Tue | Documentation.SBV.Examples.Optimization.Enumerate
Tuesday | Documentation.SBV.Examples.Queries.Enums
tuple | Data.SBV.Tuple
TupleAccess | Data.SBV.Internals
TupleConstructor | Data.SBV.Internals
U |
1 (Type/Class) | Documentation.SBV.Examples.Misc.FirstOrderLogic
2 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
u0 | Documentation.SBV.Examples.Crypto.AES
u0Func | Documentation.SBV.Examples.Crypto.AES
u1 | Documentation.SBV.Examples.Crypto.AES
u2 | Documentation.SBV.Examples.Crypto.AES
U2Member | Documentation.SBV.Examples.Puzzles.U2Bridge
u3 | Documentation.SBV.Examples.Crypto.AES
ucCore | Documentation.SBV.Examples.Queries.UnsatCore
UFLRA | Data.SBV.Trans, Data.SBV
UFNIA | Data.SBV.Trans, Data.SBV
UICgC | Data.SBV.Internals
UICodeKind | Data.SBV.Internals
UINone | Data.SBV.Internals
UISMT | Data.SBV.Internals
Unbounded | Data.SBV.Tools.Range
uncache | Data.SBV.Internals
uncacheAI | Data.SBV.Internals
uncons |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
UNeg | Data.SBV.Internals
unEval | Documentation.SBV.Examples.Transformers.SymbolicEval
uninterpret | Data.SBV.Trans, Data.SBV
Uninterpreted | Data.SBV.Internals
Union | Data.SBV.RegExp, Data.SBV.Internals
union | Data.SBV.Set
unions | Data.SBV.Set
universal |
1 (Function) | Data.SBV.Set
2 (Function) | Documentation.SBV.Examples.Uninterpreted.Shannon
univOK | Documentation.SBV.Examples.Uninterpreted.Shannon
Unk | Data.SBV.Trans.Control, Data.SBV.Control
Unknown | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
UnknownIncomplete | Data.SBV.Trans, Data.SBV
UnknownMemOut | Data.SBV.Trans, Data.SBV
UnknownOther | Data.SBV.Trans, Data.SBV
UnknownTimeOut | Data.SBV.Trans, Data.SBV
unliteral | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
UnOp | Documentation.SBV.Examples.Queries.FourFours
unsafeCastSBV | Documentation.SBV.Examples.Transformers.SymbolicEval
unsafeShiftL | Data.SBV.Trans, Data.SBV
unsafeShiftR | Data.SBV.Trans, Data.SBV
unSArray | Data.SBV.Internals
Unsat | Data.SBV.Trans.Control, Data.SBV.Control
Unsatisfiable | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
unSBox | Documentation.SBV.Examples.Crypto.AES
unSBoxTable | Documentation.SBV.Examples.Crypto.AES
unSBV | Data.SBV.Internals
Unstable | Data.SBV.Tools.WeakestPreconditions
untuple | Data.SBV.Tuple
unzipPL | Documentation.SBV.Examples.BitPrecise.PrefixSum
usb5 | Documentation.SBV.Examples.CodeGeneration.CRC_USB5
V | Documentation.SBV.Examples.Misc.FirstOrderLogic
valid |
1 (Function) | Documentation.SBV.Examples.Puzzles.Birthday
2 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku
validateModel | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
ValidFloat | Data.SBV
validPick | Documentation.SBV.Examples.Puzzles.Garden
validSequence | Documentation.SBV.Examples.Lists.BoundedMutex
validTurns | Documentation.SBV.Examples.Lists.BoundedMutex
Value |
1 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.AOC_2021_24
Var | Documentation.SBV.Examples.Transformers.SymbolicEval
VarContext | Data.SBV.Internals
VC | Data.SBV.Tools.WeakestPreconditions
verbose | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
Version | Data.SBV.Trans.Control, Data.SBV.Control
Victim | Documentation.SBV.Examples.Puzzles.Murder
Volleyball | Documentation.SBV.Examples.Puzzles.Fish
w | Documentation.SBV.Examples.Puzzles.AOC_2021_24
Water | Documentation.SBV.Examples.Puzzles.Fish
Wed | Documentation.SBV.Examples.Optimization.Enumerate
Wednesday | Documentation.SBV.Examples.Queries.Enums
weekendJustOver | Documentation.SBV.Examples.Optimization.Enumerate
whenS | Documentation.SBV.Examples.Puzzles.U2Bridge
whereIs | Documentation.SBV.Examples.Puzzles.U2Bridge
While | Data.SBV.Tools.WeakestPreconditions
White | Documentation.SBV.Examples.Puzzles.Fish
whiteSpace | Data.SBV.RegExp
whiteSpaceNoNewLine | Data.SBV.RegExp
Word | Data.SBV.Trans, Data.SBV
Word16 | Data.SBV.Trans, Data.SBV
Word32 | Data.SBV.Trans, Data.SBV
Word64 | Data.SBV.Trans, Data.SBV
Word8 | Data.SBV.Trans, Data.SBV
WordN | Data.SBV.Trans, Data.SBV
wordSize | Documentation.SBV.Examples.Crypto.SHA
wordToDouble | Data.SBV.Internals
wordToFloat | Data.SBV.Internals
WPConfig |
1 (Type/Class) | Data.SBV.Tools.WeakestPreconditions
2 (Data Constructor) | Data.SBV.Tools.WeakestPreconditions
wpProve | Data.SBV.Tools.WeakestPreconditions
wpProveWith | Data.SBV.Tools.WeakestPreconditions
wpSolver | Data.SBV.Tools.WeakestPreconditions
wpVerbose | Data.SBV.Tools.WeakestPreconditions
write | Documentation.SBV.Examples.Puzzles.AOC_2021_24
writeArray | Data.SBV.Internals, Data.SBV.Trans, Data.SBV
writeSArr | Data.SBV.Dynamic
writeSTree | Data.SBV.Tools.STree
x |
1 (Function) | Documentation.SBV.Examples.ProofTools.BMC
2 (Function) | Documentation.SBV.Examples.ProofTools.Strengthen
3 (Function) | Documentation.SBV.Examples.Puzzles.AOC_2021_24
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
xferFlash | Documentation.SBV.Examples.Puzzles.U2Bridge
xferPerson | Documentation.SBV.Examples.Puzzles.U2Bridge
XOr | Data.SBV.Internals
Xor |
1 (Type/Class) | Data.SBV.Trans, Data.SBV
2 (Data Constructor) | Data.SBV.Trans, Data.SBV
xor | Data.SBV.Trans, Data.SBV
xs |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Append
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
y |
1 (Function) | Documentation.SBV.Examples.ProofTools.BMC
2 (Function) | Documentation.SBV.Examples.ProofTools.Strengthen
3 (Function) | Documentation.SBV.Examples.Puzzles.AOC_2021_24
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv
Yellow |
1 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Fish
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Garden
Yices | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
yices | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
ys |
1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Append
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length
z | Documentation.SBV.Examples.Puzzles.AOC_2021_24
Z3 | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
z3 | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
zeroBits | Data.SBV.Trans, Data.SBV
ZeroExtend | Data.SBV.Internals
zeroExtend |
1 (Function) | Data.SBV.Trans
2 (Function) | Data.SBV
zip | Data.SBV.List
zipPL | Documentation.SBV.Examples.BitPrecise.PrefixSum
zipWith | Data.SBV.List
zs | Documentation.SBV.Examples.WeakestPreconditions.Append
\\ | Data.SBV.Set
^. | Data.SBV.Tuple
_1 | Data.SBV.Tuple
_2 | Data.SBV.Tuple
_3 | Data.SBV.Tuple
_4 | Data.SBV.Tuple
_5 | Data.SBV.Tuple
_6 | Data.SBV.Tuple
_7 | Data.SBV.Tuple
_8 | Data.SBV.Tuple
_cvKind | Data.SBV.Internals, Data.SBV.Dynamic
|-> | Data.SBV.Trans.Control, Data.SBV.Control