Z3：复数？

Question

一直在搜索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 中看到任何关于这个理论的参考。

Answer 1

AFAIK 没有向 SMT-LIB 添加复数的计划。有一个Google group for SMT-LIB，发个帖子看看那里有没有兴趣。

注意，那篇博文说“找到 a 根”；这只是可满足性，即它找到了一种解决方案，而不是所有解决方案。 （但您可以通过添加一个断言来要求另一个结果，即 x 应该与第一个结果不同。）