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

Index - P

pDocumentation.SBV.Examples.Queries.UnsatCore
pAddData.SBV.Tools.Polynomial
ParetoData.SBV.Internals, Data.SBV.Trans, Data.SBV
ParetoResultData.SBV.Trans, Data.SBV, Data.SBV.Dynamic
parseCVsData.SBV.Trans, Data.SBV
PartialCorrectnessData.SBV.Tools.Induction
pbAtLeastData.SBV.Trans, Data.SBV
pbAtMostData.SBV.Trans, Data.SBV
pbEqData.SBV.Trans, Data.SBV
pbExactlyData.SBV.Trans, Data.SBV
pbGeData.SBV.Trans, Data.SBV
pbLeData.SBV.Trans, Data.SBV
pbMutexedData.SBV.Trans, Data.SBV
PBOpData.SBV.Internals
pbStronglyMutexedData.SBV.Trans, Data.SBV
PB_AtLeastData.SBV.Internals
PB_AtMostData.SBV.Internals
PB_EqData.SBV.Internals
PB_ExactlyData.SBV.Internals
PB_GeData.SBV.Internals
PB_LeData.SBV.Internals
pDivData.SBV.Tools.Polynomial
pDivModData.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
PetDocumentation.SBV.Examples.Puzzles.Fish
pgm1Documentation.SBV.Examples.ProofTools.Strengthen
pgm2Documentation.SBV.Examples.ProofTools.Strengthen
pgmAssignmentsData.SBV.Internals
playDocumentation.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
pModData.SBV.Tools.Polynomial
pMultData.SBV.Tools.Polynomial
pokeDocumentation.SBV.Examples.BitPrecise.Legato
polyDivModDocumentation.SBV.Examples.Misc.Polynomials
PolynomialData.SBV.Tools.Polynomial
polynomialData.SBV.Tools.Polynomial
pop 
1 (Function)Data.SBV.Trans.Control
2 (Function)Data.SBV.Control
pop8Documentation.SBV.Examples.CodeGeneration.PopulationCount
popCountData.SBV.Trans, Data.SBV
popCountDefaultData.SBV.Trans, Data.SBV
popCountFastDocumentation.SBV.Examples.CodeGeneration.PopulationCount
popCountSlowDocumentation.SBV.Examples.CodeGeneration.PopulationCount
posDocumentation.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
postconditionData.SBV.Tools.WeakestPreconditions
PowerListDocumentation.SBV.Examples.BitPrecise.PrefixSum
powerOfTwoCorrectDocumentation.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
preconditionData.SBV.Tools.WeakestPreconditions
PredicateData.SBV.Trans, Data.SBV
prepareMessageDocumentation.SBV.Examples.Crypto.SHA
preprocessData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
PrettyNumData.SBV.Internals
prgaDocumentation.SBV.Examples.Crypto.RC4
printBaseData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
printRealPrecData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
PrintTimingData.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
ProduceAssertionsData.SBV.Trans.Control, Data.SBV.Control
ProduceAssignmentsData.SBV.Trans.Control, Data.SBV.Control
ProduceInterpolantsData.SBV.Trans.Control, Data.SBV.Control
ProduceProofsData.SBV.Trans.Control, Data.SBV.Control
ProduceUnsatAssumptionsData.SBV.Trans.Control, Data.SBV.Control
ProduceUnsatCoresData.SBV.Trans.Control, Data.SBV.Control
productionDocumentation.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
programData.SBV.Tools.WeakestPreconditions
projectData.SBV.Control
ProofErrorData.SBV.Internals, Data.SBV.Trans, Data.SBV, Data.SBV.Dynamic
ProofResultData.SBV.Tools.WeakestPreconditions
Property 
1 (Type/Class)Documentation.SBV.Examples.Transformers.SymbolicEval
2 (Data Constructor)Documentation.SBV.Examples.Transformers.SymbolicEval
ProvableData.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
ProvedDocumentation.SBV.Examples.Transformers.SymbolicEval
Proven 
1 (Data Constructor)Data.SBV.Tools.WeakestPreconditions
2 (Data Constructor)Data.SBV.Tools.Induction
proveSArrayDocumentation.SBV.Examples.Uninterpreted.AUF
proveSFunArrayDocumentation.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
psDocumentation.SBV.Examples.BitPrecise.PrefixSum
PseudoBooleanData.SBV.Internals
punctuationData.SBV.RegExp
push 
1 (Function)Data.SBV.Trans.Control
2 (Function)Data.SBV.Control
PuzzleDocumentation.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
puzzle0Documentation.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
puzzle4Documentation.SBV.Examples.Puzzles.Sudoku
puzzle5Documentation.SBV.Examples.Puzzles.Sudoku
puzzle6Documentation.SBV.Examples.Puzzles.Sudoku