SMTLib1

Documentation

newtype Name

Constructors

N String

Instances

Eq Name

Methods

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

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

Data Name

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

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

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

IsString Name

Methods

fromString :: String -> Name

PP Name

Methods

pp :: Name -> Doc

data Ident

Constructors

I Name [Integer]

Instances

Eq Ident

Methods

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

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

Data Ident

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

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

Methods

showsPrec :: Int -> Ident -> ShowS

show :: Ident -> String

showList :: [Ident] -> ShowS

IsString Ident

Methods

fromString :: String -> Ident

PP Ident

Methods

pp :: Ident -> Doc

data Quant

Constructors

Exists

Forall

Instances

Eq Quant

Methods

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

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

Data Quant

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

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

Methods

showsPrec :: Int -> Quant -> ShowS

show :: Quant -> String

showList :: [Quant] -> ShowS

PP Quant

Methods

pp :: Quant -> Doc

data Conn

Constructors

Not

Implies

And

Or

Xor

Iff

IfThenElse

Instances

Eq Conn

Methods

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

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

Data Conn

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

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

Methods

showsPrec :: Int -> Conn -> ShowS

show :: Conn -> String

showList :: [Conn] -> ShowS

PP Conn

Methods

pp :: Conn -> Doc

data Formula

Constructors

FTrue

FFalse

FPred Ident [Term]

FVar Name

Conn Conn [Formula]

Quant Quant [Binder] Formula

Let Name Term Formula

FLet Name Formula Formula

FAnnot Formula [Annot]

Instances

Eq Formula

Methods

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

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

Data Formula

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

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

Methods

showsPrec :: Int -> Formula -> ShowS

show :: Formula -> String

showList :: [Formula] -> ShowS

PP Formula

Methods

pp :: Formula -> Doc

type Sort = Ident

data Binder

Constructors

Bind

Fields

• bindVar :: Name
• bindSort :: Sort

Instances

Eq Binder

Methods

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

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

Data Binder

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

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

Methods

showsPrec :: Int -> Binder -> ShowS

show :: Binder -> String

showList :: [Binder] -> ShowS

PP Binder

Methods

pp :: Binder -> Doc

data Term

Constructors

Var Name

App Ident [Term]

Lit Literal

ITE Formula Term Term

TAnnot Term [Annot]

Instances

Eq Term

Methods

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

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

Fractional Term

Methods

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

recip :: Term -> Term

fromRational :: Rational -> Term

Data Term

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

Methods

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

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

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

negate :: Term -> Term

abs :: Term -> Term

signum :: Term -> Term

fromInteger :: Integer -> Term

Ord Term

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

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

IsString Term

Methods

fromString :: String -> Term

PP Term

Methods

pp :: Term -> Doc

data Literal

Constructors

LitNum Integer

LitFrac Rational

LitStr String

Instances

Eq Literal

Methods

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

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

Data Literal

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

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

Methods

showsPrec :: Int -> Literal -> ShowS

show :: Literal -> String

showList :: [Literal] -> ShowS

PP Literal

Methods

pp :: Literal -> Doc

data Annot

Constructors

Attr

Fields

• attrName :: Name
• attrVal :: Maybe String

Instances

Eq Annot

Methods

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

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

Data Annot

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

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

Methods

showsPrec :: Int -> Annot -> ShowS

show :: Annot -> String

showList :: [Annot] -> ShowS

PP Annot

Methods

pp :: Annot -> Doc

data FunDecl

Constructors

FunDecl

Fields

• funName :: Ident
• funArgs :: [Sort]
• funRes :: Sort
• funAnnots :: [Annot]

Instances

Data FunDecl

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

Methods

pp :: FunDecl -> Doc

data PredDecl

Constructors

PredDecl

Fields

• predName :: Ident
• predArgs :: [Sort]
• predAnnots :: [Annot]

Instances

Data PredDecl

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

Methods

pp :: PredDecl -> Doc

data Status

Constructors

Sat

Unsat

Unknown

Instances

Data Status

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

Methods

pp :: Status -> Doc

data Command

Constructors

CmdLogic Ident

CmdAssumption Formula

CmdFormula Formula

CmdStatus Status

CmdExtraSorts [Sort]

CmdExtraFuns [FunDecl]

CmdExtraPreds [PredDecl]

CmdNotes String

CmdAnnot Annot

Instances

Data Command

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

Methods

pp :: Command -> Doc

data Script

Constructors

Script

Fields

• scrName :: Ident
• scrCommands :: [Command]

Instances

PP Script

Methods

pp :: Script -> Doc

(===) :: Term -> Term -> Formula

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

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

For Int

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

For Int

tInt :: Sort

funDef :: Ident -> [Sort] -> Sort -> Command

constDef :: Ident -> Sort -> Command

logic :: Ident -> Command

assume :: Formula -> Command

goal :: Formula -> Command

class PP t where

Minimal complete definition

pp

Methods

pp :: t -> Doc

Instances

PP Script

Methods

pp :: Script -> Doc

PP Command

Methods

pp :: Command -> Doc

PP Status

Methods

pp :: Status -> Doc

PP PredDecl

Methods

pp :: PredDecl -> Doc

PP FunDecl

Methods

pp :: FunDecl -> Doc

PP Annot

Methods

pp :: Annot -> Doc

PP Literal

Methods

pp :: Literal -> Doc

PP Term

Methods

pp :: Term -> Doc

PP Binder

Methods

pp :: Binder -> Doc

PP Formula

Methods

pp :: Formula -> Doc

PP Conn

Methods

pp :: Conn -> Doc

PP Quant

Methods

pp :: Quant -> Doc

PP Ident

Methods

pp :: Ident -> Doc

PP Name

Methods

pp :: Name -> Doc