Z3 python將x ** 2與x * x不同？

Question

看來，Z3 Python接口不喜歡**操作，它可以處理X * X，但不是X，如圖下面的例子

>>> 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

您可能正在使用4.3版** 2。 0在Linux或OSX上。版本4.3.0在這些平臺上存在配置問題。如果是這樣的話，我建議你下載版本4.3.1。版本4.3.1將證明在Linux和OSX上的兩個查詢。在版本4.3.0中，Linux和OSX上的默認情況下未啓用自動配置。因此，Z3將始終使用一種通用求解器，該求解器對於非線性算術來說不完整，也不支持電力操作員。當啓用自動配置時，Z3檢測到這兩個問題出現在非線性實數算術片段中，並切換到nlsat solver。

順便說一句，要手動啓用4.3.0版本的自動配置，您可以使用命令z3.set_option(auto_config=True)。