모델 불일치 정렬

Question

QF_AUFLIA에서 z3으로 수식을 분석했습니다. 결과는 sat입니다. (get-model)에 의해 반환되는 모델은 다음 줄을 포함하십시오 SMTLIBv2 언어에 대한 이해에 따르면

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

을,이 문장의 형식이 잘못되었습니다. =은 같은 종류의 인수에만 적용해야합니다. 그러나 2은 Int 및 false의 정렬은 Bool입니다.

invalid function application, sort mismatch on argument at position 2 

이 버그가 : 내가 내지 z3 단지이 두 줄을 피드백 할 때

, 그것은 말로 나와 함께 동의?

그렇지 않다면 어떻게 해석해야합니까 (= 2 false)?

Answer 1

입력에 유형 오류가 있기 때문에 문제가 발생했습니다. 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)