kdrag.utils.free_in

kdrag.utils.free_in(vs: list[ExprRef], t: ExprRef) → bool

Returns True if none of the variables in vs exist unbound in t.

>>> x,y,z = smt.Ints("x y z")
>>> assert not free_in([x], x + y + z)
>>> assert free_in([x], y + z)
>>> assert free_in([x], smt.Lambda([x], x + y + z))

Parameters:

• vs (list[ExprRef])

• t (ExprRef)

Return type:

bool