Z3中如何处理递归函数？

Question

(set-option :smt.mbqi true)
(declare-fun R(Int) Int)
(declare-const a Int)
(assert (= (R 0) 0))
(assert (forall ((n Int)) (=> (> n 0) (= (R n ) (+ (R (- n 1)) 1)))))
(assert (not (= a 5)))
(assert (not (= (R a) 5)))
(check-sat)

我已经在Z3中尝试了上面的代码，但是Z3无法回答。你能指导我哪里出错了吗？

Answer 1

作为一般模式，不要期望 MBQI 生成涉及仅具有无限范围的不同值的函数的模型。如果确实必须，那么您可以使用 Define-fun-rec 构造来定义递归函数。Z3 当前相信定义是格式良好的（例如，对应于函数定义的方程是可满足的）。

(set-option :smt.mbqi true)
(declare-fun F (Int) Int)
(define-fun-rec R ((n Int)) Int
   (if (= n 0) 0
       (if (> n 0) (+ (R (- n 1)) 1)
            (F n))))

(declare-const a Int)
(assert (not (= a 5)))
(assert (not (= (R a) 5)))
(check-sat)
(get-model)

Z3 在搜索过程中被动地使用递归定义的函数：只要存在约束基础部分的候选模型，它就会检查函数图是否在候选模型的值上充分定义。如果不是，则在所选值上实例化函数定义，直到在与地面约束相关的值上很好地定义它为止。