Create a singleton set containing e.
(e: ExprRef, sort: SortRef | None = None)
| 3712 | |
| 3713 | |
| 3714 | def Singleton(e: ExprRef, sort: SortRef | None = None) -> ArrayRef: |
| 3715 | """Create a singleton set containing e.""" |
| 3716 | if sort is None: |
| 3717 | sort = e._sort |
| 3718 | return SetAdd(EmptySet(sort), e) |
| 3719 | |
| 3720 | |
| 3721 | def FiniteSetSize(s: ArrayRef) -> ArithRef: |