Большое спасибо Джошу и Леонардо за ответы на предыдущий вопрос.
У меня еще несколько вопросов.
‹1> Рассмотрим другой пример.
(exists k) i * k > = 4 and k > 1.
У этого есть простое решение i> 0. (как для Int, так и для Real случая)
Однако, когда я попытался подписаться,
(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k) 4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))
Z3 Не удалось исключить здесь квантификатор.
Однако в реальном случае это могло исключить. (когда i и k оба действительные числа) Сложнее ли исключение квантификатора для целых чисел?
‹2> Я использую Z3 C API в своей системе. Я добавляю некоторые нелинейные ограничения для целых чисел с кванторами в моей системе. Z3 в настоящее время проверяет выполнимость и дает мне правильную модель, когда система удовлетворительна.
Я знаю, что после исключения квантора эти ограничения сводятся к линейным ограничениям.
Я думал, что z3 автоматически исключает квантификатор перед проверкой выполнимости. Но поскольку он не мог этого сделать в случае 1 выше, теперь я думаю, что он обычно находит модель без исключения квантификатора. Я прав?
В настоящее время z3 может разрешить ограничения в моей системе. Но это может дать сбой в сложных системах. В таком случае, стоит ли выполнить исключение квантора каким-либо другим методом без z3 и добавить ограничения к z3 позже?
‹3> Я могу подумать о добавлении в мою систему реальных нелинейных ограничений вместо целочисленных нелинейных ограничений. В таком случае, как я могу заставить z3 выполнять исключение квантификатора с помощью C-API?
‹4> Наконец, неплохо ли заставить z3 выполнять исключение квантификатора? Или он обычно находит модель более разумно, не выполняя исключения квантификатора?
Спасибо.
