z3의 교차 곱

Question

z3은 두 목록에 대해 교차 곱 함수를 제공합니까? 그렇지 않은 경우 고차 함수를 사용하거나 제공된 목록 함수를 사용하지 않고 정의 할 수 있습니까? 나는 하나를 정의하는 데 어려움을 겪고있다. 지도를 사용하여지도를 정의하는 방법을 알고 있지만지도가 z3에서 지원되지 않는다고 생각합니다.

Answer 1

SMT 2.0에서 교차 제품 기능을 선언 할 수 있습니다. 그러나 사소한 속성의 경우 유도로 증명해야합니다. Z3은 현재 유도에 의한 증명을 지원하지 않습니다. 따라서 매우 간단한 사실 만 입증 할 수있을 것입니다. BTW,리스트의 교차 곱에 의해, 나는리스트를 얻는 함수를 원한다고 가정한다. [a, b]과 [c, d]은리스트 또는 페어 [(a, c), (a, d), (b, c), (b, d)]을 리턴한다. 여기에 product 함수를 정의하는 스크립트가 있습니다. 이 스크립트는 SMT 2.0 언어의 몇 가지 제한 사항을 보여줍니다. 예를 들어, SMT 2.0은 파라 메트릭 공리 또는 함수의 정의를 지원하지 않습니다. 그래서, "해석"하기 위해 해석되지 않은 종류를 사용했습니다. 나는 또한 보조 함수 append과 product-aux을 정의해야했다. 당신은 온라인이 예제를 시도 할 수 있습니다 : http://rise4fun.com/Z3/QahiP는

또한이 예제에서는 l = product([a], [b]) 경우, 다음 first(head(l))는 a해야한다는 다음과 같은 사소한 사실을 증명한다.

평범하지 않은 속성을 증명하는 데 관심이있는 경우. 두 가지 옵션이 있습니다. 우리는 Z3을 사용하여 기본 케이스와 유도 케이스를 증명하려고 시도 할 수 있습니다. 이 접근법의 가장 큰 단점은 이러한 사례를 수동으로 만들어야하고 실수가 발생할 수 있다는 것입니다. 또 다른 옵션은 Isabelle과 같은 대화 형 정리 프로 버를 사용하는 것입니다. BTW, Isabelle은 훨씬 풍부한 입력 언어를 사용하며 Z3을 호출하기위한 전술을 제공합니다.

Z3의 대수 데이터 유형에 대한 자세한 내용은 온라인 자습서 http://rise4fun.com/Z3/tutorial/guide (섹션 데이터 유형)을 참조하십시오.

;; List is a builtin datatype in Z3 
;; It has the constructors insert and nil 

;; Declaring Pair type using algebraic datatypes 
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 

;; SMT 2.0 does not support parametric function definitions. 
;; So, I'm using two uninterpreted sorts. 
(declare-sort T1) 
(declare-sort T2) 
;; Remark: We can "instantiate" these sorts to interpreted sorts (Int, Real) by replacing the declarations above 
;; with the definitions 
;; (define-sort T1() Int) 
;; (define-sort T2() Real) 

(declare-fun append ((List (Pair T1 T2)) (List (Pair T1 T2))) (List (Pair T1 T2))) 
;; Remark: I'm using (as nil (Pair T1 T2)) because nil is overloaded. So, I must tell which one I want. 
(assert (forall ((l (List (Pair T1 T2)))) 
       (= (append (as nil (List (Pair T1 T2))) l) l))) 
(assert (forall ((h (Pair T1 T2)) (t (List (Pair T1 T2))) (l (List (Pair T1 T2)))) 
       (= (append (insert h t) l) (insert h (append t l))))) 

;; Auxiliary definition 
;; Given [a, b, c], d returns [(a, d), (b, d), (c, d)] 
(declare-fun product-aux ((List T1) T2) (List (Pair T1 T2))) 
(assert (forall ((v T2)) 
       (= (product-aux (as nil (List T1)) v) 
        (as nil (List (Pair T1 T2)))))) 
(assert (forall ((h T1) (t (List T1)) (v T2)) 
       (= (product-aux (insert h t) v) 
        (insert (mk-pair h v) (product-aux t v))))) 

(declare-fun product ((List T1) (List T2)) (List (Pair T1 T2))) 

(assert (forall ((l (List T1))) 
       (= (product l (as nil (List T2))) (as nil (List (Pair T1 T2)))))) 

(assert (forall ((l (List T1)) (h T2) (t (List T2))) 
       (= (product l (insert h t)) 
        (append (product-aux l h) (product l t))))) 

(declare-const a T1) 
(declare-const b T2) 
(declare-const l (List (Pair T1 T2))) 

(assert (= (product (insert a (as nil (List T1))) (insert b (as nil (List T2)))) 
      l)) 

(assert (not (= (first (head l)) a))) 

(check-sat) 

Answer 2

smt-lib 형식에 대한 #include 지시어가 없습니다. Z3은 입력을 제공하는 여러 가지 다른 방법을 제공합니다. Python 입력 형식은 모든 Python을 사용하므로 파일 가져 오기가 자연스럽게 지원됩니다. Z3Py에 대한 자습서가 http://rise4fun.com/z3py입니다.