api: Add note to Solver::mkDatatypeSorts. (#7799)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e38030abe719bdb1b1c236fb381aa82e26fdda3f..e3f64349fc593519de8a92b7dbae4b03744f1b8d 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -436,9 +436,10 @@ class CVC5_EXPORT Sort
 
   /**
    * Is this a parametric datatype sort? A parametric datatype sort is either
-   * one that is returned by a call to Solver::mkDatatypeSort() or Solver::mkDatatypeSorts() for a
-   * parametric datatype, or an instantiated datatype sort returned by
-   * Sort::instantiate() for parametric datatype sort `s`.
+   * one that is returned by a call to Solver::mkDatatypeSort() or
+   * Solver::mkDatatypeSorts() for a parametric datatype, or an instantiated
+   * datatype sort returned by Sort::instantiate() for parametric datatype
+   * sort `s`.
    * @return true if the sort is a parametric datatype sort
    */
   bool isParametricDatatype() const;
@@ -2588,6 +2589,8 @@ class CVC5_EXPORT Grammar
    * with bound variables via purifySygusGTerm, and binding these variables
    * via a lambda.
    *
+   * @note Create unresolved sorts with Solver::mkUninterpretedSort().
+   *
    * @param dt the non-terminal's datatype to which a constructor is added
    * @param term the sygus operator of the constructor
    * @param ntsToUnres mapping from non-terminals to their unresolved sorts
@@ -3151,6 +3154,8 @@ class CVC5_EXPORT Solver
    * When constructing datatypes, unresolved sorts are replaced by the datatype
    * sort constructed for the datatype declaration it is associated with.
    *
+   * @note Create unresolved sorts with Solver::mkUninterpretedSort().
+   *
    * @param dtypedecls the datatype declarations from which the sort is created
    * @param unresolvedSorts the list of unresolved sorts
    * @return the datatype sorts