Safe Haskell	Safe
Language	Haskell98

SMTLib2

Documentation

newtype Script Source #

Constructors

Script [Command]

Instances

PP Script Source #
Methods pp :: Script -> Doc Source #

data Binder Source #

Constructors

Bind
Fields bindVar :: Name bindType :: Type

Instances

Eq Binder Source #
Methods (==) :: Binder -> Binder -> Bool # (/=) :: Binder -> Binder -> Bool #
Data Binder Source #
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 Source #
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 #
Methods showsPrec :: Int -> Binder -> ShowS # show :: Binder -> String # showList :: [Binder] -> ShowS #
PP Binder Source #
Methods pp :: Binder -> Doc Source #

data Defn Source #

Constructors

Defn
Fields defVar :: Name defExpr :: Expr

Instances

Eq Defn Source #
Methods (==) :: Defn -> Defn -> Bool # (/=) :: Defn -> Defn -> Bool #
Data Defn Source #
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 Source #
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 #
Methods showsPrec :: Int -> Defn -> ShowS # show :: Defn -> String # showList :: [Defn] -> ShowS #
PP Defn Source #
Methods pp :: Defn -> Doc Source #

data Type Source #

Constructors

TApp Ident [Type]
TVar Name

Instances

Eq Type Source #
Methods (==) :: Type -> Type -> Bool # (/=) :: Type -> Type -> Bool #
Data Type Source #
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 Source #
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 #
Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
IsString Type Source #
Methods fromString :: String -> Type #
PP Type Source #
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 #
Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
Fractional Expr Source #
Methods (/) :: Expr -> Expr -> Expr # recip :: Expr -> Expr # fromRational :: Rational -> Expr #
Data Expr Source #
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 Source #
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 #
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 #
Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
IsString Expr Source #
Methods fromString :: String -> Expr #
PP Expr Source #
Methods pp :: Expr -> Doc Source #

newtype Name Source #

Constructors

N String

Instances

Eq Name Source #
Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Data Name Source #
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 Source #
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 #
Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
IsString Name Source #
Methods fromString :: String -> Name #
PP Name Source #
Methods pp :: Name -> Doc Source #

data Ident Source #

Constructors

I Name [Integer]

Instances

Eq Ident Source #
Methods (==) :: Ident -> Ident -> Bool # (/=) :: Ident -> Ident -> Bool #
Data Ident Source #
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 Source #
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 #
Methods showsPrec :: Int -> Ident -> ShowS # show :: Ident -> String # showList :: [Ident] -> ShowS #
IsString Ident Source #
Methods fromString :: String -> Ident #
PP Ident Source #
Methods pp :: Ident -> Doc Source #

data Quant Source #

Constructors

Exists
Forall

Instances

Eq Quant Source #
Methods (==) :: Quant -> Quant -> Bool # (/=) :: Quant -> Quant -> Bool #
Data Quant Source #
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 Source #
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 #
Methods showsPrec :: Int -> Quant -> ShowS # show :: Quant -> String # showList :: [Quant] -> ShowS #
PP Quant Source #
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 #
Methods (==) :: Literal -> Literal -> Bool # (/=) :: Literal -> Literal -> Bool #
Data Literal Source #
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 Source #
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 #
Methods showsPrec :: Int -> Literal -> ShowS # show :: Literal -> String # showList :: [Literal] -> ShowS #
PP Literal Source #
Methods pp :: Literal -> Doc Source #

data Attr Source #

Constructors

Attr
Fields attrName :: Name attrVal :: Maybe AttrVal

Instances

Eq Attr Source #
Methods (==) :: Attr -> Attr -> Bool # (/=) :: Attr -> Attr -> Bool #
Data Attr Source #
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 Source #
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 #
Methods showsPrec :: Int -> Attr -> ShowS # show :: Attr -> String # showList :: [Attr] -> ShowS #
PP Attr Source #
Methods pp :: Attr -> Doc Source #

type AttrVal = Expr Source #

data Command Source #

Instances

Data Command Source #
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 Source #
Methods pp :: Command -> Doc Source #

data Option Source #

Instances

Data Option Source #
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 Source #
Methods pp :: Option -> Doc Source #

data InfoFlag Source #

Constructors

InfoAllStatistics
InfoErrorBehavior
InfoName
InfoAuthors
InfoVersion
InfoStatus
InfoReasonUnknown
InfoAttr Attr

Instances

Data InfoFlag Source #
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 Source #
Methods pp :: InfoFlag -> Doc Source #

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

class PP t where Source #

Minimal complete definition

pp

Methods

pp :: t -> Doc Source #

Instances

PP Bool Source #
Methods pp :: Bool -> Doc Source #
PP Integer Source #
Methods pp :: Integer -> Doc Source #
PP Script Source #
Methods pp :: Script -> Doc Source #
PP Command Source #
Methods pp :: Command -> Doc Source #
PP InfoFlag Source #
Methods pp :: InfoFlag -> Doc Source #
PP Option Source #
Methods pp :: Option -> Doc Source #
PP Attr Source #
Methods pp :: Attr -> Doc Source #
PP Expr Source #
Methods pp :: Expr -> Doc Source #
PP Type Source #
Methods pp :: Type -> Doc Source #
PP Literal Source #
Methods pp :: Literal -> Doc Source #
PP Defn Source #
Methods pp :: Defn -> Doc Source #
PP Binder Source #
Methods pp :: Binder -> Doc Source #
PP Quant Source #
Methods pp :: Quant -> Doc Source #
PP Ident Source #
Methods pp :: Ident -> Doc Source #
PP Name Source #
Methods pp :: Name -> Doc Source #

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

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