kdrag.rewrite.unfold

kdrag.rewrite.unfold(e: ExprRef, decls: Sequence[FuncDeclRef] | None = None, trace=None) → ExprRef

>>> x = smt.Int("x")
>>> f = kd.define("f", [x], x + 42)
>>> trace = []
>>> unfold(f(1), trace=trace)
1 + 42
>>> trace
[|= f(1) == 1 + 42]

>>> unfold(smt.Lambda([x], f(x)))
Lambda(x, x + 42)

Parameters:

Return type:

ExprRef