kdrag.theories.logic.axioms.unfold

kdrag.theories.logic.axioms.unfold(e: ExprRef, defn_eqs: Sequence[Proof])

Unfold a definitional equation. The order of variables is off from what kd.define returns.

>>> x = smt.Int("x")
>>> y = smt.Real("y")
>>> f = smt.Function("test_f", smt.IntSort(), smt.RealSort(), smt.RealSort())
>>> defn = kd.axiom(smt.ForAll([y,x], f(x,y) == (x + 2*y)))
>>> unfold(f(7,8), [defn])
|= test_f(7, 8) == ToReal(7) + 2*8

Parameters:

• e (ExprRef)

• defn_eqs (Sequence[Proof])