z3 - 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 在搜索过程中被动地使用递归定义的函数:每当约束的地面部分有一个候选模型，它检查函数图是否根据候选模型的值充分定义。如果不是，则函数定义在所选值上实例化，直到它在相关值上得到良好定义到地面约束。