kdrag.utils.lambda_lift

kdrag.utils.lambda_lift(expr: ExprRef) → tuple[ExprRef, list[BoolRef]]

Traverses expression and lifts out lambdas to fresh top level functions. https://en.wikipedia.org/wiki/Lambda_lifting

>>> x,y,z = smt.Ints("x y z")
>>> lambda_lift(smt.ForAll([x,y], smt.Exists([z], x + y + 1 == smt.Lambda([z], x)[z])))
(ForAll([x, y], Exists(z, x + y + 1 == f!...(x, y)[z])), [ForAll([x, y, z], f!...(x, y)[z] == x)])

Parameters:

expr (ExprRef)

Return type:

tuple[ExprRef, list[BoolRef]]