kdrag.rewrite.unfold

kdrag.rewrite.unfold(e: ExprRef, decls=None, trace=None) → ExprRef

Do a single unfold sweep, unfolding definitions defined by kd.define. The optional trace parameter will record proof along the way. decls is an optional list of declarations to unfold. If None, all definitions are unfolded.

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

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

Parameters:

e (ExprRef)

Return type:

ExprRef