kdrag.smt.codomain

kdrag.smt.codomain(f: FuncRef | ArraySortRef) → SortRef

>>> x = Int("x")
>>> y = Int("y")
>>> f = Array("f", IntSort(), RealSort())
>>> codomain(f)
Real
>>> lam = Lambda([x, y], x + y)
>>> codomain(lam)
Int

Parameters:

f (FuncRef | ArraySortRef)

Return type:

SortRef