Language.SMTLib2.Internals.Evaluate

Documentation

data EvalResult fun con field res where

Constructors

ValueResult :: Value con res -> EvalResult fun con field res

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

data ArrayModel fun con field idx el where

Constructors

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

ArrayFun :: Function fun con field `(idx, res)` -> ArrayModel fun con field idx res

ArrayMap :: Function fun con field `(arg, res)` -> List (ArrayModel fun con field idx) arg -> List Repr idx -> ArrayModel fun con field idx res

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

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

type FieldEval m fun con field = forall dt args tp. IsDatatype dt => field `(dt, tp)` -> con `(args, dt)` -> List (Value con) args -> m (EvalResult fun con field tp)

evalResultType :: (GetFunType fun, GetConType con, GetFieldType field) => EvalResult fun con field res -> Repr res

arrayModelType :: (GetFunType fun, GetConType con, GetFieldType field) => ArrayModel fun con field idx res -> (List Repr idx, Repr res)

evaluateArray :: (Monad m, Typeable con, GCompare con, GetFunType fun, GetConType con, GetFieldType field) => FunctionEval m fun con field -> FieldEval m fun con field -> ArrayModel fun con field idx el -> List (EvalResult fun con field) idx -> m (EvalResult fun con field el)

typeNumElements :: Repr t -> Maybe Integer

evalResultEq :: (Monad m, Typeable con, GCompare con, GetFunType fun, GetConType con, GetFieldType field) => FunctionEval m fun con field -> FieldEval m fun con field -> EvalResult fun con field res -> EvalResult fun con field res -> m Bool

arrayModelEq :: (Monad m, Typeable con, GCompare con, GetFunType fun, GetConType con, GetFieldType field) => FunctionEval m fun con field -> FieldEval m fun con field -> ArrayModel fun con field idx t -> ArrayModel fun con field idx t -> [List (EvalResult fun con field) idx] -> m Bool

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

evaluateFun :: forall m fun con field arg res. (Monad m, Typeable con, GCompare con, GetFunType fun, GetConType con, GetFieldType field) => FunctionEval m fun con field -> FieldEval m fun con field -> Function fun con field `(arg, res)` -> List (EvalResult fun con field) arg -> m (EvalResult fun con field res)