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

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name Source #

toConstr :: Name -> Constr Source #

dataTypeOf :: Name -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) Source #

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

gmapT :: (forall b. Data b => b -> b) -> Name -> Name Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name Source #

IsString Name Source # |
Instance details Defined in SMTLib1.AST Methods fromString :: String -> Name Source #
Show Name Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
Eq Name Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Name -> Name -> Bool Source # (/=) :: Name -> Name -> Bool Source #
Ord Name Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
PP Name Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Name -> Doc Source #

data Ident Source #

Constructors

I Name [Integer] |

#### Instances

Instances details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Ident Source #

toConstr :: Ident -> Constr Source #

dataTypeOf :: Ident -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Ident) Source #

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

gmapT :: (forall b. Data b => b -> b) -> Ident -> Ident Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Ident -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ident -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ident -> m Ident Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ident -> m Ident Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ident -> m Ident Source #

IsString Ident Source # |
Instance details Defined in SMTLib1.AST Methods fromString :: String -> Ident Source #
Show Ident Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Ident -> ShowS Source # show :: Ident -> String Source # showList :: [Ident] -> ShowS Source #
Eq Ident Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Ident -> Ident -> Bool Source # (/=) :: Ident -> Ident -> Bool Source #
Ord Ident Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Ident -> Ident -> Ordering Source # (<) :: Ident -> Ident -> Bool Source # (<=) :: Ident -> Ident -> Bool Source # (>) :: Ident -> Ident -> Bool Source # (>=) :: Ident -> Ident -> Bool Source # max :: Ident -> Ident -> Ident Source # min :: Ident -> Ident -> Ident Source #
PP Ident Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Ident -> Doc Source #

data Quant Source #

Constructors

Exists |
Forall |

#### Instances

Instances details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quant Source #

toConstr :: Quant -> Constr Source #

dataTypeOf :: Quant -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quant) Source #

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

gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quant -> m Quant Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant Source #

Show Quant Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Quant -> ShowS Source # show :: Quant -> String Source # showList :: [Quant] -> ShowS Source #
Eq Quant Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Quant -> Quant -> Bool Source # (/=) :: Quant -> Quant -> Bool Source #
Ord Quant Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Quant -> Quant -> Ordering Source # (<) :: Quant -> Quant -> Bool Source # (<=) :: Quant -> Quant -> Bool Source # (>) :: Quant -> Quant -> Bool Source # (>=) :: Quant -> Quant -> Bool Source # max :: Quant -> Quant -> Quant Source # min :: Quant -> Quant -> Quant Source #
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

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

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

toConstr :: Conn -> Constr Source #

dataTypeOf :: Conn -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show Conn Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Conn -> ShowS Source # show :: Conn -> String Source # showList :: [Conn] -> ShowS Source #
Eq Conn Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Conn -> Conn -> Bool Source # (/=) :: Conn -> Conn -> Bool Source #
Ord Conn Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Conn -> Conn -> Ordering Source # (<) :: Conn -> Conn -> Bool Source # (<=) :: Conn -> Conn -> Bool Source # (>) :: Conn -> Conn -> Bool Source # (>=) :: Conn -> Conn -> Bool Source # max :: Conn -> Conn -> Conn Source # min :: Conn -> Conn -> Conn Source #
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

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

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

toConstr :: Formula -> Constr Source #

dataTypeOf :: Formula -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show Formula Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Formula -> ShowS Source # show :: Formula -> String Source # showList :: [Formula] -> ShowS Source #
Eq Formula Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Formula -> Formula -> Bool Source # (/=) :: Formula -> Formula -> Bool Source #
Ord Formula Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Formula -> Formula -> Ordering Source # (<) :: Formula -> Formula -> Bool Source # (<=) :: Formula -> Formula -> Bool Source # (>) :: Formula -> Formula -> Bool Source # (>=) :: Formula -> Formula -> Bool Source # max :: Formula -> Formula -> Formula Source # min :: Formula -> Formula -> Formula Source #
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

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Binder Source #

toConstr :: Binder -> Constr Source #

dataTypeOf :: Binder -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Binder) Source #

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

gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Binder -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder -> m Binder Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder Source #

Show Binder Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Binder -> ShowS Source # show :: Binder -> String Source # showList :: [Binder] -> ShowS Source #
Eq Binder Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Binder -> Binder -> Bool Source # (/=) :: Binder -> Binder -> Bool Source #
Ord Binder Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Binder -> Binder -> Ordering Source # (<) :: Binder -> Binder -> Bool Source # (<=) :: Binder -> Binder -> Bool Source # (>) :: Binder -> Binder -> Bool Source # (>=) :: Binder -> Binder -> Bool Source # max :: Binder -> Binder -> Binder Source # min :: Binder -> Binder -> Binder Source #
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

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

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

