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

Safe Haskell | Safe
Language | Haskell98

SMTLib1

Synopsis

- newtype Name = N String
- data Ident = I Name [Integer]
- data Quant
  - = Exists
  - | Forall
- data Conn
  - = Not
  - | Implies
  - | And
  - | Or
  - | Xor
  - | Iff
  - | IfThenElse
- data Formula
  - = 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]
- type Sort = Ident
- data Binder = Bind {
  - bindVar :: Name
  - bindSort :: Sort
  }
- data Term
  - = Var Name
  - | App Ident [Term]
  - | Lit Literal
  - | ITE Formula Term Term
  - | TAnnot Term [Annot]
- data Literal
  - = LitNum Integer
  - | LitFrac Rational
  - | LitStr String
- data Annot = Attr {
  - attrName :: Name
  - attrVal :: Maybe String
  }
- data FunDecl = FunDecl {
  - funName :: Ident
  - funArgs :: [Sort]
  - funRes :: Sort
  - funAnnots :: [Annot]
  }
- data PredDecl = PredDecl {
  - predName :: Ident
  - predArgs :: [Sort]
  - predAnnots :: [Annot]
  }
- data Status
  - = Sat
  - | Unsat
  - | Unknown
- data Command
  - = CmdLogic Ident
  - | CmdAssumption Formula
  - | CmdFormula Formula
  - | CmdStatus Status
  - | CmdExtraSorts [Sort]
  - | CmdExtraFuns [FunDecl]
  - | CmdExtraPreds [PredDecl]
  - | CmdNotes String
  - | CmdAnnot Annot
- data Script = Script {
  - scrName :: Ident
  - scrCommands :: [Command]
  }
- (===) :: Term -> Term -> Formula
- (=/=) :: Term -> Term -> Formula
- (.<.) :: Term -> Term -> Formula
- (.>.) :: Term -> Term -> Formula
- tInt :: Sort
- funDef :: Ident -> [Sort] -> Sort -> Command
- constDef :: Ident -> Sort -> Command
- logic :: Ident -> Command
- assume :: Formula -> Command
- goal :: Formula -> Command
- class PP t where
  - pp :: t -> Doc

# 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 #

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

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 #

type Sort = Ident Source #

data Binder Source #

Constructors

Bind |

Fields

- bindVar :: Name
- bindSort :: Sort

#### 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 #

Constructors

Var Name |
App Ident [Term] |
Lit Literal |
ITE Formula Term Term |
TAnnot Term [Annot] |

#### 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

- attrName :: Name
- attrVal :: Maybe String

#### 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

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

#### 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

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

#### 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 #

Constructors

CmdLogic Ident |
CmdAssumption Formula |
CmdFormula Formula |
CmdStatus Status |
CmdExtraSorts [Sort] |
CmdExtraFuns [FunDecl] |
CmdExtraPreds [PredDecl] |
CmdNotes String |
CmdAnnot Annot |

#### 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

- scrName :: Ident
- scrCommands :: [Command]

#### Instances

Instances details

PP Script Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Script -> Doc Source #

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

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

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

For `Int`

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

For `Int`

tInt :: Sort Source #

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

constDef :: Ident -> Sort -> Command Source #

logic :: Ident -> Command Source #

assume :: Formula -> Command Source #

goal :: Formula -> Command Source #

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 #