Safe Haskell | Safe |
---|---|
Language | Haskell98 |
SMTLib2
Documentation
Instances
Data Binder Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder -> c Binder Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Binder Source # toConstr :: Binder -> Constr Source # dataTypeOf :: Binder -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Binder) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder) Source # gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Binder -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder -> m Binder Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder Source # | |
Show Binder Source # | |
Eq Binder Source # | |
Ord Binder Source # | |
PP Binder Source # | |
Instances
Data Defn Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defn -> c Defn Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defn Source # toConstr :: Defn -> Constr Source # dataTypeOf :: Defn -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Defn) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn) Source # gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defn -> m Defn Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn Source # | |
Show Defn Source # | |
Eq Defn Source # | |
Ord Defn Source # | |
PP Defn Source # | |
Instances
Data Type Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type Source # toConstr :: Type -> Constr Source # dataTypeOf :: Type -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) Source # gmapT :: (forall b. Data b => b -> b) -> Type -> Type Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type Source # | |
IsString Type Source # | |
Defined in SMTLib2.AST Methods fromString :: String -> Type Source # | |
Show Type Source # | |
Eq Type Source # | |
Ord Type Source # | |
PP Type Source # | |
Constructors
Lit Literal | |
App Ident (Maybe Type) [Expr] | |
Quant Quant [Binder] Expr | |
Let [Defn] Expr | |
Annot Expr [Attr] |
Instances
Data Expr Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr Source # toConstr :: Expr -> Constr Source # dataTypeOf :: Expr -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) Source # gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source # | |
IsString Expr Source # | |
Defined in SMTLib2.AST Methods fromString :: String -> Expr Source # | |
Num Expr Source # | |
Fractional Expr Source # | |
Show Expr Source # | |
Eq Expr Source # | |
Ord Expr Source # | |
PP Expr Source # | |
Instances
Data Name Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name Source # toConstr :: Name -> Constr Source # dataTypeOf :: Name -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) Source # gmapT :: (forall b. Data b => b -> b) -> Name -> Name Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name Source # | |
IsString Name Source # | |
Defined in SMTLib2.AST Methods fromString :: String -> Name Source # | |
Show Name Source # | |
Eq Name Source # | |
Ord Name Source # | |
PP Name Source # | |
Instances
Data Ident Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ident -> c Ident Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Ident Source # toConstr :: Ident -> Constr Source # dataTypeOf :: Ident -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Ident) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident) Source # gmapT :: (forall b. Data b => b -> b) -> Ident -> Ident Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Ident -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Ident -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ident -> m Ident Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ident -> m Ident Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ident -> m Ident Source # | |
IsString Ident Source # | |
Defined in SMTLib2.AST Methods fromString :: String -> Ident Source # | |
Show Ident Source # | |
Eq Ident Source # | |
Ord Ident Source # | |
Defined in SMTLib2.AST | |
PP Ident Source # | |
Instances
Data Quant Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quant -> c Quant Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quant Source # toConstr :: Quant -> Constr Source # dataTypeOf :: Quant -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quant) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant) Source # gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quant -> m Quant Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant Source # | |
Show Quant Source # | |
Eq Quant Source # | |
Ord Quant Source # | |
Defined in SMTLib2.AST | |
PP Quant Source # | |
Constructors
LitBV Integer Integer | value, width (in bits) |
LitNum Integer | |
LitFrac Rational | |
LitStr String |
Instances
Data Literal Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Literal -> c Literal Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Literal Source # toConstr :: Literal -> Constr Source # dataTypeOf :: Literal -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Literal) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal) Source # gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Literal -> m Literal Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal Source # | |
Show Literal Source # | |
Eq Literal Source # | |
Ord Literal Source # | |
PP Literal Source # | |
Instances
Data Attr Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Attr -> c Attr Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Attr Source # toConstr :: Attr -> Constr Source # dataTypeOf :: Attr -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Attr) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr) Source # gmapT :: (forall b. Data b => b -> b) -> Attr -> Attr Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Attr -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Attr -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Attr -> m Attr Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Attr -> m Attr Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Attr -> m Attr Source # | |
Show Attr Source # | |
Eq Attr Source # | |
Ord Attr Source # | |
PP Attr Source # | |
Constructors
Instances
Data Command Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Command -> c Command Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Command Source # toConstr :: Command -> Constr Source # dataTypeOf :: Command -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Command) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command) Source # gmapT :: (forall b. Data b => b -> b) -> Command -> Command Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Command -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Command -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Command -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Command -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Command -> m Command Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Command -> m Command Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Command -> m Command Source # | |
PP Command Source # | |
Constructors
Instances
Data Option Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Option -> c Option Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Option Source # toConstr :: Option -> Constr Source # dataTypeOf :: Option -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Option) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option) Source # gmapT :: (forall b. Data b => b -> b) -> Option -> Option Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Option -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Option -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Option -> m Option Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Option -> m Option Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Option -> m Option Source # | |
PP Option Source # | |
Constructors
InfoAllStatistics | |
InfoErrorBehavior | |
InfoName | |
InfoAuthors | |
InfoVersion | |
InfoStatus | |
InfoReasonUnknown | |
InfoAttr Attr |
Instances
Data InfoFlag Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InfoFlag -> c InfoFlag Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InfoFlag Source # toConstr :: InfoFlag -> Constr Source # dataTypeOf :: InfoFlag -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InfoFlag) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag) Source # gmapT :: (forall b. Data b => b -> b) -> InfoFlag -> InfoFlag Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r Source # gmapQ :: (forall d. Data d => d -> u) -> InfoFlag -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> InfoFlag -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag Source # | |
PP InfoFlag Source # | |