Language.SMTLib2.Pipe

Documentation

data SMTPipe

An SMT backend which uses process pipes to communicate with an SMT solver process.

Instances

MonadIO m => SMTBackend SMTPipe m

Methods

smtHandle :: Typeable * response => SMTPipe -> SMTRequest response -> m (response, SMTPipe)

smtGetNames :: SMTPipe -> m (Integer -> String)

smtNextName :: SMTPipe -> m (Maybe String -> String)

newtype FunctionParser

Constructors

FunctionParser

Fields

• parseFun :: Lisp -> FunctionParser -> DataTypeInfo -> Maybe FunctionParser'

Instances

Monoid FunctionParser

Methods

mempty :: FunctionParser

mappend :: FunctionParser -> FunctionParser -> FunctionParser

mconcat :: [FunctionParser] -> FunctionParser

createSMTPipe

Arguments

:: String

Path to the binary of the SMT solver

-> [String]

Command line arguments to be passed to the SMT solver

-> IO SMTPipe

Spawn a new SMT solver process and create a pipe to communicate with it.

withPipe :: MonadIO m => String -> [String] -> SMT' m a -> m a

exprToLisp :: SMTExpr t -> (Integer -> String) -> DataTypeInfo -> Lisp

exprToLispWith :: (forall a. (Typeable a, Ord a, Show a) => a -> Lisp) -> SMTExpr t -> (Integer -> String) -> DataTypeInfo -> Lisp

lispToExpr

Arguments

:: FunctionParser

The parser to use for function symbols

-> (Text -> Maybe (SMTExpr Untyped))

How to handle variable names

-> DataTypeInfo

Information about declared data types

-> (forall a. SMTType a => SMTExpr a -> b)

A function to apply to the resulting SMT expression

-> Maybe Sort

If you know the sort of the expression, you can pass it here.

-> Integer

The current quantification level

-> Lisp

The lisp expression to parse

-> Maybe b

Parse a lisp expression into an SMT expression. Since we cannot know what type the expression might have, we pass a general function which may take any SMT expression and produce the desired result.

lispToExprWith

Arguments

:: (forall b. FunctionParser -> (Text -> Maybe (SMTExpr Untyped)) -> DataTypeInfo -> (forall a. SMTType a => SMTExpr a -> b) -> Maybe Sort -> Integer -> Lisp -> Maybe b)

Recursive descend function

-> FunctionParser

The parser to use for function symbols

-> (Text -> Maybe (SMTExpr Untyped))

How to handle variable names

-> DataTypeInfo

Information about declared data types

-> (forall a. SMTType a => SMTExpr a -> b)

A function to apply to the resulting SMT expression

-> Maybe Sort

If you know the sort of the expression, you can pass it here.

-> Integer

The current quantification level

-> Lisp

The lisp expression to parse

-> Maybe b

sortToLisp :: Sort -> Lisp

lispToSort :: Lisp -> Maybe Sort

Parse a lisp expression into an SMT sort.

renderExpr :: (SMTType t, Monad m) => SMTExpr t -> SMT' m String

renderExpr' :: SMTType t => (Integer -> String) -> DataTypeInfo -> SMTExpr t -> String

renderSMTRequest :: (Maybe String -> String) -> (Integer -> String) -> DataTypeInfo -> SMTRequest r -> Either Lisp String

renderSMTResponse :: (Integer -> String) -> DataTypeInfo -> SMTRequest response -> response -> Maybe String

commonFunctions :: FunctionParser

A parser for all available SMT logics.

commonTheorems :: FunctionParser

A map which contains signatures for a few common theorems which can be used in the proofs which getProof returns.

simpleParser :: (Liftable arg, SMTType res, Unit (ArgAnnotation arg), Unit (SMTAnnotation res)) => SMTFunction arg res -> FunctionParser

data FunctionParser'

Constructors

OverloadedParser

Fields

• sortConstraint :: [Sort] -> Bool
• deriveRetSort :: [Sort] -> Maybe Sort
• parseOverloaded :: forall a. [Sort] -> Sort -> (forall arg res. (Liftable arg, SMTType res) => SMTFunction arg res -> a) -> Maybe a

DefinedParser

Fields

• definedArgSig :: [Sort]
• definedRetSig :: Sort
• parseDefined :: forall a. (forall arg res. (Liftable arg, SMTType res) => SMTFunction arg res -> a) -> Maybe a