kdrag.property.assoc_norm

kdrag.property.assoc_norm(e: ExprRef, trace=None) → ExprRef

>>> T = smt.DeclareSort("T")
>>> x, y, z,w = smt.Ints("x y z w")
>>> assoc_norm((x + y) + (z + w)).eq(x + (y + (z + w)))
True