kdrag.theories.logic.axioms.rename_vars2
- kdrag.theories.logic.axioms.rename_vars2(pf: Proof, vs: list[ExprRef], patterns=[], no_patterns=[]) Proof
Rename bound variables and also attach triggers
>>> x,y = smt.Ints("x y") >>> f = smt.Function("f", smt.IntSort(), smt.IntSort()) >>> rename_vars2(kd.prove(smt.ForAll([x, y], x + 1 > x)), [y,x], patterns=[x+y]) |= ForAll([y, x], y + 1 > y) >>> rename_vars2(kd.prove(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))