Function get_interpolant 

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

Get an interpolant.

Given that @f$A \rightarrow B@f$ is valid, this function determines a term @f$I@f$ over the shared variables of @f$A@f$ and @f$B@f$, such that @f$A \rightarrow I@f$ and @f$I \rightarrow B@f$ are valid, if such a term exits. @f$A@f$ is the current set of assertions and @f$B@f$ is the conjecture, given as conj.

SMT-LIB:

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

(get-interpolant <symbol> <conj>)

.. note:: In SMT-LIB, <symbol> assigns a symbol to the interpolant.

.. note:: Requires option :ref:produce-interpolants <lbl-option-produce-interpolants> to be set to a mode different from none. \endverbatim

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

@param cvc5 The solver instance. @param conj The conjecture term. @return The interpolant, if an interpolant exists, else the null term.