python - Z3Py 中的替换

Question

似乎substitute(f,t)Z3Py 中的函数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过程是使用可以在简化期间应用替换的简化器来实现的。substitutePython 过程调用Z3_substitute文件api_ast.cpp中的Z3 C API 。在内部，简化器称为th_rewriter（理论重写器）。

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