String or sequence length.
(s: StringRef | SeqRef)
| 2285 | |
| 2286 | |
| 2287 | def Length(s: StringRef | SeqRef) -> ArithRef: |
| 2288 | """String or sequence length.""" |
| 2289 | if isinstance(s, SeqRef): |
| 2290 | return ArithRef(SeqLenNode(s._ast), IntSort(), s._vars) |
| 2291 | return ArithRef(StrLenNode(s._ast), IntSort(), s._vars) |
| 2292 | |
| 2293 | |
| 2294 | def Contains(s: StringRef | SeqRef, t: StringRef | SeqRef) -> BoolRef: |