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 #