diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 150efd545..9297dee47 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2259,6 +2259,24 @@ class JavaExample System.out.println(e1.equals(e3)); } + public void stringExample() { + System.out.println("String example"); + Context ctx = new Context(); + var a = ctx.mkToRe(ctx.mkString("abcd")); + var b = ctx.mkFullRe(ctx.mkReSort(ctx.mkStringSort())); + System.out.println(a); + System.out.println(b); + System.out.println(a.getSort()); + System.out.println(b.getSort()); + var c = ctx.mkConcat(ctx.mkToRe(ctx.mkString("abc")), + ctx.mkFullRe(ctx.mkReSort(ctx.mkStringSort())), + ctx.mkEmptyRe(ctx.mkReSort(ctx.mkStringSort())), + ctx.mkAllcharRe(ctx.mkReSort(ctx.mkStringSort())), + ctx.mkToRe(ctx.mkString("d"))); + System.out.println(c); + + } + public static void main(String[] args) { JavaExample p = new JavaExample(); @@ -2274,12 +2292,15 @@ class JavaExample System.out.print("Z3 Full Version String: "); System.out.println(Version.getFullVersion()); + p.stringExample(); + p.simpleExample(); { // These examples need model generation turned on. HashMap cfg = new HashMap(); cfg.put("model", "true"); Context ctx = new Context(cfg); + p.optimizeExample(ctx); p.basicTests(ctx); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 06b312303..da2426305 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2175,10 +2175,10 @@ public class Context implements AutoCloseable { /** * Convert a regular expression that accepts sequence s. */ - public final ReExpr mkToRe(Expr> s) + public final ReExpr> mkToRe(Expr> s) { checkContextMatch(s); - return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject())); + return (ReExpr>) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject())); } @@ -2296,7 +2296,7 @@ public class Context implements AutoCloseable { * Create the empty regular expression. * Coresponds to re.none */ - public final ReExpr mkEmptyRe(R s) + public final ReExpr mkEmptyRe(ReSort s) { return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); } @@ -2305,16 +2305,17 @@ public class Context implements AutoCloseable { * Create the full regular expression. * Corresponds to re.all */ - public final ReExpr mkFullRe(R s) + public final ReExpr mkFullRe(ReSort s) { return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); } /** * Create regular expression that accepts all characters + * R has to be a sequence sort. * Corresponds to re.allchar */ - public final ReExpr mkAllcharRe(R s) + public final ReExpr mkAllcharRe(ReSort s) { return (ReExpr) Expr.create(this, Native.mkReAllchar(nCtx(), s.getNativeObject())); } @@ -2322,10 +2323,10 @@ public class Context implements AutoCloseable { /** * Create a range expression. */ - public final ReExpr mkRange(Expr> lo, Expr> hi) + public final ReExpr> mkRange(Expr> lo, Expr> hi) { checkContextMatch(lo, hi); - return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject())); + return (ReExpr>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject())); } /**