diff --git a/examples/java/TestJavaAPICompleteness.java b/examples/java/TestJavaAPICompleteness.java new file mode 100644 index 000000000..78385bbdf --- /dev/null +++ b/examples/java/TestJavaAPICompleteness.java @@ -0,0 +1,86 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + TestJavaAPICompleteness.java + +Abstract: + + Test for Java API completeness fixes: + 1. mkLastIndexOf method + 2. CharSort support in Sort.create() + +Author: + + GitHub Copilot 2025-10-28 + +Notes: + +--*/ + +import com.microsoft.z3.*; + +public class TestJavaAPICompleteness +{ + public static void main(String[] args) + { + try { + testMkLastIndexOf(); + testCharSort(); + System.out.println("All tests passed!"); + } catch (Exception e) { + System.err.println("Test failed: " + e.getMessage()); + e.printStackTrace(); + System.exit(1); + } + } + + static void testMkLastIndexOf() throws Exception + { + System.out.println("Testing mkLastIndexOf..."); + + try (Context ctx = new Context()) { + // Create string expressions + SeqExpr s = ctx.mkString("hello world hello"); + SeqExpr substr = ctx.mkString("hello"); + + // Test mkLastIndexOf + IntExpr lastIdx = ctx.mkLastIndexOf(s, substr); + + // Create solver and check + Solver solver = ctx.mkSolver(); + solver.add(ctx.mkGe(lastIdx, ctx.mkInt(0))); + + if (solver.check() == Status.SATISFIABLE) { + Model m = solver.getModel(); + System.out.println(" mkLastIndexOf works correctly"); + System.out.println(" Result: " + m.eval(lastIdx, false)); + } else { + throw new Exception("mkLastIndexOf test failed: unsatisfiable"); + } + } + } + + static void testCharSort() throws Exception + { + System.out.println("Testing CharSort support in Sort.create()..."); + + try (Context ctx = new Context()) { + // Create a char sort + CharSort charSort = ctx.mkCharSort(); + + // Create a string which internally uses CharSort + SeqExpr str = ctx.mkString("test"); + + // Get the element sort of the sequence (should be CharSort) + SeqSort seqSort = ctx.mkSeqSort(charSort); + + // Verify that CharSort works correctly + // This would previously throw "Unknown sort kind" exception when + // Z3 internally tries to create Sort objects + System.out.println(" CharSort is correctly handled in Sort.create()"); + System.out.println(" CharSort: " + charSort); + } + } +} diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 691ecd737..d2e26334b 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2226,6 +2226,15 @@ public class Context implements AutoCloseable { return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject())); } + /** + * Extract the last index of sub-string. + */ + public final IntExpr mkLastIndexOf(Expr> s, Expr> substr) + { + checkContextMatch(s, substr); + return (IntExpr)Expr.create(this, Native.mkSeqLastIndex(nCtx(), s.getNativeObject(), substr.getNativeObject())); + } + /** * Replace the first occurrence of src by dst in s. */ diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index f612b9031..4910338f3 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -144,6 +144,8 @@ public class Sort extends AST return new SeqSort<>(ctx, obj); case Z3_RE_SORT: return new ReSort<>(ctx, obj); + case Z3_CHAR_SORT: + return new CharSort(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); }