why z3 solver give bool variable "none", how to get rid of it?

Question

I am new to Z3py. I am trying to list all satisfied solutions to a bool formula (or to get the truth table which generate only True).

My code is here, inspired from another answer finding all satisfying models:

from z3 import *
A1, B1, B2, C1, C2, E1, E2, F4 = Bools('A1 B1 B2 C1 C2 E1 E2 F4')
s = Solver()
s.add(simplify(Or(And(A1, Or(C1, C2), Or(B1, B2), E2, F4), 
    And(A1, C2, Or(B1, B2), E1))))

while s.check() == sat:
  print(s.model())
  s.add(Or(A1 != s.model()[A1],
    B1 != s.model()[B1],
    B2 != s.model()[B2],
    C1 != s.model()[C1],
    C2 != s.model()[C2],
    E1 != s.model()[E1],
    E2 != s.model()[E2],
    F4 != s.model()[F4])) 

but I got results like this:

True,True,None,None,True,True,False,None

True,True,None,None,True,True,False,None

True,True,None,None,True,True,False,None

True,True,None,None,True,True,False,None
...

as you can see, they have duplicated results, and there are "None" in it, why is this happening? Isn't it true that Bool variable has only "true" or "false"? Why there are duplicated models in it? Thank you very much.

Answer 1

As Cristoph mentioned, if you are interested in complete enumeration, you want to make sure the "don't-care" assignments are always fixed at a particular value. To address the issue, you can use the following code:

from z3 import *
A1, B1, B2, C1, C2, E1, E2, F4 = Bools('A1 B1 B2 C1 C2 E1 E2 F4')
s = Solver()
s.add(simplify(Or(And(A1, Or(C1, C2), Or(B1, B2), E2, F4),.
    And(A1, C2, Or(B1, B2), E1))))

vars = [A1, B1, B2, C1, C2, E1, E2, F4]
while s.check() == sat:
    m = s.model()
    for v in vars:
      print("%s = %5s" % (v, m.evaluate(v, model_completion = True))),
    print
    s.add(Or([p != v for p, v in [(v, m.evaluate(v, model_completion = True)) for v in vars]]))

When run, this prints:

A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 = False B2 =  True C1 =  True C2 = False E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 = False E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 = False B2 =  True C1 =  True C2 = False E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 = False E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 = False E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 = False E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 =  True E2 = False F4 =  True

Which doesn't have any Nones or duplications.