SMTLib2

Documentation

newtype Script

Constructors

Script [Command]

Instances

PP Script

Defined in SMTLib2.PP

Methods

pp :: Script -> Doc

data Binder

Constructors

Bind

Fields

• bindVar :: Name
• bindType :: Type

Instances

Eq Binder

Defined in SMTLib2.AST

Methods

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

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

Data Binder

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Binder -> ShowS

show :: Binder -> String

showList :: [Binder] -> ShowS

PP Binder

Defined in SMTLib2.PP

Methods

pp :: Binder -> Doc

data Defn

Constructors

Defn

Fields

• defVar :: Name
• defExpr :: Expr

Instances

Eq Defn

Defined in SMTLib2.AST

Methods

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

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

Data Defn

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Defn -> ShowS

show :: Defn -> String

showList :: [Defn] -> ShowS

PP Defn

Defined in SMTLib2.PP

Methods

pp :: Defn -> Doc

data Type

Constructors

TApp Ident [Type]

TVar Name

Instances

Eq Type

Defined in SMTLib2.AST

Methods

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

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

Data Type

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

IsString Type

Defined in SMTLib2.AST

Methods

fromString :: String -> Type

PP Type

Defined in SMTLib2.PP

Methods

pp :: Type -> Doc

data Expr

Constructors

Lit Literal

App Ident (Maybe Type) [Expr]

Quant Quant [Binder] Expr

Let [Defn] Expr

Annot Expr [Attr]

Instances

Eq Expr

Defined in SMTLib2.AST

Methods

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

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

Fractional Expr

Defined in SMTLib2.AST

Methods

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

recip :: Expr -> Expr

fromRational :: Rational -> Expr

Data Expr

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

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

IsString Expr

Defined in SMTLib2.AST

Methods

fromString :: String -> Expr

PP Expr

Defined in SMTLib2.PP

Methods

pp :: Expr -> Doc

newtype Name

Constructors

N String

Instances

Eq Name

Defined in SMTLib2.AST

Methods

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

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

Data Name

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

IsString Name

Defined in SMTLib2.AST

Methods

fromString :: String -> Name

PP Name

Defined in SMTLib2.PP

Methods

pp :: Name -> Doc

data Ident

Constructors

I Name [Integer]

Instances

Eq Ident

Defined in SMTLib2.AST

Methods

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

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

Data Ident

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Ident -> ShowS

show :: Ident -> String

showList :: [Ident] -> ShowS

IsString Ident

Defined in SMTLib2.AST

Methods

fromString :: String -> Ident

PP Ident

Defined in SMTLib2.PP

Methods

pp :: Ident -> Doc

data Quant

Constructors

Exists

Forall

Instances

Eq Quant

Defined in SMTLib2.AST

Methods

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

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

Data Quant

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Quant -> ShowS

show :: Quant -> String

showList :: [Quant] -> ShowS

PP Quant

Defined in SMTLib2.PP

Methods

pp :: Quant -> Doc

data Literal

Constructors

LitBV Integer Integer

value, width (in bits)

LitNum Integer

LitFrac Rational

LitStr String

Instances

Eq Literal

Defined in SMTLib2.AST

Methods

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

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

Data Literal

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Literal -> ShowS

show :: Literal -> String

showList :: [Literal] -> ShowS

PP Literal

Defined in SMTLib2.PP

Methods

pp :: Literal -> Doc

data Attr

Constructors

Attr

Fields

• attrName :: Name
• attrVal :: Maybe AttrVal

Instances

Eq Attr

Defined in SMTLib2.AST

Methods

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

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

Data Attr

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

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

Defined in SMTLib2.AST

Methods

showsPrec :: Int -> Attr -> ShowS

show :: Attr -> String

showList :: [Attr] -> ShowS

PP Attr

Defined in SMTLib2.PP

Methods

pp :: Attr -> Doc

type AttrVal = Expr

data Command

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

Data Command

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

Defined in SMTLib2.PP

Methods

pp :: Command -> Doc

data Option

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

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

Defined in SMTLib2.PP

Methods

pp :: Option -> Doc

data InfoFlag

Constructors

InfoAllStatistics

InfoErrorBehavior

InfoName

InfoAuthors

InfoVersion

InfoStatus

InfoReasonUnknown

InfoAttr Attr

Instances

Data InfoFlag

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

Defined in SMTLib2.PP

Methods

pp :: InfoFlag -> Doc

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

class PP t where

Methods

pp :: t -> Doc

Instances

PP Bool

Defined in SMTLib2.PP

Methods

pp :: Bool -> Doc

PP Integer

Defined in SMTLib2.PP

Methods

pp :: Integer -> Doc

PP Script

Defined in SMTLib2.PP

Methods

pp :: Script -> Doc

PP Command

Defined in SMTLib2.PP

Methods

pp :: Command -> Doc

PP InfoFlag

Defined in SMTLib2.PP

Methods

pp :: InfoFlag -> Doc

PP Option

Defined in SMTLib2.PP

Methods

pp :: Option -> Doc

PP Attr

Defined in SMTLib2.PP

Methods

pp :: Attr -> Doc

PP Expr

Defined in SMTLib2.PP

Methods

pp :: Expr -> Doc

PP Type

Defined in SMTLib2.PP

Methods

pp :: Type -> Doc

PP Literal

Defined in SMTLib2.PP

Methods

pp :: Literal -> Doc

PP Defn

Defined in SMTLib2.PP

Methods

pp :: Defn -> Doc

PP Binder

Defined in SMTLib2.PP

Methods

pp :: Binder -> Doc

PP Quant

Defined in SMTLib2.PP

Methods

pp :: Quant -> Doc

PP Ident

Defined in SMTLib2.PP

Methods

pp :: Ident -> Doc

PP Name

Defined in SMTLib2.PP

Methods

pp :: Name -> Doc