1

z3 は 2 つのリストに対してクロス積関数を提供しますか? そうでない場合、高次関数を使用せずに、または提供されたリスト関数を使用せずに定義することは可能ですか? 私はそれを定義しようとして苦労してきました。マップを使用してマップを定義する方法は知っていますが、z3 ではサポートされていないと思います。

4

2 に答える 2

1

外積関数は SMT 2.0 で宣言できます。ただし、自明でないプロパティは帰納法による証明が必要です。Z3 は現在、帰納法による証明をサポートしていません。したがって、非常に単純な事実しか証明できません。ところで、リストの外積により、リストを指定してリストまたはペア[a, b]を返す関数が必要であると想定しています。関数を定義するスクリプトを次に示します。このスクリプトは、SMT 2.0 言語のいくつかの制限も示しています。たとえば、SMT 2.0 はパラメトリック公理または関数の定義をサポートしていません。そのため、解釈されないソートを使用してそれを「シミュレート」しました。補助関数とも定義する必要がありました。この例をオンラインで試すことができます: http://rise4fun.com/Z3/QahiP[c, d][(a, c), (a, d), (b, c), (b, d)]productappendproduct-aux

この例は、次の自明な事実も証明してl = product([a], [b])いfirst(head(l))ますa。

自明ではないプロパティを証明することに興味がある場合。2 つの選択肢があります。Z3 を使用して、基本ケースと帰納ケースを証明することができます。このアプローチの主な欠点は、これらのケースを手動で作成する必要があり、間違いが発生する可能性があることです。もう 1 つのオプションは、 Isabelleなどの対話型定理証明器を使用することです。ところで、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)
于 2012-05-17T20:53:48.370 に答える
0

smt-lib 形式の #include ディレクティブはありません。Z3 は、入力を提供する他のいくつかの方法を提供します。Python 入力形式はすべての Python を利用するため、ファイルのインポートは当然サポートされます。http://rise4fun.com/z3pyに Z3Py のチュートリアルがあります。

于 2012-05-18T03:23:19.057 に答える