sbv-5.14: 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

pAdd | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
parseCWs | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
pConstrain | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
pDiv | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
pDivMod | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
peek |
1 (Function) | Data.SBV.Examples.BitPrecise.Legato
2 (Function) | Data.SBV.Examples.Puzzles.U2Bridge
Pet | Data.SBV.Examples.Puzzles.Fish
pgmAssignments | Data.SBV.Internals
Plus | Data.SBV.Internals
pMod | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
pMult | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
poke | Data.SBV.Examples.BitPrecise.Legato
polyDivMod | Data.SBV.Examples.Polynomials.Polynomials
Polynomial | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
polynomial | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
pop8 | Data.SBV.Examples.CodeGeneration.PopulationCount
popCount | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
popCountDefault | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
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
PredefinedLogic | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
Predicate | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
PrettyNum | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
prga | Data.SBV.Examples.Crypto.RC4
printBase | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
printRealPrec | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
problem | Data.SBV.Examples.Misc.Auxiliary
Program | Data.SBV.Examples.BitPrecise.Legato
Proof | Data.SBV.Internals
ProofError | Data.SBV.Internals, Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3, Data.SBV.Dynamic
Provable | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
prove |
1 (Function) | Data.SBV
2 (Function) | Data.SBV.Bridge.ABC
3 (Function) | Data.SBV.Bridge.Boolector
4 (Function) | Data.SBV.Bridge.CVC4
5 (Function) | Data.SBV.Bridge.MathSAT
6 (Function) | Data.SBV.Bridge.Yices
7 (Function) | Data.SBV.Bridge.Z3
proveThm1 | Data.SBV.Examples.Uninterpreted.AUF
proveThm2 | Data.SBV.Examples.Uninterpreted.AUF
proveWith |
1 (Function) | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Function) | Data.SBV.Dynamic
proveWithAll |
1 (Function) | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Function) | Data.SBV.Dynamic
proveWithAny |
1 (Function) | Data.SBV, Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
2 (Function) | Data.SBV.Dynamic
ps | Data.SBV.Examples.BitPrecise.PrefixSum
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
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