Z3に配列の更新を「記憶」させることができるかどうか知りたいです。
たとえば、次の入力は充足可能です。
(declare-const x Int)
(declare-const a1 (Array Int Int))
(assert (= (select (store a1 x 2) x) 2))
(assert (not (= (select a1 x) 2)))
(check-sat)
最初のアサーションの「ストア」は、2番目のアサーションには影響しません。アレイにストア操作を実行して、アレイに永遠の変更を加えることはできますか？つまり、配列でstoreを使用すると、その場合、配列は永久に変更されます。たとえば、'（store a1 x 2）'を使用した後、毎回（select a1 x）は2に等しくなります。これを知っている人はいますか？ありがとう。
式(= (select (store a1 x 2) x) 2)はと同等trueです。配列理論の公理の1つがであるため、これは空虚な主張ですforall a,i,v: select(store(a,i,v), i) = v。したがって、この式は公理（Z3に組み込まれている）の単なるインスタンスであり、このため冗長です。
おそらく、あなたはを主張するつもりでした(assert (= (select a1 x) 2))。このアサーションは、位置にある配列の値がであると言いxます2。つまり、Z3によって生成されたソリューション2は、配列のこの位置に割り当てる必要がありa1ます。
Z3には、アサーションの「前」と「後」の概念、または副作用がないことに注意してください。たとえば、式はZ3a = a + 1と同等です。falseプログラミング言語の割り当てをZ3にエンコードするために使用される一般的な手法の1つは、プログラム変数ごとに複数の変数を使用します。「プログラムの場所」ごとに1つの変数。たとえば、コードブロックa = a + 1; b = 2*a; a = b + 1はとしてエンコードされa_1 = a_0 + 1 and b_1 = 2*a_0 and a_2 = b_1 + 1ます。次の記事には、より多くの例/詳細が含まれています：http ://dl.acm.org/citation.cfm?id=1995394
プログラムで使用される配列更新をエンコードする場合はa1、更新前の配列を表す1つの配列とa2、更新後の配列を表す1つの配列が必要です。つまり、次のように記述(assert (= a2 (store a1 x 2)))し、最後のアサーションを（assert(not (= (select a2 x) 2)))