Z3Py 中的替换 [英] substitution in Z3Py

问题描述

似乎Z3Py中的substitute(f,t)函数在进行替换之前先对f进行了简化.有没有办法禁止这种情况?

It seems that the substitute(f,t) function in Z3Py performs simplification on f first before doing the substitution. Is there a way to disallow this?

我希望发生以下行为:

f = And(x,Not(x))
result = substitute(f,*[(Not(x),BoolVal(True))])  #sub Not(x) => True
#if we simplify f first then the result = False,  but if we do the substitution first then result = x

推荐答案

不幸的是，substitute 过程是使用简化器实现的，它可以在简化过程中应用替换.substitute Python 过程调用文件 api_ast.cpp.在内部，简化器称为 th_rewriter(理论重写器).

Unfortunately, the substitute procedure is implemented using the simplifier which can apply substitutions during the simplification. The substitute Python procedure invokes the Z3 C API Z3_substitute in the file api_ast.cpp. Internally, the simplifier is called th_rewriter (theory rewriter).

话虽如此，我同意这并不好，并且在某些情况下可能非常不方便.我将在下一个版本中更改它.

That being said, I agree this is not nice and may be very inconvenient in some cases. I will change that for the next release.

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