| p | Data.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) | Data.SBV.Examples.BitPrecise.Legato |
| 2 (Function) | Data.SBV.Examples.Puzzles.U2Bridge |
| Penalty | |
| 1 (Type/Class) | Data.SBV.Internals, Data.SBV |
| 2 (Data Constructor) | Data.SBV.Internals, Data.SBV |
| Pet | Data.SBV.Examples.Puzzles.Fish |
| pgmAssignments | Data.SBV.Internals |
| play | Data.SBV.Examples.Queries.GuessNumber |
| Plus | |
| 1 (Data Constructor) | Data.SBV.Internals |
| 2 (Data Constructor) | Data.SBV.Examples.Queries.FourFours |
| pMod | Data.SBV.Tools.Polynomial |
| pMult | Data.SBV.Tools.Polynomial |
| poke | Data.SBV.Examples.BitPrecise.Legato |
| polyDivMod | Data.SBV.Examples.Polynomials.Polynomials |
| Polynomial | Data.SBV.Tools.Polynomial |
| polynomial | Data.SBV.Tools.Polynomial |
| pop | Data.SBV.Control |
| pop8 | Data.SBV.Examples.CodeGeneration.PopulationCount |
| popCount | Data.SBV |
| popCountDefault | Data.SBV |
| popCountFast | Data.SBV.Examples.CodeGeneration.PopulationCount |
| popCountSlow | Data.SBV.Examples.CodeGeneration.PopulationCount |
| pos | Data.SBV.Examples.Uninterpreted.Shannon |
| PowerList | Data.SBV.Examples.BitPrecise.PrefixSum |
| powerOfTwoCorrect | Data.SBV.Examples.BitPrecise.BitTricks |
| Predicate | Data.SBV |
| PrettyNum | Data.SBV.Internals |
| prga | Data.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) | Data.SBV.Examples.Misc.Auxiliary |
| 2 (Function) | Data.SBV.Examples.Optimization.ExtField |
| 3 (Function) | Data.SBV.Examples.Optimization.LinearOpt |
| ProduceAssertions | Data.SBV.Control |
| ProduceAssignments | Data.SBV.Control |
| ProduceProofs | Data.SBV.Control |
| ProduceUnsatAssumptions | Data.SBV.Control |
| ProduceUnsatCores | Data.SBV.Control |
| production | Data.SBV.Examples.Optimization.Production |
| Program | Data.SBV.Examples.BitPrecise.Legato |
| ProofError | Data.SBV.Internals, Data.SBV, Data.SBV.Dynamic |
| Provable | Data.SBV |
| prove | Data.SBV |
| proveThm1 | Data.SBV.Examples.Uninterpreted.AUF |
| proveThm2 | Data.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 | Data.SBV.Examples.BitPrecise.PrefixSum |
| PseudoBoolean | Data.SBV.Internals |
| push | Data.SBV.Control |
| Puzzle | Data.SBV.Examples.Puzzles.Sudoku |
| puzzle | |
| 1 (Function) | Data.SBV.Examples.Puzzles.Birthday |
| 2 (Function) | Data.SBV.Examples.Puzzles.Coins |
| 3 (Function) | Data.SBV.Examples.Puzzles.Counts |
| 4 (Function) | Data.SBV.Examples.Puzzles.DogCatMouse |
| 5 (Function) | Data.SBV.Examples.Queries.FourFours |
| puzzle0 | Data.SBV.Examples.Puzzles.Sudoku |
| puzzle1 | Data.SBV.Examples.Puzzles.Sudoku |
| puzzle2 | Data.SBV.Examples.Puzzles.Sudoku |
| puzzle3 | Data.SBV.Examples.Puzzles.Sudoku |
| puzzle4 | Data.SBV.Examples.Puzzles.Sudoku |
| puzzle5 | Data.SBV.Examples.Puzzles.Sudoku |
| puzzle6 | Data.SBV.Examples.Puzzles.Sudoku |