smtLib-1.0.9: A library for working with the SMTLIB format.
SMTLib2
newtype Script Source #
Constructors
Instances
Methods
pp :: Script -> Doc Source #
data Binder Source #
Fields
(==) :: Binder -> Binder -> Bool #
(/=) :: Binder -> Binder -> Bool #
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 #
compare :: Binder -> Binder -> Ordering #
(<) :: Binder -> Binder -> Bool #
(<=) :: Binder -> Binder -> Bool #
(>) :: Binder -> Binder -> Bool #
(>=) :: Binder -> Binder -> Bool #
max :: Binder -> Binder -> Binder #
min :: Binder -> Binder -> Binder #
showsPrec :: Int -> Binder -> ShowS #
show :: Binder -> String #
showList :: [Binder] -> ShowS #
pp :: Binder -> Doc Source #
data Defn Source #
(==) :: Defn -> Defn -> Bool #
(/=) :: Defn -> Defn -> Bool #
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 #
toConstr :: Defn -> Constr #
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 :: (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 #
compare :: Defn -> Defn -> Ordering #
(<) :: Defn -> Defn -> Bool #
(<=) :: Defn -> Defn -> Bool #
(>) :: Defn -> Defn -> Bool #
(>=) :: Defn -> Defn -> Bool #
max :: Defn -> Defn -> Defn #
min :: Defn -> Defn -> Defn #
showsPrec :: Int -> Defn -> ShowS #
show :: Defn -> String #
showList :: [Defn] -> ShowS #
pp :: Defn -> Doc Source #
data Type Source #
(==) :: Type -> Type -> Bool #
(/=) :: Type -> Type -> Bool #
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 #
toConstr :: Type -> Constr #
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 :: (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 #
compare :: Type -> Type -> Ordering #
(<) :: Type -> Type -> Bool #
(<=) :: Type -> Type -> Bool #
(>) :: Type -> Type -> Bool #
(>=) :: Type -> Type -> Bool #
max :: Type -> Type -> Type #
min :: Type -> Type -> Type #
showsPrec :: Int -> Type -> ShowS #
show :: Type -> String #
showList :: [Type] -> ShowS #
fromString :: String -> Type #
pp :: Type -> Doc Source #
data Expr Source #
(==) :: Expr -> Expr -> Bool #
(/=) :: Expr -> Expr -> Bool #
(/) :: Expr -> Expr -> Expr #
recip :: Expr -> Expr #
fromRational :: Rational -> Expr #
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 #
toConstr :: Expr -> Constr #
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 :: (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 #
(+) :: Expr -> Expr -> Expr #
(-) :: Expr -> Expr -> Expr #
(*) :: Expr -> Expr -> Expr #
negate :: Expr -> Expr #
abs :: Expr -> Expr #
signum :: Expr -> Expr #
fromInteger :: Integer -> Expr #
compare :: Expr -> Expr -> Ordering #
(<) :: Expr -> Expr -> Bool #
(<=) :: Expr -> Expr -> Bool #
(>) :: Expr -> Expr -> Bool #
(>=) :: Expr -> Expr -> Bool #
max :: Expr -> Expr -> Expr #
min :: Expr -> Expr -> Expr #
showsPrec :: Int -> Expr -> ShowS #
show :: Expr -> String #
showList :: [Expr] -> ShowS #
fromString :: String -> Expr #
pp :: Expr -> Doc Source #
newtype Name Source #
(==) :: Name -> Name -> Bool #
(/=) :: Name -> Name -> Bool #
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 :: (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 #
compare :: Name -> Name -> Ordering #
(<) :: Name -> Name -> Bool #
(<=) :: Name -> Name -> Bool #
(>) :: Name -> Name -> Bool #
(>=) :: Name -> Name -> Bool #
max :: Name -> Name -> Name #
min :: Name -> Name -> Name #
showsPrec :: Int -> Name -> ShowS #
show :: Name -> String #
showList :: [Name] -> ShowS #
fromString :: String -> Name #
pp :: Name -> Doc Source #
data Ident Source #
(==) :: Ident -> Ident -> Bool #
(/=) :: Ident -> Ident -> Bool #
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 :: (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 #
compare :: Ident -> Ident -> Ordering #
(<) :: Ident -> Ident -> Bool #
(<=) :: Ident -> Ident -> Bool #
(>) :: Ident -> Ident -> Bool #
(>=) :: Ident -> Ident -> Bool #
max :: Ident -> Ident -> Ident #
min :: Ident -> Ident -> Ident #
showsPrec :: Int -> Ident -> ShowS #
show :: Ident -> String #
showList :: [Ident] -> ShowS #
fromString :: String -> Ident #
pp :: Ident -> Doc Source #
data Quant Source #
(==) :: Quant -> Quant -> Bool #
(/=) :: Quant -> Quant -> Bool #
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 :: (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 #
compare :: Quant -> Quant -> Ordering #
(<) :: Quant -> Quant -> Bool #
(<=) :: Quant -> Quant -> Bool #
(>) :: Quant -> Quant -> Bool #
(>=) :: Quant -> Quant -> Bool #
max :: Quant -> Quant -> Quant #
min :: Quant -> Quant -> Quant #
showsPrec :: Int -> Quant -> ShowS #
show :: Quant -> String #
showList :: [Quant] -> ShowS #
pp :: Quant -> Doc Source #
data Literal Source #
value, width (in bits)
(==) :: Literal -> Literal -> Bool #
(/=) :: Literal -> Literal -> Bool #
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 #
compare :: Literal -> Literal -> Ordering #
(<) :: Literal -> Literal -> Bool #
(<=) :: Literal -> Literal -> Bool #
(>) :: Literal -> Literal -> Bool #
(>=) :: Literal -> Literal -> Bool #
max :: Literal -> Literal -> Literal #
min :: Literal -> Literal -> Literal #
showsPrec :: Int -> Literal -> ShowS #
show :: Literal -> String #
showList :: [Literal] -> ShowS #
pp :: Literal -> Doc Source #
data Attr Source #
(==) :: Attr -> Attr -> Bool #
(/=) :: Attr -> Attr -> Bool #
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 #
toConstr :: Attr -> Constr #
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 :: (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 #
compare :: Attr -> Attr -> Ordering #
(<) :: Attr -> Attr -> Bool #
(<=) :: Attr -> Attr -> Bool #
(>) :: Attr -> Attr -> Bool #
(>=) :: Attr -> Attr -> Bool #
max :: Attr -> Attr -> Attr #
min :: Attr -> Attr -> Attr #
showsPrec :: Int -> Attr -> ShowS #
show :: Attr -> String #
showList :: [Attr] -> ShowS #
pp :: Attr -> Doc Source #
type AttrVal = Expr Source #
data Command Source #
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 -> Doc Source #
data Option Source #
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 #
toConstr :: Option -> Constr #
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 :: (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 -> Doc Source #
data InfoFlag Source #
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 :: (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 -> Doc Source #
app :: Ident -> [Expr] -> Expr Source #
class PP t where Source #
Minimal complete definition
pp
pp :: t -> Doc Source #
pp :: Bool -> Doc Source #
pp :: Integer -> Doc Source #