toConstr :: Term -> Constr Source #

dataTypeOf :: Term -> DataType Source #

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

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

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

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

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

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

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

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

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

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

IsString Term Source # |
Instance details Defined in SMTLib1.AST Methods fromString :: String -> Term Source #
Num Term Source # |
Instance details Defined in SMTLib1.AST Methods (+) :: Term -> Term -> Term Source # (-) :: Term -> Term -> Term Source # (*) :: Term -> Term -> Term Source # negate :: Term -> Term Source # abs :: Term -> Term Source # signum :: Term -> Term Source # fromInteger :: Integer -> Term Source #
Fractional Term Source # |
Instance details Defined in SMTLib1.AST Methods (/) :: Term -> Term -> Term Source # recip :: Term -> Term Source # fromRational :: Rational -> Term Source #
Show Term Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Term -> ShowS Source # show :: Term -> String Source # showList :: [Term] -> ShowS Source #
Eq Term Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Term -> Term -> Bool Source # (/=) :: Term -> Term -> Bool Source #
Ord Term Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Term -> Term -> Ordering Source # (<) :: Term -> Term -> Bool Source # (<=) :: Term -> Term -> Bool Source # (>) :: Term -> Term -> Bool Source # (>=) :: Term -> Term -> Bool Source # max :: Term -> Term -> Term Source # min :: Term -> Term -> Term Source #
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

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Literal Source #

toConstr :: Literal -> Constr Source #

dataTypeOf :: Literal -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Literal) Source #

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

gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Literal -> m Literal Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal Source #

Show Literal Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Literal -> ShowS Source # show :: Literal -> String Source # showList :: [Literal] -> ShowS Source #
Eq Literal Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Literal -> Literal -> Bool Source # (/=) :: Literal -> Literal -> Bool Source #
Ord Literal Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Literal -> Literal -> Ordering Source # (<) :: Literal -> Literal -> Bool Source # (<=) :: Literal -> Literal -> Bool Source # (>) :: Literal -> Literal -> Bool Source # (>=) :: Literal -> Literal -> Bool Source # max :: Literal -> Literal -> Literal Source # min :: Literal -> Literal -> Literal Source #
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

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

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

toConstr :: Annot -> Constr Source #

dataTypeOf :: Annot -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show Annot Source # |
Instance details Defined in SMTLib1.AST Methods showsPrec :: Int -> Annot -> ShowS Source # show :: Annot -> String Source # showList :: [Annot] -> ShowS Source #
Eq Annot Source # |
Instance details Defined in SMTLib1.AST Methods (==) :: Annot -> Annot -> Bool Source # (/=) :: Annot -> Annot -> Bool Source #
Ord Annot Source # |
Instance details Defined in SMTLib1.AST Methods compare :: Annot -> Annot -> Ordering Source # (<) :: Annot -> Annot -> Bool Source # (<=) :: Annot -> Annot -> Bool Source # (>) :: Annot -> Annot -> Bool Source # (>=) :: Annot -> Annot -> Bool Source # max :: Annot -> Annot -> Annot Source # min :: Annot -> Annot -> Annot Source #
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 Source #

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

toConstr :: FunDecl -> Constr Source #

dataTypeOf :: FunDecl -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

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

toConstr :: PredDecl -> Constr Source #

dataTypeOf :: PredDecl -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

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

toConstr :: Status -> Constr Source #

dataTypeOf :: Status -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Command Source #

toConstr :: Command -> Constr Source #

dataTypeOf :: Command -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Command) Source #

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

gmapT :: (forall b. Data b => b -> b) -> Command -> Command Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Command -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Command -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Command -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Command -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Command -> m Command Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Command -> m Command Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Command -> m Command Source #

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 Annot Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Annot -> Doc Source #
PP Binder Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Binder -> Doc Source #
PP Command Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Command -> Doc Source #
PP Conn Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Conn -> Doc Source #
PP Formula Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Formula -> Doc Source #
PP FunDecl Source # |
Instance details Defined in SMTLib1.PP Methods pp :: FunDecl -> Doc Source #
PP Ident Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Ident -> Doc Source #
PP Literal Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Literal -> Doc Source #
PP Name Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Name -> Doc Source #
PP PredDecl Source # |
Instance details Defined in SMTLib1.PP Methods pp :: PredDecl -> Doc Source #
PP Quant Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Quant -> Doc Source #
PP Script Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Script -> Doc Source #
PP Status Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Status -> Doc Source #
PP Term Source # |
Instance details Defined in SMTLib1.PP Methods pp :: Term -> Doc Source #