Z3中长BitVec逐位相等为何比整体相等性能更优？

我编写了一个QF_BV类型的Z3 SMT查询，核心逻辑是求解带通配符的hand，要求存在digits推导得到的required与hand完全相等。查询代码如下：

(set-logic QF_BV)

(declare-const orig_hand (_ BitVec 136))
(assert (= orig_hand #x0001121000000011100000011100000000))

(declare-const wildcard (_ BitVec 136))
(assert (or
  (= wildcard #x1000000000000000000000000000000000)
  (= wildcard #x0100000000000000000000000000000000)
  (= wildcard #x0010000000000000000000000000000000)
  (= wildcard #x0001000000000000000000000000000000)
  (= wildcard #x0000100000000000000000000000000000)
  (= wildcard #x0000010000000000000000000000000000)
  (= wildcard #x0000001000000000000000000000000000)
  (= wildcard #x0000000100000000000000000000000000)
  (= wildcard #x0000000010000000000000000000000000)
  (= wildcard #x0000000001000000000000000000000000)
  (= wildcard #x0000000000100000000000000000000000)
  (= wildcard #x0000000000010000000000000000000000)
  (= wildcard #x0000000000001000000000000000000000)
  (= wildcard #x0000000000000100000000000000000000)
  (= wildcard #x0000000000000010000000000000000000)
  (= wildcard #x0000000000000001000000000000000000)
  (= wildcard #x0000000000000000100000000000000000)
  (= wildcard #x0000000000000000010000000000000000)
  (= wildcard #x0000000000000000001000000000000000)
  (= wildcard #x0000000000000000000100000000000000)
  (= wildcard #x0000000000000000000010000000000000)
  (= wildcard #x0000000000000000000001000000000000)
  (= wildcard #x0000000000000000000000100000000000)
  (= wildcard #x0000000000000000000000010000000000)
  (= wildcard #x0000000000000000000000001000000000)
  (= wildcard #x0000000000000000000000000100000000)
  (= wildcard #x0000000000000000000000000010000000)
  (= wildcard #x0000000000000000000000000001000000)
  (= wildcard #x0000000000000000000000000000100000)
  (= wildcard #x0000000000000000000000000000010000)
  (= wildcard #x0000000000000000000000000000001000)
  (= wildcard #x0000000000000000000000000000000100)
  (= wildcard #x0000000000000000000000000000000010)
  (= wildcard #x0000000000000000000000000000000001)))

(declare-const hand (_ BitVec 136))
(assert (= hand (bvadd orig_hand wildcard)))

(declare-const digits (_ BitVec 136))

; 将`digits`的所有十六进制位相加，确保结果模16等于4
(declare-const digits_2 (_ BitVec 136))
(assert (= digits_2 (bvand #x00000000000000000FFFFFFFFFFFFFFFFF (bvadd digits (bvlshr digits (_ bv68 136))))))
(declare-const digits_4 (_ BitVec 136))
(assert (= digits_4 (bvand #x0000000000000000000000000FFFFFFFFF (bvadd digits_2 (bvlshr digits_2 (_ bv36 136))))))
(declare-const digits_8 (_ BitVec 136))
(assert (= digits_8 (bvand #x00000000000000000000000000000FFFFF (bvadd digits_4 (bvlshr digits_4 (_ bv20 136))))))
(declare-const digits_16 (_ BitVec 136))
(assert (= digits_16 (bvand #x0000000000000000000000000000000FFF (bvadd digits_8 (bvlshr digits_8 (_ bv12 136))))))
(declare-const digits_32 (_ BitVec 136))
(assert (= digits_32 (bvand #x00000000000000000000000000000000FF (bvadd digits_16 (bvlshr digits_16 (_ bv8 136))))))
(declare-const digits_sum (_ BitVec 136))
(assert (= digits_sum (bvand #x000000000000000000000000000000000F (bvadd digits_32 (bvlshr digits_32 (_ bv4 136))))))
(assert (= (_ bv4 4) ((_ extract 3 0) digits_sum)))

(declare-const required (_ BitVec 136))
(assert (= required (bvadd digits (bvlshr digits (_ bv4 136)) (bvlshr digits (_ bv8 136)))))

我尝试了两种断言hand与required相等的方式：

方式一：直接BitVec相等 #

(assert (= hand required))
(check-sat)

此方法在我的机器上耗时约0.55秒。

方式二：逐位提取后比较 #

(assert (= ((_ extract 0 0) hand) ((_ extract 0 0) required)))
(assert (= ((_ extract 1 1) hand) ((_ extract 1 1) required)))
...
(assert (= ((_ extract 134 134) hand) ((_ extract 134 134) required)))
(assert (= ((_ extract 135 135) hand) ((_ extract 135 135) required)))
(check-sat)

此方法仅需0.08秒，性能差异显著。

两种方式语义完全等价，为何会出现如此大的耗时差异？是否长BitVec上不应直接使用=断言相等？

原因分析 #

1. 约束处理的粒度差异
   Z3求解器对整体BitVec相等约束和逐位相等约束的处理逻辑不同：

• 直接的(= hand required)会被当作一个整体的位向量约束，求解器可能会尝试用更通用的BitVec等式处理策略，而这种策略在面对长BitVec时，内部转换和推理的开销更大。
• 逐位拆分的约束是原子的1位相等断言，求解器可以直接触发位级别的约束传播，结合问题中wildcard仅翻转单一位的特性，能快速定位需要满足的位，减少不必要的计算。

2. 简化器的效率差异
   Z3的前置简化器对两种约束的处理效率不同：

• 逐位约束更贴合求解器内部的位级推理模型，简化器可以更快地将这些约束与digits的求和规则、required的定义结合，提前排除不可能的分支。
• 整体相等约束需要先被拆分为位级约束才能进行深度简化，但这个自动拆分的步骤可能不如手动拆分高效，尤其是当BitVec长度达到136位时，自动拆分的额外开销会被放大。

3. 问题特性的适配性
   问题中hand的特性非常明确：仅与orig_hand有一位不同。逐位比较时，求解器可以针对每一位单独验证，快速过滤掉不需要修改的位；而整体相等约束需要求解器先处理这个大等式，再结合其他约束推导，无法直接利用“仅单一位不同”的特性，导致耗时增加。

结论 #

两种约束在语义上完全等价，但Z3的内部处理机制导致了性能差异。长BitVec上直接使用=并非绝对不可行，但在某些场景（比如存在单一位修改的强约束），手动拆分成位级约束能触发更高效的求解策略。

不过需要注意：这种优化并非通用。如果BitVec较短，或者问题中没有明确的位级特性，直接使用整体相等约束的性能可能更优，因为手动拆分反而会增加约束数量，带来额外的管理开销。

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