Z3 v4.3+ 是不是支持非线性算术的量词消除

Posted 2023-03-28

【中文标题】Z3 v4.3+ 是不是支持非线性算术的量词消除

【英文标题】：Does Z3 v4.3+ support quantifier elimination for NON-linear arithmeticZ3 v4.3+ 是否支持非线性算术的量词消除

【发布时间】：2013-04-17 09:08:58

【问题描述】：

我不知道 Z3 完全支持哪种量词消除。 我所拥有的是一个普遍量化的公式，一般来说是非线性项。我想获得一个等效的无量词公式。 Z3 可以吗？

谢谢， 弗里德里希

【参考方案1】：

Z3 对非线性算术的量词消除的支持非常有限。此外，默认情况下未启用它。这是一个关于如何启用它的示例，并展示了限制。也可以在线获取here。

(set-option :pp-max-depth 20) ;; set option for Z3 pretty printer
(declare-const a Real)
(assert (exists ((x Real)) (= (* x x) a )))
(apply qe)
(echo "enabling nonlinear support...")
(apply (! qe :qe-nonlinear true))
;; It is very limited, it will fail in the following example
(echo "trying a cubic polynomial...")
(assert (exists ((x Real)) (= (* x x x) a)))
(apply (! qe :qe-nonlinear true))

【讨论】：

嗨，Leo，qe 对非线性算术的支持会在不久的将来扩展吗？

近期不会。除非有人想为此工作。顺便说一句，我们拥有执行基于 CAD 的量词消除程序的所有机制。

谢谢，这听起来是一个非常有趣的项目。