Quantifiers and patterns (QBF formula)

Question

I'm trying to encode a QBF in smt-lib 2 syntax for z3. Running z3 results in a warning

WARNING: failed to find a pattern for quantifier (quantifier id: k!14)

and the satisfiability result is "unknown".

The code is as follows:

(declare-fun R (Bool Bool Bool Bool) Bool)
(assert
  (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool))
      (forall ((x1 Bool))
        (R x1 x2 x3 y)
      )
    )
  )
)
(check-sat)

I got rid of the warning by rewriting the code to

(set-option :auto-config false)
(set-option :mbqi false)
(declare-fun R (Bool Bool Bool Bool) Bool)
(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(declare-fun y () Bool)
(assert
  (forall ((x2 Bool) (x3 Bool)) 
  (!
    (exists ((y Bool))
    (!
      (forall ((x1 Bool))
      (!
        (R x1 x2 x3 y)
      :pattern((R x1 x2 x3 y)))
      )
    :pattern((R x1 x2 x3 y)))
    )
  :pattern((R x1 x2 x3 y)))
  )
)
(check-sat)

The result for the sat-query, however, remains "unknown".

I'm guessing that I need to get the patterns right? How do I specify them for nested quantifiers? Simpler examples with quantifiers seem to work without pattern annotation, though.

The answer to What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) " and the z3 guide didn't help me too much, unfortunately.

Answer 1

This warning message can be ignored. It is just informing you that the E-matching engine will not be able to process this quantified formula.

E-matching is only effective for showing that a problem is unsatisfiable. Since your example is satisfiable, E-matching will not be very useful. That is, Z3 will not be able to return sat using the E-matching engine. Model based quantifier instantiation (MBQI) is the only engine in Z3 that is capable of showing that problems containing quantifiers are satisfiable.

Using the default configuration, Z3 will return sat for your example. It returns unknown because you disabled the MBQI module.

The MBQI engine guarantees that Z3 is a decision procedure for many fragments (see http://rise4fun.com/Z3/tutorial/guide). However, it is very expensive in general, and should be disabled when quick and approximated answers are sufficient. In this case, unknown may be read as probably sat. Verification tools such as VCC disable MBQI module since it is incapable of deciding formulas produced by them. That is, the formulas produced by VCC are not in any of the fragments that can be decided by the MBQI engine. We say a fragment can be decided by Z3 when for any formula in the fragment Z3 will return sat or unsat (i.e., it does not return unknown). Of course, this claim assumes we have a unlimited amount of resources. That is, Z3 may also fail (i.e., return unknown) for decidable fragments when it runs out of memory, or a timeout was specified by the user.

Finally, Z3 3.2 has a bug in the MBQI engine. The bug has been fixed, and it does not affect your problem. If you need I can give you a pre-release version of Z3 4.0 which contains the bug fix.