Странное поведение seq.nth в exists-выражении - PullRequest
Новая
       90

Странное поведение seq.nth в exists-выражении

0 голосов
/ 27 мая 2020

Запуск z3 на этом 

(assert (< (seq.nth (seq.unit 0) 0) 0))
(check-sat)

приводит к UNSAT

Но запуск 

(assert (exists ((x Int))
  (< (seq.nth (seq.unit 0) x) 0)))

(check-sat)
(get-model)

- это SAT. Глядя на модель 

(model 
  (define-fun seq.nth_u ((x!0 Seq) (x!1 Int)) Int
    (- 1))
)

Итак, не означает ли это, что seq.nth обрабатывается как переменная над функцией? Разве это не должна быть постоянная функция (всегда возвращающая индексированное значение seq)?

Я бы ожидал, что второй случай также будет UNSAT. Чтобы добиться этого, как я могу сделать seq.nth функцией без переменных?

Помощь приветствуется ...

1 Ответ

0 голосов
/ 27 мая 2020

Функция seq.nth недооценена. То есть, если вы запрашиваете элемент, который находится за пределами границ (т. Е. Либо с отрицательным индексом, либо с индексом, большим, чем последний), тогда он может вернуть любое значение, которое хочет решатель. (И решающая программа всегда будет выбирать значение, чтобы сделать ваш запрос выполнимым.)

Это типично для SMTLib, где недостаточно заданные функции могут просто принимать любое значение, когда заданы аргументы, которые не входят в область их аргументов. Итак, z3 сообщает вам, что существует такая модель, индексируя границы с использованием последовательности (seq.unit 0). т.е. мы можем проиндексировать его по некоторому отрицательному значению или по некоторому индексу, большему, чем 0.

Обратите внимание, что значение seq.nth_u, указанное в модели (обратите внимание на суффикс _u!), является ориентировочным того, как моделируется поведение недостаточного / переполнения. Его не следует путать со значением функции seq.nth.

Фактически вы можете заставить z3 отображать значение индекса x, если вы сделаете его экзистенциальным верхним уровнем: 

(declare-fun x () Int)

(assert (< (seq.nth (seq.unit 0) x) 0))

(check-sat)
(get-value (x))

Для этого z3 говорит: 

sat
((x (- 1)))

, то есть индекс в месте -1. Но не путайте это с -1, которое вы видите в интерпретации seq.nth_u. Фактически, если мы также добавим: 

(assert (> x 0))

, тогда z3 скажет: 

sat
((x 1))

Однако, если мы добавим: 

(assert (>= x 0))
(assert (<  x 1))

, мы получим unsat как и ожидалось. И при работе с последовательностями вы должны добавить такого рода ограничения (если возможно!), Чтобы избежать доступа за пределы.

...