Z3 v4.3 +支持非線性算術的量詞消除

Question

Z3完全支持什麼樣的量詞消除我找不到。 我所擁有的是一個普遍量化的公式，它是一般非線性項。我想獲得一個等效的量詞免費公式。 Z3有可能嗎？

感謝， 弗里德里希

Answer 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))