z3 - Z3 でリレーションを定義できますか?

Question

z3 SMT ソルバーは初めてです。関数の代わりにリレーションを定義する必要があります。複数の値を返すことができる関数を意味します。チュートリアルを調べましたが、何も見つかりませんでした。この点で私を助けていただければ幸いです。

どうもありがとう。

Answer 1

ArrayEx理論をサポートするロジックの 1 つを使用します。これは、配列を操作するための配列並べ替えと関連する関数を提供します。次に、任意の数の Int や Bool などを含むことができる配列値を関数に返すようにできます。

この SMT チュートリアルは、多くの SMT の詳細を 1 か所にまとめた優れたリソースです。

Answer 2

ある意味では、SMT は "自然に" リレーショナル プログラミングをサポートします。引数の可能な値を単純に分離することで、目的の結果を得ることができます。何かのようなもの：

(declare-fun foo ((Int)) Int)
(assert (or (= (foo 3) 4) (= (foo 3) 5)))
(check-sat)
(eval (foo 3))   ; might produce 4 of 5
(assert (distinct (foo 3) 4))
(check-sat)
(eval (foo 3))   ; will produce 5
(assert (distinct (foo 3) 5))
(check-sat)      ; will declare unsat 

fooに適用されると、 、 、または3を生成できると言っています。そして、必要に応じて「さらに」事実を主張して、スペースを制限することができます。または無料のままにしてください。このトリックを使用して、本質的にリレーションとしてモデル化できます。SMT ソルバーをリレーショナル プログラミング言語として動作させる..45foo

もちろん、リレーションをどのようにモデリングしたいかは、目前の問題によって異なります。上記は、問題に最適な選択ではない可能性があります。

Answer 3

次の例は、おそらくあなたが探しているものだと思います。

(define-fun sqrt ((a Int) (b Int)) Bool
    (= (* b b) a)
)
(declare-const a  Int)
(declare-const b1 Int)
(declare-const b2 Int)
(assert (sqrt a b1))
(assert (sqrt a b2))
(assert (not (= b1 b2)))
(check-sat)
(get-model)

z3 を呼び出すと、次のようになります。

$ z3 -smt2 rel.smt
sat
(model 
  (define-fun b2 () Int
    2)
  (define-fun a () Int
    4)
  (define-fun b1 () Int
    (- 2))
)

リレーションは、sqrt順序付けられたペアのセットです: {(a,b) | a == b*b}. と の両方がこの関係(4,2)に(4,-2)属します。SMT の言い回しでは、これは と の両方が であることを意味sqrt(4,2)しsqrt(4,-2)ますtrue。4これは、複数の値を持つことができる質問の言い回しに対応しています。残念ながら、を使用するような他の回答は、foo 関係を実際に処理するのではなく、ソルバーに 2 つの関数のどちらかを選択するように求めます。