z3.Bool() 和 z3.FreshBool() 函数有什么区别？ 我在 python 上的 z3 中的代码在我使用 Bool() 时失败（求解器在不应该返回 unsat 时），但在我使用 FreshBool() 时工作正常（观察到所需的行为）。
我无法在此处提供代码的详细信息，因为它是我大学提供的课程中正在进行的作业的一部分。 尽管如此，如果这些信息还不够，我可以尝试在不相关的代码中重新创建，为您提供更好的示例来处理。 谢谢
【问题讨论】：
标签： syntax z3 z3py sat sat-solvers
如果您使用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() 等；旨在以完全相同的方式使用。
【讨论】：