为何Z3无法证明该查询为unsat而cvc5可以？

我有一个SMT查询，理论上应返回unsat：heap1包含两个元素，满足0.6 + 0.5 > 1且valid(heap1)，违反了全称断言的约束。用cvc5提交能得到预期的unsat，但Z3返回unknown。以下是具体的查询代码、原因分析和解决方法。

SMT查询代码 #

(set-logic AUFLIRA)
(set-option :produce-models true)

(declare-sort Loc 0)
(declare-sort HeapChunk 0)
(declare-sort HeapIndex 0)

(declare-fun makeHeapChunk (Loc Real) HeapChunk)
(declare-fun valid ((Array HeapIndex HeapChunk)) Bool)

(declare-const empty (Array HeapIndex HeapChunk))

(assert (
    forall (
        (heap (Array HeapIndex HeapChunk))
        (i1 HeapIndex) 
        (i2 HeapIndex) 
        (l1 Loc) 
        (l2 Loc) 
        (own_val1 Real) 
        (own_val2 Real)
    )

    (=> 
        (and
            (valid heap)
            (= (select heap i1) (makeHeapChunk l1 own_val1)) 
            (= (select heap i2) (makeHeapChunk l2 own_val2)) 
            (> (+ own_val1 own_val2) 1)
            (not (= i1 i2))
        )

        (not (= l1 l2))
    )
))

(declare-const index0 HeapIndex)
(declare-const index1 HeapIndex)
(assert (not (= index0 index1)))

(declare-const l1 Loc)

(declare-const heap0 (Array HeapIndex HeapChunk))
(assert (valid heap0))

(assert (= heap0 (store empty index0 (makeHeapChunk l1 0.6))))

(declare-const heap1 (Array HeapIndex HeapChunk))
(assert (valid heap1))
(assert (= heap1 (store heap0 index1 (makeHeapChunk l1 0.5))))

(check-sat)
(get-model)
(exit)

原因分析 #

Z3返回unknown的核心原因是量词实例化策略未触发必要的冲突检查：

1. 全称量词中同时涉及未解释排序（Loc、HeapChunk、HeapIndex）、数组操作（select/store）和自定义构造函数（makeHeapChunk），Z3的启发式实例化规则没能自动识别出需要将问题中的具体常量（heap1、index0、index1、l1、0.6、0.5）代入量词生成冲突。
2. AUFLIRA理论支持数组、未解释函数和线性算术，但Z3对该理论组合下的量词处理成熟度不如cvc5，尤其是复杂约束场景下的实例化触发逻辑不够完善。

解决办法 #

1. 显式添加量词实例化断言 #

直接把全称量词的变量替换为问题中的具体常量，手动触发冲突检查。在查询末尾添加以下断言：

(assert (=> 
    (and
        (valid heap1)
        (= (select heap1 index0) (makeHeapChunk l1 0.6))
        (= (select heap1 index1) (makeHeapChunk l1 0.5))
        (> (+ 0.6 0.5) 1)
        (not (= index0 index1))
    )
    (not (= l1 l1))
))

添加后Z3会直接推导出(not (= l1 l1))的矛盾，返回unsat。

2. 调整Z3的量词实例化策略 #

修改Z3的配置选项，强制更积极的量词实例化：
在查询开头添加：

(set-option :smt.qi.eager_threshold 1)
(set-option :quantifier-sort-symbols true)

• :smt.qi.eager_threshold 1：让Z3对所有量词尝试更急切的实例化，而非依赖启发式过滤。
• :quantifier-sort-symbols true：允许Z3针对未解释排序生成实例化候选，覆盖问题中的具体常量。

3. 简化约束结构，添加投影函数 #

将makeHeapChunk的属性拆分为显式的投影函数，帮助Z3关联数组元素的内部属性：

(set-logic AUFLIRA)
(set-option :produce-models true)

(declare-sort Loc 0)
(declare-sort HeapChunk 0)
(declare-sort HeapIndex 0)

(declare-fun makeHeapChunk (Loc Real) HeapChunk)
(declare-fun getLoc (HeapChunk) Loc)
(declare-fun getVal (HeapChunk) Real)
(declare-fun valid ((Array HeapIndex HeapChunk)) Bool)

;; 添加投影函数的一致性断言
(assert (forall (l Loc v Real) (and 
    (= (getLoc (makeHeapChunk l v)) l)
    (= (getVal (makeHeapChunk l v)) v)
)))

(declare-const empty (Array HeapIndex HeapChunk))

(assert (
    forall (
        (heap (Array HeapIndex HeapChunk))
        (i1 HeapIndex) 
        (i2 HeapIndex) 
    )

    (=> 
        (and
            (valid heap)
            (> (+ (getVal (select heap i1)) (getVal (select heap i2))) 1)
            (not (= i1 i2))
        )

        (not (= (getLoc (select heap i1)) (getLoc (select heap i2))))
    )
))

(declare-const index0 HeapIndex)
(declare-const index1 HeapIndex)
(assert (not (= index0 index1)))

(declare-const l1 Loc)

(declare-const heap0 (Array HeapIndex HeapChunk))
(assert (valid heap0))

(assert (= heap0 (store empty index0 (makeHeapChunk l1 0.6))))

(declare-const heap1 (Array HeapIndex HeapChunk))
(assert (valid heap1))
(assert (= heap1 (store heap0 index1 (makeHeapChunk l1 0.5))))

(check-sat)
(get-model)
(exit)

这个版本通过投影函数getLoc和getVal直接提取HeapChunk的属性，简化了全称量词的结构，Z3能更容易识别出需要实例化的变量组合，返回unsat。

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