Safe Haskell | Safe |
---|---|
Language | Haskell98 |
SMTLib1
Synopsis
- newtype Name = N String
- data Ident = I Name [Integer]
- data Quant
- data Conn
- data Formula
- type Sort = Ident
- data Binder = Bind {}
- data Term
- data Literal
- data Annot = Attr {}
- data FunDecl = FunDecl {}
- data PredDecl = PredDecl {}
- data Status
- 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
Constructors
N String |
Instances
Eq Name Source # | |
Data Name Source # | |
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 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 # | |
Show Name Source # | |
IsString Name Source # | |
Defined in SMTLib1.AST Methods fromString :: String -> Name | |
PP Name Source # | |
Defined in SMTLib1.PP |
Instances
Eq Ident Source # | |
Data Ident Source # | |
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 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 # | |
Show Ident Source # | |
IsString Ident Source # | |
Defined in SMTLib1.AST Methods fromString :: String -> Ident | |
PP Ident Source # | |
Defined in SMTLib1.PP |
Instances
Eq Quant Source # | |
Data Quant Source # | |
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 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 # | |
Show Quant Source # | |
PP Quant Source # | |
Defined in SMTLib1.PP |
Instances
Eq Conn Source # | |
Data Conn Source # | |
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 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 # | |
Show Conn Source # | |
PP Conn Source # | |
Defined in SMTLib1.PP |
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 Source # | |
Data Formula Source # | |
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 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 # | |
Show Formula Source # | |
PP Formula Source # | |
Defined in SMTLib1.PP |
Instances
Eq Binder Source # | |
Data Binder Source # | |
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 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 # | |
Show Binder Source # | |
PP Binder Source # | |
Defined in SMTLib1.PP |
Instances
Eq Term Source # | |
Fractional Term Source # | |
Defined in SMTLib1.AST | |
Data Term Source # | |
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 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 # | |
Ord Term Source # | |
Show Term Source # | |
IsString Term Source # | |
Defined in SMTLib1.AST Methods fromString :: String -> Term | |
PP Term Source # | |
Defined in SMTLib1.PP |
Instances
Eq Literal Source # | |
Data Literal Source # | |
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 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 # | |
Show Literal Source # | |
PP Literal Source # | |
Defined in SMTLib1.PP |
Instances
Eq Annot Source # | |
Data Annot Source # | |
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 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 # | |
Show Annot Source # | |
PP Annot Source # | |
Defined in SMTLib1.PP |
Instances
Data FunDecl Source # | |
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 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 # | |
Defined in SMTLib1.PP |
Instances
Data PredDecl Source # | |
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 # | |
Defined in SMTLib1.PP |
Instances
Data Status Source # | |
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 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 # | |
Defined in SMTLib1.PP |
Constructors
CmdLogic Ident | |
CmdAssumption Formula | |
CmdFormula Formula | |
CmdStatus Status | |
CmdExtraSorts [Sort] | |
CmdExtraFuns [FunDecl] | |
CmdExtraPreds [PredDecl] | |
CmdNotes String | |
CmdAnnot Annot |
Instances
Data Command Source # | |
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 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 # | |
Defined in SMTLib1.PP |
Constructors
Script | |
Fields
|
Instances
PP Script Source # | |
Defined in SMTLib1.PP | |
PP Command Source # | |
Defined in SMTLib1.PP | |
PP Status Source # | |
Defined in SMTLib1.PP | |
PP PredDecl Source # | |
Defined in SMTLib1.PP | |
PP FunDecl Source # | |
Defined in SMTLib1.PP | |
PP Annot Source # | |
Defined in SMTLib1.PP | |
PP Literal Source # | |
Defined in SMTLib1.PP | |
PP Term Source # | |
Defined in SMTLib1.PP | |
PP Binder Source # | |
Defined in SMTLib1.PP | |
PP Formula Source # | |
Defined in SMTLib1.PP | |
PP Conn Source # | |
Defined in SMTLib1.PP | |
PP Quant Source # | |
Defined in SMTLib1.PP | |
PP Ident Source # | |
Defined in SMTLib1.PP | |
PP Name Source # | |
Defined in SMTLib1.PP |