smtLib-1.1: A library for working with the SMTLIB format.
Safe HaskellSafe
LanguageHaskell98

SMTLib2

Documentation

newtype Script Source #

Constructors

Script [Command] 

Instances

Instances details
PP Script Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Script -> Doc Source #

data Binder Source #

Constructors

Bind 

Fields

Instances

Instances details
Eq Binder Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Binder -> Binder -> Bool

(/=) :: Binder -> Binder -> Bool

Data Binder Source # 
Instance details

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

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

toConstr :: Binder -> Constr

dataTypeOf :: Binder -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder

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

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

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

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

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

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

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

Ord Binder Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Binder -> Binder -> Ordering

(<) :: Binder -> Binder -> Bool

(<=) :: Binder -> Binder -> Bool

(>) :: Binder -> Binder -> Bool

(>=) :: Binder -> Binder -> Bool

max :: Binder -> Binder -> Binder

min :: Binder -> Binder -> Binder

Show Binder Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Binder -> ShowS

show :: Binder -> String

showList :: [Binder] -> ShowS

PP Binder Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Binder -> Doc Source #

data Defn Source #

Constructors

Defn 

Fields

Instances

Instances details
Eq Defn Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Defn -> Defn -> Bool

(/=) :: Defn -> Defn -> Bool

Data Defn Source # 
Instance details

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

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

toConstr :: Defn -> Constr

dataTypeOf :: Defn -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn

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

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

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

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

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

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

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

Ord Defn Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Defn -> Defn -> Ordering

(<) :: Defn -> Defn -> Bool

(<=) :: Defn -> Defn -> Bool

(>) :: Defn -> Defn -> Bool

(>=) :: Defn -> Defn -> Bool

max :: Defn -> Defn -> Defn

min :: Defn -> Defn -> Defn

Show Defn Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Defn -> ShowS

show :: Defn -> String

showList :: [Defn] -> ShowS

PP Defn Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Defn -> Doc Source #

data Type Source #

Constructors

TApp Ident [Type] 
TVar Name 

Instances

Instances details
Eq Type Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Type -> Type -> Bool

(/=) :: Type -> Type -> Bool

Data Type Source # 
Instance details

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

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

toConstr :: Type -> Constr

dataTypeOf :: Type -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Type -> Type

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

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

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

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

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

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

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

Ord Type Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Type -> Type -> Ordering

(<) :: Type -> Type -> Bool

(<=) :: Type -> Type -> Bool

(>) :: Type -> Type -> Bool

(>=) :: Type -> Type -> Bool

max :: Type -> Type -> Type

min :: Type -> Type -> Type

Show Type Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

IsString Type Source # 
Instance details

Defined in SMTLib2.AST

Methods

fromString :: String -> Type

PP Type Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Type -> Doc Source #

data Expr Source #

Constructors

Lit Literal 
App Ident (Maybe Type) [Expr] 
Quant Quant [Binder] Expr 
Let [Defn] Expr 
Annot Expr [Attr] 

Instances

Instances details
Eq Expr Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Expr -> Expr -> Bool

(/=) :: Expr -> Expr -> Bool

Fractional Expr Source # 
Instance details

Defined in SMTLib2.AST

Methods

(/) :: Expr -> Expr -> Expr

recip :: Expr -> Expr

fromRational :: Rational -> Expr

Data Expr Source # 
Instance details

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

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

toConstr :: Expr -> Constr

dataTypeOf :: Expr -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr

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

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

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

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

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

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

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

Num Expr Source # 
Instance details

Defined in SMTLib2.AST

Methods

(+) :: Expr -> Expr -> Expr

(-) :: Expr -> Expr -> Expr

(*) :: Expr -> Expr -> Expr

negate :: Expr -> Expr

abs :: Expr -> Expr

signum :: Expr -> Expr

fromInteger :: Integer -> Expr

Ord Expr Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Expr -> Expr -> Ordering

(<) :: Expr -> Expr -> Bool

(<=) :: Expr -> Expr -> Bool

(>) :: Expr -> Expr -> Bool

(>=) :: Expr -> Expr -> Bool

max :: Expr -> Expr -> Expr

min :: Expr -> Expr -> Expr

Show Expr Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

IsString Expr Source # 
Instance details

Defined in SMTLib2.AST

Methods

fromString :: String -> Expr

PP Expr Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Expr -> Doc Source #

newtype Name Source #

Constructors

N String 

Instances

Instances details
Eq Name Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Data Name Source # 
Instance details

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

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

toConstr :: Name -> Constr

dataTypeOf :: Name -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Name -> Name

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

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

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

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

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

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

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

Ord Name Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Name -> Name -> Ordering

(<) :: Name -> Name -> Bool

(<=) :: Name -> Name -> Bool

(>) :: Name -> Name -> Bool

(>=) :: Name -> Name -> Bool

max :: Name -> Name -> Name

min :: Name -> Name -> Name

Show Name Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

IsString Name Source # 
Instance details

Defined in SMTLib2.AST

Methods

fromString :: String -> Name

PP Name Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Name -> Doc Source #

data Ident Source #

Constructors

I Name [Integer] 

Instances

Instances details
Eq Ident Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Ident -> Ident -> Bool

(/=) :: Ident -> Ident -> Bool

Data Ident Source # 
Instance details

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

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

