# | Data.SBV.Trans, Data.SBV |
% | Data.SBV.Trans, Data.SBV |
*! | Data.SBV.Tools.Overflow |
+! | Data.SBV.Tools.Overflow |
-! | Data.SBV.Tools.Overflow |
.!! | |
1 (Function) | Data.SBV.String |
2 (Function) | Data.SBV.List |
.&& | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
.&. | Data.SBV.Trans, Data.SBV |
.++ | |
1 (Function) | Data.SBV.String |
2 (Function) | Data.SBV.List |
./= | Data.SBV.Trans, Data.SBV |
./== | 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.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.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 (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 |
Actions | Documentation.SBV.Examples.Puzzles.U2Bridge |
Adam | Documentation.SBV.Examples.Puzzles.U2Bridge |
adc | Documentation.SBV.Examples.BitPrecise.Legato |
addAxiom | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
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 |
aes128IsCorrect | Documentation.SBV.Examples.Crypto.AES |
aesDecrypt | Documentation.SBV.Examples.Crypto.AES |
aesEncrypt | 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 | Documentation.SBV.Examples.Puzzles.Murder |
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 |
allEqual | 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 |
allowQuantifiedQueries | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
allPossibleTrees | Documentation.SBV.Examples.Queries.FourFours |
allPuzzles | Documentation.SBV.Examples.Puzzles.Sudoku |
allSat | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
allSatHasPrefixExistentials | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
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 |
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 |
And | |
1 (Data Constructor) | Data.SBV.Internals |
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval |
and | Documentation.SBV.Examples.Uninterpreted.Deduce |
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 |
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 |
august | Documentation.SBV.Examples.Puzzles.Birthday |
Authors | Data.SBV.Trans.Control, Data.SBV.Control |
ax1 | Documentation.SBV.Examples.Uninterpreted.Deduce |
ax2 | Documentation.SBV.Examples.Uninterpreted.Deduce |
ax3 | Documentation.SBV.Examples.Uninterpreted.Deduce |
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.Queries.FourFours |
3 (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 |
Baseball | Documentation.SBV.Examples.Puzzles.Fish |
basis | Documentation.SBV.Examples.Existentials.Diophantine |
bcc | Documentation.SBV.Examples.BitPrecise.Legato |
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 |
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 |
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 |
Black | Documentation.SBV.Examples.Puzzles.HexPuzzle |
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.SHA |
2 (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 | Data.SBV.Trans, Data.SBV |
bvExtract | Data.SBV.Trans, 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 | Data.SBV.Trans, 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 |
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 |
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 |
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 |
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 |
CodeGen | Data.SBV.Internals |
codeGen | |
1 (Function) | Data.SBV.Internals |
2 (Function) | Documentation.SBV.Examples.BitPrecise.MergeSort |
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 |
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 |
constrainWithAttribute | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
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 |
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 |
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 |
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 |
Dane | Documentation.SBV.Examples.Puzzles.Fish |
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 |
decrypt | 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 |
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 |
dispSolution | Documentation.SBV.Examples.Puzzles.Sudoku |
distinct | Data.SBV.Trans, Data.SBV |
distinctExcept | Data.SBV.Trans, Data.SBV |
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 |
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 |
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 |
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 | 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 |
envX | Documentation.SBV.Examples.Transformers.SymbolicEval |
envY | Documentation.SBV.Examples.Transformers.SymbolicEval |
Epsilon | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
eqSArr | Data.SBV.Dynamic |
EqSymbolic | 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 |
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 | Documentation.SBV.Examples.Queries.Interpolants |
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 |
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 (Function) | Data.SBV.Internals, Data.SBV.Trans |
2 (Function) | Data.SBV |
existsDay | Documentation.SBV.Examples.Puzzles.Birthday |
existsMonth | Documentation.SBV.Examples.Puzzles.Birthday |
existsOK | Documentation.SBV.Examples.Uninterpreted.Shannon |
exists_ | |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
2 (Function) | Data.SBV |
exit | |
1 (Function) | Data.SBV.Trans.Control |
2 (Function) | Data.SBV.Control |
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 |
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 |
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 |
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 |
Football | Documentation.SBV.Examples.Puzzles.Fish |
forAll | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
forall | |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
2 (Function) | Data.SBV |
forallDay | Documentation.SBV.Examples.Puzzles.Birthday |
forallMonth | Documentation.SBV.Examples.Puzzles.Birthday |
forAll_ | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
forall_ | |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
2 (Function) | Data.SBV |
forceSVArg | Data.SBV.Internals |
forSome | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
forSome_ | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
Forte | Data.SBV.Tools.GenTest |
four | Documentation.SBV.Examples.Misc.Enumerate |
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 |
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 |
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 |
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 |
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.Trans, Data.SBV |
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 |
generateSMTBenchmark | |
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 |
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 |
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 |
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 |
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 |
Goal | Data.SBV.Trans, Data.SBV |
Good | Data.SBV.Tools.WeakestPreconditions |
goodSum | Documentation.SBV.Examples.Queries.AllSat |
GreaterEq | Data.SBV.Internals |
GreaterThan | |
1 (Data Constructor) | Data.SBV.Internals |
2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval |
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 |
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 |
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 |
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 |
ignoreExitCode | Data.SBV.Trans.Control, Data.SBV.Control, Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
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 | 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 |
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 |
init | |
1 (Function) | Data.SBV.String |
2 (Function) | Data.SBV.List |
initCgState | Data.SBV.Internals |
Initiation | Data.SBV.Tools.Induction |
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 |
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 |
invMixColumns | Documentation.SBV.Examples.Crypto.AES |
io | |
1 (Function) | Data.SBV.Trans.Control |
2 (Function) | Data.SBV.Control |
IRun | Data.SBV.Internals |
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 |
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 |
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 |
isPermutationOf | Documentation.SBV.Examples.BitPrecise.MergeSort |
isPrefixOf | |
1 (Function) | Data.SBV.String |
2 (Function) | Data.SBV.List |
isPrintL1 | Data.SBV.Char |
isProperSubsetOf | Data.SBV.Set |
isPunctuationL1 | Data.SBV.Char |
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 |
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 |
isVacuous | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
isVacuousWith | |
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 |
Join | Data.SBV.Internals |
july | Documentation.SBV.Examples.Puzzles.Birthday |
june | 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 |
Key | |
1 (Type/Class) | Documentation.SBV.Examples.Crypto.AES |
2 (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 |
knownAnswerTests | Documentation.SBV.Examples.Crypto.SHA |
KPlus | Data.SBV.RegExp, Data.SBV.Internals |
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 |
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 |
LenC | |
1 (Type/Class) | Documentation.SBV.Examples.WeakestPreconditions.Length |
2 (Data Constructor) | Documentation.SBV.Examples.WeakestPreconditions.Length |
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.U2Bridge |
location | Documentation.SBV.Examples.Puzzles.Murder |
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.ProofTools.Fibonacci |
2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib |
magic | Documentation.SBV.Examples.Puzzles.MagicSquare |
maj | Documentation.SBV.Examples.Crypto.SHA |
Male | Documentation.SBV.Examples.Puzzles.Murder |
map | Data.SBV.Maybe |
mapCV | Data.SBV.Internals |
mapCV2 | Data.SBV.Internals |
maskAndMult | Documentation.SBV.Examples.BitPrecise.MultMask |
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 |
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 |
mergeSFunArr | 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.Trans, Data.SBV |
MetricSpace | Data.SBV.Trans, 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 |
mkCoin | Documentation.SBV.Examples.Puzzles.Coins |
mkConstCV | Data.SBV.Internals |
mkExistVars | |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
2 (Function) | Data.SBV |
mkFibs | Documentation.SBV.Examples.Lists.Fibonacci |
mkForallVars | |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
2 (Function) | Data.SBV |
mkFreeVars | |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
2 (Function) | Data.SBV |
mkQuery | Documentation.SBV.Examples.Transformers.SymbolicEval |
mkResult | Documentation.SBV.Examples.Transformers.SymbolicEval |
mkSkolemZero | Data.SBV.Internals |
mkSMTResult | |
1 (Function) | Data.SBV.Trans.Control |
2 (Function) | Data.SBV.Control |
mkSTree | Data.SBV.Tools.STree |
mkSymbolicEnumeration | Data.SBV.Trans, Data.SBV |
mkSymSBV | Data.SBV.Internals |
mkSymVal | |
1 (Function) | Data.SBV.Internals, Data.SBV.Trans |
2 (Function) | Data.SBV |
mkUninterpretedSort | Data.SBV.Trans, Data.SBV |
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 |
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 |
MProvable | Data.SBV.Trans |
msb | Data.SBV.Trans, Data.SBV |
msMaximize | Data.SBV.Trans, Data.SBV |
msMinimize | Data.SBV.Trans, Data.SBV |
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 |
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 |
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 |
newSFunArr | Data.SBV.Dynamic |
newUninterpreted | Data.SBV.Internals |
next | Documentation.SBV.Examples.Puzzles.HexPuzzle |
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 |
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 | 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 |
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 |
offsetIndexOf | |
1 (Function) | Data.SBV.String |
2 (Function) | Data.SBV.List |
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 |
ord | Data.SBV.Char |
OrdSymbolic | Data.SBV.Trans, Data.SBV |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
Provable | Data.SBV.Trans, Data.SBV |
prove | |
1 (Function) | Data.SBV.Trans |
2 (Function) | Data.SBV |
proveConcurrentWithAll | |
1 (Function) | Data.SBV.Trans, Data.SBV |
2 (Function) | Data.SBV.Dynamic |
proveConcurrentWithAny | |
1 (Function) | Data.SBV.Trans, 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 |
proveSFunArray | 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.Trans, Data.SBV |
2 (Function) | Data.SBV.Dynamic |
proveWithAny | |
1 (Function) | Data.SBV.Trans, Data.SBV |
2 (Function) | Data.SBV.Dynamic |
ps | Documentation.SBV.Examples.BitPrecise.PrefixSum |
PseudoBoolean | Data.SBV.Internals |
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.Birthday |
2 (Function) | Documentation.SBV.Examples.Puzzles.Coins |
3 (Function) | Documentation.SBV.Examples.Puzzles.Counts |
4 (Function) | Documentation.SBV.Examples.Puzzles.DogCatMouse |
5 (Function) | Documentation.SBV.Examples.Puzzles.Garden |
6 (Function) | Documentation.SBV.Examples.Puzzles.Murder |
7 (Function) | Documentation.SBV.Examples.Queries.FourFours |
puzzle0 | Documentation.SBV.Examples.Puzzles.Sudoku |
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 |
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 |
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 |
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 |
Quot | Data.SBV.Internals |
r | Documentation.SBV.Examples.WeakestPreconditions.IntDiv |
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 |
RationalCV | Data.SBV |
RatIrreducible | Data.SBV |
RC4 | Documentation.SBV.Examples.Crypto.RC4 |
rc4IsCorrect | Documentation.SBV.Examples.Crypto.RC4 |
RCSet | Data.SBV.Internals, Data.SBV |
readArray | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
readBin | Data.SBV.Internals |
readSArr | Data.SBV.Dynamic |
readSFunArr | 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 |
RegA | Documentation.SBV.Examples.BitPrecise.Legato |
RegExp | Data.SBV.RegExp, Data.SBV.Internals |
RegExpMatchable | Data.SBV.RegExp |
Register | Documentation.SBV.Examples.BitPrecise.Legato |
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 |
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 |
resAxioms | Data.SBV.Internals |
resConstraints | Data.SBV.Internals |
resConsts | Data.SBV.Internals |
resetAssertions | |
1 (Function) | Data.SBV.Trans.Control |
2 (Function) | Data.SBV.Control |
resInputs | Data.SBV.Internals |
reskinds | Data.SBV.Internals |
resObservables | Data.SBV.Internals |
resOutputs | 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 |
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 |
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 | Documentation.SBV.Examples.Puzzles.U2Bridge |
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 | Documentation.SBV.Examples.Misc.Enumerate |
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 |
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 |
satCmd | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
satConcurrentWithAll | |
1 (Function) | Data.SBV.Trans, Data.SBV |
2 (Function) | Data.SBV.Dynamic |
satConcurrentWithAny | |
1 (Function) | Data.SBV.Trans, Data.SBV |
2 (Function) | Data.SBV.Dynamic |
SatExtField | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
Satisfiable | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
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 |
satTrackUFs | Data.SBV.Internals, 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.Trans, Data.SBV |
2 (Function) | Data.SBV.Dynamic |
satWithAny | |
1 (Function) | Data.SBV.Trans, Data.SBV |
2 (Function) | Data.SBV.Dynamic |
SaveTiming | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
SB | Documentation.SBV.Examples.Uninterpreted.Deduce |
sB | Documentation.SBV.Examples.Misc.Enumerate |
sBar | Documentation.SBV.Examples.Puzzles.Murder |
sBarrelRotateLeft | Data.SBV.Trans, Data.SBV |
sBarrelRotateRight | Data.SBV.Trans, Data.SBV |
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.AES |
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 |
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 |
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 |
sbvUninterpret | Data.SBV.Trans, Data.SBV |
sBystander | Documentation.SBV.Examples.Puzzles.Murder |
sC | Documentation.SBV.Examples.Misc.Enumerate |
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 |
sDane | Documentation.SBV.Examples.Puzzles.Fish |
SDay | |
1 (Type/Class) | Documentation.SBV.Examples.Optimization.Enumerate |
2 (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 |
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 | Documentation.SBV.Examples.Misc.Enumerate |
search | Documentation.SBV.Examples.Puzzles.HexPuzzle |
second | Data.SBV.Either |
secondQuery | Documentation.SBV.Examples.Queries.Concurrency |
sEdge | Documentation.SBV.Examples.Puzzles.U2Bridge |
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.Trans, 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 |
SeqIndexOf | Data.SBV.Internals |
SeqLen | 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 |
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 |
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 |
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 |
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 |
SFunArr | Data.SBV.Dynamic |
SFunArray | |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
2 (Data Constructor) | Data.SBV.Internals |
sgcd | Documentation.SBV.Examples.CodeGeneration.GCD |
sgcdIsCorrect | Documentation.SBV.Examples.CodeGeneration.GCD |
sGerman | Documentation.SBV.Examples.Puzzles.Fish |
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 |
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 |
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 |
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 |
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.Trans, 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 |
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 |
sJust | Data.SBV.Maybe |
sKiller | Documentation.SBV.Examples.Puzzles.Murder |
Skip | Data.SBV.Tools.WeakestPreconditions |
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.U2Bridge |
sMale | Documentation.SBV.Examples.Puzzles.Murder |
smax | Data.SBV.Trans, Data.SBV |
SMaybe | Data.SBV.Internals, Data.SBV |
sMaybe | Data.SBV |
sMaybes | Data.SBV |
sMaybe_ | Data.SBV |
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 |
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 |
SMTErrorBehavior | Data.SBV.Trans.Control, Data.SBV.Control |
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 |
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.Trans, Data.SBV |
sNothing | Data.SBV.Maybe |
sObserve | Data.SBV |
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 |
solveAll | Documentation.SBV.Examples.Puzzles.Sudoku |
solveCrossword | Documentation.SBV.Examples.Strings.RegexCrossword |
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 |
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 |
sQuot | Data.SBV.Trans, Data.SBV |
sQuotRem | Data.SBV.Trans, 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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
supportsUnboundedInts | Data.SBV.Internals |
supportsUninterpretedSorts | Data.SBV.Internals |
SV | |
1 (Type/Class) | Data.SBV.Internals |
2 (Data Constructor) | Data.SBV.Internals |
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 |
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 |
svStructuralLessThan | Data.SBV.Dynamic |
svSymbolicMerge | Data.SBV.Dynamic |
svTestBit | Data.SBV.Dynamic |
svTimes | Data.SBV.Dynamic |
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 |
swap | 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 |
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 |
targetName | Data.SBV.Internals |
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 |
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.Trans, Data.SBV |
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 |
translate | Data.SBV.Internals |
trueCV | Data.SBV.Internals |
trueSV | Data.SBV.Internals |
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 | 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 |
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 | |
1 (Data Constructor) | Data.SBV.Internals |
2 (Type/Class) | Data.SBV.Trans, Data.SBV |
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 |
unSFunArray | 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 |
valid | |
1 (Function) | Documentation.SBV.Examples.Puzzles.Birthday |
2 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku |
validate | Data.SBV.Trans |
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 | Documentation.SBV.Examples.BitPrecise.Legato |
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 |
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 |
writeArray | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
writeSArr | Data.SBV.Dynamic |
writeSFunArr | 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.WeakestPreconditions.Basics |
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD |
5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv |
6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt |
xferFlash | Documentation.SBV.Examples.Puzzles.U2Bridge |
xferPerson | Documentation.SBV.Examples.Puzzles.U2Bridge |
XOr | Data.SBV.Internals |
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.WeakestPreconditions.Basics |
4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD |
5 (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 |
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.Trans, Data.SBV |
zipPL | Documentation.SBV.Examples.BitPrecise.PrefixSum |
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 |