Empty sequence / set.
(s: SortRef)
| 3921 | |
| 3922 | |
| 3923 | def Empty(s: SortRef) -> ExprRef: |
| 3924 | """Empty sequence / set.""" |
| 3925 | if isinstance(s, StringSortRef): |
| 3926 | return StringVal("") |
| 3927 | if isinstance(s, ArraySortRef): |
| 3928 | return EmptySet(s.domain()) |
| 3929 | if isinstance(s, SeqSortRef): |
| 3930 | return SeqRef(SeqEmptyNode(s._elem._ast_sort), s) |
| 3931 | return StringVal("") |
| 3932 | |
| 3933 | |
| 3934 | def Full(s: SortRef) -> ExprRef: |