I have created a list of boolean variables like below:
lk=[Bool("a_0"), Bool("a_1"), Bool("a_2")]
I would like to initialize all these boolean variables to False.
If I write
for i in lk: i=False
It does not set variables a_0, a_1, a_2 to False.
How can I assign True or False values to variables declared in List in Z3Py? Help in this regard is highly appreciated.
The proper way to do this would be:
from z3 import *
lk = [Bool("a_0"), Bool("a_1"), Bool("a_2")]
s = Solver()
for i in lk:
s.add(i == False)
print(s.check())
print(s.model())
Note that we directly tell the solver that you want these variables to be set to False via the s.add calls. When I run this I get:
sat
[a_0 = False, a_1 = False, a_2 = False]
However, I suspect your actual intention is to "initialize" these variables, and later on change their value. This is not possible in z3py; you should not think of the values a_0, a_1, etc., as mutable variables like you'd have in regular Python: z3py is a "functional programming" environment, i.e., you cannot mutate declared variables. (Of course, you can assert constraints about them.)
If your intention is to model a programming language, where variables get declared, initialized, and mutated; you first have to convert to the so called SSA (static single assignment) form, see: https://en.wikipedia.org/wiki/Static_single_assignment_form
There are other questions on stack-overflow that deal with similar issues. See this one, for instance: Z3py: Add value to computed result and make another check