В настоящее время мы реструктурируем Z3 и отходим от подхода: решателя с «тысячами» параметров.Мы продвигаем Z3 к более модульному и гибкому подходу для объединения решателей и определения стратегий.Вы можете найти больше информации об этом новом подходе в следующем draft .
Относительно опций INI, некоторые из них устарели и существуют только потому, что мы не завершили переход на новыйподход еще.Некоторые из этих опций были добавлены для конкретных проектов и сейчас устарели.Они существуют только для обратной совместимости.
Что касается QF_BV, Z3 3.2 содержит два решателя QF_BV: старый (тот, что из 2.x) и новый.Новый (официальный) доступен только в официальном формате ввода Z3: SMT 2.0.Низкоуровневые форматы ввода SMT 1.0, Simplify и Z3 устарели.Большинство улучшений производительности в Z3 3.x доступны только при использовании формата ввода SMT 2.0.
Через пару месяцев язык спецификации стратегии будет официально поддерживаться в Z3.У нас будет учебное пособие и документация, описывающая, как его использовать.Тем временем я настоятельно рекомендую вам использовать конфигурацию по умолчанию и формат ввода SMT 2.0 для логики, такой как QF_BV.