Language.SMTLib2.Internals.Evaluate

Documentation

data EvalResult fun res where

Constructors

ValueResult :: Value res -> EvalResult fun res

ArrayResult :: ArrayModel fun idx el -> EvalResult fun (ArrayType idx el)

Instances

GCompare ([Type], Type) fun => GCompare Type (EvalResult fun)

Methods

gcompare :: f a -> f b -> GOrdering (EvalResult fun) a b

GEq ([Type], Type) fun => GEq Type (EvalResult fun)

Methods

geq :: f a -> f b -> Maybe ((EvalResult fun := a) b)

GShow ([Type], Type) fun => GShow Type (EvalResult fun)

Methods

gshowsPrec :: Int -> t a -> ShowS

GetFunType fun => GetType (EvalResult fun)

Methods

getType :: EvalResult fun tp -> Repr tp

GShow ([Type], Type) fun => Show (EvalResult fun res)

Methods

showsPrec :: Int -> EvalResult fun res -> ShowS

show :: EvalResult fun res -> String

showList :: [EvalResult fun res] -> ShowS

data ArrayModel fun idx el where

Constructors

ArrayConst :: EvalResult fun el -> List Repr idx -> ArrayModel fun idx el

ArrayFun :: Function fun '(idx, res) -> ArrayModel fun idx res

ArrayMap :: Function fun '(arg, res) -> List (ArrayModel fun idx) arg -> List Repr idx -> ArrayModel fun idx res

ArrayStore :: List (EvalResult fun) idx -> EvalResult fun el -> ArrayModel fun idx el -> ArrayModel fun idx el

Instances

GShow ([Type], Type) fun => GShow Type (ArrayModel fun idx)

Methods

gshowsPrec :: Int -> t a -> ShowS

GShow ([Type], Type) fun => Show (ArrayModel fun idx el)

Methods

showsPrec :: Int -> ArrayModel fun idx el -> ShowS

show :: ArrayModel fun idx el -> String

showList :: [ArrayModel fun idx el] -> ShowS

type FunctionEval m fun = forall tps r. fun '(tps, r) -> List (EvalResult fun) tps -> m (EvalResult fun r)

type FieldEval m fun = forall dt par args tp. IsDatatype dt => List Repr par -> Field dt tp -> List Value args -> m (EvalResult fun (CType tp par))

evalResultType :: GetFunType fun => EvalResult fun res -> Repr res

arrayModelType :: GetFunType fun => ArrayModel fun idx res -> (List Repr idx, Repr res)

evaluateArray :: (Monad m, GetFunType fun) => FunctionEval m fun -> FieldEval m fun -> ArrayModel fun idx el -> List (EvalResult fun) idx -> m (EvalResult fun el)

typeNumElements :: Repr t -> Maybe Integer

evalResultEq :: (Monad m, GetFunType fun) => FunctionEval m fun -> FieldEval m fun -> EvalResult fun res -> EvalResult fun res -> m Bool

arrayModelEq :: (Monad m, GetFunType fun) => FunctionEval m fun -> FieldEval m fun -> ArrayModel fun idx t -> ArrayModel fun idx t -> [List (EvalResult fun) idx] -> m Bool

evaluateExpr :: (Monad m, GCompare lv, GetFunType fun) => (forall t. v t -> m (EvalResult fun t)) -> (forall t. qv t -> m (EvalResult fun t)) -> (forall t. fv t -> m (EvalResult fun t)) -> FunctionEval m fun -> FieldEval m fun -> (forall arg. Quantifier -> List qv arg -> e BoolType -> m (EvalResult fun BoolType)) -> DMap lv (EvalResult fun) -> (forall t. DMap lv (EvalResult fun) -> e t -> m (EvalResult fun t)) -> Expression v qv fun fv lv e res -> m (EvalResult fun res)

evaluateFun :: forall m fun arg res. (Monad m, GetFunType fun) => FunctionEval m fun -> FieldEval m fun -> Function fun '(arg, res) -> List (EvalResult fun) arg -> m (EvalResult fun res)

getArrayModelType :: GetFunType fun => ArrayModel fun idx el -> (List Repr idx, Repr el)

geqArrayModel :: GEq fun => ArrayModel fun idx1 el1 -> ArrayModel fun idx2 el2 -> Maybe (idx1 :~: idx2, el1 :~: el2)

gcompareArrayModel :: GCompare fun => ArrayModel fun idx1 el1 -> ArrayModel fun idx2 el2 -> (GOrdering idx1 idx2, GOrdering el1 el2)