python - Z3Py 中的替换

Question

看来Z3Py中的substitute(f,t)函数在进行替换之前首先对f执行简化。有没有办法禁止这种情况？

我希望发生以下行为:

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

Answer 1

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

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