What is the difference between z3.Bool() and z3.FreshBool() functions? My code in z3 on python fails when I use Bool() (the solver returns unsat when it shouldn't), but works fine when I use FreshBool() (Desired behaviour is observed).
I cannot give out details of the code here, as it is part of an ongoing assignment in a course offered in my college. Even still, if this information isn't sufficient, I can try and recreate in an unrelated code, to provide you with a better sample to work on. Thanks
If you use FreshBool() then z3 will create a new variable that does not exist elsewhere in the system. When you use Bool and give it a name, then it will be the same variable if created elsewhere.
To wit, consider:
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())
This will print:
sat
since the variables are different. (And hence can have different values in the model.)
But if you try:
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())
Then you'll get:
unsat
because a and b are the same variable since they have the same name.
Most end-user code should simply use Bool, since this is the usual intended semantics: You refer to different variables with their names when you created them. But when developing libraries, you might want to create a temporary variable that is not the same as any other variable in the system. In these cases, you use FreshBool. Note that in this latter case the string you provide is used as a prefix. If you add print(get_model()) at the end of the first program, it'll print:
sat
[a!0 = True, a!1 = False]
showing the internally created "fresh" names.
z3 also provides similar functions for other types too, such as Int() vs FreshInt(), Real() vs FreshReal() etc.; intended to be used in exactly the same manner.