Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.SBV.Plugin.Data

Description

Internal data-structures for the sbvPlugin

Synopsis

data SBVOption
- = IgnoreFailure
- | Skip String
- | Verbose
- | Debug
- | QuickCheck
- | Uninterpret
- | Names [String]
- | ListSize Int
- | Z3
- | Yices
- | Boolector
- | CVC4
- | MathSAT
- | ABC
- | AnySolver
newtype SBVAnnotation = SBV {
- options :: [SBVOption]
}
sbv :: SBVAnnotation
theorem :: SBVAnnotation
type Proved a = a

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 Methods showsPrec :: Int -> SBVOption -> ShowS # show :: SBVOption -> String # showList :: [SBVOption] -> ShowS #
Eq SBVOption Source #
Instance details Defined in Data.SBV.Plugin.Data Methods (==) :: SBVOption -> SBVOption -> Bool # (/=) :: SBVOption -> SBVOption -> Bool #

newtype SBVAnnotation Source #

The actual annotation.

Constructors

SBV
Fields options :: [SBVOption]

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 Methods (==) :: SBVAnnotation -> SBVAnnotation -> Bool # (/=) :: SBVAnnotation -> SBVAnnotation -> Bool #

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