수량 한정 기호가있는 수식에 Z3을 사용하는 방법

Question

배열 집합에 한정 기호를 사용하는 간단한 수식이 있습니다. Z3 (4.3.2)은 "알 수 없음"을 반환합니다.

(assert (forall ((a (Array Int Int)) (b (Array Int Int))) (=> (forall ((i Int)) (= (select a i) (select b i))) (= a b)))) 
(check-sat) 

용장은 다음과 같습니다

(simplifier :num-exprs 12 :num-asts 185 :time 0.00 :before-memory 2.49 :after-memory 2.49) 
(smt.simplifier-done) 
(smt.searching) 
(smt.mbqi) 
(smt.simplifier-done) 
(smt.searching) 
(smt.simplifying-clause-set :num-deleted-clauses 1) 
(smt.simplifier-done) 
(smt.searching) 
(smt.simplifying-clause-set :num-deleted-clauses 1) 
(smt.mbqi :failed k!1) 
(smt.restarting :propagations 0 :decisions 0 :conflicts 0 :restart 100 :agility 0.00) 
(tactic-exception "smt tactic failed to show goal to be sat/unsat") 

Z3 수식의이 종류를 허용 보인다. 내가 장황한 것에 대한 나의 불완전한 이해에서, 사용할 몇 가지 전술을 놓쳤는가? 이 공식을 해결하는 데 도움을 주시겠습니까?

Answer 1

Z3 tutorial (섹션 수량 한정자)은 Z3이 완료된 부분을 설명합니다. 일반적인 문제는 결정할 수 없습니다.

예제와 관련하여 배열을 넘어서는 한정사를 포함하는 만족스런 인스턴스에서 Z3이 실패합니다. 수식이 만족 스럽습니다. 우리가이를 부정하면 Z3은 자동으로 만족스럽지 않음을 증명합니다.

(assert (not (forall ((a (Array Int Int)) (b (Array Int Int))) 
      (=> (forall ((i Int)) (= (select a i) (select b i))) (= a b))))) 
(check-sat) 

참고 : Z3은 본질적으로 만족할만한 검사기입니다. 공식 F을 증명하기 위해, 우리는 부정이 만족스럽지 않다는 것을 보여줍니다.

Answer 2

사실, 처음에는 한정 기호를 제거하려고 할 수 있습니다. 전술 'qe', 'qe-sat'또는 'qe-light'를 사용하면 도움이 될 수 있습니다. 나는 그것을 시도하고 그것은 '사실'로 바뀌어 보인다.