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)); } + /// + /// Map function f over the sequence s. + /// + 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)); + } + + /// + /// Map function f over the sequence s at index i. + /// + 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)); + } + + /// + /// Fold left the function f over the sequence s with initial value a. + /// + 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)); + } + + /// + /// Fold left with index the function f over the sequence s with initial value a starting at index i. + /// + 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)); + } + /// /// Convert a regular expression that accepts sequence s. ///