Z3断言量化位向量数组公理后无法找到简单可满足解

问题描述 #

当自定义存储位向量的数组类型并断言第一条数组更新公理后，后续简单断言会让Z3持续运行，既不返回sat也不返回unsat：

(declare-sort MyArray)
; Indices into the array
(declare-sort Id)

; Returns the value in the array located at the specified index
(declare-fun index
    (MyArray Id)
    (_ BitVec 8))

; Updates the array so that the provided value is stored at the specified index
(declare-fun upd 
    (MyArray Id (_ BitVec 8))
    MyArray)

; First array update axiom
(assert (forall ((a MyArray) (i Id) (v (_ BitVec 8)))
    (= 
        (index (upd a i v) i)
        v)))

(declare-const x Int)
(declare-const y Int)
(echo "")
(echo "Sanity check, should be sat:")
(assert (= x y))
(check-sat)

但如果数组存储自定义排序的元素，Z3能快速返回sat：

(declare-sort MyArray)
; Indices into the array
(declare-sort Id)
; Values stored in the array
(declare-sort Elem)

; Returns the value in the array located at the specified index
(declare-fun index
    (MyArray Id)
    Elem)

; Updates the array so that the provided value is stored at the specified index
(declare-fun upd 
    (MyArray Id Elem)
    MyArray)

; First array update axiom
(assert (forall ((a MyArray) (i Id) (v Elem))
    (= 
        (index (upd a i v) i)
        v)))

(declare-const x Int)
(declare-const y Int)
(echo "")
(echo "Sanity check, should be sat:")
(assert (= x y))
(check-sat)

疑问点：

• 为何仅在位向量作为元素时出现求解停滞？是否和Z3位向量的量词消除策略有关？
• 因需求涉及8位位向量操作（如bvxor），是否需要自行定义位向量操作，或有更优方案避免混合量词、位向量和数组理论？

原因分析 #

核心问题在于Z3的量词实例化策略与位向量理论的交互：

1. 量词实例化循环：当使用位向量作为数组元素时，全称量词的实例化会触发针对位向量的启发式规则。由于upd函数既接收又返回MyArray类型，Z3可能反复尝试生成新的实例，陷入无限循环。
2. 位向量量词处理限制：正如Nikolaj所述，Z3针对位向量的量词消除策略相对简单，缺乏针对自定义数组结构的优化。而自定义排序Elem属于未解释类型，Z3会采用更保守的实例化策略，不会触发过度的探索。

解决方案 #

针对8位位向量的需求，推荐以下几种方案：

1. 使用Z3原生数组理论 #

直接使用Z3内置的数组类型，而非自定义MyArray、index和upd：

(declare-sort Id)
; 原生数组类型：Id -> (_ BitVec 8)
(declare-const arr (Array Id (_ BitVec 8)))
(declare-const i Id)
(declare-const v (_ BitVec 8))
; 更新数组
(declare-const arr_upd (Array Id (_ BitVec 8)))
(assert (= arr_upd (store arr i v)))
; 读取数组
(assert (= (select arr_upd i) v))

(declare-const x Int)
(declare-const y Int)
(assert (= x y))
(check-sat)

Z3对原生数组理论有深度优化，能正确处理量词与位向量的组合，避免实例化循环。

2. 限制量词实例化范围 #

如果必须自定义数组结构，可通过添加模式(pattern) 引导Z3的量词实例化，避免无意义的循环：

(declare-sort MyArray)
(declare-sort Id)

(declare-fun index (MyArray Id) (_ BitVec 8))
(declare-fun upd (MyArray Id (_ BitVec 8)) MyArray)

; 添加模式，仅当(index (upd a i v) i)出现时才实例化量词
(assert (forall ((a MyArray) (i Id) (v (_ BitVec 8)))
    (! (= (index (upd a i v) i) v)
       :pattern ((index (upd a i v) i)))))

(declare-const x Int)
(declare-const y Int)
(assert (= x y))
(check-sat)

模式告诉Z3只有当特定子表达式出现时才实例化量词，减少不必要的实例生成。

3. 转换为整数运算替代位向量 #

若场景允许，可将8位位向量转换为0-255范围的整数，用整数理论替代位向量理论，结合自定义数组结构。需手动映射位运算（如bvxor对应整数异或），适合位操作较少的场景。

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