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.

diff --git a/docs/api/cpp/Doxyfile.in b/docs/api/cpp/Doxyfile.in
index b55c4ec481c7669ca147cc368821bfb5631a78bd..be6f50172e68475dedb750d0eb447a5df8cedebd 100644 (file)
--- 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 2fcf74767ac4ccebbcb9426312e4a836a31389cd..974f15e0fe6a719c264d899e77e51051d0a33fa1 100644 (file)
--- 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/<!-- Generated by javadoc [^>]* -->//' {} "\;"
     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 d3662c832f0ff3e1bd19e7b4cc70a6f2254e7394..fa85524587508865312e7c8d8c0e4af72cbadf5b 100644 (file)
--- 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 <lbl-option-model-cores>`
-   * \endverbatim
+   * \verbatim embed:rst:inline :ref:`model-cores <lbl-option-model-cores>` \endverbatim
    * has been set.
    *
    * @param v The term in question
@@ -4263,8 +4261,6 @@ class CVC5_EXPORT Solver
    * :ref:`produce-models <lbl-option-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 e97adf53b32e66d302a374314598cfdf8082e40e..89a7732a8e2d61f60649fcbc7561a4132e33f4c6 100644 (file)
--- 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& children)
+   *   - `mkTerm(Kind kind, Term child1, Term child2)`
+   *   - `mkTerm(Kind kind, Term child1, Term child2, Term child3)`
+   *   - `mkTerm(Kind kind, const std::vector<Term>& 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<Term>& children)
+   *   - `mkTerm(Kind kind, Term child1, Term child2)`
+   *   - `mkTerm(Kind kind, Term child1, Term child2, Term child3)`
+   *   - `mkTerm(Kind kind, const std::vector<Term>& 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 d843d55edcf8a721c0e79d42772040ca01d79bbe..12eec9b1a27dcd3e6274ca5a0d2a9395a79d68dc 100644 (file)
--- 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 4af1f526e4f5a57dc574b21b6cd78dbbd96a5554..74f0e421e405489d887f7683b17c89aa4d516349 100644 (file)
--- 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")