kdrag.rewrite.rewrite

kdrag.rewrite.rewrite(t: ExprRef, rules: list[RewriteRule], trace=None) → ExprRef

Sweep through term once performing rewrites.

>>> x = smt.Real("x")
>>> rule = RewriteRule([x], x**2, x*x)
>>> rewrite((x**2)**2, [rule])
x*x*x*x

Parameters:

Return type:

ExprRef