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

SMTLib1

Synopsis

Documentation

newtype Name Source #

Constructors

N String 

Instances

Instances details
Eq Name Source # 
Instance details

Defined in SMTLib1.AST

Methods

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

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

Data Name Source # 
Instance details

Defined in SMTLib1.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 SMTLib1.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 SMTLib1.AST

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

IsString Name Source # 
Instance details

Defined in SMTLib1.AST

Methods

fromString :: String -> Name

PP Name Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Name -> Doc Source #

data Ident Source #

Constructors

I Name [Integer] 

Instances

Instances details
Eq Ident Source # 
Instance details

Defined in SMTLib1.AST

Methods

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

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

Data Ident Source # 
Instance details

Defined in SMTLib1.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 SMTLib1.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 SMTLib1.AST

Methods

showsPrec :: Int -> Ident -> ShowS

show :: Ident -> String

showList :: [Ident] -> ShowS

IsString Ident Source # 
Instance details

Defined in SMTLib1.AST

Methods

fromString :: String -> Ident

PP Ident Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Ident -> Doc Source #

data Quant Source #

Constructors

Exists 
Forall 

Instances

Instances details
Eq Quant Source # 
Instance details

Defined in SMTLib1.AST

Methods

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

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

Data Quant Source # 
Instance details

Defined in SMTLib1.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 SMTLib1.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 SMTLib1.AST

Methods

showsPrec :: Int -> Quant -> ShowS

show :: Quant -> String

showList :: [Quant] -> ShowS

PP Quant Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Quant -> Doc Source #

data Conn Source #

Constructors

Not 
Implies 
And 
Or 
Xor 
Iff 
IfThenElse 

Instances

Instances details
Eq Conn Source # 
Instance details

Defined in SMTLib1.AST

Methods

(==) :: Conn -> Conn -> Bool

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

Data Conn Source # 
Instance details

Defined in SMTLib1.AST

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Conn -> c Conn

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Conn

toConstr :: Conn -> Constr

dataTypeOf :: Conn -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Conn)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conn)

gmapT :: (forall b. Data b => b -> b) -> Conn -> Conn

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r

gmapQ :: (forall d. Data d => d -> u) -> Conn -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Conn -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Conn -> m Conn

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Conn -> m Conn

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Conn -> m Conn

Ord Conn Source # 
Instance details

Defined in SMTLib1.AST

Methods

compare :: Conn -> Conn -> Ordering

(<) :: Conn -> Conn -> Bool

(<=) :: Conn -> Conn -> Bool

(>) :: Conn -> Conn -> Bool

(>=) :: Conn -> Conn -> Bool

max :: Conn -> Conn -> Conn

min :: Conn -> Conn -> Conn

Show Conn Source # 
Instance details

Defined in SMTLib1.AST

Methods

showsPrec :: Int -> Conn -> ShowS

show :: Conn -> String

showList :: [Conn] -> ShowS

PP Conn Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Conn -> Doc Source #

data Formula Source #

Instances

Instances details
Eq Formula Source # 
Instance details

Defined in SMTLib1.AST

Methods

(==) :: Formula -> Formula -> Bool

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

Data Formula Source # 
Instance details

Defined in SMTLib1.AST

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formula -> c Formula

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Formula

toConstr :: Formula -> Constr

dataTypeOf :: Formula -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Formula)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)

gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r

gmapQ :: (forall d. Data d => d -> u) -> Formula -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Formula -> m Formula

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula

Ord Formula Source # 
Instance details

Defined in SMTLib1.AST

Methods

compare :: Formula -> Formula -> Ordering

(<) :: Formula -> Formula -> Bool

(<=) :: Formula -> Formula -> Bool

(>) :: Formula -> Formula -> Bool

(>=) :: Formula -> Formula -> Bool

max :: Formula -> Formula -> Formula

min :: Formula -> Formula -> Formula

Show Formula Source # 
Instance details

Defined in SMTLib1.AST

Methods

showsPrec :: Int -> Formula -> ShowS

show :: Formula -> String

showList :: [Formula] -> ShowS

PP Formula Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Formula -> Doc Source #

data Binder Source #

Constructors

Bind 

Fields

Instances

Instances details
Eq Binder Source # 
Instance details

Defined in SMTLib1.AST

Methods

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

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

Data Binder Source # 
Instance details

Defined in SMTLib1.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 SMTLib1.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 SMTLib1.AST

Methods

showsPrec :: Int -> Binder -> ShowS

show :: Binder -> String

showList :: [Binder] -> ShowS

PP Binder Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Binder -> Doc Source #

data Term Source #

Instances

Instances details
Eq Term Source # 
Instance details

Defined in SMTLib1.AST

Methods

(==) :: Term -> Term -> Bool

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

Fractional Term Source # 
Instance details

Defined in SMTLib1.AST

Methods

(/) :: Term -> Term -> Term

recip :: Term -> Term

fromRational :: Rational -> Term

Data Term Source # 
Instance details

Defined in SMTLib1.AST

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term

toConstr :: Term -> Constr

dataTypeOf :: Term -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)

gmapT :: (forall b. Data b => b -> b) -> Term -> Term

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

Num Term Source # 
Instance details

