Language.SMTLib2.Timing

Documentation

data TimingBackend b

Instances

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

Methods

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

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

Methods

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

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

Methods

gshowsPrec :: Int -> t a -> ShowS

Backend b => Backend (TimingBackend b)

Associated Types

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

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

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

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

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

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

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

type ClauseId (TimingBackend b) :: *

type Model (TimingBackend b) :: *

type Proof (TimingBackend b) :: *

Methods

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

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

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

push :: SMTAction (TimingBackend b) ()

pop :: SMTAction (TimingBackend b) ()

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

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

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

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

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

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

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

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

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

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

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

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

getModel :: SMTAction (TimingBackend b) (Model (TimingBackend b))

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

getProof :: SMTAction (TimingBackend b) (Proof (TimingBackend b))

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

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

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

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

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

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

exit :: SMTAction (TimingBackend b) ()

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

Methods

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

type Proof (TimingBackend b)

type Proof (TimingBackend b) = Proof b

type Model (TimingBackend b)

type Model (TimingBackend b) = Model b

type ClauseId (TimingBackend b)

type ClauseId (TimingBackend b) = ClauseId b

type LVar (TimingBackend b)

type LVar (TimingBackend b) = LVar b

type FunArg (TimingBackend b)

type FunArg (TimingBackend b) = FunArg b

type Fun (TimingBackend b)

type Fun (TimingBackend b) = Fun b

type QVar (TimingBackend b)

type QVar (TimingBackend b) = QVar b

type Var (TimingBackend b)

type Var (TimingBackend b) = Var b

data Expr (TimingBackend b)

data Expr (TimingBackend b) = TimingExpr (Expr b tp)

type SMTMonad (TimingBackend b)

type SMTMonad (TimingBackend b) = SMTMonad b

timingBackend :: (Backend b, MonadIO (SMTMonad b)) => (NominalDiffTime -> SMTMonad b ()) -> b -> TimingBackend b