From 3b16d73f478041d7c1f0473ac95cc9eb122d870a Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 17 Jan 2026 19:01:47 +0000
Subject: [PATCH] Add advanced sequence operations to C# API

- Add MkSeqMap: Map function over sequence
- Add MkSeqMapi: Map function over sequence with index
- Add MkSeqFoldLeft: Fold left operation on sequence
- Add MkSeqFoldLeftI: Fold left with index on sequence

These functions match Python's SeqMap, SeqMapI, SeqFoldLeft, and SeqFoldLeftI and provide feature parity with other language bindings.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/dotnet/Context.cs | 48 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 70fcbacb7..0d624ab0c 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2647,6 +2647,54 @@ namespace Microsoft.Z3
             return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
         }
 
+        /// <summary>
+        /// Map function f over the sequence s.
+        /// </summary>
+        public Expr MkSeqMap(Expr f, SeqExpr s)
+        {
+            Debug.Assert(f != null);
+            Debug.Assert(s != null);
+            CheckContextMatch(f, s);
+            return Expr.Create(this, Native.Z3_mk_seq_map(nCtx, f.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Map function f over the sequence s at index i.
+        /// </summary>
+        public Expr MkSeqMapi(Expr f, Expr i, SeqExpr s)
+        {
+            Debug.Assert(f != null);
+            Debug.Assert(i != null);
+            Debug.Assert(s != null);
+            CheckContextMatch(f, i, s);
+            return Expr.Create(this, Native.Z3_mk_seq_mapi(nCtx, f.NativeObject, i.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Fold left the function f over the sequence s with initial value a.
+        /// </summary>
+        public Expr MkSeqFoldLeft(Expr f, Expr a, SeqExpr s)
+        {
+            Debug.Assert(f != null);
+            Debug.Assert(a != null);
+            Debug.Assert(s != null);
+            CheckContextMatch(f, a, s);
+            return Expr.Create(this, Native.Z3_mk_seq_foldl(nCtx, f.NativeObject, a.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Fold left with index the function f over the sequence s with initial value a starting at index i.
+        /// </summary>
+        public Expr MkSeqFoldLeftI(Expr f, Expr i, Expr a, SeqExpr s)
+        {
+            Debug.Assert(f != null);
+            Debug.Assert(i != null);
+            Debug.Assert(a != null);
+            Debug.Assert(s != null);
+            CheckContextMatch(f, i, a, s);
+            return Expr.Create(this, Native.Z3_mk_seq_foldli(nCtx, f.NativeObject, i.NativeObject, a.NativeObject, s.NativeObject));
+        }
+
         /// <summary>
         /// Convert a regular expression that accepts sequence s.
         /// </summary>