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?