Safe Haskell | Safe |
---|---|
Language | Haskell98 |
SMTLib2
Documentation
Instances
Eq Binder Source # | |
Data Binder Source # | |
Defined in SMTLib2.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 SMTLib2.PP |
Instances
Eq Defn Source # | |
Data Defn Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defn -> c Defn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defn dataTypeOf :: Defn -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Defn) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn) gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defn -> m Defn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn | |
Ord Defn Source # | |
Show Defn Source # | |
PP Defn Source # | |
Defined in SMTLib2.PP |
Instances
Eq Type Source # | |
Data Type Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type dataTypeOf :: Type -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) gmapT :: (forall b. Data b => b -> b) -> Type -> Type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type | |
Ord Type Source # | |
Show Type Source # | |
IsString Type Source # | |
Defined in SMTLib2.AST Methods fromString :: String -> Type | |
PP Type Source # | |
Defined in SMTLib2.PP |
Constructors
Lit Literal | |
App Ident (Maybe Type) [Expr] | |
Quant Quant [Binder] Expr | |
Let [Defn] Expr | |
Annot Expr [Attr] |
Instances
Eq Expr Source # | |
Fractional Expr Source # | |
Defined in SMTLib2.AST | |
Data Expr Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr dataTypeOf :: Expr -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr | |
Num Expr Source # | |
Ord Expr Source # | |
Show Expr Source # | |
IsString Expr Source # | |
Defined in SMTLib2.AST Methods fromString :: String -> Expr | |
PP Expr Source # | |
Defined in SMTLib2.PP |
Constructors
N String |
Instances
Eq Name Source # | |
Data Name Source # | |
Defined in SMTLib2.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 SMTLib2.AST Methods fromString :: String -> Name | |
PP Name Source # | |
Defined in SMTLib2.PP |
Instances
Eq Ident Source # | |
Data Ident Source # | |
Defined in SMTLib2.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 SMTLib2.AST Methods fromString :: String -> Ident | |
PP Ident Source # | |
Defined in SMTLib2.PP |
Instances
Eq Quant Source # | |
Data Quant Source # | |
Defined in SMTLib2.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 SMTLib2.PP |
Constructors
LitBV Integer Integer | value, width (in bits) |
LitNum Integer | |
LitFrac Rational | |
LitStr String |
Instances
Eq Literal Source # | |
Data Literal Source # | |
Defined in SMTLib2.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 SMTLib2.PP |
Instances
Eq Attr Source # | |
Data Attr Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Attr -> c Attr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Attr dataTypeOf :: Attr -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Attr) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr) gmapT :: (forall b. Data b => b -> b) -> Attr -> Attr gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r gmapQ :: (forall d. Data d => d -> u) -> Attr -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Attr -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Attr -> m Attr gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Attr -> m Attr gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Attr -> m Attr | |
Ord Attr Source # | |
Show Attr Source # | |
PP Attr Source # | |
Defined in SMTLib2.PP |
Constructors
Instances
Data Command Source # | |
Defined in SMTLib2.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 SMTLib2.PP |
Constructors
OptPrintSuccess Bool | |
OptExpandDefinitions Bool | |
OptInteractiveMode Bool | |
OptProduceProofs Bool | |
OptProduceUnsatCores Bool | |
OptProduceModels Bool | |
OptProduceAssignments Bool | |
OptRegularOutputChannel String | |
OptDiagnosticOutputChannel String | |
OptRandomSeed Integer | |
OptVerbosity Integer | |
OptAttr Attr |
Instances
Data Option Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Option -> c Option gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Option dataTypeOf :: Option -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Option) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option) gmapT :: (forall b. Data b => b -> b) -> Option -> Option gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r gmapQ :: (forall d. Data d => d -> u) -> Option -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Option -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Option -> m Option gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Option -> m Option gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Option -> m Option | |
PP Option Source # | |
Defined in SMTLib2.PP |
Constructors
InfoAllStatistics | |
InfoErrorBehavior | |
InfoName | |
InfoAuthors | |
InfoVersion | |
InfoStatus | |
InfoReasonUnknown | |
InfoAttr Attr |
Instances
Data InfoFlag Source # | |
Defined in SMTLib2.AST Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InfoFlag -> c InfoFlag gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InfoFlag toConstr :: InfoFlag -> Constr dataTypeOf :: InfoFlag -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InfoFlag) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag) gmapT :: (forall b. Data b => b -> b) -> InfoFlag -> InfoFlag gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r gmapQ :: (forall d. Data d => d -> u) -> InfoFlag -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> InfoFlag -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag | |
PP InfoFlag Source # | |
Defined in SMTLib2.PP |
Instances
PP Bool Source # | |
Defined in SMTLib2.PP | |
PP Integer Source # | |
Defined in SMTLib2.PP | |
PP Script Source # | |
Defined in SMTLib2.PP | |
PP Command Source # | |
Defined in SMTLib2.PP | |
PP InfoFlag Source # | |
Defined in SMTLib2.PP | |
PP Option Source # | |
Defined in SMTLib2.PP | |
PP Attr Source # | |
Defined in SMTLib2.PP | |
PP Expr Source # | |
Defined in SMTLib2.PP | |
PP Type Source # | |
Defined in SMTLib2.PP | |
PP Literal Source # | |
Defined in SMTLib2.PP | |
PP Defn Source # | |
Defined in SMTLib2.PP | |
PP Binder Source # | |
Defined in SMTLib2.PP | |
PP Quant Source # | |
Defined in SMTLib2.PP | |
PP Ident Source # | |
Defined in SMTLib2.PP | |
PP Name Source # | |
Defined in SMTLib2.PP |