Что такое INST_GEN в z3

Question

Контекст: я занимаюсь проверкой ограниченной Java-программы с использованием z3. Я хочу получить модель оптимизации по проблеме линеаризации. Стандартным подходом может быть поэтапный поиск в модели, пока не будет найден ненадлежащий случай. Но производительность кажется проблемой, и она разрушает переносимость кода, вводя JNI, который интегрирует z3 c/ C++ api в мой инструмент.

Теперь я хочу добавить ограничения на все входные данные метода Java. Я использую количественные массивы (я использую теорию массива для моделирования куч). Тем не менее, z3 всегда возвращает "неизвестно" сразу же при удовлетворительной проблеме. Кажется, что невозможно создать модель. Я замечаю, что есть опция z3, INST_GEN, тогда я пытаюсь ее понять. Я кормлю следующие формулы к z3.

(set-option :INST_GEN true)
(define-sort S () (_ BitVec 2))
(declare-fun s () S)
(assert (= s (_ bv0 2)))

(define-sort A () (Array S S))
(push) ;; 1st case    
(assert (forall ((a A)) (= (select a s) s)))
(check-sat)
(get-model)
(pop)

(push) ;; 2nd case
(declare-fun a () A)
(assert (forall ((t S)) (= (select a t) t)))
(check-sat)
(get-model)
(pop)

(push) ;; 3rd case
(check-sat)
(get-model)
(pop)

И в 1-м, и во 2-м случаях z3 возвращает "ошибку сегментации" в Linux, в то время как в Windows 7 происходит сбой. Оба z3 - версия 4.0, x64.

В третьем случае он не содержит количественных показателей, и Z3 успешно генерирует модель.

sat 
(model (define-fun s () (_ BitVec 2) #b00) )

Мой первый вопрос: как работает эта опция? Перечисляет ли он массивы?

Второй вопрос: я заметил, что z3 может успешно возвращать "unsat" в случае неудовлетворенной проблемы с массивами количественного определения. Поддерживает ли z3 какой-либо вариант или подход для создания модели в удовлетворенной задаче с количественными массивами, с ограниченными индексами и элементами? например, используя предложение if-then-else.

Спасибо за ваше чтение и внимание! Любые предложения с благодарностью!

Answer 1

Во-первых, вариант INST_GEN был частью эксперимента. Он не должен был подвергаться воздействию внешних пользователей. Этот вариант не был серьезно проверен. Это будет скрыто в будущих версиях. Извини за это.

Во-вторых, в общем, Z3 не сможет решить выполнимые задачи, которые количественно определяют по массивам. В следующем уроке (раздел Квантификаторы) описывается множество фрагментов, где Z3 завершен.

Наконец, у Z3 есть много разных движков / решателей. Однако только один из них поддерживает пошаговое решение. Всякий раз, когда, push/pop команды используются, Z3 автоматически переключится на этот пошаговый решатель. Если мы удалим push а также pop команды, то Z3 может показать, что вторая задача выполнима. Вот ссылка с измененным примером: http://rise4fun.com/Z3/apcQ.