Does pull_nested_quantifiers option work with simplify in Z3?

Question

I would like to pull all nested quantifiers in a formula to the outermost level. I expected the following commands to work in Z3 but they don't:

(set-option :pull-nested-quantifiers true)
(simplify (exists ((x Int)) (and (>= x 0) 
                            (forall ((y Int)) (and (>= y 1) (> x y))))))

What is the purpose of :pull-nested-quantifiers? How can I pull nested quantifiers using SMT-LIB or Z3 API?

Answer 1

In Z3 3.x, the simplify command applies only general purpose local simplification steps. "Pull-nested-quantifiers" is a pre-processing step. It will be available as a tactic/strategy in future releases. Z3 3.2 already has many built-in strategies/tactics in the SMT 2.0 front-end. The next release will have a much bigger set of tactics. They will be available also in the API. If you need this feature for some project, just send me an email and I will make a non-official (beta) release for you.

Finally, we have this preprocessing step, because the model-based quantifier instantiation MBQI module works much better if universal quantifiers do not have nested (universal) quantifiers. Your example is ok, since Z3 will eliminate the existential and replace x with a fresh constant.