2017-07-04 8 views
1

私は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ユーザーは、それをエンコードする素晴らしい方法があります。ありがとう。

答えて

2

疑似ブール関数が必要ですか?たいていの場合/少なくとも/まったく/まったくNの場合は本当ですか?そしておそらく係数で?

もしそうなら、Z3はSMT-LibとさまざまなAPIの両方からこの機能を直接サポートしています。 Pythonのはこちらをご覧ください:SMTLibについてはhttps://github.com/Z3Prover/z3/blob/b27a4a3593fd15c003d3e30da20b35ac96b7218e/src/api/python/z3/z3.py#L7718-L7793

は、ここでの議論を参照してください。K-out-of-N constraint in Z3Py

+0

感謝を。乾杯、 – user2754673

関連する問題