Documentation

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 () #

Methods

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

Methods

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

Methods

gshowsPrec :: Int -> t a -> ShowS #

Methods

getType :: Expr SMTPipe tp -> Repr tp #

Methods

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

show :: Expr SMTPipe t -> String #

showList :: [Expr SMTPipe t] -> ShowS #