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でZ3CAPIを呼び出します。内部的には、単純化器が呼び出されth_rewriterます（理論リライター）。

そうは言っても、これは良くなく、場合によっては非常に不便かもしれないことに同意します。次のリリースで変更します。