Настройте устранение квантификатора LIA в Z3

Question

Я делаю устранение квантификаторов в LIA, используя F # и Z3 3.2 API.

Z3 имел конфигурацию QUANT_ARITH, которая указывает на использование метода Купера или теста Омеги для устранения квантификатора LIA.Но эта опция была заменена на ELIM_QUANTIFIERS в Z3 2.6 (см. Замечания к выпуску Z3 ).

Я хочу спросить внутренне, как Z3 3.2 знает, какой метод использовать для исключения квантификаторов?Могут ли пользователи повлиять на выбор метода, подобного QUANT_ARITH раньше?

Кроме того, с введением языка спецификации стратегии , позволит ли Z3 настраивать исключение кванторов, расширяя или комбинируя эти методы?

Answer 1

Модуль исключения квантификатора был повторно реализован.Новая реализация должна быть быстрее и правильнее.Последний Z3 не имеет реализации метода Купера или теста Омеги.Вы можете найти более подробную информацию о действительной процедуре исключения квантификатора, используемой в Z3, по адресу: «Устранение линейного квантификатора как абстрактная процедура принятия решений, Николай Бьернер, IJCAR 2010».

Что касается языка спецификации стратегии, мы в конечном итоге представим тактикудля выполнения квантификатора исключения.В настоящее время мы работаем над этой инфраструктурой, скоро появятся новые новости.