添加 z3 约束，使得 z3 变量的值等于某个函数的返回值答案

【问题标题】：Add a z3 constraint, such that the value of a z3 variable equals to the return value of some function添加 z3 约束，使得 z3 变量的值等于某个函数的返回值
【发布时间】：2022-01-16 08:48:33
【问题描述】：

我有一个 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"。我面临以下问题：

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

有没有可能实现我想要的？

【问题讨论】：

标签： python z3 z3py

【解决方案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 没有这些。相反，它使用双精度浮点数。但幸运的是，z3 可以理解浮点数，因此对于更真实的编码，请使用 Float64 排序。详情请见here。

【讨论】：

感谢您提供出色的答案和链接！我将问题标记为已解决，因为它解决了问题 :) 但是，在我的本地情况下，情况有点复杂，因为 Python 函数的输入被进一步传递给 JS 函数，该函数完成了工作。如果我尝试将所有这些都翻译成 z3 将会非常复杂 :) 但是，我学到了一些新东西 :) 谢谢！
确实这将非常棘手，因为您还必须找到一种方法来“建模” JS 所做的一切。一般来说，这一切都不是一件容易的事，但我认为如果你只需要担心几个这样的功能，这是完全可行的。不幸的是，这些都不是自动化的，所以你必须手动完成；至少目前是这样。