私はZ3のUOD(ここではリスト)に「正確にN」をエンコードしようとしています。 IはCBMC(C有界モデルチェッカー)で達成するために使用される方法は、私は_Boolよく、それはZ3に単純ではないunsigned int型とちょうど状態B1 == N.Z3で正確にnの符号化
// L is the length of the List b1.
unsigned int B1 = 0
for i in range(L):
B1 = b[i] + B1
....
__CPROVER_assume (B1 == N);
を使用するようにリストを定義することです変数は式であり、型の値自体ではありません。だから私の最初の試みは、「少なくともN」と「最大N」をエンコードし、それらを組み合わせて「完全にN」を得ることでした。最初のアイデアを改善し、私の論理クラスを使って、私は 'At N most'を(Not) '少なくともN + 1'に置き換えました。しかし、L =〜600のN> = 5の場合。私の4Gb RAMマシンでメモリが不足しています。
# b1 is the List
X_list = []
for i in range(L-3):
for j in range(i+1,L-2):
l = And (b1[j], b1[i])
for k in range(j+1,L-1):
l1 = And (l, b1[k])
for l in range(k+1,L):
X_list.append(And (b1[l], l1))
B1 = Or(X_list)
File "file1.py", line 49, in <module> X_list.append(And (b1[l], l1)) File "/usr/lib/python2.7/dist-packages/z3/z3.py", line 1611, in And return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) File "/usr/lib/python2.7/dist-packages/z3/z3core.py", line 1653, in Z3_mk_and raise Z3Exception(lib().Z3_get_error_msg(a0, err)) z3.z3types.Z3Exception: out of memory
Z3でこれをエンコードする任意のより良い方法はあります。たぶんシーズンに入ったZ3ユーザーは、それをエンコードする素晴らしい方法があります。ありがとう。
感謝を。乾杯、 – user2754673