From 7c27981f65d554ef24a513d8d2bb96cb5139e1db Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 10 Dec 2021 15:36:27 -0800 Subject: [PATCH] api: Use 'note' constructs for API documentation. (#7794) This uses '@note' for notes in the C++ API documentation, '.. note::' for Python, and '@apiNote' for Java. --- docs/api/java/CMakeLists.txt | 1 + src/api/cpp/cvc5.h | 115 +++++++++++--------- src/api/java/io/github/cvc5/api/Solver.java | 18 +-- src/api/java/io/github/cvc5/api/Sort.java | 2 +- src/api/java/io/github/cvc5/api/Term.java | 15 +-- src/api/python/cvc5.pxi | 79 ++++++++------ 6 files changed, 123 insertions(+), 107 deletions(-) diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 8a728407f..2fcf74767 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -31,6 +31,7 @@ if(BUILD_BINDINGS_JAVA) -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/:${CMAKE_BINARY_DIR}/src/api/java/ -d ${JAVADOC_OUTPUT_DIR} -cp ${CVC5_JAR_FILE} + -tag "apiNote:a:Note:" -notimestamp COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's///' {} "\;" COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 9899e346e..b65db16a3 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -275,8 +275,9 @@ class CVC5_EXPORT Result /** * The interal result wrapped by this result. - * Note: This is a shared_ptr rather than a unique_ptr since cvc5::Result is - * not ref counted. + * + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` + * since ``cvc5::Result`` is not ref counted. */ std::shared_ptr d_result; }; @@ -544,7 +545,7 @@ class CVC5_EXPORT Sort * or return value for any term that is function-like. * This is mainly to avoid higher order. * - * Note that arrays are explicitly not considered function-like here. + * @note Arrays are explicitly not considered function-like here. * * @return true if this is a function-like sort */ @@ -751,7 +752,7 @@ class CVC5_EXPORT Sort * non-instantiated parametric datatype, this returns the parameter sorts of * the underlying datatype. If this sort is an instantiated parametric * datatype, then this returns the sort parameters that were used to - * construct the sort via ``Sort::instantiate``. + * construct the sort via Sort::instantiate(). * * @return the parameter sorts of a parametric datatype sort. */ @@ -808,9 +809,10 @@ class CVC5_EXPORT Sort /** * The internal type wrapped by this sort. - * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (cvc5::Type is already ref counted, so this - * could be a unique_ptr instead). + * + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to + * avoid overhead due to memory allocation (``cvc5::Type`` is already + * ref counted, so this could be a ``std::unique_ptr`` instead). */ std::shared_ptr d_type; }; @@ -957,9 +959,11 @@ class CVC5_EXPORT Op bool isNullHelper() const; /** - * Note: An indexed operator has a non-null internal node, d_node - * Note 2: We use a helper method to avoid having API functions call - * other API functions (we need to call this internally) + * @note An indexed operator has a non-null internal node (``d_node``). + * + * @note We use a helper method to avoid having API functions call other API + * functions (we need to call this internally). + * * @return true iff this Op is indexed */ bool isIndexedHelper() const; @@ -987,9 +991,10 @@ class CVC5_EXPORT Op /** * The internal node wrapped by this operator. - * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (cvc5::Node is already ref counted, so this - * could be a unique_ptr instead). + * + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to + * avoid overhead due to memory allocation (``cvc5::Node`` is already + * ref counted, so this could be a ``std::unique_ptr`` instead). */ std::shared_ptr d_node; }; @@ -1133,8 +1138,9 @@ class CVC5_EXPORT Term bool hasOp() const; /** + * @note This is safe to call when hasOp() returns true. + * * @return the Op used to create this term - * Note: This is safe to call when hasOp() returns true. */ Op getOp() const; @@ -1210,9 +1216,9 @@ class CVC5_EXPORT Term /** * Iterator for the children of a Term. - * Note: This treats uninterpreted functions as Term just like any other term - * for example, the term f(x, y) will have Kind APPLY_UF and three - * children: f, x, and y + * @note This treats uninterpreted functions as Term just like any other term + * for example, the term ``f(x, y)`` will have Kind ``APPLY_UF`` and + * three children: ``f``, ``x``, and ``y`` */ class CVC5_EXPORT const_iterator { @@ -1246,7 +1252,7 @@ class CVC5_EXPORT Term /** * Constructor * @param slv the associated solver object - * @param e a shared pointer to the node that we're iterating over + * @param e a ``std::shared pointer`` to the node that we're iterating over * @param p the position of the iterator (e.g. which child it's on) */ const_iterator(const Solver* slv, @@ -1369,9 +1375,9 @@ class CVC5_EXPORT Term */ bool isStringValue() const; /** - * Note: This method is not to be confused with toString() which returns - * the term in some string representation, whatever data it may hold. Asserts - * isStringValue(). + * Asserts isStringValue(). + * @note This method is not to be confused with toString(), which returns + * some string representation of the term, whatever data it may hold. * @return the string term as a native string value. */ std::wstring getStringValue() const; @@ -1399,9 +1405,8 @@ class CVC5_EXPORT Term */ std::pair getReal64Value() const; /** + * @note A term of kind PI is not considered to be a real value. * @return true if the term is a rational value. - * - * Note that a term of kind PI is not considered to be a real value. */ bool isRealValue() const; /** @@ -1506,8 +1511,8 @@ class CVC5_EXPORT Term * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see * also @ref Term::operator>(const Term&) const). * - * Note that a universe set term (kind SET_UNIVERSE) is not considered to be - * a set value. + * @note A universe set term (kind SET_UNIVERSE) is not considered to be + * a set value. */ bool isSetValue() const; /** @@ -1522,9 +1527,9 @@ class CVC5_EXPORT Term bool isSequenceValue() const; /** * Asserts isSequenceValue(). - * Note that it is usually necessary for sequences to call - * `Solver::simplify()` to turn a sequence that is constructed by, e.g., - * concatenation of unit sequences, into a sequence value. + * @note It is usually necessary for sequences to call `Solver::simplify()` + * to turn a sequence that is constructed by, e.g., concatenation of + * unit sequences, into a sequence value. * @return the representation of a sequence value as a vector of terms. */ std::vector getSequenceValue() const; @@ -1592,9 +1597,9 @@ class CVC5_EXPORT Term bool isCastedReal() const; /** * The internal node wrapped by this term. - * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (cvc5::Node is already ref counted, so this - * could be a unique_ptr instead). + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to + * avoid overhead due to memory allocation (``cvc5::Node`` is already + * ref counted, so this could be a ``std::unique_ptr`` instead). */ std::shared_ptr d_node; }; @@ -1749,8 +1754,8 @@ class CVC5_EXPORT DatatypeConstructorDecl /** * The internal (intermediate) datatype constructor wrapped by this * datatype constructor declaration. - * Note: This is a shared_ptr rather than a unique_ptr since - * cvc5::DTypeConstructor is not ref counted. + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` + * since ``cvc5::DTypeConstructor`` is not ref counted. */ std::shared_ptr d_ctor; }; @@ -1855,8 +1860,8 @@ class CVC5_EXPORT DatatypeDecl /** * The internal (intermediate) datatype wrapped by this datatype * declaration. - * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is - * not ref counted. + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` + * since ``cvc5::DType`` is not ref counted. */ std::shared_ptr d_dtype; }; @@ -1931,8 +1936,8 @@ class CVC5_EXPORT DatatypeSelector /** * The internal datatype selector wrapped by this datatype selector. - * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is - * not ref counted. + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` + * since ``cvc5::DType`` is not ref counted. */ std::shared_ptr d_stor; }; @@ -1981,9 +1986,9 @@ class CVC5_EXPORT DatatypeConstructor * DatatypeConstructor is the one corresponding to nil, and retSort is * (List Int). * - * Furthermore note that the returned constructor term t is an operator, - * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above - * (nullary) application of nil. + * @note the returned constructor term ``t`` is an operator, while + * ``Solver::mkTerm(APPLY_CONSTRUCTOR, t)`` is used to construct the + * above (nullary) application of nil. * * @param retSort the desired return sort of the constructor * @return the constructor term @@ -2176,8 +2181,8 @@ class CVC5_EXPORT DatatypeConstructor /** * The internal datatype constructor wrapped by this datatype constructor. - * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is - * not ref counted. + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` + * since ``cvc5::DType`` is not ref counted. */ std::shared_ptr d_ctor; }; @@ -2433,8 +2438,8 @@ class CVC5_EXPORT Datatype /** * The internal datatype wrapped by this datatype. - * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is - * not ref counted. + * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` + * since ``cvc5::DType`` is not ref counted. */ std::shared_ptr d_dtype; }; @@ -3340,12 +3345,13 @@ class CVC5_EXPORT Solver /* .................................................................... */ /** - * Create an operator for a builtin Kind + * Create an operator for a builtin Kind. + * * The Kind may not be the Kind for an indexed operator - * (e.g. BITVECTOR_EXTRACT) - * Note: in this case, the Op simply wraps the Kind. - * The Kind can be used in mkTerm directly without - * creating an op first. + * (e.g. BITVECTOR_EXTRACT). + * + * @note In this case, the ``Op`` simply wraps the ``Kind``. The Kind can be + * used in ``Solver::mkTerm`` directly without creating an ``Op`` first. * @param kind the kind to wrap */ Op mkOp(Kind kind) const; @@ -3551,7 +3557,7 @@ class CVC5_EXPORT Solver /** * Create a bit-vector constant of given size and value. * - * Note: The given value must fit into a bit-vector of the given size. + * @note The given value must fit into a bit-vector of the given size. * * @param size the bit-width of the bit-vector sort * @param val the value of the constant @@ -3563,7 +3569,7 @@ class CVC5_EXPORT Solver * Create a bit-vector constant of a given bit-width from a given string of * base 2, 10 or 16. * - * Note: The given value must fit into a bit-vector of the given size. + * @note The given value must fit into a bit-vector of the given size. * * @param size the bit-width of the constant * @param s the string representation of the constant @@ -4328,9 +4334,10 @@ class CVC5_EXPORT Solver void setOption(const std::string& option, const std::string& value) const; /** - * If needed, convert this term to a given sort. Note that the sort of the - * term must be convertible into the target sort. Currently only Int to Real - * conversions are supported. + * If needed, convert this term to a given sort. + * + * @note The sort of the term must be convertible into the target sort. + * Currently only Int to Real conversions are supported. * @param t the term * @param s the target sort * @return the term wrapped into a sort conversion if needed diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 16220228c..6f86928ca 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -639,10 +639,9 @@ public class Solver implements IPointer, AutoCloseable /** * Create an operator for a builtin Kind * The Kind may not be the Kind for an indexed operator - * (e.g. BITVECTOR_EXTRACT) - * Note: in this case, the Op simply wraps the Kind. - * The Kind can be used in mkTerm directly without - * creating an op first. + * (e.g. BITVECTOR_EXTRACT). + * @apiNote In this case, the Op simply wraps the Kind. The Kind can be used + * in mkTerm directly without creating an op first. * @param kind the kind to wrap */ public Op mkOp(Kind kind) @@ -1017,7 +1016,7 @@ public class Solver implements IPointer, AutoCloseable /** * Create a bit-vector constant of given size and value. * - * Note: The given value must fit into a bit-vector of the given size. + * @apiNote The given value must fit into a bit-vector of the given size. * * @param size the bit-width of the bit-vector sort * @param val the value of the constant @@ -1037,7 +1036,7 @@ public class Solver implements IPointer, AutoCloseable * Create a bit-vector constant of a given bit-width from a given string of * base 2, 10 or 16. * - * Note: The given value must fit into a bit-vector of the given size. + * @apiNote The given value must fit into a bit-vector of the given size. * * @param size the bit-width of the constant * @param s the string representation of the constant @@ -2355,9 +2354,10 @@ public class Solver implements IPointer, AutoCloseable private native void setOption(long pointer, String option, String value); /** - * If needed, convert this term to a given sort. Note that the sort of the - * term must be convertible into the target sort. Currently only Int to Real - * conversions are supported. + * If needed, convert this term to a given sort. + * + * @apiNote The sort of the term must be convertible into the target sort. + * Currently only Int to Real conversions are supported. * @param t the term * @param s the target sort * @return the term wrapped into a sort conversion if needed diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index 26a963a56..6bd87a9af 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -372,7 +372,7 @@ public class Sort extends AbstractPointer implements Comparable * or return value for any term that is function-like. * This is mainly to avoid higher order. * - * Note that arrays are explicitly not considered function-like here. + * @apiNote Arrays are explicitly not considered function-like here. * * @return true if this is a function-like sort */ diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java index fc09767ed..db780f9bd 100644 --- a/src/api/java/io/github/cvc5/api/Term.java +++ b/src/api/java/io/github/cvc5/api/Term.java @@ -190,7 +190,7 @@ public class Term extends AbstractPointer implements Comparable, Iterable< /** * @return the Op used to create this term - * Note: This is safe to call when hasOp() returns true. + * @apiNote This is safe to call when hasOp() returns true. */ public Op getOp() { @@ -367,10 +367,11 @@ public class Term extends AbstractPointer implements Comparable, Iterable< /** * @return the stored string constant. - *

- * Note: This method is not to be confused with toString() which returns the - * term in some string representation, whatever data it may hold. + * * Asserts isString(). + * + * @apiNote This method is not to be confused with toString() which returns + * the term in some string representation, whatever data it may hold. */ public String getStringValue() { @@ -623,9 +624,9 @@ public class Term extends AbstractPointer implements Comparable, Iterable< /** * Asserts isSequenceValue(). - * Note that it is usually necessary for sequences to call - * `Solver::simplify()` to turn a sequence that is constructed by, e.g., - * concatenation of unit sequences, into a sequence value. + * @apiNote It is usually necessary for sequences to call + * `Solver::simplify()` to turn a sequence that is constructed by, + * e.g., concatenation of unit sequences, into a sequence value. * @return the representation of a sequence value as a vector of terms. */ public Term[] getSequenceValue() diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 7135f0e03..6220545a1 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2439,16 +2439,16 @@ cdef class Sort: def isFunctionLike(self): """ - Is this a function-LIKE sort? + Is this a function-LIKE sort? - Anything function-like except arrays (e.g., datatype selectors) is - considered a function here. Function-like terms can not be the argument - or return value for any term that is function-like. - This is mainly to avoid higher order. + Anything function-like except arrays (e.g., datatype selectors) is + considered a function here. Function-like terms can not be the argument + or return value for any term that is function-like. + This is mainly to avoid higher order. - Note that arrays are explicitly not considered function-like here. + .. note:: Arrays are explicitly not considered function-like here. - :return: True if this is a function-like sort + :return: True if this is a function-like sort """ return self.csort.isFunctionLike() @@ -2855,10 +2855,10 @@ cdef class Term: def getOp(self): """ - Note: This is safe to call when :py:meth:`hasOp()` returns True. + .. note:: This is safe to call when :py:meth:`hasOp()` returns True. - :return: the :py:class:`pycvc5.Op` used to create this Term. - """ + :return: the :py:class:`pycvc5.Op` used to create this Term. + """ cdef Op op = Op(self.solver) op.cop = self.cterm.getOp() return op @@ -2988,13 +2988,15 @@ cdef class Term: def getStringValue(self): """ - Note: This method is not to be confused with :py:meth:`__str__()` which - returns the term in some string representation, whatever data it - may hold. - Asserts :py:meth:`isStringValue()`. + Asserts :py:meth:`isStringValue()`. - :return: the string term as a native string value. - """ + .. note:: + This method is not to be confused with :py:meth:`__str__()` which + returns the term in some string representation, whatever data it + may hold. + + :return: the string term as a native string value. + """ cdef Py_ssize_t size cdef c_wstring s = self.cterm.getStringValue() return PyUnicode_FromWideChar(s.data(), s.size()) @@ -3060,19 +3062,23 @@ cdef class Term: def isSetValue(self): """ - A term is a set value if it is considered to be a (canonical) constant set - value. A canonical set value is one whose AST is: - - (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) - - where ``c1 ... cn`` are values ordered by id such that ``c1 > ... > cn`` (see - also :cpp:func:`cvc5::api::Term::operator>()`). - - Note that a universe set term ``(kind SET_UNIVERSE)`` is not considered to be + A term is a set value if it is considered to be a (canonical) constant + set value. A canonical set value is one whose AST is: + + .. code:: + + (union + (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) + + where ``c1 ... cn`` are values ordered by id such that + ``c1 > ... > cn`` (see also :cpp:func:`cvc5::api::Term::operator>()`). + + .. note:: + A universe set term ``(kind SET_UNIVERSE)`` is not considered to be a set value. - :return: True if the term is a set value. - """ + :return: True if the term is a set value. + """ return self.cterm.isSetValue() def getSetValue(self): @@ -3094,14 +3100,15 @@ cdef class Term: def getSequenceValue(self): """ - Asserts :py:meth:`isSequenceValue()`. - - Note that it is usually necessary for sequences to call - :py:meth:`Solver.simplify()` to turn a sequence that is constructed by, e.g., - concatenation of unit sequences, into a sequence value. - - :return: the representation of a sequence value as a vector of terms. - """ + Asserts :py:meth:`isSequenceValue()`. + + .. note:: + It is usually necessary for sequences to call + :py:meth:`Solver.simplify()` to turn a sequence that is constructed + by, e.g., concatenation of unit sequences, into a sequence value. + + :return: the representation of a sequence value as a vector of terms. + """ elems = [] for e in self.cterm.getSequenceValue(): term = Term(self.solver) @@ -3144,7 +3151,7 @@ cdef class Term: def isRealValue(self): """ - Note that a term of kind PI is not considered to be a real value. + .. note:: A term of kind PI is not considered to be a real value. :return: True iff this term is a rational value. """ -- 2.30.2