在Spacer/Z3的HORN逻辑中使用数组及Horn查询中使用UIF的问题

核心问题解答 #

Horn查询可以直接使用未解释函数（UIF），你提供的代码无法运行的原因是：标准HORN逻辑不包含数组理论，而你声明了数组类型foo，这超出了该逻辑片段的默认支持范围。

修复方案 #

有两种可行的修复方式：

方式1：用未解释函数替代数组 #

将数组foo替换为未解释函数，完全贴合HORN逻辑的要求。修改后的代码如下：

(set-logic HORN)

(declare-fun k1 (Int) Bool)

; 用未解释函数替代数组
(declare-fun foo (Int) Int)

(assert (forall ((v Int)) (=> (< 666 (foo v)) (k1 v))))

(assert (forall ((v Int)) (=> (k1 v) (< 0 (foo v)))))

(check-sat)
(get-model)

这段代码可正常运行，求解器会返回sat并输出对应的模型。

方式2：启用求解器的HORN+Arrays扩展支持 #

部分求解器（如Z3）支持扩展的HORN逻辑，允许结合数组理论。你可以保留原代码，通过添加求解器选项适配：

(set-logic HORN)
; 启用数组支持的扩展选项
(set-option :horn.array.extensional true)
(set-option :smt.mbqi true)

(declare-fun k1 (Int) Bool)

(declare-const foo (Array Int Int))

(assert (forall ((v Int)) (=> (< 666 (select foo v)) (k1 v))))

(assert (forall ((v Int)) (=> (k1 v) (< 0 (select foo v)))))

(check-sat)
(get-model)

这种方式依赖求解器的扩展能力，兼容性不如方式1广泛。

补充说明 #

Horn逻辑的核心是带全称量词的蕴涵式（Horn子句），未解释函数是其原生支持的基础元素。数组属于一阶理论扩展，不在标准HORN逻辑的默认支持范围内，因此需要通过上述方式适配。

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