Инкрементальные вызовы Z3 на UFBV с push-вызовами и без них

Z3 3.x имеет «язык спецификации стратегии», основанный на тактике и тактике. Я пока не "рекламирую" это, потому что работа продолжается. Основная идея описана в этом слайде. У нас есть разные встроенные стратегии для каждой логики. Стратегии обычно не поддерживают пошаговое решение, потому что они могут применять преобразования, использующие предположение о «закрытом мире». Например, у нас есть преобразования, которые отображают линейную целочисленную арифметику 0-1 в SAT. Всякий раз, когда Z3 обнаруживает, что пользователь «хочет» инкрементное решение (например, несколько команд check-sat, push и pop), он переключается на решатель общего назначения. В будущих версиях мы предоставим больше возможностей для управления поведением Z3.

Кстати, если у вас есть две последовательные команды (check-sat) (check-sat), Z3 не обязательно входит в инкрементный режим. Он войдет, только если между двумя вызовами есть команда assert или push.

Теперь предположим, что ваш запрос имеет форму: (check-sat) <assertions> (check-sat), а второй запрос имеет форму (check-sat) <assertions> (push) (check-sat). В обоих случаях Z3 будет в инкрементном режиме во втором (check-sat). Однако поведение все равно не то. Инкрементальный решатель «компилирует» утвержденные формулы во внутренний формат, и на его поведение влияет выполнение команды push. Например, он будет использовать более эффективное кодирование двоичных предложений только в том случае, если пользовательская область отсутствует. Под областью пользователя я имею в виду количество push команд - количество pop команд. Это происходит потому, что структура данных, используемая в более эффективном кодировании, не имеет эффективной операции отмены/инверсии.