Quantifiers and Templates (QBF Formula)

Question

I am trying to encode QBF in smt-lib 2 syntax for z3. Running z3 leads to a warning

ATTENTION: the template for the quantifier could not be found (quantifier identifier: k! 14)

and the result of feasibility 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

 (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 assume I need to get the templates correctly? How to specify them for nested quantifiers? Simpler quantifier examples seem to work without drawing annotations.

Answer to What is the reason for the warning in Z3: "could not find a template for the quantifier (quantifier identifier: k! 18)" and the z3 manual did not help me very much, unfortunately.

Answer 1

This warning can be ignored. It simply informs you that the E-correspondence mechanism will not be able to process this quantitative formula.

E-compliance is effective only to show that the problem is unsatisfactory. Since your example is doable, E-matching will not be very useful. That is, Z3 will not be able to return sat with the E-matching mechanism. Model-based quantization instance (MBQI) is the only engine in Z3 that can show that problems containing quantifiers are doable.

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

The MBQI mechanism ensures that Z3 is a decision procedure for many fragments (see http://rise4fun.com/Z3/tutorial/guide ). However, it is very expensive overall and should be turned off when quick and rough answers are enough. In this case, unknown can be read as probably sat . Validation tools, such as VCC , disable the MBQI module because it is unable to accept the formula they create. That is, the formulas created by VCC do not enter into any of the fragments that can be determined by the MBQI mechanism. We say that a fragment can be defined by Z3 when sat or unsat returns for any formula in Z3 (i.e., it will not return unknown ). Of course, this statement assumes that we have an unlimited amount of resources. That is, Z3 can also fail (i.e., return unknown ) for resolvable 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 was fixed, and this did not affect your problem. If you need, I can give you a preliminary version of Z3 4.0, which contains a bug fix.