kdrag.theories.set.EClass

kdrag.theories.set.EClass(x: ExprRef, eqrel) → QuantifierRef

Equivalence class [x] under equivalence relation eqrel. The set of all v such that eqrel(x, v) holds. https://en.wikipedia.org/wiki/Equivalence_class

>>> x,y = smt.Ints("x y")
>>> (A := EClass(x, lambda a,b: a % 3 == b % 3))
Lambda(v!..., x%3 == v!...%3)
>>> kd.prove(EClass(3, lambda a,b: a % 3 == b % 3)[3])
|= Lambda(v!..., 3%3 == v!...%3)[3]

Parameters:

x (ExprRef)

Return type:

QuantifierRef