kdrag.utils.propagate_eqs

kdrag.utils.propagate_eqs(terms: list[ExprRef], known: BoolRef) → list[BoolRef]

Given a list of terms, propagate equalities among them that are implied by known. >>> x,y,z = smt.Ints(“x y z”) >>> terms = [x, y, z, x + 1, y + 1] >>> known = smt.And(x == y, y == z) >>> propagate_eqs(terms, known) [y == x, z == x, z == y, y + 1 == x + 1]

Parameters: