| # | 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 |
| bfoldl | Data.SBV.List.Bounded |
| bfoldr | 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.HexPuzzle |
| bmap | 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 |
| BoundedCW | Data.SBV.Internals, Data.SBV |
| bprod | Data.SBV.List.Bounded |
| Briton | Documentation.SBV.Examples.Puzzles.Fish |
| 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 |
| 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 |
| Color | |
| 1 (Type/Class) | Documentation.SBV.Examples.Puzzles.Fish |
| 2 (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 | Documentation.SBV.Examples.Puzzles.Counts |
| 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 |
| 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 |
| 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 |
| 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.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 | Data.SBV.RegExp, Data.SBV.Internals |
| 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.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 |