所以我正在寻找一种方法来简化 Z3py 中的以下代码，因为每次我想检查这个断言（在我自己的计算机或http://rise4fun.com/z3py/上）它只是超时所以我认为可能是最快的方法。
Task = Datatype('Task')
Task.declare("cons",("num", IntSort()),("order",IntSort()),("arrival",IntSort()))
Task = Task.create()
order = Task.order
num = Task.num
x = Int('x')
y = Int('y')
s = Solver()
tasks = (Task.cons(0,0,0),\
Task.cons(0,1,0),\
Task.cons(0,2,0),\
Task.cons(0,3,0),\
Task.cons(1,0,1),\
Task.cons(1,1,1),\
Task.cons(1,2,1),\
Task.cons(2,0,3),\
Task.cons(2,1,3),\
Task.cons(2,2,3),\
Task.cons(2,3,3),\
Task.cons(2,4,3),\
Task.cons(3,0,1),\
Task.cons(3,1,1))
p1 = Function('p1',IntSort(),Task)
p2 = Function('p2',IntSort(),Task)
order = And([Exists([x,y],Or(And(p1(x)==t1,p1(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
And(p1(x)==t1,p2(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
And(p2(x)==t1,p1(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
And(p2(x)==t1,p2(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True))))\
for t1 in tasks for t2 in tasks])
s.add(order)
如您所见，这确实是一个很大的公式，但我没有找到使其更小的方法...目的是确保任务的每个部分都井井有条，即使它们由不同的处理器处理（p1或 p2)
如果您能帮助我，请提前非常感谢（即使只是可以帮助我更改公式的提示也会很棒）
编辑：我只是单独测试了该约束并且它有效，它给出了奇怪的结果但仍然有效，但我仍然需要它与其他约束一起工作，所以如果你能帮助我优化它，欢迎你。