smtLib-1.0.9: A library for working with the SMTLIB format.

Safe Haskell | Safe
Language | Haskell98

SMTLib2

# Documentation

newtype Script Source #

Constructors

Script [Command] |

Instances

PP Script Source # |
Instance details Defined in SMTLib2.PP Methods pp :: Script -> Doc Source #

data Binder Source #

Constructors

Bind |

Fields

- bindVar :: Name
- bindType :: Type

Instances

Eq Binder Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Binder -> Binder -> Bool Source # (/=) :: Binder -> Binder -> Bool Source #
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 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 :: (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 #

Ord Binder Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Binder -> Binder -> Ordering Source # (<) :: Binder -> Binder -> Bool Source # (<=) :: Binder -> Binder -> Bool Source # (>) :: Binder -> Binder -> Bool Source # (>=) :: Binder -> Binder -> Bool Source # max :: Binder -> Binder -> Binder Source # min :: Binder -> Binder -> Binder Source #
Show Binder Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Binder -> ShowS Source # show :: Binder -> String Source # showList :: [Binder] -> ShowS Source #
PP Binder Source # |
Instance details Defined in SMTLib2.PP Methods pp :: Binder -> Doc Source #

data Defn Source #

Constructors

Defn |

Fields

- defVar :: Name
- defExpr :: Expr

Instances

Eq Defn Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Defn -> Defn -> Bool Source # (/=) :: Defn -> Defn -> Bool Source #
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 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 :: (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 #

Ord Defn Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Defn -> Defn -> Ordering Source # (<) :: Defn -> Defn -> Bool Source # (<=) :: Defn -> Defn -> Bool Source # (>) :: Defn -> Defn -> Bool Source # (>=) :: Defn -> Defn -> Bool Source # max :: Defn -> Defn -> Defn Source # min :: Defn -> Defn -> Defn Source #
Show Defn Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Defn -> ShowS Source # show :: Defn -> String Source # showList :: [Defn] -> ShowS Source #
PP Defn Source # |
Instance details Defined in SMTLib2.PP Methods pp :: Defn -> Doc Source #

data Type Source #

Constructors

TApp Ident [Type] |
TVar Name |

Instances

Eq Type Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Type -> Type -> Bool Source # (/=) :: Type -> Type -> Bool Source #
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 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 :: (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 #

Ord Type Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Type -> Type -> Ordering Source # (<) :: Type -> Type -> Bool Source # (<=) :: Type -> Type -> Bool Source # (>) :: Type -> Type -> Bool Source # (>=) :: Type -> Type -> Bool Source # max :: Type -> Type -> Type Source # min :: Type -> Type -> Type Source #
Show Type Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Type -> ShowS Source # show :: Type -> String Source # showList :: [Type] -> ShowS Source #
IsString Type Source # |
Instance details Defined in SMTLib2.AST Methods fromString :: String -> Type Source #
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

Eq Expr Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Expr -> Expr -> Bool Source # (/=) :: Expr -> Expr -> Bool Source #
Fractional Expr Source # |
Instance details Defined in SMTLib2.AST Methods (/) :: Expr -> Expr -> Expr Source # recip :: Expr -> Expr Source # fromRational :: Rational -> Expr Source #
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 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 :: (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 #

Num Expr Source # |
Instance details Defined in SMTLib2.AST Methods (+) :: Expr -> Expr -> Expr Source # (-) :: Expr -> Expr -> Expr Source # (*) :: Expr -> Expr -> Expr Source # negate :: Expr -> Expr Source # abs :: Expr -> Expr Source # signum :: Expr -> Expr Source # fromInteger :: Integer -> Expr Source #
Ord Expr Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Expr -> Expr -> Ordering Source # (<) :: Expr -> Expr -> Bool Source # (<=) :: Expr -> Expr -> Bool Source # (>) :: Expr -> Expr -> Bool Source # (>=) :: Expr -> Expr -> Bool Source # max :: Expr -> Expr -> Expr Source # min :: Expr -> Expr -> Expr Source #
Show Expr Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Expr -> ShowS Source # show :: Expr -> String Source # showList :: [Expr] -> ShowS Source #
IsString Expr Source # |
Instance details Defined in SMTLib2.AST Methods fromString :: String -> Expr Source #
PP Expr Source # |
Instance details Defined in SMTLib2.PP Methods pp :: Expr -> Doc Source #

newtype Name Source #

Constructors

N String |

Instances

Eq Name Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Name -> Name -> Bool Source # (/=) :: Name -> Name -> Bool Source #
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 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 :: (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 #

Ord Name Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
Show Name Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
IsString Name Source # |
Instance details Defined in SMTLib2.AST Methods fromString :: String -> Name Source #
PP Name Source # |
Instance details Defined in SMTLib2.PP Methods pp :: Name -> Doc Source #

data Ident Source #

Constructors

I Name [Integer] |

Instances

Eq Ident Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Ident -> Ident -> Bool Source # (/=) :: Ident -> Ident -> Bool Source #
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 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 :: (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 #

Ord Ident Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Ident -> Ident -> Ordering Source # (<) :: Ident -> Ident -> Bool Source # (<=) :: Ident -> Ident -> Bool Source # (>) :: Ident -> Ident -> Bool Source # (>=) :: Ident -> Ident -> Bool Source # max :: Ident -> Ident -> Ident Source # min :: Ident -> Ident -> Ident Source #
Show Ident Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Ident -> ShowS Source # show :: Ident -> String Source # showList :: [Ident] -> ShowS Source #
IsString Ident Source # |
Instance details Defined in SMTLib2.AST Methods fromString :: String -> Ident Source #
PP Ident Source # |
Instance details Defined in SMTLib2.PP Methods pp :: Ident -> Doc Source #

data Quant Source #

Constructors

Exists |
Forall |

Instances

Eq Quant Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Quant -> Quant -> Bool Source # (/=) :: Quant -> Quant -> Bool Source #
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 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 :: (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 #

Ord Quant Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Quant -> Quant -> Ordering Source # (<) :: Quant -> Quant -> Bool Source # (<=) :: Quant -> Quant -> Bool Source # (>) :: Quant -> Quant -> Bool Source # (>=) :: Quant -> Quant -> Bool Source # max :: Quant -> Quant -> Quant Source # min :: Quant -> Quant -> Quant Source #
Show Quant Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Quant -> ShowS Source # show :: Quant -> String Source # showList :: [Quant] -> ShowS Source #
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

Eq Literal Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Literal -> Literal -> Bool Source # (/=) :: Literal -> Literal -> Bool Source #
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 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 :: (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 #

Ord Literal Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Literal -> Literal -> Ordering Source # (<) :: Literal -> Literal -> Bool Source # (<=) :: Literal -> Literal -> Bool Source # (>) :: Literal -> Literal -> Bool Source # (>=) :: Literal -> Literal -> Bool Source # max :: Literal -> Literal -> Literal Source # min :: Literal -> Literal -> Literal Source #
Show Literal Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Literal -> ShowS Source # show :: Literal -> String Source # showList :: [Literal] -> ShowS Source #
PP Literal Source # |
Instance details Defined in SMTLib2.PP Methods pp :: Literal -> Doc Source #

data Attr Source #

Constructors

Attr |

Fields

- attrName :: Name
- attrVal :: Maybe AttrVal

Instances

Eq Attr Source # |
Instance details Defined in SMTLib2.AST Methods (==) :: Attr -> Attr -> Bool Source # (/=) :: Attr -> Attr -> Bool Source #
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 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 :: (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 #

Ord Attr Source # |
Instance details Defined in SMTLib2.AST Methods compare :: Attr -> Attr -> Ordering Source # (<) :: Attr -> Attr -> Bool Source # (<=) :: Attr -> Attr -> Bool Source # (>) :: Attr -> Attr -> Bool Source # (>=) :: Attr -> Attr -> Bool Source # max :: Attr -> Attr -> Attr Source # min :: Attr -> Attr -> Attr Source #
Show Attr Source # |
Instance details Defined in SMTLib2.AST Methods showsPrec :: Int -> Attr -> ShowS Source # show :: Attr -> String Source # showList :: [Attr] -> ShowS Source #
PP Attr Source # |
Instance details Defined in SMTLib2.PP Methods pp :: Attr -> Doc Source #

type AttrVal = Expr Source #

data Command Source #

Constructors

CmdSetLogic Name |
CmdSetOption Option |
CmdSetInfo Attr |
CmdDeclareType Name Integer |
CmdDefineType Name [Name] Type |
CmdDeclareFun Name [Type] Type |
CmdDefineFun Name [Binder] Type Expr |
CmdPush Integer |
CmdPop Integer |
CmdAssert Expr |
CmdCheckSat |
CmdGetAssertions |
CmdGetValue [Expr] |
CmdGetProof |
CmdGetUnsatCore |
CmdGetInfo InfoFlag |
CmdGetOption Name |
CmdComment String |
CmdExit |

Instances

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 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 :: (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 # |
Instance details Defined in SMTLib2.PP Methods pp :: Command -> Doc Source #

data Option Source #

Constructors

OptPrintSuccess Bool |
OptExpandDefinitions Bool |
OptInteractiveMode Bool |
OptProduceProofs Bool |
OptProduceUnsatCores Bool |
OptProduceModels Bool |
OptProduceAssignments Bool |
OptRegularOutputChannel String |
OptDiagnosticOutputChannel String |
OptRandomSeed Integer |
OptVerbosity Integer |
OptAttr Attr |

Instances

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 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 :: (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 # |
Instance details Defined in SMTLib2.PP Methods pp :: Option -> Doc Source #

data InfoFlag Source #

Constructors

InfoAllStatistics |
InfoErrorBehavior |
InfoName |
InfoAuthors |
InfoVersion |
InfoStatus |
InfoReasonUnknown |
InfoAttr Attr |

Instances

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 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 :: (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 # |
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

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 #