python - Z3 での変数の削除

Question

z3 を使用して制約システムを解決した後、いくつかの変数が None に設定されているモデルを取得します (私は Pyz3 を使用しています)。それらの変数が排除されたということですか？

ありがとう！

Answer 1

割り当てられていない変数は、「ドント ケア」として解釈する必要があります。つまり、どの代入も入力式を満たすことになります。ここに小さな例があります (こちらからも入手できます)。Z3 によって作成された割り当ては、 にのみ割り当てxられ1ます。の値は関係ありyません。

(set-option :auto-config false)
(declare-const x Int)
(declare-const y Int)
(assert (or (= x 1) (= y 1)))
(check-sat)
(get-model)