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

newtype FunctionParser

Constructors

FunctionParser

Fields

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

Instances

Monoid 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.

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