Z3'te özyinelemeyle nasıl baş edilir?

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) 

Yukarıdaki kodu Z3'te denedim, fakat Z3 cevap veremiyor.Yanlışımı yaptığım yerde bana yol gösterebilir misiniz?

Answer 1

Genel bir model olarak, MBQI'nin modellerini yalnızca sonsuz sayıda farklı değere sahip olduğu işlevleri içeren bir model üretmesini beklemeyin. Gerçekten yapmanız gerekiyorsa, 'u özyinelemeli bir işlev tanımlamak için define-fun-rec yapısını kullanabilirsiniz. Z3 şu anda, tanımının iyi oluşturulduğuna (örneğin, tanımına karşılık gelen denklemin tatmin edici olduğu) güvenmektedir. kısıtlamaları zemin bölümü için bir aday model var olduğu zaman, bu fonksiyon grafiği yeterli aday model değerleri tanımlanır kontrol eder:

(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 yinelemeli arama sırasında pasif olarak işlevleri tarif kullanır. Eğer değilse, o zaman fonksiyon tanımları, seçilen kısıtlamalara göre ilgili değerleri üzerinde iyi tanımlanana kadar seçilen değerler üzerinde başlatılır.