1

Probably a basic question related to Z3: i am trying to get all solutions of a boolean expression, e.g. for a OR b, i want to get {(true, true),(false,true),(true,false)}

Based on other responses found, e.g. Z3: finding all satisfying models, i have the following code:

a = Bool('a')
b = Bool('b')

f1=Or(a,b)
s=Solver()
s.add(f1)

while s.check() == sat:
  print s
  s.add(Not(And(a == s.model()[a], b == s.model()[b])))

The issue is that it enters an infinite loop as at the second iteration: the constraint a == s.model()[a] is evaluated to false b/c s.model()[a] does not exist anymore.

Can someone tell what i am doing wrong?

f1f2
  • 23
  • 3

1 Answers1

2

I would advice you to try writing your loop like this instead:

from z3 import *

a = Bool('a')
b = Bool('b')

f1 = Or(a,b)
s = Solver()
s.add(f1)

while s.check() == sat:

    m = s.model()

    v_a = m.eval(a, model_completion=True)
    v_b = m.eval(b, model_completion=True)

    print("Model:")
    print("a := " + str(v_a))
    print("b := " + str(v_b))

    bc = Or(a != v_a, b != v_b)
    s.add(bc)

The output is:

Model:
a := True
b := False
Model:
a := False
b := True
Model:
a := True
b := True

The argument model_completion=True is necessary because otherwise m.eval(x) behaves like the identity relation for any x Boolean variable with a don't care value in the current model m and it returns x as a result instead of True/False. (See related Q/A)

NOTE: since z3 kindly marks don't care Boolean variables, an alternative option would be to write your own model generator that auto-completes any partial model. This would reduce the number of calls to s.check(). The performance impact of this implementation is hard to gauge, but it might be slightly faster.

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
  • Thanks Patrick for your quick reply - The output i get from your script is ```[a = True, b = False] [b = True]``` - The infinite loop is indeed fixed, but how can i deduce the set of solutions? – f1f2 Mar 26 '20 at 14:34
  • Instead of printing in the loop, simply put the values a and b as a pair in an accumulated list and return it at the end. – alias Mar 26 '20 at 14:45
  • forgive my ignorance, but how does it solve the issue? The loop will still iterate only twice while i am expecting it to iterate three times. Or should i understand that when only ```[b = True]``` is returned, this means that ```a``` can take any value? – f1f2 Mar 26 '20 at 14:58
  • @f1f2 the issue is that the model value of `a` is equal to `a` at the second iteration, this is likely because the value of `a` is a `don't care` in the second model. I've to think a couple minutes how to fix the script :) – Patrick Trentin Mar 26 '20 at 15:47
  • Patrick's solution works great. But to add to my comment, when you do an `eval`, you explicitly get a value, so you avoid the "completion" problem. – alias Mar 26 '20 at 17:23
  • @alias without `model_completion=True`, not necessarily.. `m.eval(a)` yields `a` at the second iteration – Patrick Trentin Mar 26 '20 at 17:44
  • On second thought, I guess the fact that `eval` takes `model_completion` as a parameter is good indication that they have anticipated this problem. So yeah, always pass `model_completion=True` to your calls to `eval`. Good advice. – alias Mar 26 '20 at 18:30
  • thank you both, your answers exceeded my expectations :) – f1f2 Mar 26 '20 at 19:05
  • @Patrick, i think the sentence "...z3 returns the identity for any don't care Boolean variables." in the accepted answer should have a negation: by default z3 does not return the identity of _don't_ _care_ variables. – f1f2 Mar 27 '20 at 08:26
  • @f1f2 what I meant to say is that `m.eval(a)` for `a` being a *don't care* returns `a`, that is, `eval` behaves like the identity relation for *don't care* Boolean variables. – Patrick Trentin Mar 27 '20 at 10:09