0

次のサンプルのように、非常に大きな Z3 python プログラムを実行しようとしています。

 S,   (cl_3,cl_39,cl_11, me_32,m_59,m_81 …………) = EnumSort('S',['cl_3','cl_39','cl_11','me_32','me_59','me_81', …………..])
#########################################  
def fun(h1 , h2):
    conds = [
    (cl_3, me_32),
    (cl_39, me_59),
    (cl_11, me_81),
    ...
    ]
    and_conds = (And(h1==a, h2==b) for a,b in conds)
    return Or(*and_conds)

#######################################
def fun2(m1 , m2):
    conds = [
    (cl_3, me_32),
    (cl_39, me_59),
    (cl_11, me_81),
    ...
    ]
    and_conds = (And(m1==a, m2==b) for a,b in conds)
    return Or(*and_conds)
#######################################
def fun3(y1 , y2):
    conds = [
    (cl_3, me_32),
    (cl_39, me_59),
    (cl_11, me_81),
    ...
    ]
    and_conds = (And(y1==a, y2==b) for a,b in conds)
    return Or(*and_conds)

一致したモデルを取得するためにセット制約を使用しました。一致したモデルは、次のように関数の引数に基づいて取得されます。

s = Solver()
x1 = Const('x1', S)
x2 = Const('x2', S)
x3 = Const('x3', S)

s.add(fun(x1,x2))
s.add(fun2(x2,x3)
.
.
.
s.add(fun3(x3,x1)

print s.check()
print s.model()

しかし、次のエラーが表示されます

ValueError: need more than 2123 values to unpack
4

1 に答える 1

3

これは良いコーディング方法ではありません:

S, (cl_3, cl_39, cl_11, me_32, m_59, m_81...) = EnumSort(...)

そのような何百もの名前付き変数を定義する代わりに、名前のリスト、値のリストを使用し、それらをマッピングする辞書を作成する必要があります。

names = ['cl_3', 'cl_39'...] # don't write this list by hand, if you can avoid it
# eg.: ['cl_{}'.format(i) for i in range(50)] + ['m_{}'.format(i) for i...]

S, values = EnumSort('S', names)

if len(names) != len(values):
    raise Exception('...')

name_to_value = dict(zip(names, values))

# then you can use name_to_value['cl_3'] and so on
于 2013-03-31T18:15:31.893 に答える