Language.SMTLib2.Pipe.Internals

Documentation

data PipeDatatype

Constructors

IsDatatype a => PipeDatatype (Proxy a)

data SMTPipe

Constructors

SMTPipe

Fields

• channelIn :: Handle
• channelOut :: Handle
• processHandle :: Maybe ProcessHandle
• names :: Map String Int
• vars :: Map Text RevVar
• datatypes :: TypeRegistry Text Text Text
• interpolationMode :: InterpolationMode

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

data RevVar

Constructors

Var !(Repr t)

QVar !(Repr t)

Fun !(List Repr arg) !(Repr t)

FunArg !(Repr t)

LVar !(Repr t)

data InterpolationMode

Constructors

Z3Interpolation [Text] [Text]

MathSATInterpolation

type PipeVar = UntypedVar Text

type PipeFun = UntypedFun Text

newtype PipeClauseId

Constructors

PipeClauseId Text

Instances

Eq PipeClauseId

Methods

(==) :: PipeClauseId -> PipeClauseId -> Bool

(/=) :: PipeClauseId -> PipeClauseId -> Bool

Ord PipeClauseId

Methods

compare :: PipeClauseId -> PipeClauseId -> Ordering

(<) :: PipeClauseId -> PipeClauseId -> Bool

(<=) :: PipeClauseId -> PipeClauseId -> Bool

(>) :: PipeClauseId -> PipeClauseId -> Bool

(>=) :: PipeClauseId -> PipeClauseId -> Bool

max :: PipeClauseId -> PipeClauseId -> PipeClauseId

min :: PipeClauseId -> PipeClauseId -> PipeClauseId

Show PipeClauseId

Methods

showsPrec :: Int -> PipeClauseId -> ShowS

show :: PipeClauseId -> String

showList :: [PipeClauseId] -> ShowS

type PipeProofNode = Proof Lisp (Expr SMTPipe) Int

data PipeProof

Constructors

PipeProof

Fields

• proofNodes :: Map Int PipeProofNode
• proofNode :: Int

Instances

Eq PipeProof

Methods

(==) :: PipeProof -> PipeProof -> Bool

(/=) :: PipeProof -> PipeProof -> Bool

Ord PipeProof

Methods

compare :: PipeProof -> PipeProof -> Ordering

(<) :: PipeProof -> PipeProof -> Bool

(<=) :: PipeProof -> PipeProof -> Bool

(>) :: PipeProof -> PipeProof -> Bool

(>=) :: PipeProof -> PipeProof -> Bool

max :: PipeProof -> PipeProof -> PipeProof

min :: PipeProof -> PipeProof -> PipeProof

Show PipeProof

Methods

showsPrec :: Int -> PipeProof -> ShowS

show :: PipeProof -> String

showList :: [PipeProof] -> ShowS

renderDeclareFun :: Map String Int -> List Repr arg -> Repr ret -> Maybe String -> (Text, Lisp, Map String Int)

renderDefineFun :: (GetType e, GetType fv) => (forall t. fv t -> Lisp) -> (forall t. e t -> Lisp) -> Map String Int -> Maybe String -> List fv arg -> e ret -> (Text, Lisp, Map String Int)

renderCheckSat :: Maybe Tactic -> CheckSatLimits -> Lisp

renderDeclareDatatype' :: Integer -> [(Text, [(Text, [(Text, Lisp)])])] -> Lisp

renderDeclareDatatype :: Map String Int -> TypeRegistry Text Text Text -> [AnyDatatype] -> (Lisp, Map String Int, TypeRegistry Text Text Text)

renderSetOption :: SMTOption -> Lisp

renderGetInfo :: SMTInfo i -> Lisp

renderDeclareVar :: Map String Int -> Repr tp -> Maybe String -> (Text, Lisp, Map String Int)

renderDefineVar :: Map String Int -> Repr t -> Maybe String -> Lisp -> (Text, Lisp, Map String Int)

renderGetValue :: SMTPipe -> Expr SMTPipe t -> Lisp

parseGetValue :: SMTPipe -> Repr t -> Lisp -> Value t

renderGetProof :: Lisp

parseGetProof :: SMTPipe -> Lisp -> PipeProof

