Z3: Does "qe" tactic preserve equivalence or only equisatisfiability?

Question

I'd like to use Z3's tactics to preprocess formulae with the requirement to preserve equivalence. Here, Leonardo de Moura stated that several tactics only produce equisatisfiable results.

In particluar, I'm using the "qe" tactic for quantifier elimination. Does somebody know whether the "qe" tactic guarantees the resulting formula to be equivalent to the original one?

Thank you!

Answer 1

There are three tactics for quantifier elimination:

• qe: preserves validity. It eliminates quantifiers from formulas producing equivalent formulas.
• qe-sat: checks satisfiability of quantified formulas. It does not produce equivalent subgoals.
• qe-lite: light-weight quantifier elimination. It preserves equivalence, but does not always eliminate quantifiers. It tries to eliminate quantifiers that are cheap to reduce.