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