Safe Haskell	Safe-Inferred
Language	GHC2021

Language.Hasmtlib.Internal.Render

Synopsis

class Render a where
- render :: a -> Builder
renderUnary :: Render a => Builder -> a -> Builder
renderBinary :: (Render a, Render b) => Builder -> a -> b -> Builder
renderTernary :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
renderNary :: Render a => Builder -> [a] -> Builder
class RenderSeq a where
- renderSeq :: a -> Seq Builder

Documentation

class Render a where Source #

Render values to their SMTLib2-Lisp form, represented as Builder.

Methods

render :: a -> Builder Source #

Instances

Instances details

Render Nat Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Nat -> Builder Source #
Render Builder Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Builder -> Builder Source #
Render SoftFormula Source #
Instance details Defined in Language.Hasmtlib.Type.OMT Methods render :: SoftFormula -> Builder Source #
Render SMTOption Source #
Instance details Defined in Language.Hasmtlib.Type.Option Methods render :: SMTOption -> Builder Source #
Render String Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: String -> Builder Source #
Render Integer Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Integer -> Builder Source #
Render Bool Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Bool -> Builder Source #
Render Char Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Char -> Builder Source #
Render Double Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Double -> Builder Source #
Render (Bitvec n) Source #
Instance details Defined in Language.Hasmtlib.Internal.Bitvec Methods render :: Bitvec n -> Builder Source #
KnownSMTSort t => Render (Expr t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods render :: Expr t -> Builder Source #
Render (SMTVar t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods render :: SMTVar t -> Builder Source #
Render (Value t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods render :: Value t -> Builder Source #
KnownSMTSort t => Render (Maximize t) Source #
Instance details Defined in Language.Hasmtlib.Type.OMT Methods render :: Maximize t -> Builder Source #
KnownSMTSort t => Render (Minimize t) Source #
Instance details Defined in Language.Hasmtlib.Type.OMT Methods render :: Minimize t -> Builder Source #
Render (SSMTSort t) Source #
Instance details Defined in Language.Hasmtlib.Type.SMTSort Methods render :: SSMTSort t -> Builder Source #

renderUnary :: Render a => Builder -> a -> Builder Source #

renderBinary :: (Render a, Render b) => Builder -> a -> b -> Builder Source #

renderTernary :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder Source #

renderNary :: Render a => Builder -> [a] -> Builder Source #

class RenderSeq a where Source #

Render values to their sequential SMTLib2-Lisp form, represented as a Seq Builder.

Methods

renderSeq :: a -> Seq Builder Source #

Instances

Instances details

RenderSeq OMT Source #
Instance details Defined in Language.Hasmtlib.Type.OMT Methods renderSeq :: OMT -> Seq Builder Source #
RenderSeq SMT Source #
Instance details Defined in Language.Hasmtlib.Type.SMT Methods renderSeq :: SMT -> Seq Builder Source #