diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5f0d35320..41df1fe69 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4216,21 +4216,44 @@ def Concat(*args): def Extract(high, low, a): - """Create a Z3 bit-vector extraction expression. - Extract is overloaded to also work on sequence extraction. - The functions SubString and SubSeq are redirected to Extract. - For this case, the arguments are reinterpreted as: - high - is a sequence (string) - low - is an offset - a - is the length to be extracted + """Create a Z3 bit-vector extraction expression or sequence extraction expression. + + Extract is overloaded to work with both bit-vectors and sequences: + + **Bit-vector extraction**: Extract(high, low, bitvector) + Extracts bits from position `high` down to position `low` (both inclusive). + - high: int - the highest bit position to extract (0-indexed from right) + - low: int - the lowest bit position to extract (0-indexed from right) + - bitvector: BitVecRef - the bit-vector to extract from + Returns a new bit-vector containing bits [high:low] + + **Sequence extraction**: Extract(sequence, offset, length) + Extracts a subsequence starting at the given offset with the specified length. + The functions SubString and SubSeq are redirected to this form of Extract. + - sequence: SeqRef or str - the sequence to extract from + - offset: int - the starting position (0-indexed) + - length: int - the number of elements to extract + Returns a new sequence containing the extracted subsequence + >>> # Bit-vector extraction examples >>> x = BitVec('x', 8) - >>> Extract(6, 2, x) + >>> Extract(6, 2, x) # Extract bits 6 down to 2 (5 bits total) Extract(6, 2, x) - >>> Extract(6, 2, x).sort() + >>> Extract(6, 2, x).sort() # Result is a 5-bit vector BitVec(5) - >>> simplify(Extract(StringVal("abcd"),2,1)) + >>> Extract(7, 0, x) # Extract all 8 bits + Extract(7, 0, x) + >>> Extract(3, 3, x) # Extract single bit at position 3 + Extract(3, 3, x) + + >>> # Sequence extraction examples + >>> s = StringVal("hello") + >>> Extract(s, 1, 3) # Extract 3 characters starting at position 1 + Extract(StringVal("hello"), 1, 3) + >>> simplify(Extract(StringVal("abcd"), 2, 1)) # Extract 1 character at position 2 "c" + >>> simplify(Extract(StringVal("abcd"), 0, 2)) # Extract first 2 characters + "ab" """ if isinstance(high, str): high = StringVal(high) @@ -11186,12 +11209,30 @@ def Strings(names, ctx=None): def SubString(s, offset, length): - """Extract substring or subsequence starting at offset""" + """Extract substring or subsequence starting at offset. + + This is a convenience function that redirects to Extract(s, offset, length). + + >>> s = StringVal("hello world") + >>> SubString(s, 6, 5) # Extract "world" + Extract(StringVal("hello world"), 6, 5) + >>> simplify(SubString(StringVal("hello"), 1, 3)) + "ell" + """ return Extract(s, offset, length) def SubSeq(s, offset, length): - """Extract substring or subsequence starting at offset""" + """Extract substring or subsequence starting at offset. + + This is a convenience function that redirects to Extract(s, offset, length). + + >>> s = StringVal("hello world") + >>> SubSeq(s, 0, 5) # Extract "hello" + Extract(StringVal("hello world"), 0, 5) + >>> simplify(SubSeq(StringVal("testing"), 2, 4)) + "stin" + """ return Extract(s, offset, length)