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