固定サイズの配列を作成し、いくつかの値で初期化します。
たとえば、次のC++コード：
a[0] = 10;
a[1] = 23;
a[2] = 27;
a[3] = 12;
a[4] = 19;
a[5] = 31;
a[6] = 41;
a[7] = 7;
それをモデル化するためのZ3のユーティリティはありますか？
質問する
5012 次
2 に答える
15
Z3は配列理論をサポートしていますが、通常、無制限の配列、または非常に大きな配列をエンコードするために使用されます。大きな意味で、数式内の配列アクセス（つまり、選択）の数は、配列の実際のサイズよりもはるかに少ないことを意味します。「問題Xをモデル化/解決するために本当に配列が必要なのか」と自問する必要があります。例のような固定サイズの配列の場合、配列の位置ごとに異なる変数を使用できます。例：a0for a[0]、a1fora[1]など。もちろん、理論を使用しない場合は、などの配列アクセスをエンコードする場合は、次のa[i]ような大きなif-then-else用語としてエンコードする必要があります。
(ite (= i 0) a0 (ite (= i 1) a1 ...))
配列サイズが既知で小さい場合、これは通常、問題をエンコードするための最も効率的なアプローチです。
一方、配列理論を使用する場合は、質問の初期化を次のようにエンコードできます。
(declare-const a (Array Int Int))
(assert (= (select a 0) 10))
...
(assert (= (select a 7) 7))
SMT2.0形式でエンコードされた例全体を次に示します。
この配列の更新をエンコードすることに注意してください。たとえば、Cステートメントの場合、a[3] = 5この割り当ての後に配列を表す新しい配列変数を作成する必要があります。最もコンパクトな方法は、次のstore式を使用します。
(declare-const a1 (Array Int Int))
(assert (= a1 (store a 3 5)))
これがアップデートの完全な例です。
Python / C++/。NetAPIを検討することもできます。それらにより、あなたのような例をはるかにコンパクトな方法でエンコードすることができます。アイデアは、配列の初期化など、一般的に使用されるパターンをエンコードする関数を実装することです。Pythonでの配列初期化の例を次に示します。
于 2012-06-17T06:37:07.993 に答える