Customize LIA quantifier elimination in Z3

Question

I'm doing quantifier elimination on LIA using F# and Z3 3.2 API.

Z3 used to have QUANT_ARITH configuration which indicates the use of Cooper's method or the Omega test for LIA quantifier elimination. But that option was replaced by ELIM_QUANTIFIERS in Z3 2.6 (see Z3 release notes).

I want to ask internally how Z3 3.2 knows which method to use for quantifier elimination? Can users affect the choice of method like QUANT_ARITH before?

Furthermore, with the introduction of strategy specification language, will Z3 allow us to customize quantifier elimination by extending or combining these methods?

Answer 1

The quantifier elimination module was re-implemented. The new implementation should be faster and correct. The latest Z3 does not have a implementation of Cooper’s method or Omega test. You can find more details about the actual quantifier elimination procedure used in Z3 at: “Linear Quantifier Elimination as an Abstract Decision Procedure, Nikolaj Bjørner, IJCAR 2010”.

Regarding the strategy specification language, we will eventually expose tactics for performing quantifier elimination. We are currently working on this infrastructure, more news are coming soon.