smtlib2-1.0: A type-safe interface to communicate with an SMT solver.

Safe HaskellNone
LanguageHaskell98

Language.SMTLib2.Internals.Evaluate

Documentation

data EvalResult fun res where Source #

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

Methods

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

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

Methods

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

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

Methods

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

GetFunType fun => GetType (EvalResult fun) Source # 

Methods

getType :: EvalResult fun tp -> Repr tp Source #

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

Methods

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

show :: EvalResult fun res -> String #

showList :: [EvalResult fun res] -> ShowS #

data ArrayModel fun idx el where Source #

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

Methods

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

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

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

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

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

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

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

typeNumElements :: Repr t -> Maybe Integer Source #

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

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

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

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

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

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

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