如何在 Z3py 函数中有超过 255 个参数？

Question

我想问一下，Z3 Python函数中如何有超过255个参数

    h1, h2 = Consts('h1 h2', S)
     def fun(h1 , h2):
          return Or(
 And( h1 == cl_4712, h2 == me_1935),
 And( h1 == cl_1871, h2 == me_1935),
 And( h1 == cl_4712, h2 == me_1935),
                   .
                   .
                   .
  And( h1 == cl_1871, h2 == me_6745)
                )

Answer 1

func(arg1, arg2, arg3)

完全等价于

args = (arg1, arg2, arg3)
func(*args)

所以将参数作为单个可迭代对象提供：

Or(*(And(...),...))

或者更清楚：

conditions = (And(...), ...)
Or(*conditions)

或者你可以只提供一个生成器来产生你的条件：

def AndCond(a, b):
    for ....:
        yield And(...)

Or(*AndCond(v1, v2))

我可能会这样写你的代码：

h1, h2 = Consts('h1 h2', S)
def fun(h1 , h2):
    # possibly this should be a set() or frozenset()
    # since logically every pair should be unique?
    h1_h2_and_conds = [
        (cl_4712, me_1935),
        (cl_1871, me_1935),
        (cl_1871, me_6745),
        # ...
    ]
    and_conds = (And(h1==a, h2==b) for a,b in h1_h2_and_conds)
    return Or(*and_conds)