mirror of
https://github.com/Z3Prover/z3
synced 2025-11-05 13:56:03 +00:00
Delete examples/java/TestJavaAPICompleteness.java
This commit is contained in:
parent
c3c33fe3b0
commit
0678c8b889
1 changed files with 0 additions and 86 deletions
|
|
@ -1,86 +0,0 @@
|
||||||
/*++
|
|
||||||
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:
|
|
||||||
|
|
||||||
Z3Prover Contributors 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<CharSort> s = ctx.mkString("hello world hello");
|
|
||||||
SeqExpr<CharSort> 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<CharSort> str = ctx.mkString("test");
|
|
||||||
|
|
||||||
// Get the element sort of the sequence (should be CharSort)
|
|
||||||
SeqSort<CharSort> 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);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue