【发布时间】：2012-05-01 17:00:15
【问题描述】：
我想知道Z3在量词消除后是否可以显示等效公式。
示例（存在 k）(i x k) = 1 且 k > 5 相当于
i > 0 和 5 i - 1
这里，量词k已经被去掉了。
这可能吗？
谢谢， 考斯图布。
【问题讨论】：
标签： z3
【发布时间】：2012-05-01 17:00:15
【问题描述】：
是的，Z3 可以检查两个公式是否等价。检查p 和q 是否等价。我们必须检查(not (iff p q))是否不可满足。
您的示例使用非线性算术i*k。 Z3 中的量词消除模块对非线性 real 算法的支持有限。它基于虚拟术语替换，这是不完整的。但是，对于您的示例就足够了。
我们必须启用 Z3 中的量词消除模块和非线性扩展（即虚拟术语替换）。
以下是我们如何在 Z3 中对您的示例进行编码：http://rise4fun.com/Z3/rXfi
【讨论】：
一般情况下，可以得到消除量词的结果。例如，在rise4fun 中输入以下内容：
(declare-const i Real)
(assert (exists ((k Real)) (and (= (* i k) 1.0) (> k 5.0))))
(apply qe)
本例涉及非线性算术，Z3没有消去量词。
【讨论】：
-
量词消除模块默认不开启对非线性算术的支持。这就是 Z3 没有消除上述脚本中的量词的原因。这是启用非线性支持的相同示例：rise4fun.com/Z3/qrW1
-
我明白了，我的错误。作为参考，我尝试使用 set-option，但这不起作用：rise4fun.com/Z3/vm7M。
-
非常感谢乔希和莱昂纳多。我还有几个问题，我将它们作为一个新线程单独提问。