{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Plugin.Data where
import Data.Data (Data, Typeable)
data SBVOption = IgnoreFailure
| Skip String
| Verbose
| Debug
| QuickCheck
| Uninterpret
| Names [String]
| ListSize Int
| Z3
| Yices
| Boolector
| CVC4
| MathSAT
| ABC
| AnySolver
deriving (Int -> SBVOption -> ShowS
[SBVOption] -> ShowS
SBVOption -> String
(Int -> SBVOption -> ShowS)
-> (SBVOption -> String)
-> ([SBVOption] -> ShowS)
-> Show SBVOption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SBVOption] -> ShowS
$cshowList :: [SBVOption] -> ShowS
show :: SBVOption -> String
$cshow :: SBVOption -> String
showsPrec :: Int -> SBVOption -> ShowS
$cshowsPrec :: Int -> SBVOption -> ShowS
Show, SBVOption -> SBVOption -> Bool
(SBVOption -> SBVOption -> Bool)
-> (SBVOption -> SBVOption -> Bool) -> Eq SBVOption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SBVOption -> SBVOption -> Bool
$c/= :: SBVOption -> SBVOption -> Bool
== :: SBVOption -> SBVOption -> Bool
$c== :: SBVOption -> SBVOption -> Bool
Eq, Typeable SBVOption
Typeable SBVOption
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVOption -> c SBVOption)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVOption)
-> (SBVOption -> Constr)
-> (SBVOption -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVOption))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption))
-> ((forall b. Data b => b -> b) -> SBVOption -> SBVOption)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r)
-> (forall u. (forall d. Data d => d -> u) -> SBVOption -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> SBVOption -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption)
-> Data SBVOption
SBVOption -> DataType
SBVOption -> Constr
(forall b. Data b => b -> b) -> SBVOption -> SBVOption
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SBVOption -> u
forall u. (forall d. Data d => d -> u) -> SBVOption -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVOption
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVOption -> c SBVOption
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVOption)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SBVOption -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SBVOption -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SBVOption -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SBVOption -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
gmapT :: (forall b. Data b => b -> b) -> SBVOption -> SBVOption
$cgmapT :: (forall b. Data b => b -> b) -> SBVOption -> SBVOption
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVOption)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVOption)
dataTypeOf :: SBVOption -> DataType
$cdataTypeOf :: SBVOption -> DataType
toConstr :: SBVOption -> Constr
$ctoConstr :: SBVOption -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVOption
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVOption
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVOption -> c SBVOption
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVOption -> c SBVOption
Data, Typeable)
newtype SBVAnnotation = SBV {SBVAnnotation -> [SBVOption]
options :: [SBVOption]}
deriving (SBVAnnotation -> SBVAnnotation -> Bool
(SBVAnnotation -> SBVAnnotation -> Bool)
-> (SBVAnnotation -> SBVAnnotation -> Bool) -> Eq SBVAnnotation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SBVAnnotation -> SBVAnnotation -> Bool
$c/= :: SBVAnnotation -> SBVAnnotation -> Bool
== :: SBVAnnotation -> SBVAnnotation -> Bool
$c== :: SBVAnnotation -> SBVAnnotation -> Bool
Eq, Typeable SBVAnnotation
Typeable SBVAnnotation
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVAnnotation)
-> (SBVAnnotation -> Constr)
-> (SBVAnnotation -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SBVAnnotation))
-> ((forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r)
-> (forall u. (forall d. Data d => d -> u) -> SBVAnnotation -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation)
-> Data SBVAnnotation
SBVAnnotation -> DataType
SBVAnnotation -> Constr
(forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u
forall u. (forall d. Data d => d -> u) -> SBVAnnotation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVAnnotation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SBVAnnotation)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SBVAnnotation -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SBVAnnotation -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
gmapT :: (forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation
$cgmapT :: (forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SBVAnnotation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SBVAnnotation)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation)
dataTypeOf :: SBVAnnotation -> DataType
$cdataTypeOf :: SBVAnnotation -> DataType
toConstr :: SBVAnnotation -> Constr
$ctoConstr :: SBVAnnotation -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVAnnotation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVAnnotation
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation
Data, Typeable)
sbv :: SBVAnnotation
sbv :: SBVAnnotation
sbv = SBV {options :: [SBVOption]
options = []}
theorem :: SBVAnnotation
theorem :: SBVAnnotation
theorem = SBVAnnotation
sbv
type Proved a = a