Z3：复数？
Z3: Complex numbers?
我一直在搜索 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 中看到任何关于这个理论的参考。
据我所知，没有计划向 SMT-LIB 添加复数。有一个 Google group for SMT-LIB，向那里发送一个 post 可能有意义，看看那里是否有任何兴趣。
请注意，那个特定的博客 post 说“找到 a root”；这只是可满足性，即它找到一个解决方案，而不是所有解决方案。 （但是你可以通过添加一个声明 x 应该与第一个结果不同的断言来请求另一个。）
我一直在搜索 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 中看到任何关于这个理论的参考。
据我所知，没有计划向 SMT-LIB 添加复数。有一个 Google group for SMT-LIB，向那里发送一个 post 可能有意义，看看那里是否有任何兴趣。
请注意，那个特定的博客 post 说“找到 a root”；这只是可满足性，即它找到一个解决方案，而不是所有解决方案。 （但是你可以通过添加一个声明 x 应该与第一个结果不同的断言来请求另一个。）