mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

fix #6644

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-03-27 09:00:38 -07:00
parent 8a3a3dc91b
commit b4ad747e0b
2 changed files with 29 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

21
examples/java/JavaExample.java
View file

@ -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,6 +2292,8 @@ 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.
@ -2281,6 +2301,7 @@ class JavaExample
cfg.put("model", "true");
Context ctx = new Context(cfg);
p.optimizeExample(ctx);
p.basicTests(ctx);
p.castingTest(ctx);

15
src/api/java/Context.java
View file

@ -2175,10 +2175,10 @@ public class Context implements AutoCloseable {
/**
* Convert a regular expression that accepts sequence s.
*/
public final <R extends Sort> ReExpr<R> mkToRe(Expr<SeqSort<R>> s)
public final <R extends Sort> ReExpr<SeqSort<R>> mkToRe(Expr<SeqSort<R>> s)
{
checkContextMatch(s);
return (ReExpr<R>) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
return (ReExpr<SeqSort<R>>) 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 <R extends Sort> ReExpr<R> mkEmptyRe(R s)
public final <R extends Sort> ReExpr<R> mkEmptyRe(ReSort<R> s)
{
return (ReExpr<R>) 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 <R extends Sort> ReExpr<R> mkFullRe(R s)
public final <R extends Sort> ReExpr<R> mkFullRe(ReSort<R> s)
{
return (ReExpr<R>) 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 <R extends Sort> ReExpr<R> mkAllcharRe(R s)
public final <R extends Sort> ReExpr<R> mkAllcharRe(ReSort<R> s)
{
return (ReExpr<R>) Expr.create(this, Native.mkReAllchar(nCtx(), s.getNativeObject()));
}
@ -2322,10 +2323,10 @@ public class Context implements AutoCloseable {
/**
* Create a range expression.
*/
public final <R extends Sort> ReExpr<R> mkRange(Expr<SeqSort<CharSort>> lo, Expr<SeqSort<CharSort>> hi)
public final ReExpr<SeqSort<CharSort>> mkRange(Expr<SeqSort<CharSort>> lo, Expr<SeqSort<CharSort>> hi)
{
checkContextMatch(lo, hi);
return (ReExpr<R>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
return (ReExpr<SeqSort<CharSort>>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
}
/**