z3 "완전히"순서가 지정된 관계보다 많음

Question

SMT 시퀀스를 만들어서 전체 정렬이 필요합니다.

예 1과 a < bb < c가

예 만족할 수 있어야 2 a < b 및 c < d 시켰음이어야한다. b < c을 추가하면 만족할만한 결과를 얻을 수 있습니다.

일반적인 경우에도 가능한 사람이 있습니까?

(declare-fun my_rel (Int Int) (Bool)) 
(assert (forall ((i Int)(j Int)) (implies (my_rel i j) (> i j)))) 
(declare-const a Int) 
(declare-const b Int) 
(declare-const c Int) 
(declare-const d Int) 
(assert (my_rel a b)) 
(assert (my_rel c d)) 
(check-sat) 

이 UNSAT를 반환해야합니다 : 지금까지 나는 다음 시도했다. (assert (my_rel b c))을 추가하면 만족해야합니다.

Answer 1

필자가 원하는 것은 유한 요소 집합 x_1 ... x_n에 대한 전 이적 순서가 사용자 어설 션 집합 P 때문에 완전하고 합법적이어야한다는 것을 확인하는 방법입니다. 주문.

< 관계는 예제에서 암시 적으로 전 이적으로 나타납니다. 암시 적으로 전 이적 인 이진 관계를 쉽게 해킹하는 쉬운 방법은 해석되지 않은 함수를 사용하여 임의의 도메인을 완전히 정렬 된 해석 도메인에 포함시키는 것입니다. 이 목적을 위해 추가 된 해석되지 않은 함수가이 "주문에 포함"하는 의미에서만 나타나는지 확인하십시오.

(declare-fun foo (U) (Int)) 
(define-fun my_rel_strict ((i U) (j U)) (Bool) (> (foo i) (foo j))) 
(define-fun my_rel_nonstrict ((i U) (j U)) (Bool) 
    (or (= (foo i) (foo j)) (my_rel_strict i j)) 

my_rel 관계 모두 타동사되며 my_rel_strict가 전체 상태 (중 (my_real_nonstrict i 서 J) 또는 (my_rel_nonstrict의 j 개의 I) 보유)를 갖는다. (http://en.wikipedia.org/wiki/Total_order 참조) my_rel에는 반 대칭이 없으므로 전체 순서도 아닙니다. 잠재적 인 문제를 피하기 위해 도메인의 카디널리티는 적어도 코모 메인의 카디널리티가되어야합니다 (또는 둘 모두 무한합니다). (my_rel_nonstrict에 대한 인코딩은 좋지 않습니다. 실제로는 = 시도해 보겠습니다.)

다음으로 원하는 내용은 함부 수표입니다. 어설 션 P가 주어지면 사용자가 정의한 추이 순서 (총칭 : <)가 합계가되어야합니까? 우리는 요소의 유한 집합에 대한 공식 총 (X_1 ... x_n) 발명 :

total(x_1 ... x_n) = (and_{for all i,j} (or (< x_i x_j) (= x_i x_j) (> x_i x_j))) 

(안 전체의 매우 즐거운 인코딩을하지만, 인코딩 모두 동일.) (즉, P는 총 수반 확인하려면 함의 보유 시켰음 경우

(assert P) (assert (not total(...))) 
; You may also need (assert (distinct x_1 ... x_n)) 

: ...), 우리는 함께 SMT 해결사를 쿼리합니다. 그것이 만족할 만하다면, 그 함의는 반대의 모범을 보였고 지키지 않습니다.

내 조언이 응용 프로그램에 적용되지 않도록 주문을 자제하는 것이 까다로울 수 있습니다. (소금물로 위의 것을 취하십시오. 나는 그것에 대해 100 %가 아닙니다.)