Language.Hasmtlib.Internal.Render

Documentation

class Render a where

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

Methods

render :: a -> Builder

Instances

Render Nat

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Nat -> Builder

Render Builder

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Builder -> Builder

Render SMTOption

Defined in Language.Hasmtlib.Type.Option

Methods

render :: SMTOption -> Builder

Render Integer

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Integer -> Builder

Render Bool

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Bool -> Builder

Render Double

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Double -> Builder

Render (Bitvec n)

Defined in Language.Hasmtlib.Internal.Bitvec

Methods

render :: Bitvec n -> Builder

KnownSMTSort t => Render (Expr t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

render :: Expr t -> Builder

Render (SMTVar t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

render :: SMTVar t -> Builder

Render (SSMTSort t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

render :: SSMTSort t -> Builder

Render (Value t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

render :: Value t -> 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