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 #