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

Index

# | Data.SBV
% | Data.SBV
&&& | 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
.++ |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
./= | Data.SBV
.: |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
.< | Data.SBV
.<= | Data.SBV
.== | Data.SBV
.> | Data.SBV
.>= | Data.SBV
.^ | Data.SBV
.|. | Data.SBV
/! | Data.SBV.Tools.Overflow
<+> | Data.SBV
<=> | Data.SBV
=== | Data.SBV
==> | Data.SBV
A | Documentation.SBV.Examples.Misc.Enumerate
ABC | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
abc | Data.SBV, Data.SBV.Dynamic
Abs | Data.SBV.Internals
Actions | Documentation.SBV.Examples.Puzzles.U2Bridge
Adam | Documentation.SBV.Examples.Puzzles.U2Bridge
adam | Documentation.SBV.Examples.Puzzles.U2Bridge
adc | Documentation.SBV.Examples.BitPrecise.Legato
addAxiom | Data.SBV.Internals, Data.SBV
AddExtCW | Data.SBV.Internals, 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
aes128LibComponents | 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
aesRound | Documentation.SBV.Examples.Crypto.AES
AlgPolyRoot | Data.SBV.Internals
AlgRational | Data.SBV.Internals
AlgReal | Data.SBV.Internals, Data.SBV
AlgRealPoly | Data.SBV.Internals
ALL | Data.SBV.Internals, Data.SBV.Dynamic
All | Data.SBV.RegExp, Data.SBV.Internals
allEqual | Data.SBV
allModels | Documentation.SBV.Examples.Misc.Auxiliary
allocate | Documentation.SBV.Examples.Optimization.VM
allPossibleTrees | Documentation.SBV.Examples.Queries.FourFours
allPuzzles | Documentation.SBV.Examples.Puzzles.Sudoku
allSat | Data.SBV
allSatMaxModelCount | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
AllSatResult |
1 (Type/Class) | Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV, Data.SBV.Dynamic
allSatWith |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
AllStatistics | Data.SBV.Control
And | Data.SBV.Internals
and | Documentation.SBV.Examples.Uninterpreted.Deduce
approxRational | Data.SBV
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
AssertionStackLevels | Data.SBV.Control
AssertWithPenalty | Data.SBV.Internals, Data.SBV
assertWithPenalty | Data.SBV
assocPlus | Documentation.SBV.Examples.Misc.Floating
assocPlusRegular | Documentation.SBV.Examples.Misc.Floating
AUFLIA | Data.SBV
AUFLIRA | Data.SBV
AUFNIRA | Data.SBV
august | Documentation.SBV.Examples.Puzzles.Birthday
Authors | Data.SBV.Control
ax1 | Documentation.SBV.Examples.Uninterpreted.Deduce
ax2 | Documentation.SBV.Examples.Uninterpreted.Deduce
ax3 | Documentation.SBV.Examples.Uninterpreted.Deduce
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
4 (Data Constructor) | Documentation.SBV.Examples.Uninterpreted.Deduce
bAll | Data.SBV
ball | Data.SBV.List.Bounded
bAnd | Data.SBV
band | Data.SBV.List.Bounded
bAny | Data.SBV
bany | Data.SBV.List.Bounded
Baseball | Documentation.SBV.Examples.Puzzles.Fish
basis | Documentation.SBV.Examples.Existentials.Diophantine
bcc | Documentation.SBV.Examples.BitPrecise.Legato
Beer | Documentation.SBV.Examples.Puzzles.Fish
belem | Data.SBV.List.Bounded
Beverage | Documentation.SBV.Examples.Puzzles.Fish
bfilter | Data.SBV.List.Bounded
bfix | Data.SBV.Tools.BoundedFix
bfoldl | Data.SBV.List.Bounded
bfoldlM | Data.SBV.List.Bounded
bfoldr | Data.SBV.List.Bounded
bfoldrM | Data.SBV.List.Bounded
bin | Data.SBV.Internals
Binary | Documentation.SBV.Examples.Uninterpreted.Shannon
BinOp | Documentation.SBV.Examples.Queries.FourFours
binS | Data.SBV.Internals
Bird | Documentation.SBV.Examples.Puzzles.Fish
Bit | Documentation.SBV.Examples.BitPrecise.Legato
bit | Data.SBV
bitDefault | Data.SBV
Bits | Data.SBV
bitSize | Data.SBV
bitSizeMaybe | Data.SBV
Black | Documentation.SBV.Examples.Puzzles.HexPuzzle
blastBE | Data.SBV
blastLE | Data.SBV
blastSDouble | Data.SBV
blastSFloat | Data.SBV
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.List.Bounded
bmapM | Data.SBV.List.Bounded
bmaximum | Data.SBV.List.Bounded
bminimum | Data.SBV.List.Bounded
bne | Documentation.SBV.Examples.BitPrecise.Legato
bnot | Data.SBV
Board |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.MagicSquare
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.Sudoku
Bono | Documentation.SBV.Examples.Puzzles.U2Bridge
bono | Documentation.SBV.Examples.Puzzles.U2Bridge
Boolean | Data.SBV
Boolector | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
boolector | Data.SBV, Data.SBV.Dynamic
bOr | Data.SBV
bor | Data.SBV.List.Bounded
Boundary | Data.SBV.Tools.Range
BoundedCW | Data.SBV.Internals, Data.SBV
bprod | Data.SBV.List.Bounded
breverse | Data.SBV.List.Bounded
Briton | Documentation.SBV.Examples.Puzzles.Fish
bsort | Data.SBV.List.Bounded
bsum | Data.SBV.List.Bounded
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
bvMulO | Data.SBV.Tools.Overflow
bvMulOFast | Data.SBV.Tools.Overflow
bvNegO | Data.SBV.Tools.Overflow
bvSubO | Data.SBV.Tools.Overflow
byteSwap16 | Data.SBV
byteSwap32 | Data.SBV
byteSwap64 | Data.SBV
bzipWith | Data.SBV.List.Bounded
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
capabilities | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
caseSplit | Data.SBV.Control
Cat | Documentation.SBV.Examples.Puzzles.Fish
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
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
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
CgVal | Data.SBV.Internals
check |
1 (Function) | Documentation.SBV.Examples.Puzzles.MagicSquare
2 (Function) | Documentation.SBV.Examples.Puzzles.Sudoku
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
checkSat | Data.SBV.Control
checkSatAssuming | Data.SBV.Control
checkSatAssumingWithUnsatisfiableSet | Data.SBV.Control
CheckSatResult | Data.SBV.Control
checkSatUsing | Data.SBV.Control
cheryl | Documentation.SBV.Examples.Puzzles.Birthday
chex | Data.SBV.Internals
chr | Data.SBV.Char
chunk | Documentation.SBV.Examples.Puzzles.MagicSquare
classify | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
clc | Documentation.SBV.Examples.BitPrecise.Legato
clearBit | Data.SBV
Closed | Data.SBV.Tools.Range
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 | Data.SBV
complementBit | 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
Cons | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
Const | Documentation.SBV.Examples.Strings.SQLInjection
constrain | Data.SBV.Internals, Data.SBV
constrainWithAttribute | Data.SBV.Internals, Data.SBV
correctness | Documentation.SBV.Examples.BitPrecise.MergeSort
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
countLeadingZeros | Data.SBV
counts | Documentation.SBV.Examples.Puzzles.Counts
countTrailingZeros | Data.SBV
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
Critical | Documentation.SBV.Examples.Lists.BoundedMutex
critical | Documentation.SBV.Examples.Lists.BoundedMutex
crossTime | Documentation.SBV.Examples.Puzzles.U2Bridge
csDemo1 | Documentation.SBV.Examples.Queries.CaseSplit
csDemo2 | Documentation.SBV.Examples.Queries.CaseSplit
CustomLogic | Data.SBV
CVC4 | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
cvc4 | Data.SBV, Data.SBV.Dynamic
cvtModel | Data.SBV
CW |
1 (Type/Class) | Data.SBV.Internals, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Dynamic
CWAlgReal | Data.SBV.Internals, Data.SBV.Dynamic
CWChar | Data.SBV.Internals, Data.SBV.Dynamic
CWDouble | Data.SBV.Internals, Data.SBV.Dynamic
CWFloat | Data.SBV.Internals, Data.SBV.Dynamic
CWInteger | Data.SBV.Internals, Data.SBV.Dynamic
CWList | Data.SBV.Internals, Data.SBV.Dynamic
cwSameType | Data.SBV.Internals
CWString | Data.SBV.Internals, Data.SBV.Dynamic
cwToBool | Data.SBV.Internals, Data.SBV.Dynamic
cwToSMTLib | Data.SBV.Internals
CWUserSort | Data.SBV.Internals, Data.SBV.Dynamic
CWVal | Data.SBV.Internals, Data.SBV.Dynamic
cwVal | Data.SBV.Internals, Data.SBV.Dynamic
Dane | Documentation.SBV.Examples.Puzzles.Fish
Day |
1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Birthday
2 (Type/Class) | Documentation.SBV.Examples.Queries.Enums
decimal | Data.SBV.RegExp
decrypt | Documentation.SBV.Examples.Crypto.RC4
defaultCgConfig | Data.SBV.Internals
DefaultPenalty | Data.SBV.Internals, Data.SBV
defaultSMTCfg | Data.SBV, Data.SBV.Dynamic
defaultSolverConfig | Data.SBV, Data.SBV.Dynamic
demo | Documentation.SBV.Examples.Queries.AllSat
denominator | Data.SBV
derivative | Documentation.SBV.Examples.Uninterpreted.Shannon
dex | Documentation.SBV.Examples.BitPrecise.Legato
diag | Documentation.SBV.Examples.Puzzles.MagicSquare
DiagnosticOutputChannel | Data.SBV.Control
diffCount | Documentation.SBV.Examples.Existentials.CRCPolynomial
digit | Data.SBV.RegExp
digitToInt | Data.SBV.Char
displayModels | Data.SBV
dispSolution | Documentation.SBV.Examples.Puzzles.Sudoku
distinct | Data.SBV
Divide | Documentation.SBV.Examples.Queries.FourFours
Dog | Documentation.SBV.Examples.Puzzles.Fish
doRounds | Documentation.SBV.Examples.Crypto.AES
drop |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
dropRe | Documentation.SBV.Examples.Strings.SQLInjection
E |
1 (Type/Class) | Documentation.SBV.Examples.BitPrecise.MergeSort
2 (Type/Class) | Documentation.SBV.Examples.Misc.Enumerate
echo | Data.SBV.Control
Edge | Documentation.SBV.Examples.Puzzles.U2Bridge
edge | Documentation.SBV.Examples.Puzzles.U2Bridge
Elem | Documentation.SBV.Examples.Puzzles.MagicSquare
elem | Data.SBV.Char
elemAt | Data.SBV.List
elts | Documentation.SBV.Examples.Misc.Enumerate
encrypt | Documentation.SBV.Examples.Crypto.RC4
end | Documentation.SBV.Examples.BitPrecise.Legato
engine | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
Epsilon | Data.SBV.Internals, Data.SBV
eqSArr | Data.SBV.Dynamic
EqSymbolic | Data.SBV
Equal | Data.SBV.Internals
Equality | Data.SBV
ErrorBehavior | Data.SBV.Control
ErrorContinuedExecution | Data.SBV.Control
ErrorImmediateExit | Data.SBV.Control
euler185 | Documentation.SBV.Examples.Puzzles.Euler185
eval |
1 (Function) | Documentation.SBV.Examples.Queries.FourFours
2 (Function) | Documentation.SBV.Examples.Strings.SQLInjection
EX | Data.SBV.Internals, Data.SBV.Dynamic
exactly | Data.SBV.RegExp
example |
1 (Function) | Documentation.SBV.Examples.Misc.SoftConstrain
2 (Function) | Documentation.SBV.Examples.Puzzles.HexPuzzle
3 (Function) | Documentation.SBV.Examples.Queries.Interpolants
exampleProgram | Documentation.SBV.Examples.Strings.SQLInjection
executable | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
existential | Documentation.SBV.Examples.Uninterpreted.Shannon
exists | Data.SBV.Internals, Data.SBV
existsDay | Documentation.SBV.Examples.Puzzles.Birthday
existsMonth | Documentation.SBV.Examples.Puzzles.Birthday
existsOK | Documentation.SBV.Examples.Uninterpreted.Shannon
exists_ | Data.SBV.Internals, Data.SBV
exit | Data.SBV.Control
exploitRe | Documentation.SBV.Examples.Strings.SQLInjection
Expt | Documentation.SBV.Examples.Queries.FourFours
ExtCW | Data.SBV.Internals, Data.SBV
extend | Data.SBV
ExtendedCW | Data.SBV.Internals, Data.SBV
extendPathCondition | Data.SBV.Internals
Extract |
1 (Data Constructor) | Data.SBV.Internals
2 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato
extractModel | Data.SBV
extractModels | Data.SBV
extractSymbolicSimulationState | Data.SBV.Internals
F | Documentation.SBV.Examples.Queries.FourFours
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
false | Data.SBV
falseCW | Data.SBV.Internals
falseSW | Data.SBV.Internals
fastMaxCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
fastMinCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
fastPopCountIsCorrect | Documentation.SBV.Examples.CodeGeneration.PopulationCount
fib0 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
fib1 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
fib2 | Documentation.SBV.Examples.CodeGeneration.Fibonacci
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
finiteBitSize | Data.SBV
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
Flower | Documentation.SBV.Examples.Puzzles.Garden
flowerCount | Documentation.SBV.Examples.Puzzles.Garden
Football | Documentation.SBV.Examples.Puzzles.Fish
forAll | Data.SBV
forall | Data.SBV.Internals, Data.SBV
forallDay | Documentation.SBV.Examples.Puzzles.Birthday
forallMonth | Documentation.SBV.Examples.Puzzles.Birthday
forAll_ | Data.SBV
forall_ | Data.SBV.Internals, Data.SBV
forceSWArg | Data.SBV.Internals
forSome | Data.SBV
forSome_ | Data.SBV
Forte | Data.SBV.Tools.GenTest
four | Documentation.SBV.Examples.Misc.Enumerate
fp2fp | Data.SBV.Internals
fpAbs | Data.SBV
fpAdd | Data.SBV
fpCompareObjectH | Data.SBV.Internals
fpDiv | Data.SBV
fpFMA | Data.SBV
fpIsEqualObject | Data.SBV
fpIsEqualObjectH | Data.SBV.Internals
fpIsInfinite | Data.SBV
fpIsNaN | Data.SBV
fpIsNegative | Data.SBV
fpIsNegativeZero | Data.SBV
fpIsNormal | Data.SBV
fpIsNormalizedH | Data.SBV.Internals
fpIsPoint | Data.SBV
fpIsPositive | Data.SBV
fpIsPositiveZero | Data.SBV
fpIsSubnormal | Data.SBV
fpIsZero | Data.SBV
fpMax | Data.SBV
fpMaxH | Data.SBV.Internals
fpMin | Data.SBV
fpMinH | Data.SBV.Internals
fpMul | Data.SBV
fpNeg | Data.SBV
FPOp | Data.SBV.Internals
fpRatio0 | Data.SBV.Internals
fpRem | Data.SBV
fpRemH | Data.SBV.Internals
fpRound0 | Data.SBV.Internals
fpRoundToIntegral | Data.SBV
fpRoundToIntegralH | Data.SBV.Internals
fpSqrt | Data.SBV
fpSub | Data.SBV
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 | Data.SBV.Internals, Data.SBV
free_ | Data.SBV.Internals, Data.SBV
freshArray | Data.SBV.Control
freshArray_ | Data.SBV.Control
freshVar | Data.SBV.Control
freshVar_ | Data.SBV.Control
Friday | Documentation.SBV.Examples.Queries.Enums
fromBitsBE | Data.SBV
fromBitsLE | Data.SBV
fromBool | Data.SBV
fromBytes | Documentation.SBV.Examples.Crypto.AES
fromCW | Data.SBV.Internals, Data.SBV
fromSDouble | Data.SBV
fromSFloat | Data.SBV
fullAdder | Data.SBV
fullMultiplier | Data.SBV
genAddSub | Documentation.SBV.Examples.CodeGeneration.AddSub
genCCode | Documentation.SBV.Examples.CodeGeneration.Uninterpreted
GeneralizedCW | Data.SBV.Internals, Data.SBV
generate | Documentation.SBV.Examples.Queries.FourFours
generateSMTBenchmark |
1 (Function) | 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
genFromCW | 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 | Data.SBV.Control
getAssertionStackDepth | Data.SBV.Control
getAssignment | Data.SBV.Control
getFlag | Documentation.SBV.Examples.BitPrecise.Legato
getInfo | Data.SBV.Control
getInterpolant | Data.SBV.Control
getModel | Data.SBV.Control
getModelAssignment |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
getModelDictionaries | Data.SBV
getModelDictionary |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
getModelObjectives | Data.SBV
getModelObjectiveValue | Data.SBV
getModelUninterpretedValue | Data.SBV
getModelUninterpretedValues | Data.SBV
getModelValue | Data.SBV
getModelValues | Data.SBV
getOption | Data.SBV.Control
getPathCondition | Data.SBV.Internals
getProof | Data.SBV.Control
getReg | Documentation.SBV.Examples.BitPrecise.Legato
getSMTResult | Data.SBV.Control
getTableIndex | Data.SBV.Internals
getTestValues | Data.SBV.Tools.GenTest
getUninterpretedValue | Data.SBV.Control
getUnknownReason | Data.SBV.Control
getUnsatCore | Data.SBV.Control
getValue | 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
goodSum | Documentation.SBV.Examples.Queries.AllSat
GreaterEq | Data.SBV.Internals
GreaterThan | Data.SBV.Internals
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
Haskell | Data.SBV.Tools.GenTest
HasKind | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
hasSign | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
head |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
Here | Documentation.SBV.Examples.Puzzles.U2Bridge
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
hexS | Data.SBV.Internals
Hockey | Documentation.SBV.Examples.Puzzles.Fish
Homogeneous | Documentation.SBV.Examples.Existentials.Diophantine
Horse | Documentation.SBV.Examples.Puzzles.Fish
identifier | Data.SBV.RegExp
Idle | Documentation.SBV.Examples.Lists.BoundedMutex
idle | Documentation.SBV.Examples.Lists.BoundedMutex
IEEEFloatConvertable | Data.SBV
IEEEFloating | Data.SBV
IEEEFP | Data.SBV.Internals
ignoreExitCode | Data.SBV.Control, Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
implode |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
Independent | Data.SBV.Internals, Data.SBV
IndependentResult | Data.SBV, Data.SBV.Dynamic
indexOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
Infinite | Data.SBV.Internals, Data.SBV
infinity | Data.SBV.Internals, Data.SBV
InfoKeyword | Data.SBV.Control
init |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
initCgState | Data.SBV.Internals
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 | Data.SBV.Control
inRange | Data.SBV
inSMTMode | Data.SBV.Internals
Instruction | Documentation.SBV.Examples.BitPrecise.Legato
Int | Data.SBV
Int16 | Data.SBV
Int32 | Data.SBV
Int64 | Data.SBV
Int8 | Data.SBV
Inter | Data.SBV.RegExp, Data.SBV.Internals
internalConstraint | Data.SBV.Internals
internalVariable | Data.SBV.Internals
Interval | Data.SBV.Internals, Data.SBV
intSizeOf | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
intToDigit | Data.SBV.Char
invMixColumns | Documentation.SBV.Examples.Crypto.AES
io | Data.SBV.Control
IRun | Data.SBV.Internals
ISafe | Data.SBV.Internals
isAlpha | Data.SBV.Char
isAlphaNum | Data.SBV.Char
isAscii | Data.SBV.Char
isAsciiLetter | Data.SBV.Char
isAsciiLower | Data.SBV.Char
isAsciiUpper | Data.SBV.Char
isBoolean | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isBounded | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isCgDriver | Data.SBV.Internals
isCgMakefile | Data.SBV.Internals
isChar | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isCodeGenMode | Data.SBV.Internals
isConcrete | Data.SBV.Internals, Data.SBV
isConcretely | Data.SBV.Internals, Data.SBV
isControl | Data.SBV.Char
isDigit | Data.SBV.Char
isDouble | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
ISetup | Data.SBV.Internals
isFloat | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isHexDigit | Data.SBV.Char
isInfixOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
isInteger | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isLatin1 | Data.SBV.Char
isLetter | Data.SBV.Char
isList | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isLower | Data.SBV.Char
isMagic | Documentation.SBV.Examples.Puzzles.MagicSquare
isMark | Data.SBV.Char
isNonModelVar | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isNumber | Data.SBV.Char
isOctDigit | Data.SBV.Char
isPermutationOf | Documentation.SBV.Examples.BitPrecise.MergeSort
isPrefixOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
isPrint | Data.SBV.Char
isPunctuation | Data.SBV.Char
isReal | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isRegularCW | Data.SBV.Internals
isSafe | Data.SBV
isSatisfiable | Data.SBV
isSatisfiableWith | Data.SBV
isSeparator | Data.SBV.Char
isSigned | Data.SBV
isSpace | Data.SBV.Char
isString | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isSuffixOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
isSymbol | Data.SBV.Char
isSymbolic | Data.SBV.Internals, Data.SBV
IStage | Data.SBV.Internals
isTheorem | Data.SBV
isTheoremWith | Data.SBV
isUninterpreted | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
isUpper | Data.SBV.Char
isVacuous | Data.SBV
isVacuousWith | Data.SBV
isValid |
1 (Function) | Documentation.SBV.Examples.Puzzles.NQueens
2 (Function) | Documentation.SBV.Examples.Puzzles.U2Bridge
Ite | Data.SBV.Internals
ite | Data.SBV
iteLazy | Data.SBV
ites | Data.SBV.Tools.Polynomial
Join | Data.SBV.Internals
july | Documentation.SBV.Examples.Puzzles.Birthday
june | Documentation.SBV.Examples.Puzzles.Birthday
KBool | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KBounded | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KChar | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KDouble | Data.SBV.Internals, 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, Data.SBV.Dynamic
Kind | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KindCast | Data.SBV.Internals
kindOf | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KList | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KPlus | Data.SBV.RegExp, Data.SBV.Internals
KReal | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KS | Documentation.SBV.Examples.Crypto.AES
KStar | Data.SBV.RegExp, Data.SBV.Internals
KString | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KUnbounded | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
KUserSort | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
L | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
Label | Data.SBV.Internals
label | Data.SBV
lAdam | Documentation.SBV.Examples.Puzzles.U2Bridge
ladyAndTigers | Documentation.SBV.Examples.Puzzles.LadyAndTigers
Larry | Documentation.SBV.Examples.Puzzles.U2Bridge
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
length |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
LessEq | Data.SBV.Internals
LessThan | Data.SBV.Internals
Lexicographic | Data.SBV.Internals, Data.SBV
LexicographicResult | Data.SBV, Data.SBV.Dynamic
lf | Documentation.SBV.Examples.BitPrecise.PrefixSum
liftCW2 | Data.SBV.Internals
liftDMod | Data.SBV.Internals
liftQRem | Data.SBV.Internals
listToListAt | Data.SBV.List
Literal | Data.SBV.RegExp, Data.SBV.Internals
literal | Data.SBV.Internals, 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.U2Bridge
Logic | Data.SBV
Logic_ALL | Data.SBV
Logic_NONE | Data.SBV
Loop | Data.SBV.RegExp, Data.SBV.Internals
LRA | Data.SBV
lsb | Data.SBV
M | Documentation.SBV.Examples.Strings.SQLInjection
magic | Documentation.SBV.Examples.Puzzles.MagicSquare
mapCW | Data.SBV.Internals
mapCW2 | Data.SBV.Internals
maskAndMult | Documentation.SBV.Examples.BitPrecise.MultMask
match | Data.SBV.RegExp
MathSAT | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
mathSAT | Data.SBV, Data.SBV.Dynamic
maxE | Documentation.SBV.Examples.Misc.Enumerate
Maximize | Data.SBV.Internals, Data.SBV
maximize | Data.SBV
may | Documentation.SBV.Examples.Puzzles.Birthday
mdp | Data.SBV.Tools.Polynomial
Memory | Documentation.SBV.Examples.BitPrecise.Legato
memory | Documentation.SBV.Examples.BitPrecise.Legato
merge | Documentation.SBV.Examples.BitPrecise.MergeSort
Mergeable | Data.SBV
mergeArrays | Data.SBV.Internals
mergeSArr | Data.SBV.Dynamic
mergeSFunArr | Data.SBV.Dynamic
mergeSort | Documentation.SBV.Examples.BitPrecise.MergeSort
Metric | 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
minimize | Data.SBV
Minus |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
mkCoin | Documentation.SBV.Examples.Puzzles.Coins
mkConstCW | Data.SBV.Internals
mkExistVars | Data.SBV.Internals, Data.SBV
mkFibs | Documentation.SBV.Examples.Lists.Fibonacci
mkForallVars | Data.SBV.Internals, Data.SBV
mkFreeVars | Data.SBV.Internals, Data.SBV
mkSkolemZero | Data.SBV.Internals
mkSMTResult | Data.SBV.Control
mkSTree | Data.SBV.Tools.STree
mkSymbolicEnumeration | Data.SBV
mkSymSBV | Data.SBV.Internals
mkSymWord | Data.SBV.Internals, Data.SBV
Modelable | Data.SBV
modelAssocs | Data.SBV.Internals
modelExists | Data.SBV
modelObjectives | Data.SBV.Internals
modelsWithYAux | Documentation.SBV.Examples.Misc.Auxiliary
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
msb | Data.SBV
MulExtCW | Data.SBV.Internals, 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
Name | Data.SBV.Control
name | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
namedConstraint | Data.SBV.Internals, Data.SBV
NamedSymVar | Data.SBV.Internals
nameRe | Documentation.SBV.Examples.Strings.SQLInjection
nan | Data.SBV.Internals, 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
nestedExample | Documentation.SBV.Examples.Lists.Nested
newArray | Data.SBV.Internals, Data.SBV
newArrayInState | Data.SBV.Internals
newArray_ | Data.SBV.Internals, Data.SBV
newExpr | Data.SBV.Internals
newline | Data.SBV.RegExp
newSArr | Data.SBV.Dynamic
newSFunArr | Data.SBV.Dynamic
newUninterpreted | Data.SBV.Internals
next | Documentation.SBV.Examples.Puzzles.HexPuzzle
Nil | Documentation.SBV.Examples.Uninterpreted.UISortAllSat
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
nonZeroAddition | Documentation.SBV.Examples.Misc.Floating
normCW | Data.SBV.Internals
Norwegian | Documentation.SBV.Examples.Puzzles.Fish
Not | Data.SBV.Internals
not | Documentation.SBV.Examples.Uninterpreted.Deduce
notElem | Data.SBV.Char
NotEqual | Data.SBV.Internals
notFair | Documentation.SBV.Examples.Lists.BoundedMutex
NoTiming | Data.SBV.Internals, Data.SBV
noWiggle | Documentation.SBV.Examples.Uninterpreted.Shannon
nQueens | Documentation.SBV.Examples.Puzzles.NQueens
null |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
numerator | Data.SBV
Objective | Data.SBV.Internals, Data.SBV
observe | Data.SBV
octal | Data.SBV.RegExp
octDigit | Data.SBV.RegExp
offsetIndexOf |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
oneIf | Data.SBV
oneOf | Data.SBV.RegExp
Op | Data.SBV.Internals
Open | Data.SBV.Tools.Range
oppositeSignsCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
Opt | Data.SBV.RegExp, Data.SBV.Internals
optimize | Data.SBV
OptimizeResult | Data.SBV, Data.SBV.Dynamic
OptimizeStyle | Data.SBV.Internals, Data.SBV
optimizeWith | Data.SBV
OptionKeyword | Data.SBV.Control
options | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
Or | Data.SBV.Internals
or | Documentation.SBV.Examples.Uninterpreted.Deduce
ord | Data.SBV.Char
OrdSymbolic | Data.SBV
output | Data.SBV.Internals, 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
ParetoResult | Data.SBV, Data.SBV.Dynamic
parseCWs | Data.SBV
pbAtLeast | Data.SBV
pbAtMost | Data.SBV
pbEq | Data.SBV
pbExactly | Data.SBV
pbGe | Data.SBV
pbLe | Data.SBV
pbMutexed | Data.SBV
PBOp | Data.SBV.Internals
pbStronglyMutexed | 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
2 (Data Constructor) | Data.SBV.Internals, Data.SBV
Pet | Documentation.SBV.Examples.Puzzles.Fish
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
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 | Data.SBV.Control
pop8 | Documentation.SBV.Examples.CodeGeneration.PopulationCount
popCount | Data.SBV
popCountDefault | Data.SBV
popCountFast | Documentation.SBV.Examples.CodeGeneration.PopulationCount
popCountSlow | Documentation.SBV.Examples.CodeGeneration.PopulationCount
pos | Documentation.SBV.Examples.Uninterpreted.Shannon
PowerList | Documentation.SBV.Examples.BitPrecise.PrefixSum
powerOfTwoCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks
Predicate | Data.SBV
PrettyNum | Data.SBV.Internals
prga | Documentation.SBV.Examples.Crypto.RC4
printBase | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
printRealPrec | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
PrintTiming | Data.SBV.Internals, Data.SBV
problem |
1 (Function) | Documentation.SBV.Examples.Misc.Auxiliary
2 (Function) | Documentation.SBV.Examples.Optimization.ExtField
3 (Function) | Documentation.SBV.Examples.Optimization.LinearOpt
ProduceAssertions | Data.SBV.Control
ProduceAssignments | Data.SBV.Control
ProduceInterpolants | Data.SBV.Control
ProduceProofs | Data.SBV.Control
ProduceUnsatAssumptions | Data.SBV.Control
ProduceUnsatCores | Data.SBV.Control
production | Documentation.SBV.Examples.Optimization.Production
Program | Documentation.SBV.Examples.BitPrecise.Legato
ProofError | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
Provable | Data.SBV
prove | Data.SBV
proveSArray | Documentation.SBV.Examples.Uninterpreted.AUF
proveSFunArray | Documentation.SBV.Examples.Uninterpreted.AUF
proveWith |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
proveWithAll |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
proveWithAny |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
ps | Documentation.SBV.Examples.BitPrecise.PrefixSum
PseudoBoolean | Data.SBV.Internals
punctuation | Data.SBV.RegExp
push | 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.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.Uninterpreted.Sort
2 (Data Constructor) | Documentation.SBV.Examples.Uninterpreted.Sort
QF_ABV | Data.SBV
QF_AUFBV | Data.SBV
QF_AUFLIA | Data.SBV
QF_AX | Data.SBV
QF_BV | Data.SBV
QF_FD | Data.SBV
QF_FP | Data.SBV
QF_FPBV | Data.SBV
QF_IDL | Data.SBV
QF_LIA | Data.SBV
QF_LRA | Data.SBV
QF_NIA | Data.SBV
QF_NRA | Data.SBV
QF_RDL | Data.SBV
QF_S | Data.SBV
QF_UF | Data.SBV
QF_UFBV | Data.SBV
QF_UFIDL | Data.SBV
QF_UFLIA | Data.SBV
QF_UFLRA | Data.SBV
QF_UFNIRA | Data.SBV
QF_UFNRA | Data.SBV
Quantifier | Data.SBV.Internals, Data.SBV.Dynamic
queries | Documentation.SBV.Examples.BitPrecise.BitTricks
Query |
1 (Type/Class) | Data.SBV.Control, Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
3 (Data Constructor) | Documentation.SBV.Examples.Strings.SQLInjection
query | Data.SBV.Control
queryAsk | Data.SBV.Internals
queryAssertionStackDepth | Data.SBV.Internals
queryConfig | Data.SBV.Internals
queryDebug | Data.SBV.Control
queryRetrieveResponse | Data.SBV.Internals
querySend | Data.SBV.Internals
QueryState |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
queryTblArrPreserveIndex | Data.SBV.Internals
queryTerminate | Data.SBV.Internals
queryTimeOutValue | Data.SBV.Internals
Quot | Data.SBV.Internals
RandomSeed | 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
Ratio | Data.SBV
Rational | Data.SBV
RC4 | Documentation.SBV.Examples.Crypto.RC4
rc4IsCorrect | Documentation.SBV.Examples.Crypto.RC4
readArray | Data.SBV.Internals, 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
ready | Documentation.SBV.Examples.Lists.BoundedMutex
ReasonUnknown | 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, 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
RegularCW | 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.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 | Data.SBV.Control
resInputs | Data.SBV.Internals
reskinds | Data.SBV.Internals
resObservables | Data.SBV.Internals
resOutputs | Data.SBV.Internals
Resp_AllStatistics | Data.SBV.Control
Resp_AssertionStackLevels | Data.SBV.Control
Resp_Authors | Data.SBV.Control
Resp_Error | Data.SBV.Control
Resp_InfoKeyword | Data.SBV.Control
Resp_Name | Data.SBV.Control
Resp_ReasonUnknown | Data.SBV.Control
Resp_Unsupported | Data.SBV.Control
Resp_Version | 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
retrieveResponseFromSolver | Data.SBV.Internals
Rol | Data.SBV.Internals
Ror | Data.SBV.Internals
rorM | Documentation.SBV.Examples.BitPrecise.Legato
rorR | Documentation.SBV.Examples.BitPrecise.Legato
rotate | Data.SBV
rotateL | Data.SBV
rotateR | 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
roundingMode | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
RoundNearestTiesToAway | Data.SBV.Internals, Data.SBV
RoundNearestTiesToEven | Data.SBV.Internals, Data.SBV
RoundTowardNegative | Data.SBV.Internals, Data.SBV
RoundTowardPositive | Data.SBV.Internals, Data.SBV
RoundTowardZero | Data.SBV.Internals, 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
runLegato | Documentation.SBV.Examples.BitPrecise.Legato
runSMT | Data.SBV
runSMTWith | Data.SBV
runSymbolic | Data.SBV.Internals
S | Documentation.SBV.Examples.Crypto.RC4
safe | Data.SBV
SafeResult |
1 (Type/Class) | Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV, Data.SBV.Dynamic
safeWith |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
sailors | Documentation.SBV.Examples.Existentials.Diophantine
SArr | Data.SBV.Dynamic
SArray |
1 (Type/Class) | Data.SBV.Internals, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
sAssert | Data.SBV
Sat | Data.SBV.Control
sat | Data.SBV
satCmd | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SatExtField | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
Satisfiable | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SatModel | Data.SBV
SatResult |
1 (Type/Class) | Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV, Data.SBV.Dynamic
Saturday | Documentation.SBV.Examples.Queries.Enums
satWith |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
satWithAll |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
satWithAny |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Dynamic
SaveTiming | Data.SBV.Internals, Data.SBV
SB | Documentation.SBV.Examples.Uninterpreted.Deduce
sbin | Data.SBV.Internals
sbinI | Data.SBV.Internals
SBinOp | Documentation.SBV.Examples.Queries.FourFours
SBool | Data.SBV.Internals, Data.SBV
sBool | Data.SBV
sBools | Data.SBV
sbox | Documentation.SBV.Examples.Crypto.AES
sboxInverseCorrect | Documentation.SBV.Examples.Crypto.AES
sboxTable | Documentation.SBV.Examples.Crypto.AES
SButton | Documentation.SBV.Examples.Puzzles.HexPuzzle
SBV |
1 (Type/Class) | Data.SBV.Internals, Data.SBV
2 (Data Constructor) | Data.SBV.Internals
SBVApp | Data.SBV.Internals
sbvAvailableSolvers | Data.SBV, Data.SBV.Dynamic
sbvCheckSolverInstallation | 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
2 (Data Constructor) | Data.SBV
sbvExceptionConfig | Data.SBV
sbvExceptionDescription | Data.SBV
sbvExceptionExitCode | Data.SBV
sbvExceptionExpected | Data.SBV
sbvExceptionHint | Data.SBV
sbvExceptionReason | Data.SBV
sbvExceptionReceived | Data.SBV
sbvExceptionSent | Data.SBV
sbvExceptionStdErr | Data.SBV
sbvExceptionStdOut | Data.SBV
SBVExpr | Data.SBV.Internals
SBVPgm |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
sbvQuickCheck | Data.SBV
SBVRunMode | Data.SBV.Internals
sbvToSW | Data.SBV.Internals
sbvToSymSW | Data.SBV.Internals
SBVType |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
sbvUninterpret | Data.SBV
sCase | Documentation.SBV.Examples.Queries.FourFours
SChar | Data.SBV.Internals, Data.SBV
sChar | Data.SBV
sChars | Data.SBV
SColor | Documentation.SBV.Examples.Puzzles.HexPuzzle
sCountLeadingZeros | Data.SBV
sCountTrailingZeros | Data.SBV
scriptBody | Data.SBV.Internals
scriptModel | Data.SBV.Internals
sCrossTime | Documentation.SBV.Examples.Puzzles.U2Bridge
SDay | Documentation.SBV.Examples.Queries.Enums
sDiv | Data.SBV
SDivisible | Data.SBV
sDivMod | Data.SBV
SDouble | Data.SBV.Internals, Data.SBV
sDouble | Data.SBV
sDoubleAsSWord64 | Data.SBV
sDoubles | Data.SBV
SE | Documentation.SBV.Examples.Misc.Enumerate
search | Documentation.SBV.Examples.Puzzles.HexPuzzle
select | Data.SBV
selectRe | Documentation.SBV.Examples.Strings.SQLInjection
sElem | Data.SBV
sendMoreMoney | Documentation.SBV.Examples.Puzzles.SendMoreMoney
sendRequestToSolver | Data.SBV.Internals
sendStringToSolver | Data.SBV.Internals
SeqConcat | Data.SBV.Internals
SeqContains | Data.SBV.Internals
SeqIndexOf | Data.SBV.Internals
SeqLen | 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
setBitTo | Data.SBV
setFlag | Documentation.SBV.Examples.BitPrecise.Legato
SetInfo | Data.SBV.Control
setInfo | Data.SBV.Internals, Data.SBV
SetLogic | Data.SBV.Control
setLogic | Data.SBV.Internals, Data.SBV
setOption | Data.SBV.Internals, Data.SBV
setReg | Documentation.SBV.Examples.BitPrecise.Legato
setTimeOut | Data.SBV.Internals, Data.SBV
SExecutable | Data.SBV
sexprToVal | Data.SBV.Control
sExtractBits | Data.SBV
SFiniteBits | Data.SBV
sFiniteBitSize | Data.SBV
SFloat | Data.SBV.Internals, Data.SBV
sFloat | Data.SBV
sFloatAsSWord32 | Data.SBV
sFloats | Data.SBV
sFromIntegral | 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
2 (Data Constructor) | Data.SBV.Internals
sgcd | Documentation.SBV.Examples.CodeGeneration.GCD
sgcdIsCorrect | Documentation.SBV.Examples.CodeGeneration.GCD
shannon | Documentation.SBV.Examples.Uninterpreted.Shannon
shannon2 | Documentation.SBV.Examples.Uninterpreted.Shannon
shex | Data.SBV.Internals
shexI | Data.SBV.Internals
shift | Data.SBV
shiftL | Data.SBV
shiftLeft | Documentation.SBV.Examples.CodeGeneration.Uninterpreted
shiftR | Data.SBV
Shl | Data.SBV.Internals
showCDouble | Data.SBV.Internals
showCFloat | Data.SBV.Internals
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, Data.SBV.Dynamic
Shr | Data.SBV.Internals
sInfinity | Data.SBV.Internals, Data.SBV
singleton |
1 (Function) | Data.SBV.String
2 (Function) | Data.SBV.List
SInt16 | Data.SBV.Internals, Data.SBV
sInt16 | Data.SBV
sInt16s | Data.SBV
SInt32 | Data.SBV.Internals, Data.SBV
sInt32 | Data.SBV
sInt32s | Data.SBV
SInt64 | Data.SBV.Internals, Data.SBV
sInt64 | Data.SBV
sInt64s | Data.SBV
SInt8 | Data.SBV.Internals, Data.SBV
sInt8 | Data.SBV
sInt8s | Data.SBV
SInteger | Data.SBV.Internals, Data.SBV
sInteger | Data.SBV
sIntegers | Data.SBV
SIntegral | Data.SBV
sIntN | Data.SBV.Dynamic
sIntN_ | Data.SBV.Dynamic
SList | Data.SBV.Internals, Data.SBV
sList | Data.SBV
sLists | Data.SBV
SLocation | Documentation.SBV.Examples.Puzzles.U2Bridge
smax | Data.SBV
smin | Data.SBV
sMod | Data.SBV
SMTConfig |
1 (Type/Class) | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SMTErrorBehavior | Data.SBV.Control
SMTInfoFlag | Data.SBV.Control
SMTInfoResponse | Data.SBV.Control
SMTLib2 | Data.SBV.Internals, 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, Data.SBV.Dynamic
smtLibVersion | Data.SBV.Internals, 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.Control
SMTProblem |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
SMTReasonUnknown | Data.SBV
SMTResult | Data.SBV.Internals, 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, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
SMTValue | Data.SBV.Control
SMTVerbosity | Data.SBV.Control
sName | Data.SBV
sName_ | Data.SBV
sNaN | Data.SBV.Internals, Data.SBV
softConstrain | Data.SBV.Internals, Data.SBV
Solution |
1 (Type/Class) | Documentation.SBV.Examples.Existentials.Diophantine
2 (Type/Class) | Documentation.SBV.Examples.Puzzles.NQueens
solve | 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, Data.SBV.Dynamic
solver | Data.SBV.Internals, 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, Data.SBV.Dynamic
solveU2 | Documentation.SBV.Examples.Puzzles.U2Bridge
split | Data.SBV
Splittable | Data.SBV
sPopCount | Data.SBV
Sport | Documentation.SBV.Examples.Puzzles.Fish
SQLExpr | Documentation.SBV.Examples.Strings.SQLInjection
Sqrt | Documentation.SBV.Examples.Queries.FourFours
sQuot | Data.SBV
sQuotRem | Data.SBV
SReal | Data.SBV.Internals, Data.SBV
sReal | Data.SBV
sReals | Data.SBV
sRealToSInteger | Data.SBV
sRem | Data.SBV
sRNA | Data.SBV.Internals, Data.SBV
sRNE | Data.SBV.Internals, Data.SBV
sRotateLeft | Data.SBV
sRotateRight | Data.SBV
SRoundingMode | Data.SBV.Internals, Data.SBV
sRoundNearestTiesToAway | Data.SBV.Internals, Data.SBV
sRoundNearestTiesToEven | Data.SBV.Internals, Data.SBV
sRoundTowardNegative | Data.SBV.Internals, Data.SBV
sRoundTowardPositive | Data.SBV.Internals, Data.SBV
sRoundTowardZero | Data.SBV.Internals, Data.SBV
sRTN | Data.SBV.Internals, Data.SBV
sRTP | Data.SBV.Internals, Data.SBV
sRTZ | Data.SBV.Internals, Data.SBV
sShiftLeft | Data.SBV
sShiftRight | Data.SBV
sSignedShiftArithRight | Data.SBV
SState | Documentation.SBV.Examples.Lists.BoundedMutex
SString | Data.SBV.Internals, Data.SBV
sString | Data.SBV
sStrings | Data.SBV
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) | Documentation.SBV.Examples.Puzzles.U2Bridge
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.U2Bridge
sTestBit | Data.SBV
STime | Documentation.SBV.Examples.Puzzles.U2Bridge
StrConcat | Data.SBV.Internals
StrContains | Data.SBV.Internals
STree | Data.SBV.Tools.STree
StrIndexOf | Data.SBV.Internals
StrInRe | Data.SBV.Internals
StrLen | Data.SBV.Internals
StrNatToStr | 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
strToNat | Data.SBV.String
strToStrAt | Data.SBV.String
StrUnit | Data.SBV.Internals
SU2Member | Documentation.SBV.Examples.Puzzles.U2Bridge
subList | Data.SBV.List
subStr | Data.SBV.String
sudoku | Documentation.SBV.Examples.Puzzles.Sudoku
Sunday | Documentation.SBV.Examples.Queries.Enums
SUnOp | Documentation.SBV.Examples.Queries.FourFours
supportsApproxReals | Data.SBV.Internals
supportsCustomQueries | Data.SBV.Internals
supportsFlattenedSequences | Data.SBV.Internals
supportsGlobalDecls | Data.SBV.Internals
supportsIEEE754 | Data.SBV.Internals
supportsOptimization | Data.SBV.Internals
supportsPseudoBooleans | Data.SBV.Internals
supportsQuantifiers | Data.SBV.Internals
supportsReals | Data.SBV.Internals
supportsUnboundedInts | Data.SBV.Internals
supportsUninterpretedSorts | 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
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
svFromIntegral | Data.SBV.Dynamic
svFromWord1 | Data.SBV.Dynamic
svGreaterEq | Data.SBV.Dynamic
svGreaterThan | Data.SBV.Dynamic
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
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
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
SW |
1 (Type/Class) | Data.SBV.Internals
2 (Data Constructor) | Data.SBV.Internals
swap | Documentation.SBV.Examples.Crypto.RC4
Swede | Documentation.SBV.Examples.Puzzles.Fish
SWord16 | Data.SBV.Internals, Data.SBV
sWord16 | Data.SBV
sWord16s | Data.SBV
SWord32 | Data.SBV.Internals, Data.SBV
sWord32 | Data.SBV
sWord32AsSFloat | Data.SBV
sWord32s | Data.SBV
SWord4 | Documentation.SBV.Examples.Misc.Word4
SWord48 | Documentation.SBV.Examples.Existentials.CRCPolynomial
SWord64 | Data.SBV.Internals, Data.SBV
sWord64 | Data.SBV
sWord64AsSDouble | Data.SBV
sWord64s | Data.SBV
SWord8 | Data.SBV.Internals, Data.SBV
sWord8 | Data.SBV
sWord8s | Data.SBV
sWordN | Data.SBV.Dynamic
sWordN_ | Data.SBV.Dynamic
SymArray | Data.SBV.Internals, Data.SBV
Symbolic | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
symbolic | Data.SBV.Internals, Data.SBV
symbolicMerge | Data.SBV
symbolics | Data.SBV.Internals, Data.SBV
SymWord | Data.SBV.Internals, Data.SBV
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
targetName | Data.SBV.Internals
Tea | Documentation.SBV.Examples.Puzzles.Fish
Tennis | Documentation.SBV.Examples.Puzzles.Fish
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
testBitDefault | Data.SBV
testGF28 | Documentation.SBV.Examples.Misc.Polynomials
TestStyle | Data.SBV.Tools.GenTest
TestVectors | Data.SBV.Tools.GenTest
There | Documentation.SBV.Examples.Puzzles.U2Bridge
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, Data.SBV.Dynamic
2 (Data Constructor) | Data.SBV, Data.SBV.Dynamic
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 | Data.SBV.Control
Times |
1 (Data Constructor) | Data.SBV.Internals
2 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours
Timing | Data.SBV.Internals, Data.SBV
timing | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
toBytes | Documentation.SBV.Examples.Crypto.AES
toIntegralSized | Data.SBV
toLower | Data.SBV.Char
toSDouble | Data.SBV
toSFloat | Data.SBV
toUpper | Data.SBV.Char
transcript | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
translate | Data.SBV.Internals
true | Data.SBV
trueCW | Data.SBV.Internals
trueSW | Data.SBV.Internals
tstShiftLeft | Documentation.SBV.Examples.CodeGeneration.Uninterpreted
Tuesday | Documentation.SBV.Examples.Queries.Enums
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
UFNIA | Data.SBV
Unbounded | Data.SBV.Tools.Range
uncache | Data.SBV.Internals
uncacheAI | Data.SBV.Internals
uncons | Data.SBV.List
UNeg | Data.SBV.Internals
uninterpret | Data.SBV
Uninterpreted |
1 (Data Constructor) | Data.SBV.Internals
2 (Type/Class) | Data.SBV
Union | Data.SBV.RegExp, Data.SBV.Internals
universal | Documentation.SBV.Examples.Uninterpreted.Shannon
univOK | Documentation.SBV.Examples.Uninterpreted.Shannon
Unk | Data.SBV.Control
Unknown | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
UnknownIncomplete | Data.SBV
UnknownMemOut | Data.SBV
UnknownOther | Data.SBV
UnknownTimeOut | Data.SBV
unliteral | Data.SBV.Internals, Data.SBV
UnOp | Documentation.SBV.Examples.Queries.FourFours
unsafeShiftL | Data.SBV
unsafeShiftR | Data.SBV
unSArray | Data.SBV.Internals
Unsat | Data.SBV.Control
Unsatisfiable | Data.SBV.Internals, 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
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
validPick | Documentation.SBV.Examples.Puzzles.Garden
validSequence | Documentation.SBV.Examples.Lists.BoundedMutex
validTurns | Documentation.SBV.Examples.Lists.BoundedMutex
Value | Documentation.SBV.Examples.BitPrecise.Legato
verbose | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
Version | Data.SBV.Control
Volleyball | Documentation.SBV.Examples.Puzzles.Fish
Water | Documentation.SBV.Examples.Puzzles.Fish
Wednesday | Documentation.SBV.Examples.Queries.Enums
whenS | Documentation.SBV.Examples.Puzzles.U2Bridge
whereIs | Documentation.SBV.Examples.Puzzles.U2Bridge
White | Documentation.SBV.Examples.Puzzles.Fish
whiteSpace | Data.SBV.RegExp
whiteSpaceNoNewLine | Data.SBV.RegExp
Word | Data.SBV
Word16 | Data.SBV
Word32 | Data.SBV
Word4 |
1 (Type/Class) | Documentation.SBV.Examples.Misc.Word4
2 (Data Constructor) | Documentation.SBV.Examples.Misc.Word4
word4 | Documentation.SBV.Examples.Misc.Word4
Word64 | Data.SBV
Word8 | Data.SBV
writeArray | Data.SBV.Internals, Data.SBV
writeSArr | Data.SBV.Dynamic
writeSFunArr | Data.SBV.Dynamic
writeSTree | Data.SBV.Tools.STree
xferFlash | Documentation.SBV.Examples.Puzzles.U2Bridge
xferPerson | Documentation.SBV.Examples.Puzzles.U2Bridge
XOr | Data.SBV.Internals
xor | Data.SBV
Yellow |
1 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Fish
2 (Data Constructor) | Documentation.SBV.Examples.Puzzles.Garden
Yices | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
yices | Data.SBV, Data.SBV.Dynamic
Z3 | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic
z3 | Data.SBV, Data.SBV.Dynamic
zeroBits | Data.SBV
zipPL | Documentation.SBV.Examples.BitPrecise.PrefixSum
_cwKind | Data.SBV.Internals, Data.SBV.Dynamic
|-> | Data.SBV.Control
||| | Data.SBV
~& | Data.SBV
~| | Data.SBV