SMT-LIB中Int与Real类型是否存在兼容性？

SMT-LIB里的相等运算符=并非要求操作数完全相同类型，而是要求类型兼容，这就是你忽略的核心点，具体解释如下：

• 对于Bool和Real的组合：Bool类型和算术类型（Int/Real）属于完全独立的类型体系，不存在子类型关系或合法的隐式转换规则，所以(= a b)（Bool与Real）会触发类型错误，这和你观察到的一致。

• 对于Int和Real的组合：在QF_LIRA（量化自由整数实数混合逻辑）中，整数类型是实数类型的子类型——所有整数都可以被视为实数的特例。求解器会自动对Int类型的操作数做隐式转换，把它转为Real类型后再进行相等判断。你写的(= a b)其实等价于显式转换的(= (to_real a) b)，完全符合该逻辑的语义规范，所以Yices和Z3都会正常接受，不会报错。

这种隐式转换是SMT-LIB针对混合算术逻辑的特殊设计，目的是简化用户编写混合约束的流程，不用手动写转换函数。

对比示例 #

报错的代码（Bool与Real）：

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

被正常接受的代码（Int与Real）：

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

内容的提问来源于stack exchange，提问作者rwallace