Что такое функция Z3Py FreshBool()?

Если вы используете 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() против FreshInt(), Real() против FreshReal() и т. д.; предназначены для использования точно таким же образом.