Obtaining models for problems with quantified boolean variables

I am using Z3 to check satisfiability in a logic with linear integer arithmetic, uninterpreted functions and quantifiers over boolean variables. 开发者_高级运维Z3 does not provide models for satisfiable problems, I suppose this is because of the quantifiers (or the logic that I have chosen: AUFLIA).

Is there a way to make Z3 give me models for such problems, except for instantiating all the boolean variables myself?

---

Z3 can, in principle, decide this fragment. I say "in principle" because the complexity of the decision problem for this fragment is very high. For example, it subsumes the Bernays–Schönfinkel fragment (aka EPR) which is NEXPTIME-complete. A list of the fragments that can be decided by Z3 can be found at: http://rise4fun.com/z3/tutorial/guide

We have to make sure that model-based quantifier instantiation (MBQI) is enabled in Z3. You can do that by using the command line option MBQI=true or the SMT2 command

(set-option :mbqi true)

Z3 also has a threshold on the number of iterations of MBQI steps. We can change the threshold by using the command line option MBQI_MAX_ITERATIONS=<value> or the command

(set-option :mbqi-max-iterations 1000000)

For each MBQI step, we can ask Z3 to display which quantifiers were not satisfied by the current candidate model. Option MBQI_TRACE=true

That being said, I recently fixed a bug (crash) exposed by the SMT2 script you sent me. The fix will be available in Z3 3.2.