z3 - 等效量词免费公式

Question

我想知道Z3是否可以在量词消除后显示等效公式。

示例 (exists k) (ixk) = 1 and k > 5 等价于

i > 0 和 5 i - 1 < 0。

在这里，量词 k 已被删除。

这可能吗？

谢谢，考斯图布。

Answer 1

是的，Z3 可以检查两个公式是否等价。检查p和q是否等价。我们必须检查是否(not (iff p q))不满足。

您的示例使用非线性算术i*k。Z3 中的量词消除模块对非线性实数运算的支持有限。它基于虚拟术语替换，这是不完整的。但是，对于您的示例就足够了。我们必须启用 Z3 中的量词消除模块和非线性扩展（即虚拟术语替换）。

以下是我们如何在 Z3 中对您的示例进行编码：http ://rise4fun.com/Z3/rXfi

Answer 2

一般来说，可以得到消除量词的结果。例如，通过在rise4fun中输入以下内容：

(declare-const i Real)
(assert (exists ((k Real)) (and (= (* i k) 1.0) (> k 5.0))))
(apply qe)

本例涉及非线性算术，Z3 不消除量词。