toConstr :: Ident -> Constr

dataTypeOf :: Ident -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Ident -> Ident

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

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

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

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

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

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

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

Ord Ident Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Ident -> Ident -> Ordering

(<) :: Ident -> Ident -> Bool

(<=) :: Ident -> Ident -> Bool

(>) :: Ident -> Ident -> Bool

(>=) :: Ident -> Ident -> Bool

max :: Ident -> Ident -> Ident

min :: Ident -> Ident -> Ident

Show Ident Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Ident -> ShowS

show :: Ident -> String

showList :: [Ident] -> ShowS

IsString Ident Source # 
Instance details

Defined in SMTLib2.AST

Methods

fromString :: String -> Ident

PP Ident Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Ident -> Doc Source #

data Quant Source #

Constructors

Exists 
Forall 

Instances

Instances details
Eq Quant Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Quant -> Quant -> Bool

(/=) :: Quant -> Quant -> Bool

Data Quant Source # 
Instance details

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

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

toConstr :: Quant -> Constr

dataTypeOf :: Quant -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant

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

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

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

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

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

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

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

Ord Quant Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Quant -> Quant -> Ordering

(<) :: Quant -> Quant -> Bool

(<=) :: Quant -> Quant -> Bool

(>) :: Quant -> Quant -> Bool

(>=) :: Quant -> Quant -> Bool

max :: Quant -> Quant -> Quant

min :: Quant -> Quant -> Quant

Show Quant Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Quant -> ShowS

show :: Quant -> String

showList :: [Quant] -> ShowS

PP Quant Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Quant -> Doc Source #

data Literal Source #

Constructors

LitBV Integer Integer

value, width (in bits)

LitNum Integer 
LitFrac Rational 
LitStr String 

Instances

Instances details
Eq Literal Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Literal -> Literal -> Bool

(/=) :: Literal -> Literal -> Bool

Data Literal Source # 
Instance details

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

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

toConstr :: Literal -> Constr

dataTypeOf :: Literal -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal

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

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

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

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

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

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

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

Ord Literal Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Literal -> Literal -> Ordering

(<) :: Literal -> Literal -> Bool

(<=) :: Literal -> Literal -> Bool

(>) :: Literal -> Literal -> Bool

(>=) :: Literal -> Literal -> Bool

max :: Literal -> Literal -> Literal

min :: Literal -> Literal -> Literal

Show Literal Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Literal -> ShowS

show :: Literal -> String

showList :: [Literal] -> ShowS

PP Literal Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Literal -> Doc Source #

data Attr Source #

Constructors

Attr 

Fields

Instances

Instances details
Eq Attr Source # 
Instance details

Defined in SMTLib2.AST

Methods

(==) :: Attr -> Attr -> Bool

(/=) :: Attr -> Attr -> Bool

Data Attr Source # 
Instance details

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

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

toConstr :: Attr -> Constr

dataTypeOf :: Attr -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Attr -> Attr

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

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

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

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

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

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

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

Ord Attr Source # 
Instance details

Defined in SMTLib2.AST

Methods

compare :: Attr -> Attr -> Ordering

(<) :: Attr -> Attr -> Bool

(<=) :: Attr -> Attr -> Bool

(>) :: Attr -> Attr -> Bool

(>=) :: Attr -> Attr -> Bool

max :: Attr -> Attr -> Attr

min :: Attr -> Attr -> Attr

Show Attr Source # 
Instance details

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Attr -> ShowS

show :: Attr -> String

showList :: [Attr] -> ShowS

PP Attr Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Attr -> Doc Source #

data Command Source #

Instances

Instances details
Data Command Source # 
Instance details

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

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

toConstr :: Command -> Constr

dataTypeOf :: Command -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Command -> Command

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

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

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

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

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

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

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

PP Command Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Command -> Doc Source #

data Option Source #

Instances

Instances details
Data Option Source # 
Instance details

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

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

toConstr :: Option -> Constr

dataTypeOf :: Option -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Option -> Option

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

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

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

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

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

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

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

PP Option Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Option -> Doc Source #

data InfoFlag Source #

Instances

Instances details
Data InfoFlag Source # 
Instance details

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

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

toConstr :: InfoFlag -> Constr

dataTypeOf :: InfoFlag -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> InfoFlag -> InfoFlag

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

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

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

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

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

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

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

PP InfoFlag Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: InfoFlag -> Doc Source #

app :: Ident -> [Expr] -> Expr Source #

class PP t where Source #

Methods

pp :: t -> Doc Source #

Instances

Instances details
PP Bool Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Bool -> Doc Source #

PP Integer Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Integer -> Doc Source #

PP Script Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Script -> Doc Source #

PP Command Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Command -> Doc Source #

PP InfoFlag Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: InfoFlag -> Doc Source #

PP Option Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Option -> Doc Source #

PP Attr Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Attr -> Doc Source #

PP Expr Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Expr -> Doc Source #

PP Type Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Type -> Doc Source #

PP Literal Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Literal -> Doc Source #

PP Defn Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Defn -> Doc Source #

PP Binder Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Binder -> Doc Source #

PP Quant Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Quant -> Doc Source #

PP Ident Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Ident -> Doc Source #

PP Name Source # 
Instance details

Defined in SMTLib2.PP

Methods

pp :: Name -> Doc Source #