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 SeqExpr mkSeqMap(Expr f, Expr> s) + { + checkContextMatch(f, s); + return (SeqExpr) 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 SeqExpr mkSeqMapi(Expr f, Expr i, Expr> s) + { + checkContextMatch(f, i, s); + return (SeqExpr) 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 Expr mkSeqFoldl(Expr f, Expr a, Expr> s) + { + checkContextMatch(f, a, s); + return (Expr) 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 Expr mkSeqFoldli(Expr f, Expr i, Expr a, Expr> s) + { + checkContextMatch(f, i, a, s); + return (Expr) Expr.create(this, Native.mkSeqFoldli(nCtx(), f.getNativeObject(), i.getNativeObject(), a.getNativeObject(), s.getNativeObject())); + } + /** * Replace the first occurrence of src by dst in s. */