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

Question

Аксиоматизация операции содержащегося в списках ( в Rise4Fun) как

(declare-fun Seq.in ((List Int) Int) Bool)

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

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

позволяет Z3 4.0 опровергнуть утверждение

(declare-const x Int)
(assert (Seq.in nil x))
(check-sat) ; UNSAT, as expected

В моих глазах эквивалентная аксиоматизация

(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))))))

результаты в unknown,

Может ли это быть проблемой с триггерами или есть что-то специфическое для домена List, которое может объяснить разницу в поведении?

Answer 1

Ваш скрипт на rise4fun отключает :mbqi двигатель. Таким образом, Z3 попытается решить проблемы, используя только E-match. Когда шаблоны (или триггеры) не предоставляются, 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 доказать, что второй и третий запросы являются неудовлетворительными. Любое ограничение механизма электронного согласования обычно обрабатывается :mbqi двигатель. Тем не мение, :mbqi отключен в вашем скрипте.

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

http://rise4fun.com/Z3/DkZd

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

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

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