递归函数的错误？

Question

我正在 z3 中尝试递归函数，我很好奇模型构建是否存在错误。考虑：

(define-fun-rec f ((x Int)) Int
                  (ite (> x 1)
                       (f (- x 1))
                       1))
(check-sat)
(get-value ((f 0)))

这里的f其实就是常量函数1，只是定义的比较傻。对于这个输入，z3 打印：

sat
(((f 0) 0))

这似乎不正确，因为 f 0 应该等于 1。

有趣的是，如果我断言 z3 提出的结果是什么，那么我会得到正确的 unsat 答案：

(define-fun-rec f ((x Int)) Int
                  (ite (> x 1)
                       (f (- x 1))
                       1))
(assert (= (f 0) 0))
(check-sat)

我得到：

unsat

所以，看起来 z3 现在确实做到了 f 0 不可能是 0；即使它在前一个案例中产生了那个模型。

更进一步，如果我发出：

(define-fun-rec f ((x Int)) Int
                  (ite (> x 1)
                       (f (- x 1))
                       1))
(assert (= (f 0) 1))
(check-sat)
(get-model)

然后z3回复：

sat
(model
  (define-fun f ((x!0 Int)) Int
    1)
)

这确实是一个合理的答案。

所以，在某些情况下，递归函数模型似乎可能存在错误？

Answer 1

用于反映递归函数定义图的模型。因此，在对求解过程中未见的值评估递归函数时，可能会产生任意结果。此行为现已更改，因为模型中包含递归定义。

递归函数的错误？

Bug with recursive functions?

recursion

z3