（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]