ValueError: Need more than 2123 values

Question

I am trying to run a very large Z3 python program, as the following sample:

 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)

I have used a set constraint to retrieve the matched models; the matched model will be retrieved based on the function arguments, as the following:

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()

But, I am getting the following error

ValueError: need more than 2123 values to unpack

Answer 1

This is not good coding practice:

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

Instead of defining hundreds of named variables like that, you should use a list of names, a list of values, and build a dict to map them:

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