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

Index - O

oneIfData.SBV, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
oppositeSignsCorrectData.SBV.Examples.BitPrecise.BitTricks
optimize 
1 (Function)Data.SBV
2 (Function)Data.SBV.Bridge.Boolector
3 (Function)Data.SBV.Bridge.CVC4
4 (Function)Data.SBV.Bridge.MathSAT
5 (Function)Data.SBV.Bridge.Yices
6 (Function)Data.SBV.Bridge.Z3
OptimizeOptsData.SBV, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
optimizeWithData.SBV, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
optionsData.SBV, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
orData.SBV.Examples.Uninterpreted.Deduce
OrdSymbolicData.SBV, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
outputData.SBV, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.MathSAT, Data.SBV.Bridge.Yices, Data.SBV.Bridge.Z3
outsideData.SBV.Examples.Misc.ModelExtract