kdrag.kernel.unfold

kdrag.kernel.unfold(e: ExprRef, decls: Sequence[FuncDeclRef]) → tuple[ExprRef, Proof]

Unfold function definitions in an expression.

>>> x,y = smt.Ints("x y")
>>> f = define("f", [x,y], x + 2*y)
>>> g = define("g", [x,y], f(x,y) + 1)
>>> unfold(f(42,13) + g(7,8), [f])
(42 + 2*13 + g(7, 8), |= f(42, 13) + g(7, 8) == 42 + 2*13 + g(7, 8))
>>> unfold(f(42,13) + g(7,8), [f,g])
(42 + 2*13 + f(7, 8) + 1, |= f(42, 13) + g(7, 8) == 42 + 2*13 + f(7, 8) + 1)

Parameters:

e (ExprRef)
decls (Sequence[FuncDeclRef])

Return type:

tuple[ExprRef, Proof]