kdrag.rewrite.beta

kdrag.rewrite.beta(e: ExprRef) → ExprRef

Do one pass of beta normalization.

>>> x = smt.Int("x")
>>> y = smt.String("y")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> beta(f(x))
f(x)
>>> beta(f(smt.Lambda([x], f(x))[1]))
f(f(1))
>>> beta(f(smt.Select(smt.Lambda([x,y], x), 1, smt.StringVal("fred"))))
f(1)

Parameters:

e (ExprRef)

Return type:

ExprRef