ValueError異常：需要超過2123個值

Question

我想運行一個非常大的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 

Answer 1

這是不好的編碼習慣：

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