Z3은 수작업으로 작성된 데이터 유형으로 대소 문자를 구분하지 않습니다

Question

boolean은 SM32이고 내 기능은 boolean_and입니다. 내 추측은입니다 및 교환 법칙이 성립입니다 :

(declare-sort boolean) 
(declare-const sk_x boolean) 
(declare-const sk_y boolean) 
(declare-const boolean_false boolean) 
(declare-const boolean_true boolean) 
(declare-fun boolean_and (boolean boolean) boolean) 

;; axiomatize booleans: false /= true and every bool is true or false 
(assert (forall ((x boolean)) (or (= x boolean_false) 
            (= x boolean_true)))) 

(assert (not (= boolean_false boolean_true))) 

;; definition of AND 
(assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false))) 
(assert (forall ((a boolean)) (= (boolean_and boolean_true a) a))) 

;; try to prove that AND is commutative 
(assert (not (= (boolean_and sk_x sk_y) 
       (boolean_and sk_y sk_x)))) 

(check-sat) 

그러나, Z3 내가 이는 skolemised 변수에 내 경우 분할 주장을 사용할 수 있어야합니다 생각에도 불구하고, 잠시 후이 문제에 대한 알 수없는보고 sk_x 및 sk_y. 내 부울 axiomatization를 제거하고 declare-datatypes로 교체하는 경우

호기심, Z3는 unsat을보고합니다

(declare-datatypes() ((boolean (boolean_true) (boolean_false)))) 

(declare-const sk_x boolean) 
(declare-const sk_y boolean) 
(declare-fun boolean_and (boolean boolean) boolean) 

(assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false))) 
(assert (forall ((a boolean)) (= (boolean_and boolean_true a) a))) 

(assert (not (= (boolean_and sk_x sk_y) 
       (boolean_and sk_y sk_x)))) 

(check-sat) 

을 내가 잘못 뭐하는 거지? 내 공리 (axiomatization)를 사용하여 z3을 대소 문자를 구분하는 방법은 무엇입니까?

Answer 1

잘못된 것은 아닙니다. 공식 버전 (v4.3.1)이이 제약은 해석의 것으로 주장되는 등

(assert (forall ((x boolean)) (or (= x boolean_false) 
            (= x boolean_true)))) 

으로 카디널리티 제약을 포함하는 문제에 실패 할 수 있습니다 종류의 boolean는 최대 두 개의 요소로 구성되어있다. 이 문제가 해결되었습니다. 수정본은 unstable 지점에서 이미 제공됩니다. Here은 unstable 분기를 컴파일하는 방법에 대한 지침입니다. 내일 nightly builds에도이 수정 프로그램이 포함될 예정입니다.