kdrag.rewrite.rewrite

kdrag.rewrite.rewrite(t: ExprRef, rules: Sequence[BoolRef | QuantifierRef | Proof | RewriteRule], 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 (Sequence[BoolRef | QuantifierRef | Proof | RewriteRule])

Return type:

ExprRef