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过程是使用简化程序实现的，它可以在简化过程中应用替换。API过程调用文件api_ast.cpp中的Z3 C Z3_substitute。在内部，简化器被称为th_rewriter (理论重写器)。

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