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は、検索中に受動的に再帰的に定義された関数を使用： 制約のグランド部の候補モデルは、関数グラフが十分候補モデルの値に定義されていることを チェックは、ある時はいつでも。そうでなければ、関数定義は、地面の制約に対して適切な値である に定義されるまで、選択された値でインスタンス化されます。