（Z3Py）聲明函數的任何限制？

Question

聲明函數是否有任何限制？

例如，這段代碼返回不飽和度。

from z3 import * 

def one_op (op, arg1, arg2): 
    if op==1: 
     return arg1*arg2 
    if op==2: 
     return arg1-arg2 
    if op==3: 
     return arg1+arg2 

    return arg1+arg2 # default 

s=Solver() 

arg1, arg2, result, unk_op=Ints ('arg1 arg2 result unk_op') 

s.add (unk_op>=1, unk_op<=3) 

s.add (arg1==1) 
s.add (arg2==2) 
s.add (result==3) 
s.add (one_op(unk_op, arg1, arg2)==result) 

print s.check() 

Z3Py如何解釋聲明的函數？它只是調用它一些時間或一些隱藏的機器也在這裏？

Answer 1

在函數調用one_op(unk_op, arg1, arg2)，unk_op是Z3表達。然後，諸如op==1和op==2（在one_op的定義中）等表達式也是Z3符號表達式。由於op==1不是Python布爾表達式False。函數one_op將始終返回Z3表達式arg1*arg2。我們可以通過執行print one_op(unk_op, arg1, arg2)來檢查。請注意，one_op定義中的if語句是Python語句。

我相信你的真實意圖是返回一個包含條件表達式Z3表達。您可以實現通過定義one_op爲：現在

def one_op (op, arg1, arg2): 
    return If(op==1, 
       arg1*arg2, 
       If(op==2, 
        arg1-arg2, 
        If(op==3, 
        arg1+arg2, 
        arg1+arg2))) 

，命令If建立一個Z3條件表達式。通過使用這個定義，我們可以找到令人滿意的解決方案。下面是完整的例子：

from z3 import * 

def one_op (op, arg1, arg2): 
    return If(op==1, 
       arg1*arg2, 
       If(op==2, 
        arg1-arg2, 
        If(op==3, 
        arg1+arg2, 
        arg1+arg2))) 

s=Solver() 

arg1, arg2, result, unk_op=Ints ('arg1 arg2 result unk_op') 

s.add (unk_op>=1, unk_op<=3) 
s.add (arg1==1) 
s.add (arg2==2) 
s.add (result==3) 
s.add (one_op(unk_op, arg1, arg2)==result) 

print s.check() 
print s.model() 

結果是：

sat 
[unk_op = 3, result = 3, arg2 = 2, arg1 = 1]