(Z3Py) 函数声明有什么限制吗? [英] (Z3Py) any limitations in functions declaring?
问题描述
函数声明有什么限制吗?
Is there any limitations in functions declaring?
比如这段代码返回unsat.
For example, this piece of code returning unsat.
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 如何解释声明的函数?它只是偶尔调用它还是一些隐藏的机器也在这里?
How Z3Py interpret declared function? Is it just calling it some times or some hidden machinery also here?
推荐答案
在函数调用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语句.
In the function call one_op(unk_op, arg1, arg2)
, unk_op
is a Z3 expression. Then, expressions such as op==1
and op==2
(in the definition of one_op
) are also Z3 symbolic expressions. Since op==1
is not the Python Boolean expression False
. The function one_op
will always return the Z3 expression arg1*arg2
. We can check that by executing print one_op(unk_op, arg1, arg2)
. Note that the if
statements in the definition of one_op
are Python statements.
我相信您的真正意图是返回包含条件表达式的 Z3 表达式.您可以通过将 one_op
定义为:
I believe your true intention is to return a Z3 expression that contains conditional expressions. You can accomplish that by defining 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 条件表达式.通过使用这个定义,我们可以找到一个令人满意的解决方案.这是完整的示例:
Now, the command If
builds a Z3 conditional expression. By using, this definition, we can find a satisfying solution. Here is the complete example:
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]
这篇关于(Z3Py) 函数声明有什么限制吗?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!