From c6c17910aa513122570ee7f998e4227d8c773af4 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 17 Jan 2026 18:41:59 +0000
Subject: [PATCH] Add four sequence operations to Java API (SeqMap, SeqMapi,
 SeqFoldl, SeqFoldli)

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

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index fad1884c9..01ca3f293 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2235,6 +2235,46 @@ public class Context implements AutoCloseable {
         return (IntExpr)Expr.create(this, Native.mkSeqLastIndex(nCtx(), s.getNativeObject(), substr.getNativeObject()));
     }
 
+    /**
+     * Map function f over sequence s.
+     * Returns a new sequence where f is applied to each element of s.
+     */
+    public final <R extends Sort> SeqExpr<R> mkSeqMap(Expr<?> f, Expr<SeqSort<R>> s)
+    {
+        checkContextMatch(f, s);
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqMap(nCtx(), f.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Map function f over sequence s starting at index i.
+     * Returns a new sequence where f is applied to each element of s along with its index starting from i.
+     */
+    public final <R extends Sort> SeqExpr<R> mkSeqMapi(Expr<?> f, Expr<IntSort> i, Expr<SeqSort<R>> s)
+    {
+        checkContextMatch(f, i, s);
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqMapi(nCtx(), f.getNativeObject(), i.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Left fold of function f over sequence s with accumulator a.
+     * Applies f to accumulate values from left to right over the sequence.
+     */
+    public final <R extends Sort, A extends Sort> Expr<A> mkSeqFoldl(Expr<?> f, Expr<A> a, Expr<SeqSort<R>> s)
+    {
+        checkContextMatch(f, a, s);
+        return (Expr<A>) Expr.create(this, Native.mkSeqFoldl(nCtx(), f.getNativeObject(), a.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Left fold of function f over sequence s with accumulator a starting at index i.
+     * Applies f to accumulate values from left to right over the sequence, tracking the index starting from i.
+     */
+    public final <R extends Sort, A extends Sort> Expr<A> mkSeqFoldli(Expr<?> f, Expr<IntSort> i, Expr<A> a, Expr<SeqSort<R>> s)
+    {
+        checkContextMatch(f, i, a, s);
+        return (Expr<A>) Expr.create(this, Native.mkSeqFoldli(nCtx(), f.getNativeObject(), i.getNativeObject(), a.getNativeObject(), s.getNativeObject()));
+    }
+
     /**
      * Replace the first occurrence of src by dst in s.
      */