kdrag.solvers.kb.orient

kdrag.solvers.kb.orient(eq: ~z3.z3.BoolRef | ~z3.z3.QuantifierRef, order=<function kbo>) → RewriteRule

Orient an equation into a rewrite rule.

>>> x,y,z = smt.Reals("x y z")
>>> orient(smt.ForAll([x], -(-x) == x))
RewriteRule(vs=[X!...], lhs=--X!..., rhs=X!..., pf=None)
>>> orient(smt.ForAll([x], x == -(-x)))
RewriteRule(vs=[X!...], lhs=--X!..., rhs=X!..., pf=None)
>>> orient(smt.ForAll([x,y,z], x + z == x + y + z + x + y))
RewriteRule(vs=[X!...], lhs=X!... + Y!... + Z!... + X!... + Y!..., rhs=X!... + Z!..., pf=None)

Parameters:

eq (BoolRef | QuantifierRef)

Return type:

RewriteRule