MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / SubString

Function SubString

lean_py/z3/core.py:2321–2328  ·  view source on GitHub ↗

Extract substring.

(s: StringRef, offset: ArithRef | int, length: ArithRef | int)

Source from the content-addressed store, hash-verified

2319
2320
2321def SubString(s: StringRef, offset: ArithRef | int, length: ArithRef | int) -> StringRef:
2322 """Extract substring."""
2323 if isinstance(offset, int):
2324 offset = IntVal(offset)
2325 if isinstance(length, int):
2326 length = IntVal(length)
2327 merged: frozenset[tuple[str, ASTSort]] = frozenset().union(s._vars, offset._vars, length._vars)
2328 return StringRef(StrSubstrNode(s._ast, offset._ast, length._ast), merged)
2329
2330
2331def IndexOf(s: StringRef, substr: StringRef, offset: ArithRef | int = 0) -> ArithRef:

Callers 5

test_substringMethod · 0.90
test_substringMethod · 0.90
test_substringMethod · 0.90
SubSeqFunction · 0.85
AtFunction · 0.85

Calls 3

StrSubstrNodeClass · 0.90
IntValFunction · 0.85
StringRefClass · 0.85

Tested by 3

test_substringMethod · 0.72
test_substringMethod · 0.72
test_substringMethod · 0.72