Z3에는 연관/교환 연산자 체인에서 하위 수식의 일치를 용이하게하는 기능이 있습니까?

Question

사용자 정의 교환 및 연상 연산자 op가 있다고 가정 해 보겠습니다. 두 개 이상의 인수가있는 op를 사용 중이므로 아래 코드는 유효하지 않습니다. 잠시 동안 그것이 유효하고 "op가 적용되는 방식"이 의미가 없다고 가정 해 봅시다.

(declare-sort T 0) 
(declare-fun op (T T) T) 
(declare-fun P (T) Bool) 
(declare-const a T) 
(declare-const b T) 
(declare-const c T) 
(declare-const d T) 
(declare-const k T) 
; associativity 
(assert (forall ((x T) (y T)) (z T)) 
       (= (op x (op y z)) 
        (op (op x y) z)))) 
; commutativity 
(assert (forall ((x T) (y T))) 
       (= (op x y) 
        (op y x)))) 
; assumption 1 
(assert (forall ((x T) (y T)) (= (op x y) k))) 
; assumption 2 
(assert (P (op a c k))) 
; conjecture 
(assert (not (P (op a b c d)))) 

것은 무슨 가정 1 X 인스턴스화 할 수 있도록하는 가장 좋은 방법이 될 것입니다, Y : =의 B, D와 그 가정 2 추측을 증명에 적용된다?

내가 고려중인 한 가지 해결책은 (op a b c d)에 해당하는 가능한 모든 이진 트리를 생성하는 것입니다. 그것은 꽤 비싸지 만 : 4 개의 잎을 가진 5 개의 다른 2 진 나무와 총 120 개의 다른 2 진 나무를위한 잎의 24 개의 다른 순열이 있습니다. 또한 z3이 연관성과 commutativity를 사용하여 가정 1의 올바른 인스턴스화를 시작하기를 희망 할 수 있습니다.

우리는 (op abc)와 같은 사슬이 보편적 인 내부에 나타날 수 있다고 생각하면 문제가 훨씬 더 짙어집니다 부량. 패턴 화 (op a (op bc)), (op b (op a c)) 등을 사용하여 계량화의 가능성을 최대화 할 수 있지만 패턴이 어딘가에 나타나야하고 z 3에는 아마도 지침이 없을 것입니다. 그것 자체로 나타나게하십시오.

더 좋은 방법이 있습니까?

감사합니다. Simon

Answer 1

Z3에는 모듈러스 A, C, AC, ACI를 일치시키는 데 특별한 지원이 없습니다. 특정 예를 가정하면 가정 1이 이라는 것이 훨씬 더 중요하다는 것이 밝혀졌습니다. 그러나 이것은이 특별한 예에 불과합니다.