sbvPlugin-9.8.2: Formally prove properties of Haskell programs using SBV/SMT
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.SBV.Plugin.Data

Description

Internal data-structures for the sbvPlugin

Synopsis

Documentation

data SBVOption Source #

Plugin options. Note that we allow picking multiple solvers, which will all be run in parallel. You can pick and choose any number of them, or if you want to run all available solvers, then use the option AnySolver. The default behavior is to error-out on failure, using the default-SMT solver picked by SBV, which is currently Z3.

Constructors

IgnoreFailure

Continue even if proof fails

Skip String

Skip the proof. Can be handy for properties that we currently do not want to focus on.

Verbose

Produce verbose output, good for debugging

Debug

Produce really verbose output, use only when things go really wrong!

QuickCheck

Perform quickCheck

Uninterpret

Uninterpret this binding for proof purposes

Names [String]

Use these names for the arguments; need not be exhaustive

ListSize Int

If a list-input is found, use this length. If not specified, we will complain!

Z3

Use Z3

Yices

Use Yices

Boolector

Use Boolector

CVC4

Use CVC4

MathSAT

Use MathSAT

ABC

Use ABC

AnySolver

Run all installed solvers in parallel, and report the result from the first to finish

Instances

Instances details
Data SBVOption Source # 
Instance details

Defined in Data.SBV.Plugin.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SBVOption -> c SBVOption #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SBVOption #

toConstr :: SBVOption -> Constr #

dataTypeOf :: SBVOption -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SBVOption) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption) #

gmapT :: (forall b. Data b => b -> b) -> SBVOption -> SBVOption #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SBVOption -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SBVOption -> r #

gmapQ :: (forall d. Data d => d -> u) -> SBVOption -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SBVOption -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption #

Show SBVOption Source # 
Instance details

Defined in Data.SBV.Plugin.Data

Eq SBVOption Source # 
Instance details

Defined in Data.SBV.Plugin.Data

newtype SBVAnnotation Source #

The actual annotation.

Constructors

SBV 

Fields

Instances

Instances details
Data SBVAnnotation Source # 
Instance details

Defined in Data.SBV.Plugin.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SBVAnnotation #

toConstr :: SBVAnnotation -> Constr #

dataTypeOf :: SBVAnnotation -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVAnnotation) #

gmapT :: (forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r #

gmapQ :: (forall d. Data d => d -> u) -> SBVAnnotation -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation #

Eq SBVAnnotation Source # 
Instance details

Defined in Data.SBV.Plugin.Data

sbv :: SBVAnnotation Source #

A property annotation, using default options.

theorem :: SBVAnnotation Source #

Synonym for sbv really, just looks cooler

type Proved a = a Source #

Importable type as an annotation alternative