python - 添加 z3 约束，使 z3 变量的值等于某个函数的返回值

Question

我有一个Python函数，它接受一个实数并返回一个字符串，例如

def fun(x):
    if x == 0.5:
        return "Hello"
    else:
        return "Bye"

我启动 z3 求解器:

from z3 import *

r = Real('r')
s = Solver()

现在我想告诉求解器 find a value of r, such that fun(r) returns "Hello" 。我面临以下问题:

1. 如果r = Real('r') ，那么我就无法调用 fun(r) ，因为r是一个 z3 变量
2. 我不能说s.add(StringVal("Hello") == StringVal(fun(r)))作为约束，因为 1) r是一个 z3 变量，2) r 的解释目前尚不清楚。因此，我没有可以从中提取值并将其传递给 fun 的模型。 .

可以实现我想要的吗？

Answer 1

在 z3 中没有现成的方法可以做到这一点，除非您愿意修改 fun 的定义以便 z3 可以理解它。像这样:

from z3 import *

def fun(x):
    return If(x == 0.5, StringVal("Hello"), StringVal("Bye"))

r = Real('r')
s = Solver()

s.add(fun(r) == StringVal("Hello"))
print(s.check())
print(s.model())

打印:

sat
[r = 1/2]

因此，我们更改了函数 fun 以使用与您想要编写的内容相对应的 z3 习惯用法。几点:

• 显然，并非每个 Python 结构都可以轻松地以这种方式进行翻译。虽然您可以表达大多数构造，但当您处理更复杂的函数时，手动转换的复杂性会变得更高。

• 据我所知，没有自动方法可以为您完成此翻译。不过，看看这个blog post有关如何通过反汇编程序执行此操作的一些想法。

• PyExZ3是一个现已不复存在的 Python 符号模拟器，使用 z3 作为后端求解器。虽然该项目不再活跃，但您也许能够恢复源代码或从中获得一些想法。

• 您已使用 Real 对参数 x 进行建模。 Z3 的 Real 值是真正的数学实数。 (严格来说，它们是代数实数，但这不是现在的重点。)然而，Python 没有这些；相反，它使用 double float 。但幸运的是，z3 可以理解 float ，因此要获得更真实的编码，请使用 Float64 排序。请参阅here了解详情。