kdrag.rewrite.full_simp

kdrag.rewrite.full_simp(e: ExprRef, trace=None) → ExprRef

Fully simplify using definitions and built in z3 simplifier until no progress is made.

>>> import kdrag.theories.nat as nat
>>> full_simp(nat.one + nat.one + nat.S(nat.one))
S(S(S(S(Z))))

>>> p = smt.Bool("p")
>>> full_simp(smt.If(p, 42, 3))
If(p, 42, 3)