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

Safe Haskell | Safe
Language | Haskell98

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

- bindVar :: Name
- bindType :: Type

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

- defVar :: Name
- defExpr :: Expr

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

- attrName :: Name
- attrVal :: Maybe AttrVal

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

type AttrVal = Expr Source #

data Command Source #

Constructors

CmdSetLogic Name |
CmdSetOption Option |
CmdSetInfo Attr |
CmdDeclareType Name Integer |
CmdDefineType Name [Name] Type |
CmdDeclareConst 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

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 #

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

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 #

Constructors

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

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