| p | Documentation.SBV.Examples.Queries.UnsatCore |
| pAdd | Data.SBV.Tools.Polynomial |
| Pareto | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| ParetoResult | Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| parseCVs | Data.SBV.Trans, Data.SBV |
| PartialCorrectness | Data.SBV.Tools.Induction |
| pbAtLeast | Data.SBV.Trans, Data.SBV |
| pbAtMost | Data.SBV.Trans, Data.SBV |
| pbEq | Data.SBV.Trans, Data.SBV |
| pbExactly | Data.SBV.Trans, Data.SBV |
| pbGe | Data.SBV.Trans, Data.SBV |
| pbLe | Data.SBV.Trans, Data.SBV |
| pbMutexed | Data.SBV.Trans, Data.SBV |
| PBOp | Data.SBV.Internals |
| pbStronglyMutexed | Data.SBV.Trans, Data.SBV |
| PB_AtLeast | Data.SBV.Internals |
| PB_AtMost | Data.SBV.Internals |
| PB_Eq | Data.SBV.Internals |
| PB_Exactly | Data.SBV.Internals |
| PB_Ge | Data.SBV.Internals |
| PB_Le | Data.SBV.Internals |
| pDiv | Data.SBV.Tools.Polynomial |
| pDivMod | Data.SBV.Tools.Polynomial |
| peek | |
| 1 (Function) | Documentation.SBV.Examples.BitPrecise.Legato |
| 2 (Function) | Documentation.SBV.Examples.Puzzles.U2Bridge |
| Penalty | |
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| 2 (Data Constructor) | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| Pet | Documentation.SBV.Examples.Puzzles.Fish |
| pgm1 | Documentation.SBV.Examples.ProofTools.Strengthen |
| pgm2 | Documentation.SBV.Examples.ProofTools.Strengthen |
| pgmAssignments | Data.SBV.Internals |
| play | Documentation.SBV.Examples.Queries.GuessNumber |
| Plus | |
| 1 (Data Constructor) | Data.SBV.Internals |
| 2 (Data Constructor) | Documentation.SBV.Examples.Queries.FourFours |
| 3 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| pMod | Data.SBV.Tools.Polynomial |
| pMult | Data.SBV.Tools.Polynomial |
| poke | Documentation.SBV.Examples.BitPrecise.Legato |
| polyDivMod | Documentation.SBV.Examples.Misc.Polynomials |
| Polynomial | Data.SBV.Tools.Polynomial |
| polynomial | Data.SBV.Tools.Polynomial |
| pop | |
| 1 (Function) | Data.SBV.Trans.Control |
| 2 (Function) | Data.SBV.Control |
| pop8 | Documentation.SBV.Examples.CodeGeneration.PopulationCount |
| popCount | Data.SBV.Trans, Data.SBV |
| popCountDefault | Data.SBV.Trans, Data.SBV |
| popCountFast | Documentation.SBV.Examples.CodeGeneration.PopulationCount |
| popCountSlow | Documentation.SBV.Examples.CodeGeneration.PopulationCount |
| pos | Documentation.SBV.Examples.Uninterpreted.Shannon |
| post | |
| 1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics |
| 2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib |
| 3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD |
| 4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv |
| 5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt |
| 6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length |
| 7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum |
| postcondition | Data.SBV.Tools.WeakestPreconditions |
| PowerList | Documentation.SBV.Examples.BitPrecise.PrefixSum |
| powerOfTwoCorrect | Documentation.SBV.Examples.BitPrecise.BitTricks |
| pre | |
| 1 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Basics |
| 2 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Fib |
| 3 (Function) | Documentation.SBV.Examples.WeakestPreconditions.GCD |
| 4 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntDiv |
| 5 (Function) | Documentation.SBV.Examples.WeakestPreconditions.IntSqrt |
| 6 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Length |
| 7 (Function) | Documentation.SBV.Examples.WeakestPreconditions.Sum |
| precondition | Data.SBV.Tools.WeakestPreconditions |
| Predicate | Data.SBV.Trans, Data.SBV |
| prepareMessage | Documentation.SBV.Examples.Crypto.SHA |
| preprocess | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| PrettyNum | Data.SBV.Internals |
| prga | Documentation.SBV.Examples.Crypto.RC4 |
| printBase | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| printRealPrec | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| PrintTiming | Data.SBV.Internals, Data.SBV.Trans, Data.SBV |
| problem | |
| 1 (Function) | Documentation.SBV.Examples.Misc.Auxiliary |
| 2 (Function) | Documentation.SBV.Examples.Misc.Newtypes |
| 3 (Function) | Documentation.SBV.Examples.Optimization.ExtField |
| 4 (Function) | Documentation.SBV.Examples.Optimization.LinearOpt |
| 5 (Function) | Documentation.SBV.Examples.ProofTools.BMC |
| 6 (Function) | Documentation.SBV.Examples.ProofTools.Strengthen |
| ProduceAssertions | Data.SBV.Trans.Control, Data.SBV.Control |
| ProduceAssignments | Data.SBV.Trans.Control, Data.SBV.Control |
| ProduceInterpolants | Data.SBV.Trans.Control, Data.SBV.Control |
| ProduceProofs | Data.SBV.Trans.Control, Data.SBV.Control |
| ProduceUnsatAssumptions | Data.SBV.Trans.Control, Data.SBV.Control |
| ProduceUnsatCores | Data.SBV.Trans.Control, Data.SBV.Control |
| production | Documentation.SBV.Examples.Optimization.Production |
| Program | |
| 1 (Type/Class) | Data.SBV.Tools.WeakestPreconditions |
| 2 (Data Constructor) | Data.SBV.Tools.WeakestPreconditions |
| 3 (Type/Class) | Documentation.SBV.Examples.BitPrecise.Legato |
| 4 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| 5 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| program | Data.SBV.Tools.WeakestPreconditions |
| project | Data.SBV.Control |
| ProofError | Data.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic |
| ProofResult | Data.SBV.Tools.WeakestPreconditions |
| Property | |
| 1 (Type/Class) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| 2 (Data Constructor) | Documentation.SBV.Examples.Transformers.SymbolicEval |
| Provable | Data.SBV.Trans, Data.SBV |
| prove | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| proveConcurrentWithAll | |
| 1 (Function) | Data.SBV.Trans, Data.SBV |
| 2 (Function) | Data.SBV.Dynamic |
| proveConcurrentWithAny | |
| 1 (Function) | Data.SBV.Trans, Data.SBV |
| 2 (Function) | Data.SBV.Dynamic |
| Proved | Documentation.SBV.Examples.Transformers.SymbolicEval |
| Proven | |
| 1 (Data Constructor) | Data.SBV.Tools.WeakestPreconditions |
| 2 (Data Constructor) | Data.SBV.Tools.Induction |
| proveSArray | Documentation.SBV.Examples.Uninterpreted.AUF |
| proveSFunArray | Documentation.SBV.Examples.Uninterpreted.AUF |
| proveWith | |
| 1 (Function) | Data.SBV.Trans |
| 2 (Function) | Data.SBV |
| 3 (Function) | Data.SBV.Dynamic |
| proveWithAll | |
| 1 (Function) | Data.SBV.Trans, Data.SBV |
| 2 (Function) | Data.SBV.Dynamic |
| proveWithAny | |
| 1 (Function) | Data.SBV.Trans, Data.SBV |
| 2 (Function) | Data.SBV.Dynamic |
| ps | Documentation.SBV.Examples.BitPrecise.PrefixSum |
| PseudoBoolean | Data.SBV.Internals |
| punctuation | Data.SBV.RegExp |
| push | |
| 1 (Function) | Data.SBV.Trans.Control |
| 2 (Function) | Data.SBV.Control |
| Puzzle | Documentation.SBV.Examples.Puzzles.Sudoku |
| puzzle | |
| 1 (Function) | Documentation.SBV.Examples.Puzzles.Birthday |
| 2 (Function) | Documentation.SBV.Examples.Puzzles.Coins |
| 3 (Function) | Documentation.SBV.Examples.Puzzles.Counts |
| 4 (Function) | Documentation.SBV.Examples.Puzzles.DogCatMouse |
| 5 (Function) | Documentation.SBV.Examples.Puzzles.Garden |
| 6 (Function) | Documentation.SBV.Examples.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 |