kdrag.rewrite.all_narrow

kdrag.rewrite.all_narrow(vs: list[ExprRef], t: ExprRef, lhs: ExprRef, rhs: ExprRef) → list[tuple[ExprRef, dict[ExprRef, ExprRef]]]

Look for pattern lhs to unify with a subterm of t. returns a list of all of those lhs -> rhs applied + the substitution resulting from the unification. The substitution is so that we can apply the other t -> s rule once we return.

This helper is asymmettric between t and lhs. You need to call it twice to get all critical pairs.

>>> x,y,z = smt.Reals("x y z")
>>> all_narrow([x,y], -(-(-(x))), -(-(y)), y)
[(y, {y: -x}), (-y, {x: y}), (--y, {x: -y})]

Parameters:

• vs (list[ExprRef])

• t (ExprRef)

• lhs (ExprRef)

• rhs (ExprRef)

Return type:

list[tuple[ExprRef, dict[ExprRef, ExprRef]]]