smtlib2-debug-1.0: Dump the communication with an SMT solver for debugging purposes.

Safe HaskellNone
LanguageHaskell98

Language.SMTLib2.Debug

Documentation

data DebugBackend b Source #

Instances

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

Methods

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

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

Methods

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

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

Methods

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

Backend b => Backend (DebugBackend b) Source # 

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

Methods

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

type Proof (DebugBackend b) Source # 
type Proof (DebugBackend b) = Proof b
type Model (DebugBackend b) Source # 
type Model (DebugBackend b) = Model b
type ClauseId (DebugBackend b) Source # 
type LVar (DebugBackend b) Source # 
type LVar (DebugBackend b) = LVar b
type FunArg (DebugBackend b) Source # 
type Fun (DebugBackend b) Source # 
type Fun (DebugBackend b) = Fun b
type QVar (DebugBackend b) Source # 
type QVar (DebugBackend b) = QVar b
type Var (DebugBackend b) Source # 
type Var (DebugBackend b) = Var b
data Expr (DebugBackend b) Source # 
data Expr (DebugBackend b) = DebugExpr (Expr b t)
type SMTMonad (DebugBackend b) Source # 

debugBackend' Source #

Arguments

:: (Backend b, MonadIO (SMTMonad b)) 
=> Bool

Display line number

-> Bool

Use color codes

-> Maybe String

Prefix name

-> Handle

Output handle

-> b 
-> DebugBackend b