Safe Haskell | Safe |
---|---|
Language | Haskell98 |
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
- 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
Documentation
Instances
Eq Name Source # | |
Data Name Source # | |
Defined in SMTLib1.AST 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 :: (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 fromString :: String -> Name # | |
PP Name Source # | |
Instances
Eq Ident Source # | |
Data Ident Source # | |
Defined in SMTLib1.AST 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 :: (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 fromString :: String -> Ident # | |
PP Ident Source # | |
Instances
Eq Quant Source # | |
Data Quant Source # | |
Defined in SMTLib1.AST 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 :: (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 # | |
Instances
Eq Conn Source # | |
Data Conn Source # | |
Defined in SMTLib1.AST 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 :: (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 # | |
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 gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formula -> c Formula # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Formula # toConstr :: Formula -> Constr # dataTypeOf :: Formula -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Formula) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula) # gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r # gmapQ :: (forall d. Data d => d -> u) -> Formula -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Formula -> m Formula # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula # | |
Ord Formula Source # | |
Show Formula Source # | |
PP Formula Source # | |
Instances
Eq Binder Source # | |
Data Binder Source # | |
Defined in SMTLib1.AST gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder -> c Binder # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Binder # toConstr :: Binder -> Constr # dataTypeOf :: Binder -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Binder) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder) # gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r # gmapQ :: (forall d. Data d => d -> u) -> Binder -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder -> m Binder # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder # | |
Ord Binder Source # | |
Show Binder Source # | |
PP Binder Source # | |
Instances
Eq Term Source # | |
Fractional Term Source # | |
Data Term Source # | |
Defined in SMTLib1.AST 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 :: (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 fromString :: String -> Term # | |
PP Term Source # | |
Instances
Eq Literal Source # | |
Data Literal Source # | |
Defined in SMTLib1.AST gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Literal -> c Literal # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Literal # toConstr :: Literal -> Constr # dataTypeOf :: Literal -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Literal) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal) # gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r # gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Literal -> m Literal # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal # | |
Ord Literal Source # | |
Show Literal Source # | |
PP Literal Source # | |
Instances
Eq Annot Source # | |
Data Annot Source # | |
Defined in SMTLib1.AST 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 :: (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 # | |
Instances
Data FunDecl Source # | |
Defined in SMTLib1.AST gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunDecl -> c FunDecl # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunDecl # toConstr :: FunDecl -> Constr # dataTypeOf :: FunDecl -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunDecl) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl) # gmapT :: (forall b. Data b => b -> b) -> FunDecl -> FunDecl # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunDecl -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunDecl -> r # gmapQ :: (forall d. Data d => d -> u) -> FunDecl -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FunDecl -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl # | |
PP FunDecl Source # | |
Instances
Data PredDecl Source # | |
Defined in SMTLib1.AST gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredDecl -> c PredDecl # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredDecl # toConstr :: PredDecl -> Constr # dataTypeOf :: PredDecl -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PredDecl) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl) # gmapT :: (forall b. Data b => b -> b) -> PredDecl -> PredDecl # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredDecl -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredDecl -> r # gmapQ :: (forall d. Data d => d -> u) -> PredDecl -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PredDecl -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl # | |
PP PredDecl Source # | |
Instances
Data Status Source # | |
Defined in SMTLib1.AST gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Status -> c Status # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Status # toConstr :: Status -> Constr # dataTypeOf :: Status -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Status) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status) # gmapT :: (forall b. Data b => b -> b) -> Status -> Status # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r # gmapQ :: (forall d. Data d => d -> u) -> Status -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Status -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Status -> m Status # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Status -> m Status # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Status -> m Status # | |
PP Status Source # | |
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 gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Command -> c Command # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Command # toConstr :: Command -> Constr # dataTypeOf :: Command -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Command) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command) # gmapT :: (forall b. Data b => b -> b) -> Command -> Command # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Command -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Command -> r # gmapQ :: (forall d. Data d => d -> u) -> Command -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Command -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Command -> m Command # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Command -> m Command # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Command -> m Command # | |
PP Command Source # | |
Script | |
|