kdrag.solvers.kb.huet

kdrag.solvers.kb.huet(E: list[~z3.z3.BoolRef | ~z3.z3.QuantifierRef], order=<function kbo>) → list[RewriteRule]

Huet completion is a particular strategy.

Parameters:

E (list[BoolRef | QuantifierRef])

Return type:

list[RewriteRule]