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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- #
- %
- *
- +
- .
- /
- =
- \
- ^
- |
- -
- _
- All

Index - P

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