From: Aina Niemetz Date: Tue, 14 Dec 2021 02:44:01 +0000 (-0800) Subject: api: Add note to Solver::mkDatatypeSorts. (#7799) X-Git-Tag: cvc5-1.0.0~672 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a380d12d651a8fc54fefcaedab12bce1fd5235d;p=cvc5.git api: Add note to Solver::mkDatatypeSorts. (#7799) --- diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index e38030abe..e3f64349f 100644 --- 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