Z3 替换 (Java)

Question

我尝试用另一个变量 y 简单地替换一个变量 x（如果重要，请设置变量）。从这里的帖子 (Substitution in Z3 java)，我认为替代品在 Java 中可以正常工作。但是，我得到与返回相同的表达式对象（打印时）。替换是否正确实施或我犯了错误？下面是关于我如何定义变量和调用替代方法的代码 sn-p，以防万一。

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);

当我打印时，formSub 公式似乎没有改变。无法从调试中找到任何提示。

谢谢。

Answer 1

我尝试复制此问题，但替换对我来说效果很好。这是我使用的代码：

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);

此代码完全按照预期打印：

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

你不是这样吗？