在函数调用中one_op(unk_op, arg1, arg2)
, unk_op
是 Z3 表达式。然后,诸如此类的表达式op==1
and 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
as:
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]