z3 - Z3 python は x**2 を x*x とは異なるものとして扱いますか?

Question

以下の例に示すように、Z3 Python インターフェイスは ** 演算子が好きではないようです。x*x は処理できますが、x**2 は処理できません。

>>> x,y = x,y=Reals('x y')
>>> z3.prove(Implies(x -6 == 0,x**2 -36 == 0))
failed to prove
[x = 6]
>>> z3.prove(Implies(x -6 == 0,x*x -36 == 0))
proved

Answer 1

Linux または OSX でバージョン 4.3.0 を使用している可能性があります。バージョン 4.3.0 には、これらのプラットフォームでの構成の問題があります。その場合は、バージョン4.3.1をダウンロードすることをお勧めします。バージョン 4.3.1 では、Linux と OSX の両方でクエリが証明されます。バージョン 4.3.0 では、Linux および OSX で自動構成がデフォルトで有効になっていません。したがって、Z3 は常に汎用ソルバーを使用しますが、これは非線形演算には完全ではなく、累乗演算子もサポートしていません。自動構成が有効になっている場合、Z3 はこれら 2 つの問題が非線形実数演算フラグメントにあることを検出し、nlsat ソルバーに切り替えます。

ところで、バージョン 4.3.0 で自動構成を手動で有効にするには、コマンドを使用できますz3.set_option(auto_config=True)。