kdrag.utils.free_vars

kdrag.utils.free_vars(t: ExprRef) → set[ExprRef]

Return free variables in an expression. Looks at kernel.defns to determine if contacts are free. If you have meaningful constants no registered there, this may not work.

>>> x,y = smt.Ints("x y")
>>> free_vars(smt.Lambda([x], x + y + 1))
{y}

Parameters:

t (ExprRef)

Return type:

set[ExprRef]