kdrag.theories.set.Set

kdrag.theories.set.Set(T)

Sets of elements of sort T. This registers a number of helper notations and useful lemmas.

>>> IntSet = Set(smt.IntSort())
>>> IntSet.empty
K(Int, False)
>>> IntSet.full
K(Int, True)
>>> A,B = smt.Consts("A B", IntSet)
>>> A & B
intersection(A, B)
>>> A | B
union(A, B)
>>> A - B
setminus(A, B)
>>> A <= B
subset(A, B)
>>> A < B
And(subset(A, B), A != B)
>>> A >= B
subset(B, A)
>>> IntSet.union_comm
|- ForAll([A, B], union(A, B) == union(B, A))