什么是 Z3Py FreshBool() 函数？

Question

z3.Bool() 和 z3.FreshBool() 函数有什么区别？当我使用 Bool() 时，我在 python 上的 z3 中的代码失败（求解器 returns 在不应该的时候不满足），但是当我使用 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() vs FreshReal() 等；旨在以完全相同的方式使用。

什么是 Z3Py FreshBool() 函数？

What is Z3Py FreshBool() function?

syntax

z3

z3py

sat

sat-solvers