Does quantifier elimination preserve equi-satisfiability or equivalence? And in Z3?

Does quantifier elimination (QE) preserve equi-satisfiability or equivalence?

I always thought QE preserves equi-satisfiability (and not equivalence) but in the book [Bradley, Manna], they say both Cooper's method (for Presburger arithmetic) and Ferrante-Rackoff (for rational arithmetic), which are QE methods, preserve equivalence.

So, does QE always preserve equivalence? Are there QE methods that preserve equi-satisfiability and others that preserve equivalence? In such case, any example of both types?

I am confused, because [ETHZ][Wiki] say that Skolemization, with which "existential quantifiers can be eliminated" preserves equi-satisfiability but not necessarily equivalence. What I think is that, even if eliminating existential quantifiers sounds to me like a QE method, Skolemization is not a QE method itself.

As for Z3 (and other solvers), I cannot find any information about whether the techniques it uses for QE preserves equivalence or equi-satisfiability.

Reference

• [Bradley, Manna] The Calculus of Computation,
  https://community.wvu.edu/~krsubramani/courses/backupcourses/dm2Spr2013/coursetext/CalcofComp.pdf

• [ETHZ]
  https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Courses/SS2017/Program%20Verification/04-Quantifiers.pdf

• [Wiki] https://en.wikipedia.org/wiki/Skolem_normal_form

You answered your own question. By definition, a QE algorithm produces an equivalent formula. (Not just equi-satisfiable.)

Skolemization only allows existentials to be removed from a formula, and it produces equi-satisfiable formulas, not equivalent formulas. (But in practice of SAT/SMT solving, this hardly matters since all we care about is satisfiability.)

Regarding specific implementations in z3: Again, by definition, if they implement a QE procedure, then that transformation preserves equivalence.

Note that skolemization is a general technique that applies to all-theories. But quantifier-elimination is theory specific: Not all theories admit QE, nor they are necessarily cheap. Skolemization, on the other hand, applies universally to all quantified formulae, it is relatively cheap, but it only preserves equi-satisfiability, and does not get rid of universals.