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
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.