Search code examples
z3z3py

Basic error using solver in Z3-Python: it is returning [] as a model

Maybe I have slept bad today, but I am really struggling with this simple query to Z3-Python:

from z3 import *

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

sss = Solver()
sss.add(Exists([a,b], True))

print(sss.check())
print(sss.model())

The check prints out sat, but the model is []. However, it should be printing some (anyone) concrete assignment, such as a=True, b=True.

The same is happening if I change the formula to, say: sss.add(Exists([a,b], Not(And(a,b)))). Also tested sss.add(True). Thus, I am missing something really basic, so sorry for the basic nature of this question.

Other codes are working normally (even with optimizers instead of solvers), so it is not a problem of my environment (Collab)

Any help?

Solution

  • Note that there's a big difference between:

    a = Bool('a')
b = Bool('b')
sss.add(Exists([a, b], True))

    and

    a = Bool('a')
b = Bool('b')
sss.add(True)   # redundant, but to illustrate

    In the first case, you're checking if the statement Exists a. Exists b. True is satisfiable; which trivially is; but there is no model to display: The variables a and b are inside quantification; and they don't play any role in model construction.

    In the second case, a and b are part of the model, and hence will be displayed.

    What's confusing is why do you need to declare the a and b in the first case. That is, why can't we just say:

    sss.add(Exists([a, b], True))

    without any a or b in the environment? After all, they are irrelevant as far as the problem is concerned. This is merely a peculiarity of the Python API; there's really no good reason other than this is how it is implemented.

    You can see the generated SMTLib by adding a statement of the form:

    print(sss.sexpr())

    and if you do that for the above segments, you'll see the first one doesn't even declare the variables at all.

    So, long story short, the formula exists a, b. True has no "model" variables and thus there's nothing to display. The only reason you declare them in z3py is because of an implementation trick that they use (so they can figure out the type of the variable), nothing more than that.

    Here're some specific comments about your questions:

    1. An SMT solver will only construct model-values for top-level declared variables. If you create "local" variables via exists/forall, they are not going to be displayed in models constructed. Note that you could have two totally separate assertions that talk about the "same" existentially quantified variable: It wouldn't even have a way of referring to that item. Rule-of-thumb: If you want to see the value in a model, it has to be declared at the top-level.

    2. Yes, this is the reason for the trick. So they can figure out what type those variables are. (And other bookkeeping.) There's just no syntax afforded by z3py to let you say something like Exists([Int(a), Int(b)], True) or some such. Note that this doesn't mean something like this cannot be implemented. They just didn't. (And is probably not worth it.)

    3. No you understood correctly. The reason you get [] is because there are absolutely no constraints on those a and b, and z3's model constructor will not assign any values because they are irrelevant. You can recover their values via model_completion parameter. But the best way to experiment with this is to add some extra constraints at the top level. (It might be easier to play around if you make a and b Ints. At the top level, assert that a = 5, b = 12. At the "existential" level assert something else. You'll see that your model will only satisfy the top-level constraints. Interestingly, if you assert something that's unsatisfiable in your existential query, the whole thing will become unsat; which is another sign of how they are treated.

    4. I said trivially true because your formula is Exists a. Exists b. True. There're no constraints, so any assignment to a and b satisfy it. It's trivial in this sense. (And all SMTLib logics work over non-empty domains, so you can always assign values freely.)

    5. Quantified variables can always be alpha-renamed without changing the semantics. So, whenever there's collision between quantified names and top-level names, imagine renaming them to be unique. I think you'll be able to answer your own question if you think of it this way.

    Extended discussions over comments is really not productive. Feel free to ask new questions if anything isn't clear.