CODEWITHSUNDEEP
z3boolean-logicz3pyboolean-operationstruthtable
QianruZhou
QianruZhou

Reputation: 41

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

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.

Upvotes: 0

Views: 461

Answers (2)

alias
alias

Reputation: 30525

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.

Upvotes: 0

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

None is a don't-care; it means that you are free to choose either True or False and both are valid models. You can ask Z3 to fill in these values by enabling model completion, for example as it's done in How to model in Z3py

Upvotes: 1

Related Questions