eval返回一個let語句

我在Z3中運行以下SMT2規範。我們的目標是在最後得到eval的答案 - 要麼是true要麼是false - 但是我得到了let聲明。這是一個錯誤，還是我應該以某種方式解釋let？手動編譯給我false，它看起來很簡單，但Z3似乎困惑。eval返回一個let語句

(declare-sort PolymorphicClass 0) 

(declare-fun PolymorphicClass!val!6() PolymorphicClass) 
(declare-fun PolymorphicClass!val!13() PolymorphicClass) 
(declare-fun PolymorphicClass!val!2() PolymorphicClass) 
(declare-fun PolymorphicClass!val!12() PolymorphicClass) 
(declare-fun PolymorphicClass!val!14() PolymorphicClass) 
(declare-fun PolymorphicClass!val!10() PolymorphicClass) 
(declare-fun PolymorphicClass!val!8() PolymorphicClass) 
(declare-fun PolymorphicClass!val!9() PolymorphicClass) 
(declare-fun PolymorphicClass!val!15() PolymorphicClass) 
(declare-fun PolymorphicClass!val!0() PolymorphicClass) 
(declare-fun PolymorphicClass!val!1() PolymorphicClass) 
(declare-fun PolymorphicClass!val!11() PolymorphicClass) 
(declare-fun PolymorphicClass!val!3() PolymorphicClass) 
(declare-fun PolymorphicClass!val!5() PolymorphicClass) 
(declare-fun PolymorphicClass!val!4() PolymorphicClass) 
(declare-fun PolymorphicClass!val!7() PolymorphicClass) 

(define-fun k!623 ((x!1 PolymorphicClass)) PolymorphicClass 
    (ite (= x!1 PolymorphicClass!val!15) PolymorphicClass!val!15 
    (ite (= x!1 PolymorphicClass!val!2) PolymorphicClass!val!2 
    (ite (= x!1 PolymorphicClass!val!7) PolymorphicClass!val!7 
    (ite (= x!1 PolymorphicClass!val!8) PolymorphicClass!val!8 
    (ite (= x!1 PolymorphicClass!val!10) PolymorphicClass!val!10 
    (ite (= x!1 PolymorphicClass!val!9) PolymorphicClass!val!9 
    (ite (= x!1 PolymorphicClass!val!14) PolymorphicClass!val!14 
    (ite (= x!1 PolymorphicClass!val!0) PolymorphicClass!val!0 
    (ite (= x!1 PolymorphicClass!val!6) PolymorphicClass!val!6 
    (ite (= x!1 PolymorphicClass!val!5) PolymorphicClass!val!5 
    (ite (= x!1 PolymorphicClass!val!1) PolymorphicClass!val!1 
    (ite (= x!1 PolymorphicClass!val!4) PolymorphicClass!val!4 
    (ite (= x!1 PolymorphicClass!val!12) PolymorphicClass!val!12 
    (ite (= x!1 PolymorphicClass!val!11) PolymorphicClass!val!11 
    PolymorphicClass!val!13))))))))))))))) 

(define-fun isBlog!641 ((x!1 PolymorphicClass)) Bool 
    (ite (= x!1 PolymorphicClass!val!0) true 
    (ite (= x!1 PolymorphicClass!val!1) true 
    false))) 

(define-fun isBlog ((x!1 PolymorphicClass)) Bool 
    (isBlog!641 (k!623 x!1))) 

(check-sat) 
(get-model) 

(eval (isBlog PolymorphicClass!val!6)) 

(exit)

下面是輸出，我從Z3得到：

sat 
(model 
) 
(let ((a!1 (ite (= PolymorphicClass!val!6 PolymorphicClass!val!9) 
       PolymorphicClass!val!9 
       (ite (= PolymorphicClass!val!6 PolymorphicClass!val!14) 
        PolymorphicClass!val!14 
        (ite (= PolymorphicClass!val!6 PolymorphicClass!val!0) 
          PolymorphicClass!val!0 
          PolymorphicClass!val!6))))) 
(let ((a!2 (ite (= PolymorphicClass!val!6 PolymorphicClass!val!7) 
       PolymorphicClass!val!7 
       (ite (= PolymorphicClass!val!6 PolymorphicClass!val!8) 
        PolymorphicClass!val!8 
        (ite (= PolymorphicClass!val!6 PolymorphicClass!val!10) 
          PolymorphicClass!val!10 
          a!1))))) 
(let ((a!3 (ite (= PolymorphicClass!val!6 PolymorphicClass!val!15) 
       PolymorphicClass!val!15 
       (ite (= PolymorphicClass!val!6 PolymorphicClass!val!2) 
        PolymorphicClass!val!2 
        a!2)))) 
      (or (= a!3 PolymorphicClass!val!0) (= a!3 PolymorphicClass!val!1)))))

來源

2013-02-04 user1751402

你的價值觀並沒有任何真正的約束被用於（僅在定義）。您可以使用模型完成來確保Z3評估約束中尚未使用的值。

所以你可以撥打：

(eval (isBlog PolymorphicClass!val!6) :model-completion true)

，以獲得適當的評估。

有關更多信息，請參閱相關問題：Z3 4.3: get complete model。

來源

2013-02-04 20:27:51

謝謝您的及時答覆！ – user1751402

eval返回一個let語句

回答

相關問題