Различные способы аксиоматизации содержащей функции для списков Z3

Ваш скрипт наrise4fun отключает движок :mbqi. Таким образом, Z3 попытается решить проблемы, используя только E-сопоставление. Когда шаблоны (также известные как триггеры) не предоставляются, Z3 выводит триггеры для нас. Z3 использует множество эвристик для определения шаблонов/триггеров. Один из них имеет отношение к вашему сценарию и объясняет, что происходит. Z3 никогда не выберет паттерн/триггер, создающий «совпадающую петлю». Мы говорим, что шаблон/триггер P создает цикл сопоставления для квантификатора Q, когда экземпляр Q создает новое сопоставление для P. Давайте рассмотрим квантификатор

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

Z3 не выберет (Seq.in xs e) в качестве шаблона/триггера для этого квантификатора, потому что это создаст соответствующий цикл. Предположим, у нас есть основной термин (Seq.in a b). Этот термин соответствует шаблону (Seq.in xs e). Создание экземпляра квантификатора с a приведет к b созданию термина (Seq.in (tail a) b), который также соответствует шаблону (Seq.in xs e). Создание квантификатора с (tail a) и b даст терм (Seq.in (tail (tail a)) b), который также соответствует шаблону (Seq.in xs e) и так далее.

Во время поиска Z3 будет блокировать совпадающие циклы, используя несколько порогов. Однако, как правило, страдает производительность. Таким образом, по умолчанию Z3 не будет выбирать (Seq.in xs e) в качестве шаблона. Вместо этого он выберет (Seq.in (tail xs) e). Этот шаблон не создает цикл сопоставления, но также не позволяет Z3 доказать, что второй и третий запросы неудовлетворительны. Любые ограничения механизма E-сопоставления обычно обрабатываются механизмом :mbqi. Однако в вашем скрипте :mbqi отключено.

Если вы предоставите шаблоны для второго и третьего запросов в вашем скрипте. Z3 докажет, что все примеры равны unsat. Вот ваш пример с явными шаблонами/триггерами:

http://rise4fun.com/Z3/DkZd

Первый пример выполняется даже без использования шаблонов, поскольку для доказательства того, что пример равен unsat, требуется только первый квантификатор.

(assert (forall ((e Int))
  (not (Seq.in nil e))))

Обратите внимание, что (Seq.in nil e) является идеальным образцом для этого квантификатора, и он выбран Z3.