Sắp xếp không khớp trong Mẫu

Question

Tôi đã phân tích công thức trong QF_AUFLIA với z3. Kết quả là sat. Các mô hình được trả về bởi (get-model) chứa các dòng sau:

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

Theo sự hiểu biết của tôi về ngôn ngữ SMTLIBv2, tuyên bố này bị thay đổi. = chỉ nên được áp dụng cho các đối số cùng loại. Tuy nhiên, 2 đã sắp xếp Int và false đã sắp xếp Bool.

Khi tôi phản hồi chỉ hai dòng này để Z3, nó đồng ý với tôi bằng cách nói:

invalid function application, sort mismatch on argument at position 2 

Đây có phải là một lỗi?

Nếu không, tôi phải giải thích như thế nào (= 2 false)?

Answer 1

Sự cố là do lỗi loại trong đầu vào. Z3 3.2 bỏ sót một số lỗi loại trong các ứng dụng macro. Sự cố này đã được khắc phục. Bản phát hành tiếp theo sẽ báo cáo chính xác lỗi kiểu (còn gọi là sắp xếp không phù hợp). Dưới đây là một ví dụ tối thiểu cho thấy vấn đề:

(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)