Defined in SMTLib1.AST

Methods

(+) :: Term -> Term -> Term

(-) :: Term -> Term -> Term

(*) :: Term -> Term -> Term

negate :: Term -> Term

abs :: Term -> Term

signum :: Term -> Term

fromInteger :: Integer -> Term

Ord Term Source # 
Instance details

Defined in SMTLib1.AST

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Show Term Source # 
Instance details

Defined in SMTLib1.AST

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

IsString Term Source # 
Instance details

Defined in SMTLib1.AST

Methods

fromString :: String -> Term

PP Term Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Term -> Doc Source #

data Literal Source #

Constructors

LitNum Integer 
LitFrac Rational 
LitStr String 

Instances

Instances details
Eq Literal Source # 
Instance details

Defined in SMTLib1.AST

Methods

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

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

Data Literal Source # 
Instance details

Defined in SMTLib1.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 SMTLib1.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 SMTLib1.AST

Methods

showsPrec :: Int -> Literal -> ShowS

show :: Literal -> String

showList :: [Literal] -> ShowS

PP Literal Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Literal -> Doc Source #

data Annot Source #

Constructors

Attr 

Fields

Instances

Instances details
Eq Annot Source # 
Instance details

Defined in SMTLib1.AST

Methods

(==) :: Annot -> Annot -> Bool

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

Data Annot Source # 
Instance details

Defined in SMTLib1.AST

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annot -> c Annot

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annot

toConstr :: Annot -> Constr

dataTypeOf :: Annot -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Annot)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annot)

gmapT :: (forall b. Data b => b -> b) -> Annot -> Annot

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r

gmapQ :: (forall d. Data d => d -> u) -> Annot -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Annot -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annot -> m Annot

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot -> m Annot

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot -> m Annot

Ord Annot Source # 
Instance details

Defined in SMTLib1.AST

Methods

compare :: Annot -> Annot -> Ordering

(<) :: Annot -> Annot -> Bool

(<=) :: Annot -> Annot -> Bool

(>) :: Annot -> Annot -> Bool

(>=) :: Annot -> Annot -> Bool

max :: Annot -> Annot -> Annot

min :: Annot -> Annot -> Annot

Show Annot Source # 
Instance details

Defined in SMTLib1.AST

Methods

showsPrec :: Int -> Annot -> ShowS

show :: Annot -> String

showList :: [Annot] -> ShowS

PP Annot Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Annot -> Doc Source #

data FunDecl Source #

Constructors

FunDecl 

Fields

Instances

Instances details
Data FunDecl Source # 
Instance details

Defined in SMTLib1.AST

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunDecl -> c FunDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunDecl

toConstr :: FunDecl -> Constr

dataTypeOf :: FunDecl -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunDecl)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl)

gmapT :: (forall b. Data b => b -> b) -> FunDecl -> FunDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunDecl -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> FunDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl

PP FunDecl Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: FunDecl -> Doc Source #

data PredDecl Source #

Constructors

PredDecl 

Fields

Instances

Instances details
Data PredDecl Source # 
Instance details

Defined in SMTLib1.AST

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredDecl -> c PredDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredDecl

toConstr :: PredDecl -> Constr

dataTypeOf :: PredDecl -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PredDecl)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl)

gmapT :: (forall b. Data b => b -> b) -> PredDecl -> PredDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredDecl -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> PredDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PredDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl

PP PredDecl Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: PredDecl -> Doc Source #

data Status Source #

Constructors

Sat 
Unsat 
Unknown 

Instances

Instances details
Data Status Source # 
Instance details

Defined in SMTLib1.AST

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Status -> c Status

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Status

toConstr :: Status -> Constr

dataTypeOf :: Status -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Status)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status)

gmapT :: (forall b. Data b => b -> b) -> Status -> Status

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r

gmapQ :: (forall d. Data d => d -> u) -> Status -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Status -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Status -> m Status

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Status -> m Status

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Status -> m Status

PP Status Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Status -> Doc Source #

data Command Source #

Instances

Instances details
Data Command Source # 
Instance details

Defined in SMTLib1.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 SMTLib1.PP

Methods

pp :: Command -> Doc Source #

data Script Source #

Constructors

Script 

Fields

Instances

Instances details
PP Script Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Script -> Doc Source #

(.<.) :: Term -> Term -> Formula Source #

For Int

(.>.) :: Term -> Term -> Formula Source #

For Int

class PP t where Source #

Methods

pp :: t -> Doc Source #

Instances

Instances details
PP Script Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Script -> Doc Source #

PP Command Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Command -> Doc Source #

PP Status Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Status -> Doc Source #

PP PredDecl Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: PredDecl -> Doc Source #

PP FunDecl Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: FunDecl -> Doc Source #

PP Annot Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Annot -> Doc Source #

PP Literal Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Literal -> Doc Source #

PP Term Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Term -> Doc Source #

PP Binder Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Binder -> Doc Source #

PP Formula Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Formula -> Doc Source #

PP Conn Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Conn -> Doc Source #

PP Quant Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Quant -> Doc Source #

PP Ident Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Ident -> Doc Source #

PP Name Source # 
Instance details

Defined in SMTLib1.PP

Methods

pp :: Name -> Doc Source #