kdrag.kernel.decl_occurs

kdrag.kernel.decl_occurs(f: FuncDeclRef, body: ExprRef) → bool

Check if symbol f appears in body.

>>> x = smt.Int("x")
>>> y = smt.Bool("y")
>>> f = smt.Function("f", smt.IntSort(), smt.BoolSort(), smt.IntSort())
>>> assert decl_occurs(f, 1 + f(x, y))
>>> assert not decl_occurs(f, x + y + 1)

Parameters:

f (FuncDeclRef)
body (ExprRef)

Return type:

bool