From 54ce4e6afd0cda5d5bca45d7c5ddc6587c50b30f Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 7 Mar 2022 22:22:44 +0100 Subject: [PATCH] Fix docs warnings (#8019) This fixes a bunch of warnings when generating our sphinx documentation. They are mostly related to incorrect indentation/spacing, line breaks where no line breaks should be, or missing code blocks. Note that running clang-format causes some of these issues. --- docs/api/cpp/Doxyfile.in | 4 +-- docs/api/java/CMakeLists.txt | 1 + src/api/cpp/cvc5.h | 6 +--- src/api/cpp/cvc5_kind.h | 59 ++++++++++++++++++++--------------- src/api/python/cvc5.pxi | 36 +++++++++++---------- src/api/python/genkinds.py.in | 12 +++++++ 6 files changed, 70 insertions(+), 48 deletions(-) diff --git a/docs/api/cpp/Doxyfile.in b/docs/api/cpp/Doxyfile.in index b55c4ec48..be6f50172 100644 --- a/docs/api/cpp/Doxyfile.in +++ b/docs/api/cpp/Doxyfile.in @@ -269,8 +269,8 @@ TAB_SIZE = 4 # commands \{ and \} for these it is advised to use the version @{ and @} or use # a double escape (\\{ and \\}) -ALIASES = -ALIASES += "rst=\verbatim embed:rst" +ALIASES = +ALIASES += "rst=\verbatim embed:rst:leading-asterisk" ALIASES += "endrst=\endverbatim" # Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 2fcf74767..974f15e0f 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -33,6 +33,7 @@ if(BUILD_BINDINGS_JAVA) -cp ${CVC5_JAR_FILE} -tag "apiNote:a:Note:" -notimestamp + --no-module-directories COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's///' {} "\;" COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete DEPENDS cvc5jar ${CVC5_JAR_FILE} diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index d3662c832..fa8552458 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4239,9 +4239,7 @@ class CVC5_EXPORT Solver * for showing the satisfiability of the last call to checkSat using the * current model. This method will only return false (for any v) if * option - * \verbatim:rst:inline - * :ref:`model-cores ` - * \endverbatim + * \verbatim embed:rst:inline :ref:`model-cores ` \endverbatim * has been set. * * @param v The term in question @@ -4263,8 +4261,6 @@ class CVC5_EXPORT Solver * :ref:`produce-models `. * \endverbatim * - * \endverbatim - * * @param sorts The list of uninterpreted sorts that should be printed in the * model. * @param vars The list of free constants that should be printed in the diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index e97adf53b..89a7732a8 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1939,12 +1939,20 @@ enum Kind : int32_t /** * Match expressions. * For example, the smt2 syntax match term - * `(match l (((cons h t) h) (nil 0)))` + * \rst + * .. code:: smtlib + * + * (match l (((cons h t) h) (nil 0))) + * \endrst * is represented by the AST * + * \rst + * .. code:: lisp + * * (MATCH l - * (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h) - * (MATCH_CASE nil 0)) + * (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h) + * (MATCH_CASE nil 0)) + * \endrst * * The type of the last argument of each case term could be equal. * @@ -1955,7 +1963,6 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` - * */ MATCH, /** @@ -2273,8 +2280,7 @@ enum Kind : int32_t * - 2: a set of type (Set T1) * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) - * const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ SET_MAP, @@ -2359,6 +2365,7 @@ enum Kind : int32_t BAG_EMPTY, /** * Bag max union. + * * Parameters: * - 1..2: Terms of bag sort * @@ -2497,6 +2504,7 @@ enum Kind : int32_t BAG_CHOOSE, /** * Bag is_singleton predicate (single element with multiplicity exactly one). + * * Parameters: * - 1: Term of bag sort, is [1] a singleton bag? * @@ -2534,8 +2542,7 @@ enum Kind : int32_t * - 2: a bag of type (Bag T1) * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) - * const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ BAG_MAP, @@ -2551,8 +2558,7 @@ enum Kind : int32_t * - 2: a bag of type (Bag T) * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) - * const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ BAG_FILTER, @@ -2567,8 +2573,7 @@ enum Kind : int32_t * - 2: a bag of type (Bag T1) * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, - * const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ BAG_FOLD, @@ -2989,7 +2994,7 @@ enum Kind : int32_t */ REGEXP_DIFF, /** - * Regexp *. + * Regexp \*. * * Parameters: * - 1: Term of sort Regexp @@ -3386,29 +3391,34 @@ enum Kind : int32_t /* * An instantiation pool. * Specifies an annotation for pool based instantiation. + * * Parameters: n > 1 - * - 1..n: Terms that comprise the pools, which are one-to-one with - * the variables of the quantified formula to be instantiated. + * - 1..n: Terms that comprise the pools, which are one-to-one with the variables of the quantified formula to be instantiated. + * * Create with: - * - `mkTerm(Kind kind, Term child1, Term child2) - * - `mkTerm(Kind kind, Term child1, Term child2, Term child3) - * - `mkTerm(Kind kind, const std::vector& children) + * - `mkTerm(Kind kind, Term child1, Term child2)` + * - `mkTerm(Kind kind, Term child1, Term child2, Term child3)` + * - `mkTerm(Kind kind, const std::vector& children)` */ INST_POOL, /* * A instantantiation-add-to-pool annotation. + * * Parameters: n = 1 * - 1: The pool to add to. + * * Create with: - * - `mkTerm(Kind kind, Term child) + * - `mkTerm(Kind kind, Term child)` */ INST_ADD_TO_POOL, /* * A skolemization-add-to-pool annotation. + * * Parameters: n = 1 * - 1: The pool to add to. + * * Create with: - * - `mkTerm(Kind kind, Term child) + * - `mkTerm(Kind kind, Term child)` */ SKOLEM_ADD_TO_POOL, /** @@ -3421,17 +3431,16 @@ enum Kind : int32_t * - 2...n: The values of the attribute. * * Create with: - * - `mkTerm(Kind kind, Term child1, Term child2) - * - `mkTerm(Kind kind, Term child1, Term child2, Term child3) - * - `mkTerm(Kind kind, const std::vector& children) + * - `mkTerm(Kind kind, Term child1, Term child2)` + * - `mkTerm(Kind kind, Term child1, Term child2, Term child3)` + * - `mkTerm(Kind kind, const std::vector& children)` */ INST_ATTRIBUTE, /** * A list of instantiation patterns and/or attributes. * * Parameters: n > 1 - * - 1..n: Terms with kind INST_PATTERN, INST_NO_PATTERN, or - * INST_ATTRIBUTE. + * - 1..n: Terms with kind INST_PATTERN, INST_NO_PATTERN, or INST_ATTRIBUTE. * * Create with: * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index d843d55ed..12eec9b1a 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -155,8 +155,7 @@ cdef class Datatype: def getParameters(self): """ - :return: the parameters of this datatype, if it is parametric. An - exception is thrown if this datatype is not parametric. + :return: the parameters of this datatype, if it is parametric. An exception is thrown if this datatype is not parametric. """ param_sorts = [] for s in self.cd.getParameters(): @@ -1678,7 +1677,7 @@ cdef class Solver: ( check-synth ) :return: the result of the check, which is unsat if the check succeeded, - in which case solutions are available via getSynthSolutions. + in which case solutions are available via getSynthSolutions. """ cdef Result r = Result() r.cr = self.csolver.checkSynthNext() @@ -2682,10 +2681,10 @@ cdef class Sort: def substitute(self, sort_or_list_1, sort_or_list_2): """ - Substitution of Sorts. + Substitution of Sorts. - :param sort_or_list_1: the subsort or subsorts to be substituted within this sort. - :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort. + :param sort_or_list_1: the subsort or subsorts to be substituted within this sort. + :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort. Note that this replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point. In the case that @@ -2693,8 +2692,8 @@ cdef class Sort: takes priority. For example, - (Array A B) .substitute([A, C], [(Array C D), (Array A B)]) will - return (Array (Array C D) B). + ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])`` will + return ``(Array (Array C D) B)``. """ # The resulting sort after substitution @@ -3018,13 +3017,17 @@ cdef class Term: """ :return: the result of simultaneously replacing the term(s) stored in ``term_or_list_1`` by the term(s) stored in ``term_or_list_2`` 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 list takes - priority. For example, calling substitute on f(x,y) with - term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ] - results in the term f(g(z),y). - """ + 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 list takes + priority. For example, calling substitute on ``f(x,y)`` with + + .. code:: python + + term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ] + + results in the term ``f(g(z),y)``. + """ # The resulting term after substitution cdef Term term = Term(self.solver) # lists for substitutions @@ -3212,7 +3215,8 @@ cdef class Term: or otherwise an exception is thrown. :return: 0 if this term is zero, -1 if this term is a negative real or - integer value, 1 if this term is a positive real or integer value. + integer value, 1 if this term is a positive real or integer + value. """ return self.cterm.getRealOrIntegerValueSign() diff --git a/src/api/python/genkinds.py.in b/src/api/python/genkinds.py.in index 4af1f526e..74f0e421e 100644 --- a/src/api/python/genkinds.py.in +++ b/src/api/python/genkinds.py.in @@ -26,6 +26,7 @@ handle nested '#if 0' pairs. import argparse import os +import re import sys # get access to cvc5/src/api/parsekinds.py @@ -83,6 +84,14 @@ def gen_pxi(parser : KindsParser, filename): doc = parser.kinds_doc.get(name, '') f.write(KINDS_ATTR_TEMPLATE.format(name=name, kind=kind, doc=doc)) +comment_repls = { + '`Solver::([a-zA-Z]+)\(([^)]*)\)[^`]*`': ':py:meth:`pycvc5.Solver.\\1`', +} +def reformat_comment(comment): + for pat,repl in comment_repls.items(): + comment = re.sub(pat, repl, comment) + return comment + if __name__ == "__main__": parser = argparse.ArgumentParser('Read a kinds header file and generate a ' 'corresponding pxd file, with simplified kind names.') @@ -100,5 +109,8 @@ if __name__ == "__main__": kp = KindsParser() kp.parse(kinds_header) + for name in kp.kinds_doc: + kp.kinds_doc[name] = reformat_comment(kp.kinds_doc[name]) + gen_pxd(kp, kinds_file_prefix + ".pxd") gen_pxi(kp, kinds_file_prefix + ".pxi") -- 2.30.2