Почему smtlib/z3/cvc4 позволяет объявить одну и ту же константу более одного раза?

Question

У меня есть вопрос о declare-const в smtlib.

Например,

В z3 / cvc4 следующая программа не сообщает об ошибке:

      C:\Users\Chansey>z3 -in
(declare-const x Int)
(declare-const x Bool)

В справочнике smt-lib сказано, что

(declare-fun f (s1 ... sn) s) ... Команда сообщает об ошибке, если символ функции с именем f уже присутствует в текущей подписи.

Итак, сорт s включено во всю подпись, верно?

Но почему это так? Какая мотивация стоит за этим?

В моем понимании xявляется идентификатором переменной, и в целом (например, в некоторых общих языках программирования) нам не разрешается объявлять одну и ту же переменную с разными типами. Поэтому я думаю, что приведенный выше код лучше всего подходит для сообщения об ошибке.

Я когда-то думал, что, возможно, z3 / smtlib может поддерживать переопределение ?, но не ...

      C:\Users\Chansey>z3 -in
(declare-const x Int)
(declare-const x Bool)
(assert (= x true))
(error "line 3 column 11: ambiguous constant reference, more than one constant with the same sort, use a qualified expre
ssion (as <symbol> <sort>) to disambiguate x")

Итак, приведенный выше код определенно неверен, почему бы не сообщить об ошибке раньше?

PS. Если я использую такую ​​же сортировку, он сообщит об ошибке (это здорово, я надеюсь, что Bool case также может сообщить об ошибке):

      C:\Users\Chansey>z3 -in
(declare-fun x () Int)
(declare-fun x () Int)
(error "line 2 column 21: invalid declaration, constant 'x' (with the given signature) already declared")

Спасибо.

Answer 1

В SMTLib символ идентифицируется не только по имени, но и по сортировке. И совершенно нормально использовать одно и то же имя, если у вас другой сорт, как вы заметили. Вот пример:

      (set-logic ALL)
(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun x () Bool)

(assert (= (as x Int) 4))
(assert (= (as x Bool) true))
(check-sat)
(get-model)
(get-value ((as x Int)))
(get-value ((as x Bool)))

Это печатает:

      sat
(
  (define-fun x () Bool
    true)
  (define-fun x () Int
    4)
)
(((as x Int) 4))
(((as x Bool) true))

Обратите внимание, как мы используем конструкцию для устранения неоднозначности между двумя xс. Это объясняется в разделе 3.6.4 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf.

Сказав это, я согласен, что процитированная вами часть документа не очень ясна по этому поводу и, возможно, может использовать немного поясняющий текст.

Что касается мотивации такого использования: Есть две основные причины. Первый - упростить создание SMTLib. Обратите внимание, что SMTLib обычно не предназначен для написания от руки. Он часто генерируется из системы более высокого уровня, в которой используется решатель SMT. Таким образом, гибкость в разрешении символам совместно использовать имя при условии, что их можно отличить с помощью явных аннотаций сортировки, может быть полезной, когда вы используете SMTLib в качестве промежуточного языка между системой более высокого уровня и самим решателем. Но когда вы пишете SMTLib вручную, вам, вероятно, следует по возможности избегать такого рода дублирования, как минимум для ясности.

Вторая причина - позволить использовать ограниченную форму «перегрузки». Например, подумайте о функции SMTLib. Эта функция может работать с любым типом объекта ( Int, Bool, Real и т. д.), но он всегда называется distinct. (У нас нет distinct-int, distinct-bool и т. д.) Решатель «различает», какой из них вы имели в виду, выполнив небольшой анализ, но в случаях, когда это невозможно, вы можете помочь ему вместе с asдекларация тоже. Таким образом, теоретические символы могут быть перегружены, что также относится к =, +, *и т. д. Конечно, SMTLib не позволяет пользователям определять такие перегруженные имена, но, как указано в документе в сноске 29 на стр. 91, это ограничение может быть снято в будущем.