parseProof :: SMTPipe -> Map Text (Expr SMTPipe BoolType) -> Map Text Int -> Map Int PipeProofNode -> Lisp -> LispParse PipeProof

parseGetModel :: SMTPipe -> Lisp -> LispParse (Model SMTPipe)

data Sort

Constructors

Sort (Repr t)

data Sorts

Constructors

Sorts (List Repr t)

data ParsedFunction fun

Constructors

ParsedFunction

Fields

• argumentTypeRequired :: Integer -> Bool
• getParsedFunction :: [Maybe Sort] -> LispParse (AnyFunction fun)

data AnyExpr e

Constructors

AnyExpr (e t)

Instances

GShow Type e => Show (AnyExpr e)

Methods

showsPrec :: Int -> AnyExpr e -> ShowS

show :: AnyExpr e -> String

showList :: [AnyExpr e] -> ShowS

data LispParser v qv fun fv lv e

Constructors

LispParser

Fields

• parseFunction :: forall a. Maybe Sort -> Text -> (forall args res. fun '(args, res) -> LispParse a) -> (forall args res. IsDatatype res => Datatype res -> Constr res args -> LispParse a) -> (forall args res. IsDatatype res => Datatype res -> Constr res args -> LispParse a) -> (forall t args res. IsDatatype t => Datatype t -> Field t res -> LispParse a) -> LispParse a
• parseDatatype :: forall a. Text -> (forall dt. IsDatatype dt => Datatype dt -> LispParse a) -> LispParse a
• parseVar :: forall a. Maybe Sort -> Text -> (forall t. v t -> LispParse a) -> (forall t. qv t -> LispParse a) -> (forall t. fv t -> LispParse a) -> (forall t. lv t -> LispParse a) -> LispParse a
• parseRecursive :: forall a. LispParser v qv fun fv lv e -> Maybe Sort -> Lisp -> (forall t. e t -> LispParse a) -> LispParse a
• registerQVar :: forall t. Text -> Repr t -> (qv t, LispParser v qv fun fv lv e)
• registerLetVar :: forall t. Text -> Repr t -> (lv t, LispParser v qv fun fv lv e)

type LispParse = Except String

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.

lispToExprUntyped :: SMTPipe -> Lisp -> (forall t. Expr SMTPipe t -> LispParse a) -> LispParse a

lispToExprTyped :: SMTPipe -> Repr t -> Lisp -> LispParse (Expr SMTPipe t)

pipeParser :: SMTPipe -> LispParser PipeVar PipeVar PipeFun PipeVar PipeVar (Expr SMTPipe)

lispToExprWith :: (GShow fun, GShow e, GetFunType fun, GetType e) => LispParser v qv fun fv lv e -> Maybe Sort -> Lisp -> (forall t. Expression v qv fun fv lv e t -> LispParse a) -> LispParse a

mkQuant :: LispParser v qv fun fv lv e -> [Lisp] -> (forall arg. LispParser v qv fun fv lv e -> List qv arg -> LispParse a) -> LispParse a

mkLet :: GetType e => LispParser v qv fun fv lv e -> [Lisp] -> (forall arg. LispParser v qv fun fv lv e -> List (LetBinding lv e) arg -> LispParse a) -> LispParse a

withEq :: Repr t -> [b] -> (forall n. Natural n -> List Repr (AllEq t n) -> a) -> a

lispToFunction :: LispParser v qv fun fv lv e -> Maybe Sort -> Lisp -> LispParse (ParsedFunction fun)

fullArgs :: Int -> [(Int, Sort)] -> Natural len -> (forall tps. Length tps ~ len => List Repr tps -> a) -> Maybe a

lispToOrdFunction :: OrdOp -> LispParse (ParsedFunction fun)

lispToArithFunction :: Maybe Sort -> ArithOp -> LispParse (ParsedFunction fun)

lispToLogicFunction :: LogicOp -> ParsedFunction fun

lispToBVCompFunction :: BVCompOp -> ParsedFunction fun

lispToBVBinFunction :: Maybe Sort -> BVBinOp -> LispParse (ParsedFunction fun)

lispToBVUnFunction :: Maybe Sort -> BVUnOp -> LispParse (ParsedFunction fun)

mkMap :: List Repr idx -> AnyFunction fun -> AnyFunction fun

asArraySort :: Sort -> Maybe (Sorts, Sort)

lispToList :: Lisp -> Maybe [Lisp]

lispToSort :: LispParser v qv fun fv lv e -> Lisp -> LispParse Sort

lispToSorts :: LispParser v qv fun fv lv e -> [Lisp] -> (forall arg. List Repr arg -> LispParse a) -> LispParse a

lispToValue :: SMTPipe -> Maybe Sort -> Lisp -> LispParse AnyValue

lispToConstant :: Lisp -> LispParse AnyValue

lispToConstrConstant :: SMTPipe -> Maybe Sort -> Lisp -> LispParse AnyValue

lispToNumber :: Lisp -> Maybe Integer

lispToReal :: Lisp -> Maybe Rational

lispToBitVec :: Lisp -> Maybe (Integer, Integer)

exprToLisp :: TypeRegistry Text Text Text -> Expression PipeVar PipeVar PipeFun PipeVar PipeVar (Expr SMTPipe) t -> Lisp

exprToLispWith

Arguments

:: (Monad m, GetType v, GetType qv, GetType fv, GetType lv, GetFunType fun, GetType e)

=> (forall t'. v t' -> m Lisp)

variables

-> (forall t'. qv t' -> m Lisp)

quantified variables

-> (forall arg res. fun '(arg, res) -> m Lisp)

functions

-> (forall arg dt. IsDatatype dt => Datatype dt -> Constr dt arg -> m Lisp)

constructor

-> (forall arg dt. IsDatatype dt => Datatype dt -> Constr dt arg -> m Lisp)

constructor tests

-> (forall dt res. IsDatatype dt => Datatype dt -> Field dt res -> m Lisp)

field accesses

-> (forall t. fv t -> m Lisp)

function variables

-> (forall t. lv t -> m Lisp)

let variables

-> (forall t'. e t' -> m Lisp)

sub expressions

-> Expression v qv fun fv lv e t

-> m Lisp

valueToLisp :: Monad m => (forall arg tp. IsDatatype tp => Datatype tp -> Constr tp arg -> m Lisp) -> Value t -> m Lisp

isOverloaded :: Function fun sig -> Bool

functionSymbol

Arguments

:: (Monad m, GetFunType fun)

=> (forall arg' res'. fun '(arg', res') -> m Lisp)

How to render user functions

-> (forall arg' dt. IsDatatype dt => Datatype dt -> Constr dt arg' -> m Lisp)

How to render constructor applications

-> (forall arg' dt. IsDatatype dt => Datatype dt -> Constr dt arg' -> m Lisp)

How to render constructor tests

-> (forall dt res'. IsDatatype dt => Datatype dt -> Field dt res' -> m Lisp)

How to render field acceses

-> Function fun '(arg, res)

-> m Lisp

functionSymbolWithSig

Arguments

:: (Monad m, GetFunType fun)

=> (forall arg' res'. fun '(arg', res') -> m Lisp)

How to render user functions

-> (forall arg' dt. IsDatatype dt => Datatype dt -> Constr dt arg' -> m Lisp)

How to render constructor applications

-> (forall arg' dt. IsDatatype dt => Datatype dt -> Constr dt arg' -> m Lisp)

How to render constructor tests

-> (forall dt res'. IsDatatype dt => Datatype dt -> Field dt res' -> m Lisp)

How to render field acceses

-> Function fun '(arg, res)

-> m Lisp

typeSymbol :: Set String -> Repr t -> Lisp

typeList :: List Repr t -> Lisp

ordSymbol :: OrdOp -> Lisp

arithSymbol :: ArithOp -> Lisp

numToLisp :: Integer -> Lisp

clearInput :: SMTPipe -> IO ()

putRequest :: SMTPipe -> Lisp -> IO ()

parseResponse :: SMTPipe -> IO Lisp

genName :: SMTPipe -> String -> (Text, SMTPipe)

genName' :: Map String Int -> String -> (Text, Map String Int)

tacticToLisp :: Tactic -> Lisp

probeToLisp :: Probe a -> Lisp