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