Блог

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

Например,

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

 C:UsersChansey>z3 -in
(declare-const x Int)
(declare-const x Bool)
 

В ссылке smt-lib говорится, что

(объявить-весело f (s1 … сн) с) … Команда сообщает об ошибке, если символ функции с именем f уже присутствует в текущей подписи.

Таким образом , сортировка s включена во всю подпись x , верно?

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

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

Однажды я подумал, что, возможно, z3/smtlib может поддерживать переопределение?, но нет…

 C:UsersChansey>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")
 

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

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

 C:UsersChansey>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")
 

Спасибо.

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

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

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

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

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