0

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

1 に答える 1

1 
func(arg1, arg2, arg3)

とまったく同等です

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

したがって、引数を単一の iterable として指定します。

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)
于 2013-03-27T16:20:45.940 に答える