Function get_quantifier_elimination 

pub unsafe extern "C" fn get_quantifier_elimination(
    cvc5: *mut Solver,
    q: Term,
) -> Term

Do quantifier elimination.

SMT-LIB:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(get-qe <q>)

\endverbatim

@note Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.

@warning This function is experimental and may change in future versions.

@param cvc5 The solver instance. @param q A quantified formula of the form @f$Q\bar{x}_1… Q\bar{x}_n. P( x_1…x_i, y_1…y_j)@f$ where @f$Q\bar{x}@f$ is a set of quantified variables of the form @f$Q x_1…x_k@f$ and @f$P( x_1…x_i, y_1…y_j )@f$ is a quantifier-free formula @return A formula @f$\phi@f$ such that, given the current set of formulas @f$A@f$ asserted to this solver: - @f$(A \wedge q)@f$ and @f$(A \wedge \phi)@f$ are equivalent - @f$\phi@f$ is quantifier-free formula containing only free variables in @f$y_1…y_n@f$.