Z3 Substitution (Java)

Question

I try to make a simple substitution of a variable x (set variable if important) with another variable y. From the post here (Substitution in Z3 java), I presume that substitute works fine in Java. However I get the same expression object (when printed) as return. Is substitution correctly implemented or I am making a mistake? The below is the code snippet on how I define my variable and call substitute method in case it is relevant.

EnumSort xSort = ctx.mkEnumSort(xs, ctx.mkSymbol("A"),ctx.mkSymbol("B"));

SetSort xSet = ctx.mkSetSort(xSort);

Expr x = ctx.mkConst("x",xSet);

/*Construct the formula "formOld".....*/

Expr y = ctx.mkConst("y",x.getSort());

BoolExpr form_sub = (BoolExpr)formOld.substitute(x, y);

The formula formSub seems unchanged when I print. Couldn't find any hint from debugging.

Thanks.

Answer 1

I tried replicating this problem, but the substitution works fine for me. Here's the code I used:

Symbol xs = ctx.mkSymbol("xs");
EnumSort xSort = ctx.mkEnumSort(xs, ctx.mkSymbol("A"),ctx.mkSymbol("B"));
SetSort xSet = ctx.mkSetSort(xSort);
Expr x = ctx.mkConst("x",xSet);
Expr z = ctx.mkConst("z",xSet);            
Expr f_old = ctx.mkEq(x, z);

System.out.println("old: " + f_old);

Expr y = ctx.mkConst("y",x.getSort());
BoolExpr f_new = (BoolExpr)f_old.substitute(x, y);

System.out.println("new: " + f_new);

And this code prints, exactly as expected:

old: (= x z)
new: (= y z)

Is this not the case for you?