Совместимы ли Int и Real как-то в SMT-LIB?

Question

Оператор равенства в SMT-LIB обычно требует, что неудивительно, чтобы его операнды были одного типа. Например, это ошибка:

      (set-logic QF_LIRA)
(declare-fun a () Bool)
(declare-fun b () Real)
(assert (= a b))
(check-sat)

Однако я ожидал, что это тоже будет ошибка:

      (set-logic QF_LIRA)
(declare-fun a () Int)
(declare-fun b () Real)
(assert (= a b))
(check-sat)

Но Yices и Z3 принимают это без жалоб.

Что мне не хватает?

Answer 1

Строго говоря, такое смешивание и сопоставление не допускается SMTLib. (См. страницу 37 https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf, где четко указано=должен принимать два аргумента одного и того же типа.)

Однако большинство решателей «мягко» относятся к своей обработке; т. е. они вводят принуждение, когда считают, что это «имеет смысл». Лично я считаю это проблематичным: приведения вряд ли когда-либо полезны (особенно в языке, который предназначен для генерации с помощью инструментов в целом), и иногда они могут скрыть ошибки, когда пользователь хотел сказать одно, но сказал неправильно, и система каким-то образом придал этому смысл. (Вы можете сравнить это со смешиванием и сопоставлением арифметических чисел разных типов во многих языках программирования. Но я отвлекся.)

Сказав это, вы можете попросить большинство решателей быть «более послушными»:

      $ z3 smtlib2_compliant=true a.smt2
success
success
success
(error "line 4 column 14: Sort mismatch at argument #1 for function (declare-fun = (Real Real) Bool) supplied sort is Int")
sat

Обратите вниманиеsmtlib2_compliantпараметр в командной строке. Аналогично, cvc5 можно сделать более строгим:

      $ cvc5 --strict-parsing a.smt2
(error "Parse Error: a.smt2:4.15: Subexpressions must have the same type:
Equation: (= a b)
Type 1: Int
Type 2: Real
")

Обратите внимание, что мне явно пришлось пройти--strict-parsingаргумент, поскольку он также вставляет приведение без этого флага.

Мое личное мнение таково, что все они должны всегда соблюдать требования; но положение дел таково, что большинство решателей вводят эти приведения, ведущие в лучшем случае к путанице, а в худшем - к сокрытию ошибок. Например, вы на самом деле не знаете, «понижает» ли он (т. е. каким-то образом усекает) вещественное значение до целого числа и проверяет равенство; или если он «преобразует» целое число в действительное. Не существует простого способа определить, какой из них произошел, не проверив сам код. (В данном конкретном случае оба решателя преобразуют целое число в действительное; так что это правильно.)