Language.SMTLib2.Debug

Documentation

data DebugBackend b

Instances

Backend b => GCompare Type (Expr (DebugBackend b))

Methods

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

Backend b => GEq Type (Expr (DebugBackend b))

Methods

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

Backend b => GShow Type (Expr (DebugBackend b))

Methods

gshowsPrec :: Int -> t a -> ShowS

Backend b => Backend (DebugBackend b)

Associated Types

type SMTMonad (DebugBackend b) :: * -> *

data Expr (DebugBackend b) (a :: Type) :: *

type Var (DebugBackend b) :: Type -> *

type QVar (DebugBackend b) :: Type -> *

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

type FunArg (DebugBackend b) :: Type -> *

type LVar (DebugBackend b) :: Type -> *

type ClauseId (DebugBackend b) :: *

type Model (DebugBackend b) :: *

type Proof (DebugBackend b) :: *

Methods

setOption :: SMTOption -> SMTAction (DebugBackend b) ()

getInfo :: SMTInfo i -> SMTAction (DebugBackend b) i

comment :: String -> SMTAction (DebugBackend b) ()

push :: SMTAction (DebugBackend b) ()

pop :: SMTAction (DebugBackend b) ()

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

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

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

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

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

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

assert :: Expr (DebugBackend b) BoolType -> SMTAction (DebugBackend b) ()

assertId :: Expr (DebugBackend b) BoolType -> SMTAction (DebugBackend b) (ClauseId (DebugBackend b))

assertPartition :: Expr (DebugBackend b) BoolType -> Partition -> SMTAction (DebugBackend b) ()

checkSat :: Maybe Tactic -> CheckSatLimits -> SMTAction (DebugBackend b) CheckSatResult

getUnsatCore :: SMTAction (DebugBackend b) [ClauseId (DebugBackend b)]

getValue :: Expr (DebugBackend b) t -> SMTAction (DebugBackend b) (Value t)

getModel :: SMTAction (DebugBackend b) (Model (DebugBackend b))

modelEvaluate :: Model (DebugBackend b) -> Expr (DebugBackend b) t -> SMTAction (DebugBackend b) (Value t)

getProof :: SMTAction (DebugBackend b) (Proof (DebugBackend b))

analyzeProof :: DebugBackend b -> Proof (DebugBackend b) -> Proof String (Expr (DebugBackend b)) (Proof (DebugBackend b))

simplify :: Expr (DebugBackend b) t -> SMTAction (DebugBackend b) (Expr (DebugBackend b) t)

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

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

declareDatatypes :: [AnyDatatype] -> SMTAction (DebugBackend b) ()

interpolate :: SMTAction (DebugBackend b) (Expr (DebugBackend b) BoolType)

exit :: SMTAction (DebugBackend b) ()

Backend b => GetType (Expr (DebugBackend b))

Methods

getType :: Expr (DebugBackend b) tp -> Repr tp

type Proof (DebugBackend b)

type Proof (DebugBackend b) = Proof b

type Model (DebugBackend b)

type Model (DebugBackend b) = Model b

type ClauseId (DebugBackend b)

type ClauseId (DebugBackend b) = ClauseId b

type LVar (DebugBackend b)

type LVar (DebugBackend b) = LVar b

type FunArg (DebugBackend b)

type FunArg (DebugBackend b) = FunArg b

type Fun (DebugBackend b)

type Fun (DebugBackend b) = Fun b

type QVar (DebugBackend b)

type QVar (DebugBackend b) = QVar b

type Var (DebugBackend b)

type Var (DebugBackend b) = Var b

data Expr (DebugBackend b)

data Expr (DebugBackend b) = DebugExpr (Expr b t)

type SMTMonad (DebugBackend b)

type SMTMonad (DebugBackend b) = SMTMonad b

debugBackend :: (Backend b, MonadIO (SMTMonad b)) => b -> DebugBackend b

namedDebugBackend :: (Backend b, MonadIO (SMTMonad b)) => String -> b -> DebugBackend b

debugBackend'

Arguments

:: (Backend b, MonadIO (SMTMonad b))

=> Bool

Display line number

-> Bool

Use color codes

-> Maybe String

Prefix name

-> Handle

Output handle

-> b

-> DebugBackend b