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

Answer 1

AFAIK没有向SMT添加复杂数字的计划.有一个SMT-LIB谷歌集团，它可能是有意义的发送一个帖子，看看那里是否有任何兴趣。

请注意，这篇特定的博客文章写着“查找根”；这只是可满足的，也就是说，它找到了一个解决方案，而不是所有的解决方案。(但您可以通过添加一个断言来请求另一个断言，即x应该与第一个结果不同。)