3

z3 で 2 つのリストを連結する方法はありますか? ML の @ 演算子に似ていますか? 私はそれを自分で定義することを考えていましたが、z3 は再帰関数の定義をサポートしていないと思います。つまり、

define-fun concat ( (List l1) (List l2) List 
   (ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) )
)
4

2 に答える 2

3

Levent のコードは機能しますが、再帰の深さに境界を設定する場合、Z3 は通常、アサーションに関する問題がはるかに少なくなります。MBQI に頼る必要さえありません。MBQI は、実用化するには時間がかかりすぎることがよくあります。概念的には、次のことを行う必要があります。

; the macro finder can figure out when universal declarations are macros
(set-option :macro-finder true)

(declare-fun len0 ((List Int)) Int)
(assert (forall ((xs (List Int))) (= (len0 xs) 0)))

(declare-fun len1 ((List Int)) Int)
(assert (forall ((xs (List Int))) (ite (= xs nil)
                                       0
                                       (+ 1 (len0 (tail xs))))))

(declare-fun len2 ((List Int)) Int)
(assert (forall ((xs (List Int))) (ite (= xs nil)
                                       0
                                       (+ 1 (len1 (tail xs))))))

... 等々。このすべてを手動で書き留めるのはおそらく面倒なので、プログラム API を使用することをお勧めします。(恥知らずなプラグ: 私はラケットのバインディングに取り組んできました。

于 2012-05-26T11:11:40.870 に答える
3

2021 アップデート

以下の回答は2012年に書かれました。9年前。それはまだ大部分が正しいままです。ただし、SMTLib では、コンストラクトを介して再帰関数の定義が明示的に許可されるようになりましdefine-fun-recた。ただし、ソルバーのサポートはまだ非常に弱く、そのような関数に関する関心のあるほとんどのプロパティは、そのままでは証明できません。要するに、そのような再帰的な定義は帰納的な証明につながり、SMT ソルバーは単純に帰納を行うための装備が整っていないということです。おそらくあと 9 年で、ユーザーが独自の不変条件を指定できるようになるでしょう。当分の間、Isabelle、Coq、ACL2、HOL、Lean などの定理証明者は、この種の問題を処理するための最良のツールであり続けます。

2012年からの回答

SMT-Lib2 が再帰的な関数定義を許可していないことは正しいです。(SMT-Lib2 では、関数定義はマクロに似ており、省略形に適しています。)

通常のトリックは、そのような記号を未解釈関数として宣言し、定義方程式を量化された公理として主張することです。もちろん、量指定子が機能するようになるとすぐに、ソルバーは「難しい」クエリを返しunknownたり開始したりできます。timeoutただし、Z3 は、典型的なソフトウェア検証タスクから生じる多くの目標に非常に優れているため、関心のある多くのプロパティを証明できるはずです。

lenこれは、リストを定義してappend上書きし、リストに関するいくつかの定理を証明する方法を示す例です。証明に帰納が必要な場合、Z3 はタイムアウトする可能性が高いことに注意してください (以下の 2 番目の例のように)。ただし、Z3 の将来のバージョンでは、帰納証明も処理できるようになる可能性があります。

試してみたい場合は、Z3 Web サイトのこの例のパーマリンクを次に示します: http://rise4fun.com/Z3/RYmx

; declare len as an uninterpreted function
(declare-fun len ((List Int)) Int)

; assert defining equations for len as an axiom
(assert (forall ((xs (List Int)))
          (ite (= nil xs)
               (= 0                     (len xs))
               (= (+ 1 (len (tail xs))) (len xs)))))

; declare append as an uninterpreted function
(declare-fun append ((List Int) (List Int)) (List Int))

; assert defining equations for append as an axiom
(assert (forall ((xs (List Int)) (ys (List Int)))
            (ite (= nil xs)
                 (= (append xs ys) ys)
                 (= (append xs ys) (insert (head xs) (append (tail xs) ys))))))

; declare some existential constants
(declare-fun x () Int)
(declare-fun xs () (List Int))
(declare-fun ys () (List Int))

; prove len (insert x xs) = 1 + len xs
; note that we assert the negation, so unsat means the theorem is valid
(push)
(assert (not (= (+ 1 (len xs)) (len (insert x xs)))))
(check-sat)
(pop)

; prove (len (append xs ys)) = len xs + len ys
; note that Z3 will time out since this proof requires induction
; future versions might very well be able to deal with it..
(push)
(assert (not (= (len (append xs ys)) (+ (len xs) (len ys)))))
(check-sat)
(pop)
于 2012-05-07T07:52:39.630 に答える