kdrag.utils.eunifyļƒ

kdrag.utils.eunify(vs: list[ExprRef], goal: BoolRef, term_gen_heuristic=None) → tuple[dict[ExprRef, ExprRef], BoolRef | None] | Noneļƒ

Bottom up E-unification. Returns a substitution and remaining constraint. It is possible it makes no progress.

https://www.philipzucker.com/smt_unify/ >>> x,y,z = smt.Ints(ā€œx y zā€) >>> eunify([x,y], smt.And(x + 1 == y, y + 1 == 3)) ({x: 1, y: 2}, None) >>> eunify([x,y,z], smt.And(x + y == z + 3*x, z + 1 + y == 3)) ({z: -2*x + y}, -2*x + 2*y == 2)

Parameters:

  • vs (list[ExprRef])

  • goal (BoolRef)

Return type:

tuple[dict[ExprRef, ExprRef], BoolRef | None] | None