Base sort.
| 119 | |
| 120 | |
| 121 | class SortRef: |
| 122 | """Base sort.""" |
| 123 | |
| 124 | __slots__ = ("_ast_sort",) |
| 125 | |
| 126 | def __init__(self, ast_sort: ASTSort) -> None: |
| 127 | self._ast_sort = ast_sort |
| 128 | |
| 129 | def __repr__(self) -> str: |
| 130 | return _sort_repr(self._ast_sort) |
| 131 | |
| 132 | def __eq__(self, other: object) -> bool: |
| 133 | return isinstance(other, SortRef) and self._ast_sort == other._ast_sort |
| 134 | |
| 135 | def __hash__(self) -> int: |
| 136 | return hash(self._ast_sort) |
| 137 | |
| 138 | def name(self) -> str: |
| 139 | """Return sort name as string (z3py compat).""" |
| 140 | return _sort_repr(self._ast_sort) |
| 141 | |
| 142 | def kind(self) -> int: |
| 143 | """Return sort kind as integer (z3py compat). |
| 144 | |
| 145 | Values match z3 Z3_sort_kind: UNINTERPRETED=0, BOOL=1, INT=2, |
| 146 | REAL=3, BV=4, ARRAY=5, DATATYPE=6, UNKNOWN=1000. |
| 147 | """ |
| 148 | s = self._ast_sort |
| 149 | if isinstance(s, PropSort): |
| 150 | return 1 # Z3_BOOL_SORT |
| 151 | if isinstance(s, IntASTSort): |
| 152 | return 2 # Z3_INT_SORT |
| 153 | if isinstance(s, NatASTSort): |
| 154 | return 2 # treat Nat as int kind |
| 155 | if isinstance(s, RealASTSort): |
| 156 | return 3 # Z3_REAL_SORT |
| 157 | if isinstance(s, BitvecASTSort): |
| 158 | return 4 # Z3_BV_SORT |
| 159 | if isinstance(s, ArrowASTSort): |
| 160 | return 5 # Z3_ARRAY_SORT |
| 161 | if isinstance(s, StringASTSort): |
| 162 | return 7 # Z3_SEQ_SORT |
| 163 | if isinstance(s, UninterpASTSort): |
| 164 | return 0 # Z3_UNINTERPRETED_SORT |
| 165 | if isinstance(s, InductiveASTSort): |
| 166 | return 6 # Z3_DATATYPE_SORT |
| 167 | return 1000 # Z3_UNKNOWN_SORT |
| 168 | |
| 169 | def sexpr(self) -> str: |
| 170 | """S-expression representation of this sort.""" |
| 171 | return _sort_repr(self._ast_sort) |
| 172 | |
| 173 | |
| 174 | class BoolSortRef(SortRef): |
no outgoing calls
no test coverage detected