Safe Haskell	Safe-Inferred
Language	GHC2021

Language.Hasmtlib.Internal.Render

Contents

Orphan instances

Synopsis

render1 :: Render a => Builder -> a -> Builder
render2 :: (Render a, Render b) => Builder -> a -> b -> Builder
render3 :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
renderN :: Render a => Builder -> [a] -> Builder
class Render a where
- render :: a -> Builder
renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder
renderSetLogic :: Builder -> Builder
renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder
renderAssert :: Expr BoolSort -> Builder
renderGetValue :: SMTVar t -> Builder
renderPush :: Integer -> Builder
renderPop :: Integer -> Builder
renderCheckSat :: Builder
renderGetModel :: Builder
class RenderProblem s where
- renderOptions :: s -> Seq Builder
- renderLogic :: s -> Builder
- renderDeclareVars :: s -> Seq Builder
- renderAssertions :: s -> Seq Builder
- renderSoftAssertions :: s -> Seq Builder
- renderMinimizations :: s -> Seq Builder
- renderMaximizations :: s -> Seq Builder

Documentation

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

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

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

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

class Render a where Source #

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

Methods

render :: a -> Builder Source #

Instances

Instances details

Render Rational Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Rational -> Builder Source #
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.Internal.Render Methods render :: SoftFormula -> Builder Source #
Render SMTOption Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: SMTOption -> Builder Source #
Render Text Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Text -> 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 #
KnownSMTSort t => Render (Expr t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Expr t -> Builder Source #
Render (SMTVar t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: SMTVar t -> Builder Source #
KnownSMTSort t => Render (Maximize t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Maximize t -> Builder Source #
KnownSMTSort t => Render (Minimize t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Minimize t -> Builder Source #
Render (SSMTSort t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: SSMTSort t -> Builder Source #
Render (Value t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Value t -> Builder Source #
Render (Bitvec enc n) Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods render :: Bitvec enc n -> Builder Source #

renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder Source #

renderSetLogic :: Builder -> Builder Source #

renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder Source #

renderAssert :: Expr BoolSort -> Builder Source #

renderGetValue :: SMTVar t -> Builder Source #

renderPush :: Integer -> Builder Source #

renderPop :: Integer -> Builder Source #

renderCheckSat :: Builder Source #

renderGetModel :: Builder Source #

class RenderProblem s where Source #

Methods

renderOptions :: s -> Seq Builder Source #

renderLogic :: s -> Builder Source #

renderDeclareVars :: s -> Seq Builder Source #

renderAssertions :: s -> Seq Builder Source #

renderSoftAssertions :: s -> Seq Builder Source #

renderMinimizations :: s -> Seq Builder Source #

renderMaximizations :: s -> Seq Builder Source #

Instances

Instances details

RenderProblem OMT Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods renderOptions :: OMT -> Seq Builder Source # renderLogic :: OMT -> Builder Source # renderDeclareVars :: OMT -> Seq Builder Source # renderAssertions :: OMT -> Seq Builder Source # renderSoftAssertions :: OMT -> Seq Builder Source # renderMinimizations :: OMT -> Seq Builder Source # renderMaximizations :: OMT -> Seq Builder Source #
RenderProblem SMT Source #
Instance details Defined in Language.Hasmtlib.Internal.Render Methods renderOptions :: SMT -> Seq Builder Source # renderLogic :: SMT -> Builder Source # renderDeclareVars :: SMT -> Seq Builder Source # renderAssertions :: SMT -> Seq Builder Source # renderSoftAssertions :: SMT -> Seq Builder Source # renderMinimizations :: SMT -> Seq Builder Source # renderMaximizations :: SMT -> Seq Builder Source #

Orphan instances

KnownSMTSort t => Show (Expr t) Source #
Instance details Methods showsPrec :: Int -> Expr t -> ShowS # show :: Expr t -> String # showList :: [Expr t] -> ShowS #
Show (Value t) Source #
Instance details Methods showsPrec :: Int -> Value t -> ShowS # show :: Value t -> String # showList :: [Value t] -> ShowS #