1

公理のセットを想定して、Z3の非ブール式を単純化する方法はありますか？

たとえば、「a == b」と主張し、式「If（a == b、1、2）」を簡略化して「1」を取得します。

特に、私は配列理論を扱うことに興味があります。

I = BitVecSort(32)
A = Array('A', I, I)
a = BitVec('a',32)
b = BitVec('b',32)
c = BitVec('c',32)
...
A2 = Store(A, a, 1) 
A3 = Store(A2, b, 2) 
A4 = Store(A3, c, 3)

simplify_assuming(A4[a], Distinct(a, b, c))

配列理論の規則に従って、すべてのインデックスが異なると仮定すると、Select式を「1」に簡略化できるため、これは「1」を返すはずです。

「ctx-solver-simplify」戦術を使用しようとしましたが、ブール式でのみ機能するようです。非ブール式を単純化する他の方法はありますか、または何らかの方法で配列リライターにインデックスが異なることを伝えますか？

ありがとう。

4

1 に答える 1

1

上記のコメントで説明されているように、Nikolajはctx-solver-simplify非ブール式の下を歩きません。もう1つのオプションは、solve-eqs表明された等式を使用して式の残りの部分を書き直す戦術を使用することです。たとえば、が等しい場合、Z3はすべての出現箇所をでa == b置き換えます（またはその逆）。その後、に書き換えられます。baif(a == b, 1, 2)1

ただし、solve-eqsなどの不等式は使用しませんDistinct(a, b, c)。別のオプションは、戦術を使用することpropagate-valuesです。アサーションのすべての出現を。に置き換えPますtrue。同様に、アサーションがある場合は、not P他のすべてのオカレンスPを。に置き換えfalseます。この戦術は、基本的にユニットブール伝播を実行しています。さらに、それは高速であることが意図されており、いかなる形式の理論的推論も適用しません。たとえば、がある場合Distinct(a, b, c)、それはに置き換えa == bられませんfalse。したがって、このアプローチは、目的には脆弱すぎる可能性があります。これを使用するスクリプトを次に示します。こちらからオンラインでも入手できます。このスクリプトではA4[a]、新しい述語を使用して式をラップしますPZ3目標はブール式のセットであるためです。私は、を一連の不等式にblast_distinct変換し、フォームの用語をフォームのに拡張するために使用します。結果には、がに簡略化されたことを示すが含まれていることに注意してください。Distinctexpand_select_storestore(A, i, v)[j]if-then-elseif(i == j, v, A[j])P(1)P(A4[a])1

I = BitVecSort(32)
A = Array('A', I, I)
a = BitVec('a',32)
b = BitVec('b',32)
c = BitVec('c',32)
A2 = Store(A, a, 1) 
A3 = Store(A2, b, 2) 
A4 = Store(A3, c, 3)

P = Function('P', I, BoolSort())
G = Goal()
G.add(P(A4[a]))
G.add(Distinct(c, b, a))

T = Then(With("simplify", blast_distinct=True, expand_select_store=True), "propagate-values")
print(T(G))
于 2013-03-24T16:59:38.423 に答える