From ece1a2253eb0b35316ef3c88666099b91419225c Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 4 Apr 2022 20:08:05 -0700 Subject: [PATCH] api: More fixes in C++ API docs. (#8570) --- docs/api/cpp/term.rst | 21 ++++++++-- src/api/cpp/cvc5.h | 85 +++++++++++++++++++++++----------------- src/api/cpp/cvc5_types.h | 13 ++++-- 3 files changed, 74 insertions(+), 45 deletions(-) diff --git a/docs/api/cpp/term.rst b/docs/api/cpp/term.rst index cb7812cac..1b92943a9 100644 --- a/docs/api/cpp/term.rst +++ b/docs/api/cpp/term.rst @@ -1,12 +1,25 @@ Term ==== -The :cpp:class:`Term ` class represents arbitrary expressions that are Boolean or from some of the supported theories. The list of all supported types (or kinds) is given by the :cpp:enum:`Kind ` enum. -The :cpp:class:`Term ` class provides methods for general inspection (e.g., comparison, retrieve the kind and sort, access sub-terms), but also methods to retrieving constant values for the supported theories (i.e., :code:`isValue()` and :code:`getValue()`, which returns the constant values in the best type standard C++ offers). +The :cpp:class:`Term ` class represents arbitrary expressions that +are Boolean or from some of the supported theories. The list of all supported +types (or kinds) is given by the :cpp:enum:`Kind ` enum. +The :cpp:class:`Term ` class provides methods for general +inspection (e.g., comparison, retrieve the kind and sort, access sub-terms), +but also methods to retrieving constant values for the supported theories +(i.e., :code:`isValue()` and :code:`getValue()`, which returns the +constant values in the best type standard C++ offers). -Additionally, a :cpp:class:`Term ` can be hashed (using :cpp:class:`std::hash\`) and given to output streams, including terms within standard containers like :code:`std::map`, :code:`std::set`, or :code:`std::vector`. +Additionally, a :cpp:class:`Term ` can be hashed (using +:cpp:class:`std::hash\`) and given to output streams, including +terms within standard containers like :code:`std::map`, :code:`std::set`, or +:code:`std::vector`. -The :cpp:class:`Term ` only offers the default constructor to create a null term. Instead, the :cpp:class:`Solver ` class provides factory functions for all other terms, e.g., :code:`Solver::mkTerm()` for generic terms and :code:`Solver::mk()` for constant values of a given type. +The :cpp:class:`Term ` only offers the default constructor to +create a null term. Instead, the :cpp:class:`Solver ` class +provides factory functions for all other terms, e.g., +:cpp:func:`Solver::mkTerm() ` for generic terms and +:code:`Solver::mk()` for constant values of a given type. .. doxygenclass:: cvc5::Term :project: cvc5 diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 4f2bf0ba5..460ee2179 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1157,23 +1157,28 @@ class CVC5_EXPORT Term Sort getSort() const; /** - * @return The result of replacing 'term' by 'replacement' in this term. + * Replace `term` with `replacement` in this term. * - * Note that this replacement is applied during a pre-order traversal and - * only once to the term. It is not run until fix point. + * @return The result of replacing `term` with `replacement` in this term. + * + * @note This replacement is applied during a pre-order traversal and + * only once (it is not run until fixed point). */ Term substitute(const Term& term, const Term& replacement) const; /** - * @return The result of simultaneously replacing 'terms' by 'replacements' - * in this term. + * Simultaneously replace `terms` with `replacements` in this term. * - * Note that this replacement is applied during a pre-order traversal and - * only once to the term. It is not run until fix point. In the case that - * terms contains duplicates, the replacement earliest in the vector takes - * priority. For example, calling substitute on f(x,y) with - * terms = { x, z }, replacements = { g(z), w } - * results in the term f(g(z),y). + * In the case that terms contains duplicates, the replacement earliest in + * the vector takes priority. For example, calling substitute on `f(x,y)` + * with `terms = { x, z }`, `replacements = { g(z), w }` results in the term + * `f(g(z),y)`. + * + * @note This replacement is applied during a pre-order traversal and + * only once (it is not run until fixed point). + * + * @return The result of simultaneously replacing `terms` with `replacements` + * in this term. */ Term substitute(const std::vector& terms, const std::vector& replacements) const; @@ -1879,7 +1884,7 @@ class CVC5_EXPORT DatatypeConstructorDecl bool isNullHelper() const; /** - * Is the underlying constructor resolved (i.e. has it been used to declare + * Is the underlying constructor resolved (i.e,. has it been used to declare * a datatype already)? */ bool isResolved() const; @@ -3262,7 +3267,7 @@ class CVC5_EXPORT Solver Sort getBooleanSort() const; /** - * @return Sort Integer (in cvc5, Integer is a subtype of Real) + * @return Sort Integer. */ Sort getIntegerSort() const; @@ -3781,7 +3786,7 @@ class CVC5_EXPORT Solver const std::optional& symbol = std::nullopt) const; /** - * Create a bound variable to be used in a binder (i.e. a quantifier, a + * Create a bound variable to be used in a binder (i.e., a quantifier, a * lambda, or a witness binder). * @param sort The sort of the variable. * @param symbol The name of the variable (optional). @@ -3834,9 +3839,11 @@ class CVC5_EXPORT Solver /* .................................................................... */ /** - * Simplify a formula without doing "much" work. Does not involve - * the SAT Engine in the simplification, but uses the current - * definitions, and assertions. It also involves theory normalization. + * Simplify a formula without doing "much" work. + * + * Does not involve the SAT Engine in the simplification, but uses the + * current definitions, and assertions. It also involves theory + * normalization. * * @warning This method is experimental and may change in future versions. * @@ -3956,9 +3963,10 @@ class CVC5_EXPORT Solver * (declare-sort ) * \endverbatim * - * @note This corresponds to mkUninterpretedSort(const std::string&) const if - * arity = 0, and to - * mkUninterpretedSortConstructorSort(const std::string&, size_t arity) const + * @note This corresponds to + * mkUninterpretedSort(const std::optional&) const + * if arity = 0, and to + * mkUninterpretedSortConstructorSort(size_t arity, const std::optional&) const * if arity > 0. * * @param symbol The name of the sort. @@ -3982,7 +3990,7 @@ class CVC5_EXPORT Solver * @param bound_vars The parameters to this function. * @param sort The sort of the return value of this function. * @param term The function body. - * @param global Determines whether this definition is global (i.e. persists + * @param global Determines whether this definition is global (i.e., persists * when popping the context). * @return The function. */ @@ -4007,7 +4015,7 @@ class CVC5_EXPORT Solver * @param bound_vars The parameters to this function. * @param sort The sort of the return value of this function. * @param term The function body. - * @param global Determines whether this definition is global (i.e. persists + * @param global Determines whether this definition is global (i.e., persists * when popping the context). * @return The function. */ @@ -4032,7 +4040,7 @@ class CVC5_EXPORT Solver * @param fun The sorted function. * @param bound_vars The parameters to this function. * @param term The function body. - * @param global Determines whether this definition is global (i.e. persists + * @param global Determines whether this definition is global (i.e., persists * when popping the context). * @return The function. */ @@ -4059,7 +4067,7 @@ class CVC5_EXPORT Solver * @param funs The sorted functions. * @param bound_vars The list of parameters to the functions. * @param terms The list of function bodies of the functions. - * @param global Determines whether this definition is global (i.e. persists + * @param global Determines whether this definition is global (i.e., persists * when popping the context). */ void defineFunsRec(const std::vector& funs, @@ -4114,15 +4122,18 @@ class CVC5_EXPORT Solver std::string getOption(const std::string& option) const; /** - * Get all option names that can be used with `setOption`, `getOption` and - * `getOptionInfo`. + * Get all option names that can be used with setOption(), getOption() and + * getOptionInfo(). * @return All option names. */ std::vector getOptionNames() const; /** - * Get some information about the given option. Check the `OptionInfo` class - * for more details on which information is available. + * Get some information about the given option. + * + * Check the OptionInfo class for more details on which information is + * available. + * * @return Information about the given option. */ OptionInfo getOptionInfo(const std::string& option) const; @@ -4166,11 +4177,11 @@ class CVC5_EXPORT Solver * :ref:`produce-unsat-cores `. * * .. note:: - * In contrast to SMT-LIB, the API does not distinguish between named and - * unnamed assertions when producing an unsatisfiable core. Additionally, - * the API allows this option to be called after a check with assumptions. - * A subset of those assumptions may be included in the unsatisfiable core - * returned by this method. + * In contrast to SMT-LIB, cvc5's API does not distinguish between named + * and unnamed assertions when producing an unsatisfiable core. + * Additionally, the API allows this option to be called after a check with + * assumptions. A subset of those assumptions may be included in the + * unsatisfiable core returned by this method. * \endverbatim * * @return A set of terms representing the unsatisfiable core. @@ -4266,15 +4277,15 @@ class CVC5_EXPORT Solver /** * This returns false if the model value of free constant v was not essential * for showing the satisfiability of the last call to checkSat using the - * current model. This method will only return false (for any v) if + * current model. This method will only return false (for any `v`) if * option - * \verbatim embed:rst:inline :ref:`model-cores ` - * \endverbatim has been set. + * \verbatim embed:rst:inline :ref:`model-cores `\endverbatim + * has been set. * * @warning This method is experimental and may change in future versions. * * @param v The term in question. - * @return True if v is a model core symbol. + * @return True if `v` is a model core symbol. */ bool isModelCoreSymbol(const Term& v) const; diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h index c05ce0698..5a746aa10 100644 --- a/src/api/cpp/cvc5_types.h +++ b/src/api/cpp/cvc5_types.h @@ -77,31 +77,36 @@ enum RoundingMode { /** * Round to the nearest even number. + * * If the two nearest floating-point numbers bracketing an unrepresentable * infinitely precise result are equally near, the one with an even least * significant digit will be delivered. */ ROUND_NEAREST_TIES_TO_EVEN, /** - * Round towards positive infinity (+oo). - * The result shall be the format's floating-point number (possibly +oo) + * Round towards positive infinity (SMT-LIB: ``+oo``). + * + * The result shall be the format's floating-point number (possibly ``+oo``) * closest to and no less than the infinitely precise result. */ ROUND_TOWARD_POSITIVE, /** - * Round towards negative infinity (-oo). - * The result shall be the format's floating-point number (possibly -oo) + * Round towards negative infinity (``-oo``). + * + * The result shall be the format's floating-point number (possibly ``-oo``) * closest to and no less than the infinitely precise result. */ ROUND_TOWARD_NEGATIVE, /** * Round towards zero. + * * The result shall be the format's floating-point number closest to and no * greater in magnitude than the infinitely precise result. */ ROUND_TOWARD_ZERO, /** * Round to the nearest number away from zero. + * * If the two nearest floating-point numbers bracketing an unrepresentable * infinitely precise result are equally near, the one with larger magnitude * will be selected. -- 2.30.2