kdrag.utils.subterms

kdrag.utils.subterms(t: ExprRef, into_binder=False)

Generate all subterms of a term

>>> x,y = smt.Ints("x y")
>>> list(subterms(x + y == y))
[x + y == y, y, x + y, y, x]
>>> list(subterms(smt.ForAll([x], x + y == y)))
[ForAll(x, x + y == y)]
>>> list(subterms(smt.ForAll([x], x + y == y), into_binder=True))
[ForAll(x, x + y == y), Var(0) + y == y, y, Var(0) + y, y, Var(0)]

Parameters:

t (ExprRef)