模型中的排序不匹配

我已經用z3分析了QF_AUFLIA中的一個公式。結果是sat。通過(get-model)返回該模型包含以下行：模型中的排序不匹配

(define-fun PCsc5_() Int 
    (ite (= 2 false) 23 33)

根據我的SMTLIBv2語言的理解，這種說法是畸形的。 =只應用於相同類型的參數。然而，2有排序Int和false有排序Bool。

invalid function application, sort mismatch on argument at position 2

這是一個錯誤：

當我反饋只是這兩條線到Z3，它跟我說同意？

如果不是，我該如何解釋(= 2 false)？

來源

2012-01-03 Georg

是的，這似乎是模型構造中的一個錯誤。你可以給我們發送這個僞造模型的公式嗎？謝謝。 – 2012-01-03 14:47:38

我剛剛給你發了一封電子郵件。 – Georg 2012-01-03 15:02:50

該問題是由於輸入中的類型錯誤造成的。 Z3 3.2錯過了宏應用程序中的某些類型錯誤。這個問題已修復。下一個版本將正確報告類型錯誤（又稱排序不匹配）。這是一個最小的例子，揭示了這個問題：

(set-option :produce-models true) 
(declare-fun q (Int) Bool) 
;; p1 is a macro 
(define-fun p1 ((z Int) (y Int)) Bool 
    (ite (q y) (= z 0) (= z 1))) 
(declare-const a Int) 
(declare-const b Bool) 
(assert (p1 a b)) ;; << TYPE ERROR: b must be an Int 
(check-sat) 
(get-model)

來源

2012-01-05 00:45:43

模型中的排序不匹配

回答

相關問題