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方法，用它可以簡化應用過程中的替代實現簡化器。 Python程序在文件api_ast.cpp中調用Z3 C API Z3_substitute。在內部，簡化器被稱爲th_rewriter（理論重寫器）。

這就是說，我同意這不是很好，在某些情況下可能會很不方便。我會在下一個版本中更改它。