kdrag.smt.domains

kdrag.smt.domains(f: FuncRef | ArraySortRef) → list[SortRef]

Get the domain sorts of a lambda or an array.

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

Parameters:

f (FuncRef | ArraySortRef)

Return type:

list[SortRef]