mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-07 09:42:14 +00:00
Code Activity

Add four sequence operations to Java API (SeqMap, SeqMapi, SeqFoldl, SeqFoldli)

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-17 18:41:59 +00:00
parent b50d5d187d
commit c6c17910aa
1 changed files with 40 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/api/java/Context.java
View file

@ -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.
*/