3

函数声明有什么限制吗？

例如，这段代码返回 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 如何解释声明的函数？它只是偶尔调用它还是这里也有一些隐藏的机器？

4

1 回答 1

3

在函数调用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]
于 2012-08-10T16:36:34.027 回答