mkAllcharRe with compilation error

[yvanlabiche]

Good day.
I am using the Java API and I get a compilation error with the provided example, specifically the statement
Expr 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")));
in the stringExample function.

Javac complains with the use of mkAllcharRe.
error: cannot find symbol
System.out.println(ctx.mkAllcharRe(ctx.mkReSort(ctx.mkStringSort())));
^
symbol: method mkAllcharRe(ReSort<SeqSort>)
location: variable ctx of type Context

It seems to me all the types match and I do not understand why Javac compains.

Any help will be welcomed.
Yvan.

[yvanlabiche]

Looking a bit further into it, although the mkAllcharRE() method is part of the documentation
https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_context.html#af60fc2f219800913c7f5892502ce9cc6
it is not in the com.microsoft.z3.jar file, nor in the source code for Context.java.