是否有职能宣布任何限制？
例如，这一段代码返回不饱和度。
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译作宣称的功能？ 难道仅仅是调用它有时还是一些隐藏的机器也在这里？
在函数调用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) 需要注意的是if语句中的定义one_op是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]
