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

Add sequence higher-order functions to Java API (#8226)

Browse source 
* Initial plan

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

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix checkContextMatch call and add test for sequence operations

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add 4-parameter checkContextMatch overload for consistency

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:54 -08:00 • committed by GitHub
parent 1be52d95a5
commit ecea5e2b4e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 132 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

84
examples/java/SeqOperationsExample.java Normal file
View file

@ -0,0 +1,84 @@
/**
* Test example for new sequence operations (SeqMap, SeqMapi, SeqFoldl, SeqFoldli)
*/
import com.microsoft.z3.*;
public class SeqOperationsExample {
public static void main(String[] args) {
Context ctx = new Context();
try {
System.out.println("Testing new sequence operations in Java API\n");
// Test 1: mkSeqMap
System.out.println("Test 1: mkSeqMap");
IntSort intSort = ctx.mkIntSort();
SeqSort<IntSort> seqIntSort = ctx.mkSeqSort(intSort);
// Create a sequence variable
Expr<SeqSort<IntSort>> seq = ctx.mkConst("s", seqIntSort);
// Create a lambda function that adds 1 to an integer: (lambda (x) (+ x 1))
Expr<IntSort> x = ctx.mkIntConst("x");
Lambda<IntSort> f = ctx.mkLambda(new Expr<?>[] { x }, ctx.mkAdd(x, ctx.mkInt(1)));
// Create map expression (conceptually maps f over seq)
SeqExpr<IntSort> mapped = ctx.mkSeqMap(f, seq);
System.out.println("mkSeqMap result type: " + mapped.getClass().getName());
System.out.println("mkSeqMap created successfully: " + mapped);
System.out.println();
// Test 2: mkSeqMapi
System.out.println("Test 2: mkSeqMapi");
// Lambda that takes index and element: (lambda (i x) (+ x i))
Expr<IntSort> xElem = ctx.mkIntConst("xElem");
Expr<IntSort> iIdx = ctx.mkIntConst("iIdx");
Lambda<IntSort> fWithIdx = ctx.mkLambda(new Expr<?>[] { iIdx, xElem }, ctx.mkAdd(xElem, iIdx));
IntExpr i = ctx.mkIntConst("start_idx");
SeqExpr<IntSort> mappedWithIndex = ctx.mkSeqMapi(fWithIdx, i, seq);
System.out.println("mkSeqMapi result type: " + mappedWithIndex.getClass().getName());
System.out.println("mkSeqMapi created successfully: " + mappedWithIndex);
System.out.println();
// Test 3: mkSeqFoldl
System.out.println("Test 3: mkSeqFoldl");
// Lambda that accumulates: (lambda (acc elem) (+ acc elem))
IntExpr accVar = ctx.mkIntConst("accVar");
IntExpr elemVar = ctx.mkIntConst("elemVar");
Lambda<IntSort> foldFunc = ctx.mkLambda(new Expr<?>[] { accVar, elemVar }, ctx.mkAdd(accVar, elemVar));
IntExpr acc = ctx.mkIntConst("acc");
Expr<IntSort> folded = ctx.mkSeqFoldl(foldFunc, acc, seq);
System.out.println("mkSeqFoldl result type: " + folded.getClass().getName());
System.out.println("mkSeqFoldl created successfully: " + folded);
System.out.println();
// Test 4: mkSeqFoldli
System.out.println("Test 4: mkSeqFoldli");
// Lambda with index: (lambda (idx acc elem) (+ acc elem idx))
IntExpr idxVar = ctx.mkIntConst("idxVar");
IntExpr accVar2 = ctx.mkIntConst("accVar2");
IntExpr elemVar2 = ctx.mkIntConst("elemVar2");
ArithExpr<?> tempSum = ctx.mkAdd(accVar2, elemVar2);
ArithExpr<?> finalSum = ctx.mkAdd(tempSum, idxVar);
Lambda<IntSort> foldFuncWithIdx = ctx.mkLambda(
new Expr<?>[] { idxVar, accVar2, elemVar2 },
(IntExpr) finalSum);
IntExpr idx = ctx.mkIntConst("start_idx2");
IntExpr acc2 = ctx.mkIntConst("acc2");
Expr<IntSort> foldedWithIndex = ctx.mkSeqFoldli(foldFuncWithIdx, idx, acc2, seq);
System.out.println("mkSeqFoldli result type: " + foldedWithIndex.getClass().getName());
System.out.println("mkSeqFoldli created successfully: " + foldedWithIndex);
System.out.println();
System.out.println("All tests passed!");
} catch (Exception e) {
System.err.println("Error: " + e.getMessage());
e.printStackTrace();
System.exit(1);
} finally {
ctx.close();
}
}
}

48
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.
*/
@ -4430,6 +4470,14 @@ public class Context implements AutoCloseable {
checkContextMatch(other3);
}
void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3, Z3Object other4)
{
checkContextMatch(other1);
checkContextMatch(other2);
checkContextMatch(other3);
checkContextMatch(other4);
}
void checkContextMatch(Z3Object[] arr)
{
if (arr != null)