Z3：複數？

我一直在搜索z3是否支持複數，發現如下：https : //leodemoura.github.io/blog/2013/01/26/complex.html

作者指出 (1) 複數尚未在 Z3 中作為內置實現（這是在 2013 年編寫的），以及 (2) 複數可以在 Z3 提供的實數之上進行編碼。

基本思想是將一個複數表示為一對實數。他用 定義了基本虛數I=(0,1)，即：I表示實部等於0，虛部等於1。

他提供了編碼（我的意思是，我們可以在我們的機器上測試它），我們可以在其中求解方程x^2+2=0。我收到以下結果：

sat
x = (-1.4142135623?)*I

該sat結果有一定道理，因為這個方程是可解的模擬複數的理論（如代數閉域理論的結果），我們剛剛作出。但是，根本結果對我來說沒有意義。我的意思是：怎麼樣(1.4142135623?)*I？

我會理解接收兩個根，但是，如果只接收一個，我不明白為什麼我會得到否定的解決方案。

也許我誤讀了一些東西，或者我錯過了一些東西。

另外，我想說是否已經在Z3中實現了複數。我的意思是，有一個標準：

x = Complex("x")

並採用一種NCA 的策略（來自非線性複雜算術）。

我也沒有在 SMT-LIB 中看到任何對這個理論的引用。