Return sort kind as integer (z3py compat). Values match z3 Z3_sort_kind: UNINTERPRETED=0, BOOL=1, INT=2, REAL=3, BV=4, ARRAY=5, DATATYPE=6, UNKNOWN=1000.
(self)
| 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.""" |
no outgoing calls