如何在Z3中验证将数组选值作为递归函数参数的SMT规范？

研究背景 #

我正在研究以Z3作为SMT求解器的程序自动验证技术，目标是解析包含预期行为规范的标注程序，自动生成证明义务并通过Z3完成验证。我了解Dafny正好实现了该能力且表现优异，但Dafny的内部实现逻辑并不透明，因此我正在探索直接使用Z3实现该需求的可行边界。目前整体运行效果良好，大多数生成的证明义务Z3都能在数秒内完成验证，但当我将从数组常量中选取的值作为递归函数的入参时，出现了意外的运行卡住问题。

问题复现 #

该问题可简化为如下最小SMT示例：

(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun d () (Array Int Int))
(declare-fun Ld () Int)
(define-funs-rec ( 
  (sometimesFalse ((x Int)) Bool))
  ((ite (<= x 0) 
    false
    (ite (= x 1)
      true
      (sometimesFalse (- x 2))
    )
  ))
)

(assert 
  (let (
    (pre0 (not (= i j)))
    (pre1 (and (<= 0 i) (< i Ld)))
    (pre2 (and (<= 0 j) (< j Ld)))
    (pre3 (forall ((k Int))
      (=> 
        (and (<= 0 k) (< k Ld))
        (sometimesFalse (select d k))
      )
    ))
    (post (sometimesFalse (select (store d j 0) i)))
  ) 
  (and pre0 pre1 pre2 pre3 (not post))
))
(check-sat)

上述SMT规范无法被Z3验证，会陷入看似无限的运行状态。如果我们稍微修改post条件，改为直接从原数组d取值，Z3就能立刻返回UNSAT完成验证，可正常验证的SMT规范如下：

(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun d () (Array Int Int))
(declare-fun Ld () Int)
(define-funs-rec ( 
  (sometimesFalse ((x Int)) Bool))
  ((ite (<= x 0) 
    false
    (ite (= x 1)
      true
      (sometimesFalse (- x 2))
    )
  ))
)

(assert 
  (let (
    (pre0 (not (= i j)))
    (pre1 (and (<= 0 i) (< i Ld)))
    (pre2 (and (<= 0 j) (< j Ld)))
    (pre3 (forall ((k Int))
      (=> 
        (and (<= 0 k) (< k Ld))
        (sometimesFalse (select d k))
      )
    ))
    (post (sometimesFalse (select d i)))
  ) 
  (and pre0 pre1 pre2 pre3 (not post))
))
(check-sat)

需要注意的是，我们显式声明了i != j，因此在SMT-LIB的数组理论规则下，(select d i)和(select (store d j 0) i)是完全等价的。

相关参考 #

生成该问题证明义务的Dafny语法标注程序如下，Dafny可以毫无问题地验证该程序，而它内部也是将程序转换为SMT后调用Z3验证，说明存在可行的方法绕过上述问题：

method test(i: int, j: int, d: array<int>) returns (unused: bool)
    modifies d;
    
    requires i != j;
    requires 0 <= i < d.Length;
    requires 0 <= j < d.Length;
    requires forall k | 0 <= k < d.Length :: sometimesFalse(d[k]);

    ensures sometimesFalse(d[i]);
{
    d[j] := 0;
}

/**
    Recursive function that returns true iff x % 2 == 1.
*/
function sometimesFalse(x: int): bool
{
    if x <= 0 then
        false
    else if x == 1 then
        true
    else
        sometimesFalse(x - 2)
}

问题诉求 #

请问这类SMT规范如何才能被Z3正常验证？由于SMT规范是自动生成的，我需要能适配所有此类问题的通用解决方案。

• 显式插入数组store等价性断言：在自动生成SMT时，只要上下文中存在i != j的约束，就先手动加入(assert (= (select (store d j v) i) (select d i)))的断言，强制Z3先完成该项等价性重写，避免后续与递归函数结合时触发不合理的求解分支。
• 为递归函数添加归纳引理：针对自定义递归函数，提前推导其等价的非递归表达形式，插入全局量词化断言。比如本案例中的sometimesFalse函数等价于判断输入为正奇数，可添加(assert (forall ((x Int)) (= (sometimesFalse x) (and (> x 0) (= (mod x 2) 1)))))，替代Z3对递归函数的自动展开，大幅降低求解复杂度。
• 调整Z3求解器参数：开启smt.array.extensional数组扩展公理，或者设置smt.mbqi.max_iterations参数限制基于模型的量词实例化迭代次数，避免求解陷入无限循环。
• 预展开有限层递归：针对输入范围有界的场景，生成SMT时可以先对递归函数做固定层数的展开，避免Z3在求解过程中无限制展开递归结构。

Dafny之所以不会出现该卡顿问题，正是因为其内部自动实现了前两项优化：会为所有递归函数自动推导并插入归纳性质断言，同时在处理数组写入操作时会先完成等价性替换，再将简化后的表达式传递给Z3求解。

内容的提问来源于stack exchange，提问作者M. van der Horst