fixing interpolation documentation

include/cvc5/c/cvc5.h

@@ -4833,7 +4833,10 @@ CVC5_EXPORT void cvc5_add_plugin(Cvc5* cvc5, Cvc5Plugin* plugin);
 /**
  * Get an interpolant.
  *
- * This determines a term @f$I@f$ such that @f$A \rightarrow I@f$ and
+ * Given that @f$A->B@f$ is valid,
+ * this function determines a term @f$I@f$ 
+ * over the shared variables of @f$A@f$ and @f$B$,
+ * 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`.
  *
@@ -4862,7 +4865,10 @@ CVC5_EXPORT Cvc5Term cvc5_get_interpolant(Cvc5* cvc5, Cvc5Term conj);
 /**
  * Get an interpolant
  *
- * This determines a term @f$I@f$, with respect to a given grammar, such that
+ * Given that @f$A->B@f$ is valid,
+ * this function determines a term @f$I@f$ 
+ * over the shared variables of @f$A@f$ and @f$B$, 
+ * with respect to a given grammar, 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`.

include/cvc5/cvc5.h

@@ -6405,8 +6405,10 @@ class CVC5_EXPORT Solver
   /**
    * Get an interpolant.
    *
-   * This determines a term @f$I@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
+   * 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. @f$A@f$ is the
    * current set of assertions and @f$B@f$ is the conjecture, given as `conj`.
    *
    * SMT-LIB:
@@ -6433,10 +6435,15 @@ class CVC5_EXPORT Solver
   /**
    * Get an interpolant.
    *
-   * This determines a term @f$I@f$, with respect to a given grammar, 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`.
+   *
+   *
+   * 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. 
+   * @f$I@f$ is constructed from the given grammar.
+   * @f$A@f$ is the
+   * current set of assertions and @f$B@f$ is the conjecture, given as `conj`.
    *
    * SMT-LIB:
    *

src/api/java/io/github/cvc5/Solver.java

@@ -3122,8 +3122,12 @@ public void pop(int nscopes) throws CVC5ApiException
    * Get an interpolant.
    *
    * <p>
-   * This determines a term {@code I} such that {@code A->I} and {@code I->B}
-   * are valid, if such a term exits. {@code A} is the current set of
+   * Given that {@code A->B} is valid,
+   * this function determines a term {@code I} 
+   * over the shared variables of {@code A} and
+   * {@code B},
+   * such that {@code A->I} and {@code I->B}
+   * are valid. {@code A} is the current set of
    * assertions and {@code B} is the conjecture, given as {@code conj}.
    * </p>
    *
@@ -3154,7 +3158,11 @@ public Term getInterpolant(Term conj)
    * Get an interpolant.
    *
    * <p>
-   * This determines a term {@code I}, with respect to a given grammar, such
+   * Given that {@code A->B} is valid,
+   * this function determines a term {@code I}, 
+   * over the shared variables of {@code A} and
+   * {@code B},
+   * with respect to a given grammar, such
    * that {@code A->I} and {@code I->B} are valid, if such a term exits.
    * {@code A} is the current set of assertions and {@code B} is the
    * conjecture, given as {@code conj}.

src/api/python/cvc5.pxi

@@ -4312,8 +4312,12 @@ cdef class Solver:
     def getInterpolant(self, Term conj, Grammar grammar=None):
         """
             Get an interpolant.
-
-            This determines a term :math:`I`, optionally with respect to a
+	    Assuming that :math:`A \\rightarrow B` is valid,
+	    this function
+            determines a term :math:`I`
+	    over the shared variables of 
+            :math`A` and :math`B`,
+	    optionally with respect to a
             a given grammar, such that :math:`A \\rightarrow I` and
             :math:`I \\rightarrow B` are valid, if such a term exits.
             :math:`A` is the current set of assertions and :math:`B` is the