z3z3pyquantifierssatisfiability

What does a model mean in a universally quantified formula? Is it a function?


Consider these two formulae:

Note that we cannot find “models” for the sat formula, e.g., using Z3 it outputs Z3Exception: model is not available for the following code:

phi = ForAll([x],Exists([y], lit))

s_def = Solver()
s_def.add(phi)
print(s_def.model())

Also, quantifier elimination does not output an elimination, but a satisfiability result [[]] (i.e., True):

x, y = Reals('x, y')

t = Tactic("qe")

lit = (y>x)

ae = Goal()
ae.add(ForAll([x],Exists([y], lit)))
ae_qe = t(ae)

print(ae_qe)

I think this happens because the value of y fully depends on x (e.g., if x is 5 then y can be 6). Thus, I have some questions:


Solution

  • You get a model-not-available, because you didn't call check. A model is only available after a call to check. Try this:

    from z3 import *
    
    x, y = Ints('x y')
    
    phi = ForAll([x], Exists([y], y > x))
    
    s = Solver()
    s.add(phi)
    print(s.check())
    print(s.model())
    

    This prints:

    sat
    []
    

    Now, you're correct that you won't get a meaningful/helpful model when you have a universal-quantifier; because the model will depend on the choice of x in each case. (You only get values for top-level existentials.) This is why the model is printed as the empty-list.

    Side Note In certain cases, you can use the skolemization trick (https://en.wikipedia.org/wiki/Skolem_normal_form) to get rid of the nested existential and get a mapping function, but this doesn't always work with SMT solvers as they can only build "finite" skolem functions. (For your example, there isn't such a finite function; i.e., a function that can be written as a case-analysis on the inputs, or an if-then-else chain.) For your specific questions:

    from z3 import *
    
    x = Int('x')
    
    skolem = Function('skolem', IntSort(), IntSort())
    phi = ForAll([x], skolem(x) > x)
    
    s = Solver()
    s.add(phi)
    print(s)
    print(s.check())
    print(s.model())
    

    The above never terminates, unfortunately. This sort of problem is simply too complicated for the push-button approach of SMT solving.