kdrag.kernel.rename_vars

kdrag.kernel.rename_vars(t: QuantifierRef, vs: list[ExprRef]) → tuple[QuantifierRef, Proof]

>>> x,y = smt.Ints("x y")
>>> rename_vars(smt.ForAll([x, y], x + 1 > y), [y,x])
(ForAll([y, x], y + 1 > x), |= (ForAll([x, y], x + 1 > y)) == (ForAll([y, x], y + 1 > x)))
>>> rename_vars(smt.Exists([x], x + 1 > y), [y])
Traceback (most recent call last):
    ...
ValueError: ('Cannot rename vars to ones that already occur in term', [y], Exists(x, x + 1 > y))

Parameters:

t (QuantifierRef)
vs (list[ExprRef])

Return type:

tuple[QuantifierRef, Proof]