mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
Code Activity

Add advanced sequence operations to C# API (#8227)

Browse source 
* Initial plan

* 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>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-17 13:02:03 -08:00 • committed by GitHub
parent c7e4332792
commit 11851c2e4c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 48 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/api/dotnet/Context.cs
View file

@ -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>