Я не смог выяснить, какой тип исключения квантификатора полностью поддерживает Z3. То, что у меня есть, — это универсальная количественная формула для нелинейных терминов, вообще говоря. Я хотел бы получить эквивалентную формулу без кванторов. Возможно ли это с Z3?
Спасибо, Фридрих
Z3 имеет очень ограниченную поддержку исключения квантификаторов нелинейной арифметики. Более того, он не включен по умолчанию. Вот пример того, как его включить, и демонстрирующий ограничения. Он также доступен онлайн здесь.
(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))
