kdrag.rewrite.rewrite_slow

kdrag.rewrite.rewrite_slow(t: ExprRef, rules: list[BoolRef | QuantifierRef | Proof], trace=None) → ExprRef

Repeat rewrite until no more rewrites are possible.

>>> x,y,z = smt.Reals("x y z")
>>> unit = kd.prove(smt.ForAll([x], x + 0 == x))
>>> x + 0 + 0 + 0 + 0
x + 0 + 0 + 0 + 0
>>> rewrite(x + 0 + 0 + 0 + 0, [unit])
x

Parameters:

t (ExprRef)
rules (list[BoolRef | QuantifierRef | Proof])

Return type:

ExprRef