Z3 java中的替换 [英] Substitution in Z3 java

问题描述

注意到在z3中调用替换时，总是简化表达式，但是在我们的项目中，只需要替换并保持原来的结构即可.根据下面的帖子，这个功能将被修复，不知道它是否已经存在?或者是否有任何方法可以关闭简化?

Noticed that when call substitution in z3, it always simplifies the expression, but in our project, it is necessary to just substitute and keep the original structure. According to the following post, such feature will be fixed, wonder if it is already there? Or if there's any way to turn the simplification off?

Z3Py 中的替代

推荐答案

是的，这个问题已经在unstable分支中修复了(见这里);这现在应该完全符合预期.

Yes, this problem has been fixed in the unstable branch (see here); this should now behave exactly as expected.

这篇关于Z3 java中的替换的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！