Z3中未记录的三角函数可修复？

Question

Z3 中官方不支持三角函数。例如，请参阅 this question 或 this one。但是，在 Z3 中有未记录的三角运算符——例如在 regression tests 中使用了它们。甚至还有一个名为pi 的内置符号。 Z3 甚至可以用这些操作符做一些简单的证明，例如：

(declare-fun x () Real)
(assert (= (cos pi) x))
(check-sat)
(get-value (x))

返回：

sat
((x (- 1.0)))

这些运算符效果不佳。例如，这个小输入文件将导致 Z3 4.4.1 出现 seg 错误，或者导致主分支为this commit（现在）的内存使用量迅速爆炸：

(declare-fun x () Real)
(assert (< (sin x) -1.0))
(check-sat)

团队说不存在的未记录功能不起作用我并不感到惊讶。我的问题是：它们可以修复吗？什么水平的性能是对 Z3 的合理补充？我知道我可以使用未解释的函数和三角恒等式对 Z3 进行许多三角证明。 Z3 团队对此有兴趣吗？

Answer 1

谢谢，Z3 在这种情况下不应该崩溃。处理这些操作应该更优雅。我现在签入了一个修复程序，9b91e6f..cb29c07。 OTOH，对于此类运算符，基本上没有理论推理。 例如，Z3 不知道 sin 的界限。您必须自己公理化这些属性。当您使用没有（部分）决策过程支持的内置函数时，Z3 返回“unknown”（或“unsat”，但不是“sat”）。