From 874810f16644d52272dd86610c6bc63e20358904 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Nov 2025 09:47:24 -0800 Subject: [PATCH] Delete examples/java/StringReplaceTest.java --- examples/java/StringReplaceTest.java | 109 --------------------------- 1 file changed, 109 deletions(-) delete mode 100644 examples/java/StringReplaceTest.java diff --git a/examples/java/StringReplaceTest.java b/examples/java/StringReplaceTest.java deleted file mode 100644 index e1548d965..000000000 --- a/examples/java/StringReplaceTest.java +++ /dev/null @@ -1,109 +0,0 @@ -/*++ - Copyright (c) 2024 Microsoft Corporation - -Module Name: - - StringReplaceTest.java - -Abstract: - - Z3 Java API: Test for string replace operations - -Notes: - ---*/ - -import com.microsoft.z3.*; - -public class StringReplaceTest { - - public static void testReplaceAll(Context ctx) throws Z3Exception { - System.out.println("Testing mkReplaceAll..."); - - // Create string expressions - SeqExpr s = ctx.mkString("hello world hello"); - SeqExpr src = ctx.mkString("hello"); - SeqExpr dst = ctx.mkString("goodbye"); - - // Create replace_all expression - SeqExpr result = ctx.mkReplaceAll(s, src, dst); - - // Create a solver and check - Solver solver = ctx.mkSolver(); - SeqExpr expected = ctx.mkString("goodbye world goodbye"); - solver.add(ctx.mkEq(result, expected)); - - Status status = solver.check(); - System.out.println(" Status: " + status); - - if (status == Status.SATISFIABLE) { - System.out.println(" PASS: mkReplaceAll works correctly"); - } else { - System.out.println(" FAIL: mkReplaceAll returned unexpected result"); - } - } - - public static void testReplaceRe(Context ctx) throws Z3Exception { - System.out.println("\nTesting mkReplaceRe..."); - - try { - // Create string expression - SeqExpr s = ctx.mkString("hello world"); - - // Create regular expression that matches "world" - ReExpr> worldRe = ctx.mkToRe(ctx.mkString("world")); - - // Create replace_re expression (replaces first match) - SeqExpr dst = ctx.mkString("universe"); - SeqExpr result = ctx.mkReplaceRe(s, worldRe, dst); - - System.out.println(" Created expression: " + result); - System.out.println(" PASS: mkReplaceRe API method works correctly"); - } catch (Exception e) { - System.out.println(" FAIL: mkReplaceRe threw exception: " + e.getMessage()); - } - } - - public static void testReplaceReAll(Context ctx) throws Z3Exception { - System.out.println("\nTesting mkReplaceReAll..."); - - try { - // Create string expression - SeqExpr s = ctx.mkString("foo bar foo"); - - // Create regular expression that matches "foo" - ReExpr> fooRe = ctx.mkToRe(ctx.mkString("foo")); - - // Create replace_re_all expression (replaces all matches) - SeqExpr dst = ctx.mkString("baz"); - SeqExpr result = ctx.mkReplaceReAll(s, fooRe, dst); - - System.out.println(" Created expression: " + result); - System.out.println(" PASS: mkReplaceReAll API method works correctly"); - } catch (Exception e) { - System.out.println(" FAIL: mkReplaceReAll threw exception: " + e.getMessage()); - } - } - - public static void main(String[] args) { - try { - System.out.println("String Replace Operations Test"); - System.out.println("==============================\n"); - - // Create Z3 context - Context ctx = new Context(); - - // Run tests - testReplaceAll(ctx); - testReplaceRe(ctx); - testReplaceReAll(ctx); - - System.out.println("\nAll tests completed!"); - - ctx.close(); - } catch (Exception e) { - System.err.println("Error: " + e.getMessage()); - e.printStackTrace(); - } - } -}