如何在Z3py函數中使用超過255個參數？

Question

我想懇請，如何有超過255個參數的Z3 Python函數

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)