| ParBool | Language.SMTLib2.Strategy |
| ParDouble | Language.SMTLib2.Strategy |
| ParInt | Language.SMTLib2.Strategy |
| ParOr | Language.SMTLib2.Strategy |
| parseArgs | Language.SMTLib2.Internals.TH |
| parseExpr | Language.SMTLib2.Internals.TH |
| parseHs | Language.SMTLib2.Internals.TH |
| parseList | Language.SMTLib2.Internals.TH |
| parseName | Language.SMTLib2.Internals.TH |
| parseSingleExpr | Language.SMTLib2.Internals.TH |
| ParThen | Language.SMTLib2.Strategy |
| Partition | Language.SMTLib2.Internals.Backend, Language.SMTLib2 |
| PartitionA | Language.SMTLib2.Internals.Backend, Language.SMTLib2 |
| PartitionB | Language.SMTLib2.Internals.Backend, Language.SMTLib2 |
| Plus | |
| 1 (Data Constructor) | Language.SMTLib2.Internals.Expression |
| 2 (Data Constructor) | Language.SMTLib2.Internals.Interface, Language.SMTLib2 |
| plus | |
| 1 (Function) | Language.SMTLib2.Internals.Expression |
| 2 (Function) | Language.SMTLib2.Internals.Interface, Language.SMTLib2 |
| plus' | Language.SMTLib2.Internals.TH |
| PlusLst | Language.SMTLib2.Internals.Interface, Language.SMTLib2 |
| pop | |
| 1 (Function) | Language.SMTLib2.Internals.Backend |
| 2 (Function) | Language.SMTLib2 |
| PrintSuccess | Language.SMTLib2.Internals.Backend, Language.SMTLib2 |
| Probe | Language.SMTLib2.Strategy |
| ProbeAnd | Language.SMTLib2.Strategy |
| ProbeBoolConst | Language.SMTLib2.Strategy |
| ProbeEq | Language.SMTLib2.Strategy |
| ProbeGe | Language.SMTLib2.Strategy |
| ProbeGt | Language.SMTLib2.Strategy |
| ProbeIntConst | Language.SMTLib2.Strategy |
| ProbeLe | Language.SMTLib2.Strategy |
| ProbeLt | Language.SMTLib2.Strategy |
| ProbeNot | Language.SMTLib2.Strategy |
| ProbeOr | Language.SMTLib2.Strategy |
| ProduceInterpolants | Language.SMTLib2.Internals.Backend, Language.SMTLib2 |
| ProduceModel | Language.SMTLib2.Strategy |
| ProduceModels | Language.SMTLib2.Internals.Backend, Language.SMTLib2 |
| ProduceProofs | |
| 1 (Data Constructor) | Language.SMTLib2.Strategy |
| 2 (Data Constructor) | Language.SMTLib2.Internals.Backend, Language.SMTLib2 |
| ProduceUnsatCores | |
| 1 (Data Constructor) | Language.SMTLib2.Strategy |
| 2 (Data Constructor) | Language.SMTLib2.Internals.Backend, Language.SMTLib2 |
| Proof | |
| 1 (Type/Class) | Language.SMTLib2.Internals.Proof |
| 2 (Type/Class) | Language.SMTLib2.Internals.Backend |
| ProofExpr | Language.SMTLib2.Internals.Proof |
| ProofResult | Language.SMTLib2.Internals.Proof |
| push | |
| 1 (Function) | Language.SMTLib2.Internals.Backend |
| 2 (Function) | Language.SMTLib2 |