Z3求解器中relevancy参数对位向量求解的影响分析

在Z3求解器的使用过程中，我们发现了一个与relevancy参数相关的有趣现象。这个参数控制着求解器在推理过程中对相关文字的选择策略，对于位向量(BitVec)类型问题的求解结果会产生直接影响。

问题现象

在特定版本的Z3中，当设置smt.relevancy=0时，对于如下形式的位向量和数组操作组合的SMT公式：

(declare-fun %s () (_ BitVec 12))
(declare-fun init_mem_1 () (Array (_ BitVec 10) (_ BitVec 4)))

(assert (let ((a!9 (select init_mem_1 ((_ extract 11 2) (bvadd #x280 %s)))))
(let ((a!13 (select (store init_mem_1 ((_ extract 11 2) %s) #x0)
                    ((_ extract 11 2) (bvadd #x280 %s)))))
  (not (= a!13 a!9)))))
(check-sat)

求解器会错误地返回SAT结果，而实际上这个公式应该是UNSAT的。这个问题出现在特定的代码提交中，后来被及时修复。

技术背景

relevancy参数是Z3求解器中的一个重要配置选项，它决定了求解器如何选择相关文字进行推理：

• relevancy=0：禁用相关文字启发式，考虑所有文字
• relevancy=1：启用基本相关文字启发式
• relevancy=2：启用更激进的相关文字启发式

对于位向量相关的公式，默认情况下Z3会在自动配置阶段将relevancy设置为0。这是因为经验表明，在位向量问题上，禁用相关文字启发式通常能获得更好的性能。

问题分析与解决

经过深入分析，开发团队发现：

1. 在某些情况下，禁用相关文字启发式会导致求解器错过关键的推理路径
2. 特别是在处理数组存储(store)和选择(select)操作的组合时，这种影响更为明显
3. 对于位向量问题，relevancy=2的设置反而能获得更好的整体性能

修复方案是恢复自动配置阶段将relevancy设置为0的行为，同时确保在各种情况下都能得到正确的结果。实际测试表明，这一修改确实减少了整体超时情况的发生。

实践建议

对于Z3使用者，在处理位向量相关问题时：

1. 可以信任Z3的自动配置机制，它会为位向量问题选择适当的relevancy设置
2. 如果遇到类似的不一致问题，可以尝试显式设置不同的relevancy值进行对比
3. 对于复杂的数组和位向量组合操作，建议进行充分的测试验证

这个案例展示了SMT求解器内部启发式策略对求解结果的重要影响，也体现了Z3团队对求解正确性的高度重视和快速响应能力。