kdrag.solvers.kb.all_pairs

kdrag.solvers.kb.all_pairs(rules)

Find all the ways the left hand side of two rules can overlap. Return a derived equation

>>> a,b,c,d = smt.Reals("a b c d")
>>> all_pairs([rw.RewriteRule(vs=[], lhs=x, rhs=y) for x,y in [(a,b), (b,c), (a,c), (a,d)]])
[b == b, b == c, b == d, c == c, c == b, c == c, c == d, d == b, d == c, d == d]