z3中的交叉產品

Question

z3是否爲兩個列表提供交叉產品功能？如果沒有，可以定義一個不使用高階函數或使用提供的列表函數？我一直無法定義一個。我知道如何定義一個使用地圖，但我不認爲這在z3中受支持。

Answer 1

您可以在SMT 2.0中聲明跨產品功能。然而，任何不平凡的財產都需要通過歸納證明。 Z3目前不支持歸納證明。因此，它只能證明非常簡單的事實。 順便說一句，通過列表的交叉積，我假設你想要一個函數，給定列表[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。順便說一句，伊莎貝爾有一個更豐富的輸入語言，並提供調用Z3的策略。

有關Z3中的代數數據類型的更多信息，請轉到在線教程http://rise4fun.com/Z3/tutorial/guide（Section Datatypes）。

;; 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