syntax - 什么是 Z3Py FreshBool() 函数？

Question

z3.Bool() 和 z3.FreshBool() 函数有什么区别？当我使用 Bool() 时，我在 python 上的 z3 中的代码失败（当求解器不应该返回 unsat 时），但是当我使用 FreshBool() 时工作​​正常（观察到所需的行为）。

我不能在这里提供代码的详细信息，因为它是我大学提供的课程中正在进行的作业的一部分。尽管如此，如果这些信息还不够，我可以尝试在不相关的代码中重新创建，为您提供更好的示例来处理。谢谢

Answer 1

如果您使用FreshBool()，那么 z3 将创建一个在系统其他地方不存在的新变量。当您使用Bool并为其命名时，如果在其他地方创建，它将是相同的变量。

也就是说，考虑：

from z3 import *

# These two are *different* variables even though they have the same name
a = FreshBool("a")
b = FreshBool("a")

s = Solver();

s.add(a != b)
print(s.check())

这将打印：

sat

因为变量不同。（因此在模型中可以有不同的值。）

但如果你尝试：

from z3 import *

# These two are the *same* variable, since they have the same name
a = Bool("a")
b = Bool("a")

s = Solver();

s.add(a != b)
print(s.check())

然后你会得到：

unsat

因为a和b是相同的变量，因为它们具有相同的名称。

大多数最终用户代码应该简单地使用Bool，因为这是通常的预期语义：您在创建它们时使用它们的名称引用不同的变量。但是在开发库时，您可能希望创建一个与系统中任何其他变量都不相同的临时变量。在这些情况下，您使用FreshBool. 请注意，在后一种情况下，您提供的字符串用作前缀。如果您print(get_model())在第一个程序的末尾添加，它将打印：

sat
[a!0 = True, a!1 = False]

显示内部创建的“新鲜”名称。

z3 也为其他类型提供了类似的功能，例如Int()vs FreshInt()，Real()vsFreshReal()等；旨在以完全相同的方式使用。