1

Z3 で個別の値を割り当てることについて質問したかったのです。

6 つの変数 A、B、C、D、E、F があるとします。ここで、それらのいくつかに個別の値を割り当てたいと思います。それらのいくつかはゼロになります。いくつの変数が明確になり、いくつの変数がゼロになるかは事前にわかりません。それは他の特定の条件に依存します。

一般的に、私が書くすべての変数について

(assert (distinct A B C D E F))

A, B, Dしかし、ゼロで他は異なるなどの制約を書くことは可能ですか? A,B, D繰り返しますが、これは変数の例に過ぎないことを思い出してください。これらは、制約に応じて動的に変更できます。

ありがとう ！

4

1 に答える 1

2

私が理解している限り、変数v 1、...、v nのセットVがあり、各変数v iはゼロであるか、他のすべての変数v j、 j ≠ iとは異なります。

例として、みましょうV = {a, b, c, d}。

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)

制約を次のようにエンコードできます

(assert (or (= a 0) (not (or (= a b) (= a c) (= a d)))))
(assert (or (= b 0) (not (or (= b a) (= b c) (= b d)))))
(assert (or (= c 0) (not (or (= c a) (= c b) (= c d)))))
(assert (or (= d 0) (not (or (= d a) (= d b) (= d c)))))

2 つの制約を追加し、モデルの Z3 をクエリする

(assert (= a 0))
(assert (not (= b 0)))

(check-sat)
(get-model)

その後、利回り

sat
(model 
  (define-fun b () Int
    (- 2))
  (define-fun c () Int
    (- 1))
  (define-fun d () Int
    0)
  (define-fun a () Int
    0)
)

「ゼロまたは個別」の制約を生成するのは面倒な作業なので、おそらく PyZ3 や Scala^Z3 などの Z3 フロントエンドで作業したいと思うでしょう。

于 2013-02-19T11:23:24.053 に答える