Language.SMTLib2.Pipe

Documentation

data SMTPipe

Instances

Backend SMTPipe

Associated Types

type SMTMonad SMTPipe :: * -> *

data Expr SMTPipe (a :: Type) :: *

type Var SMTPipe :: Type -> *

type QVar SMTPipe :: Type -> *

type Fun SMTPipe :: ([Type], Type) -> *

type FunArg SMTPipe :: Type -> *

type LVar SMTPipe :: Type -> *

type ClauseId SMTPipe :: *

type Model SMTPipe :: *

type Proof SMTPipe :: *

Methods

setOption :: SMTOption -> SMTAction SMTPipe ()

getInfo :: SMTInfo i -> SMTAction SMTPipe i

comment :: String -> SMTAction SMTPipe ()

push :: SMTAction SMTPipe ()

pop :: SMTAction SMTPipe ()

declareVar :: Repr t -> Maybe String -> SMTAction SMTPipe (Var SMTPipe t)

createQVar :: Repr t -> Maybe String -> SMTAction SMTPipe (QVar SMTPipe t)

createFunArg :: Repr t -> Maybe String -> SMTAction SMTPipe (FunArg SMTPipe t)

defineVar :: Maybe String -> Expr SMTPipe t -> SMTAction SMTPipe (Var SMTPipe t)

declareFun :: List Type Repr arg -> Repr t -> Maybe String -> SMTAction SMTPipe (Fun SMTPipe (([Type], Type) arg t))

defineFun :: Maybe String -> List Type (FunArg SMTPipe) arg -> Expr SMTPipe r -> SMTAction SMTPipe (Fun SMTPipe (([Type], Type) arg r))

assert :: Expr SMTPipe BoolType -> SMTAction SMTPipe ()

assertId :: Expr SMTPipe BoolType -> SMTAction SMTPipe (ClauseId SMTPipe)

assertPartition :: Expr SMTPipe BoolType -> Partition -> SMTAction SMTPipe ()

checkSat :: Maybe Tactic -> CheckSatLimits -> SMTAction SMTPipe CheckSatResult

getUnsatCore :: SMTAction SMTPipe [ClauseId SMTPipe]

getValue :: Expr SMTPipe t -> SMTAction SMTPipe (Value t)

getModel :: SMTAction SMTPipe (Model SMTPipe)

modelEvaluate :: Model SMTPipe -> Expr SMTPipe t -> SMTAction SMTPipe (Value t)

getProof :: SMTAction SMTPipe (Proof SMTPipe)

analyzeProof :: SMTPipe -> Proof SMTPipe -> Proof String (Expr SMTPipe) (Proof SMTPipe)

simplify :: Expr SMTPipe t -> SMTAction SMTPipe (Expr SMTPipe t)

toBackend :: Expression (Var SMTPipe) (QVar SMTPipe) (Fun SMTPipe) (FunArg SMTPipe) (LVar SMTPipe) (Expr SMTPipe) t -> SMTAction SMTPipe (Expr SMTPipe t)

fromBackend :: SMTPipe -> Expr SMTPipe t -> Expression (Var SMTPipe) (QVar SMTPipe) (Fun SMTPipe) (FunArg SMTPipe) (LVar SMTPipe) (Expr SMTPipe) t

declareDatatypes :: [AnyDatatype] -> SMTAction SMTPipe ()

interpolate :: SMTAction SMTPipe (Expr SMTPipe BoolType)

exit :: SMTAction SMTPipe ()

GCompare Type (Expr SMTPipe)

Methods

gcompare :: f a -> f b -> GOrdering (Expr SMTPipe) a b

GEq Type (Expr SMTPipe)

Methods

geq :: f a -> f b -> Maybe ((Expr SMTPipe := a) b)

GShow Type (Expr SMTPipe)

Methods

gshowsPrec :: Int -> t a -> ShowS

GetType (Expr SMTPipe)

Methods

getType :: Expr SMTPipe tp -> Repr tp

Show (Expr SMTPipe t)

Methods

showsPrec :: Int -> Expr SMTPipe t -> ShowS

show :: Expr SMTPipe t -> String

showList :: [Expr SMTPipe t] -> ShowS

type Proof SMTPipe

type Proof SMTPipe = PipeProof

type Model SMTPipe

type Model SMTPipe = AssignmentModel SMTPipe

type ClauseId SMTPipe

type ClauseId SMTPipe = PipeClauseId

type LVar SMTPipe

type LVar SMTPipe = PipeVar

type FunArg SMTPipe

type FunArg SMTPipe = PipeVar

type Fun SMTPipe

type Fun SMTPipe = PipeFun

type QVar SMTPipe

type QVar SMTPipe = PipeVar

type Var SMTPipe

type Var SMTPipe = PipeVar

data Expr SMTPipe

data Expr SMTPipe = PipeExpr (Expression PipeVar PipeVar PipeFun PipeVar PipeVar (Expr SMTPipe) t)

type SMTMonad SMTPipe

type SMTMonad SMTPipe = IO

createPipe

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.

createPipeFromHandle

Arguments

:: Handle

Input handle

-> Handle

Output handle

-> IO SMTPipe

Create a SMT pipe by giving the input and output handle.

withPipe :: String -> [String] -> SMT SMTPipe a -> IO a