Improve Extract function documentation to clarify bit-vector vs sequence usage (#7701)

* Initial plan

* Improve Extract function documentation to clarify bit-vector vs sequence usage

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

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)