具有遞歸函數的錯誤？

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

模型用於不反映遞歸函數定義的圖形。 因此，在求解遞歸函數時，在解決這個問題時可能會產生任意結果。此行爲現​​在已更改爲遞歸定義包含在模型中。